1 | % (c) 2009-2023 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(pref_definitions,[b_get_preferences_from_specification/0, b_get_preferences_from_specification/1, | |
6 | b_get_important_preferences_from_raw_machine/2, | |
7 | b_get_set_pref_definition/3, | |
8 | b_get_definition_string_list_from_spec/2, | |
9 | b_get_definition_string_from_spec/3]). | |
10 | ||
11 | :- use_module(module_information). | |
12 | :- module_info(group,tools). | |
13 | :- module_info(description,'Tools for extracting information from DEFINITIONS.'). | |
14 | ||
15 | :- use_module(error_manager). | |
16 | :- use_module(self_check). | |
17 | :- use_module(tools,[ajoin/2, ajoin_with_sep/3]). | |
18 | :- use_module(bmachine,[b_definition_prefixed/5,b_get_typed_definition/3]). | |
19 | :- use_module(preferences,[temporary_set_preference/2,eclipse_preference/2,deprecated_eclipse_preference/4, | |
20 | preference_val_type/2, pref_type_synonym/2]). | |
21 | :- use_module(btypechecker,[unify_types_werrors/4]). | |
22 | :- use_module(bsyntaxtree). | |
23 | :- use_module(debug,[debug_println/2]). | |
24 | % get and set important preferences from a raw, untyped machine (as they | |
25 | % may influence type checking,...); | |
26 | % example: IGNORE_PRJ_TYPES, WARN_IF_DEFINITION_HIDES_VARIABLE | |
27 | b_get_important_preferences_from_raw_machine(RawMachine,RawModelType) :- | |
28 | (b_get_important_pref_type(RawModelType,Pref,PVal) ; | |
29 | b_get_important_pref_mach(RawMachine,Pref,PVal)), | |
30 | (temporary_set_preference(Pref,PVal) | |
31 | -> debug_println(9,set_important_pref(Pref,PVal)) | |
32 | ; add_error(pref_definitions,'Could not set DEFINITION preference to specified value: ',PVal) | |
33 | ), | |
34 | fail. | |
35 | b_get_important_preferences_from_raw_machine(_,_). | |
36 | ||
37 | b_get_important_pref_mach(RawMachine,Pref,PVal) :- | |
38 | ? | member(definitions(_Pos,Defs),RawMachine), |
39 | ? | member(expression_definition(_DPOS,DefName,[],RawVALUE),Defs), |
40 | (atom(DefName) -> true ; add_internal_error('Non-atomic DEFINITION id:',DefName),fail), | |
41 | atom_concat('SET_PREF_',PREFString,DefName), | |
42 | (eclipse_preference(PREFString,Pref) -> true | |
43 | ; additional_important_preference_during_loading(PREFString), Pref=PREFString), | |
44 | preference_val_type(Pref,PType), | |
45 | (PType=bool ; PType=xbool ; PType=dbool; PType=solver_name), % at the moment only boolean preferences supported | |
46 | convert_raw_pref_val(PType,RawVALUE,PVal). | |
47 | ||
48 | ||
49 | % important preferences that influence type checking, loading, deferred set setup, ... | |
50 | % these preferences should be set before a machine is typechecked and pre-compiled (they are used in ast_cleanup) | |
51 | additional_important_preference_during_loading(convert_comprehension_sets_into_closures). | |
52 | additional_important_preference_during_loading(detect_lambdas). | |
53 | additional_important_preference_during_loading(disprover_mode). | |
54 | additional_important_preference_during_loading(ignore_prj_types). | |
55 | additional_important_preference_during_loading(lift_existential_quantifiers). | |
56 | additional_important_preference_during_loading(normalize_ast). | |
57 | additional_important_preference_during_loading(normalize_ast_sort_commutative). | |
58 | additional_important_preference_during_loading(optimize_ast). | |
59 | additional_important_preference_during_loading(optimize_enum_set_elems). % hidden, has no eclipse_preference fact | |
60 | additional_important_preference_during_loading(perform_enumeration_order_analysis). | |
61 | additional_important_preference_during_loading(perform_stricter_static_checks). | |
62 | additional_important_preference_during_loading(prob_safe_mode). | |
63 | additional_important_preference_during_loading(remove_implied_constraints). | |
64 | additional_important_preference_during_loading(use_clpfd_solver). | |
65 | additional_important_preference_during_loading(use_common_subexpression_elimination). | |
66 | additional_important_preference_during_loading(use_static_symmetry_detection). | |
67 | additional_important_preference_during_loading(useless_code_elimination). | |
68 | additional_important_preference_during_loading('KODKOD'). % deprecated, but can still be set | |
69 | ||
70 | b_get_important_pref_type(system(Pos),Pref,PVal) :- | |
71 | % SET_PREF_ALLOW_NEW_OPERATIONS_IN_REFINEMENT == TRUE; for Event-B Atelier-B style; alternatively we could set animation_minor_mode ? | |
72 | add_message(pref_definitions,'Detected Event-B model; setting ALLOW_NEW_OPERATIONS_IN_REFINEMENT to ','TRUE',Pos), | |
73 | Pref=allow_new_ops_in_refinement, PVal=true. | |
74 | ||
75 | ||
76 | convert_raw_pref_val(xbool,Raw,Res) :- convert_raw_pref_val(bool,Raw,Res). % full | |
77 | convert_raw_pref_val(dbool,Raw,Res) :- convert_raw_pref_val(bool,Raw,Res). % TODO: support default | |
78 | convert_raw_pref_val(bool,boolean_true(_),true). | |
79 | convert_raw_pref_val(bool,boolean_false(_),false). | |
80 | convert_raw_pref_val(solver_name,string(_,String),String). | |
81 | %convert_raw_pref_val(int,integer(_,V),V). | |
82 | %convert_raw_pref_val(nat,integer(_,V),V). % range checking done in temporary_set_preference | |
83 | %convert_raw_pref_val(nat1,integer(_,V),V). | |
84 | %convert_raw_pref_val(neg,integer(_,V),V). | |
85 | %convert_raw_pref_val(range(_,_),integer(_,V),V). | |
86 | %convert_raw_pref_val(string(_),string(_,S),S). | |
87 | ||
88 | :- use_module(translate,[translate_bexpression/2]). | |
89 | b_get_preferences_from_specification(List) :- | |
90 | findall(set_pref(String,ValS),(get_def_aux(String,TExpr),translate_bexpression(TExpr,ValS)),List). | |
91 | % now a version that does not need to obtain a list with all preferences set: | |
92 | b_get_preferences_from_specification :- get_def_aux(_,_),fail. | |
93 | b_get_preferences_from_specification. | |
94 | ||
95 | get_def_aux(String,TExpr) :- | |
96 | b_get_set_pref_definition(_DefName,String,TExpr,DefPos), | |
97 | set_pref_from_machine(String,DefPos,TExpr). | |
98 | ||
99 | b_get_set_pref_definition(DefName,String,TExpr) :- | |
100 | b_get_set_pref_definition(DefName,String,TExpr,_). | |
101 | ||
102 | b_get_set_pref_definition(DefName,String,TExpr,DefPos) :- animation_mode(xtl),!, | |
103 | xtl_get_definition_string(DefName,ValString), | |
104 | atom(DefName), | |
105 | atom_concat('SET_PREF_',String,DefName), | |
106 | DefPos=unknown, | |
107 | generate_value(ValString,TExpr). | |
108 | b_get_set_pref_definition(DefName,String,TExpr,DefPos) :- | |
109 | b_definition_prefixed(_,'SET_PREF_',String,DefName,DefPos), | |
110 | b_get_typed_definition(DefName,[],TExpr). | |
111 | ||
112 | ||
113 | :- use_module(tools,[safe_number_codes/2]). | |
114 | generate_value(Nr,Res) :- integer(Nr), !, | |
115 | Res = b(integer(Nr),integer,[]). | |
116 | % TO DO: booleans | |
117 | generate_value(ValString,b(string(ValString),string,[])). | |
118 | ||
119 | :- use_module(tools_matching,[get_possible_preferences_matches_msg/2]). | |
120 | set_pref_from_machine(String,DefPos,TExpr) :- | |
121 | (eclipse_preference(String,Pref) -> preference_val_type(Pref,PType) | |
122 | ; preference_val_type(String,_) -> Pref=String, % user uses directly internal Prolog Name | |
123 | preference_val_type(Pref,PType) | |
124 | ; deprecated_eclipse_preference(String,PType,Pref,Mapping) | |
125 | ), | |
126 | !, | |
127 | convert_pref_val(PType,TExpr,PVal), | |
128 | (Mapping=[],temporary_set_preference(Pref,PVal) | |
129 | -> add_debug_message(pref_definitions,'Setting DEFINITION preference: ',(String:PVal),DefPos) | |
130 | ; member(PVal/NewVal,Mapping), temporary_set_preference(Pref,NewVal) | |
131 | -> add_debug_message(pref_definitions,'Setting deprecated DEFINITION preference: ',(String:NewVal),DefPos) | |
132 | ; add_error(pref_definitions,'Could not set DEFINITION preference: ',(String:PVal),DefPos) | |
133 | ). | |
134 | set_pref_from_machine(String,DefPos,_TExpr) :- | |
135 | get_possible_preferences_matches_msg(String,FuzzyMatches), | |
136 | !, | |
137 | ajoin(['Error in SET_PREF DEFINITION. Preference ',String,' does not exist! Did you mean: '],Msg), | |
138 | add_warning(pref_definitions,Msg,FuzzyMatches,DefPos),fail. | |
139 | set_pref_from_machine(String,DefPos,_TExpr) :- | |
140 | add_warning(pref_definitions,'Error in SET_PREF DEFINITION. Preference does not exist: ',String,DefPos),fail. | |
141 | ||
142 | convert_pref_val(int,TExpr,Val) :- !, | |
143 | check_type(integer,TExpr), | |
144 | compute_expr(TExpr,int(Val)). | |
145 | convert_pref_val(nat,TExpr,Val) :- !, | |
146 | convert_pref_val(int,TExpr,Val), | |
147 | ((ground(Val),Val >= 0) -> true ; error(TExpr,'Value must be a natural (>= 0)')). | |
148 | convert_pref_val(neg,TExpr,Val) :- !, | |
149 | convert_pref_val(int,TExpr,Val), | |
150 | ((ground(Val),Val =< 0) -> true ; error(TExpr,'Value must be non-positive (<= 0)')). | |
151 | convert_pref_val(nat1,TExpr,Val) :- !, | |
152 | convert_pref_val(int,TExpr,Val), | |
153 | ((ground(Val),Val >= 1) -> true ; error(TExpr,'Value must be a natural >= 1')). | |
154 | convert_pref_val(range(Low,Up),TExpr,Val) :-!, | |
155 | convert_pref_val(int,TExpr,Val), | |
156 | ( ground(Val),Val >= Low, Val =< Up -> true | |
157 | ; ajoin(['Value must be in the interval [',Low,',',Up,']'],Msg), | |
158 | error(TExpr,Msg)). | |
159 | convert_pref_val(bool,TExpr,Val) :- !, | |
160 | check_type(boolean, TExpr), | |
161 | compute_expr(TExpr,BVal), | |
162 | ( BVal = pred_true /* bool_true */ -> Val = true | |
163 | ; BVal = pred_false /* bool_false */ -> Val = false | |
164 | ; add_error(pref_definitions,'Unexpected result (neither true nor false)',BVal)). | |
165 | convert_pref_val(xbool,TExpr,Val) :- !, % extended boolean | |
166 | (get_texpr_type(TExpr,boolean) -> true ; check_type(string,TExpr)), | |
167 | compute_expr(TExpr,BVal), | |
168 | ( BVal = pred_true /* bool_true */ -> Val = true | |
169 | ; BVal = pred_false /* bool_false */ -> Val = false | |
170 | ; BVal=string(Val),member(Val,[false,true,full]) -> true | |
171 | ; add_error(pref_definitions,'Unexpected result (neither true, false nor full)',BVal)). | |
172 | convert_pref_val(dbool,TExpr,Val) :- !, % extended boolean | |
173 | (get_texpr_type(TExpr,boolean) -> true ; check_type(string,TExpr)), | |
174 | compute_expr(TExpr,BVal), | |
175 | ( BVal = pred_true /* bool_true */ -> Val = true | |
176 | ; BVal = pred_false /* bool_false */ -> Val = false | |
177 | ; BVal=string(Val),member(Val,[false,true,default]) -> true | |
178 | ; add_error(pref_definitions,'Unexpected result (neither true, false nor default)',BVal)). | |
179 | convert_pref_val(string,TExpr,Val) :- !, | |
180 | check_type(string, TExpr), | |
181 | get_texpr_expr(TExpr,string(Val)). | |
182 | convert_pref_val(path,TExpr,Val) :- !, | |
183 | check_type(string, TExpr), | |
184 | get_texpr_expr(TExpr,string(Val)). | |
185 | convert_pref_val([H|T],TExpr,Val) :- !, | |
186 | check_type(string, TExpr), | |
187 | get_texpr_expr(TExpr,string(Val)), | |
188 | (member(Val,[H|T]) -> true | |
189 | ; ajoin_with_sep(['Value must be one of:',H|T],' ',Msg), | |
190 | error(TExpr,Msg)). | |
191 | convert_pref_val(Type,TExpr,Val) :- pref_type_synonym(Type,OtherType),!, | |
192 | convert_pref_val(OtherType,TExpr,Val). | |
193 | convert_pref_val(PrefType,_,_) :- | |
194 | add_error(pref_definitions,'Unsupported preference type in definitions:',PrefType),fail. | |
195 | ||
196 | :- use_module(b_interpreter,[b_compute_expression_nowf/6]). | |
197 | compute_expr(TExpr,Res) :- | |
198 | if( b_compute_expression_nowf(TExpr,[],[],R,'DEFINITION preference',0) , Res=R , | |
199 | add_error_fail(pref_definitions,'Computing expression failed: ',TExpr)). | |
200 | error(TExpr,Msg) :- | |
201 | get_texpr_pos(TExpr,Pos), | |
202 | add_all_perrors([error(Msg,Pos)]), | |
203 | fail. | |
204 | ||
205 | check_type(Type,TExpr) :- | |
206 | get_texpr_type(TExpr,EType), | |
207 | get_texpr_pos(TExpr,Pos), | |
208 | unify_types_werrors(Type,EType,Pos,'PREFERENCE'). | |
209 | ||
210 | % ------------------- | |
211 | ||
212 | ||
213 | :- use_module(tools,[safe_atom_codes/2, string_concatenate/3]). | |
214 | :- use_module(bmachine,[b_definition_prefixed/5,b_get_definition_string_from_machine/3]). | |
215 | :- use_module(specfile,[animation_mode/1]). | |
216 | :- use_module(xtl_interface,[xtl_get_definition_string/2]). | |
217 | ||
218 | /* for tcltk: */ | |
219 | b_get_definition_string_list_from_spec(Def_Name_Prefix,Result) :- | |
220 | atom_codes(Def_Name_Prefix,Codes), append(Codes,_,CodesPrefix), | |
221 | findall(S, (b_get_definition_string_from_spec(Def_Name,_,DS), | |
222 | safe_atom_codes(Def_Name,CodesPrefix), /* check that name begins with the same characters as Def_Name_Prefix */ | |
223 | string_concatenate(DS,';',S)), Result). | |
224 | ||
225 | b_get_definition_string_from_spec(Def_Name,Pos,DS) :- animation_mode(xtl),!, Pos=unknown, | |
226 | xtl_get_definition_string(Def_Name,DS). | |
227 | %TODO: also support CSP | |
228 | b_get_definition_string_from_spec(_,_,_) :- animation_mode(cspm),!,fail. | |
229 | b_get_definition_string_from_spec(Def_Name,Pos,DS) :- | |
230 | b_get_definition_string_from_machine(Def_Name,Pos,DS). | |
231 |