1 | | % (c) 2009-2025 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 | | obsolete_preference/1, preference_val_type/2, pref_type_synonym/2, is_of_type/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; |
72 | | % for Event-B Atelier-B style; alternatively we could set animation_minor_mode ? |
73 | | % TODO: we could have an implementation machine which refines a system model |
74 | | add_message(pref_definitions,'Detected Event-B model; setting ALLOW_NEW_OPERATIONS_IN_REFINEMENT to ','TRUE',Pos), |
75 | | Pref=allow_new_ops_in_refinement, PVal=true. |
76 | | % maybe we should also set SHOW_EVENTB_ANY_VALUES (show_eventb_any_arguments) to TRUE |
77 | | |
78 | | convert_raw_pref_val(axbool,Raw,Res) :- convert_raw_pref_val(bool,Raw,Res). % full |
79 | ? | convert_raw_pref_val(xbool,Raw,Res) :- convert_raw_pref_val(bool,Raw,Res). % full |
80 | ? | convert_raw_pref_val(dbool,Raw,Res) :- convert_raw_pref_val(bool,Raw,Res). % TODO: support default |
81 | | convert_raw_pref_val(bool,boolean_true(_),true). |
82 | | convert_raw_pref_val(bool,boolean_false(_),false). |
83 | | convert_raw_pref_val(solver_name,string(_,String),String). |
84 | | %convert_raw_pref_val(int,integer(_,V),V). |
85 | | %convert_raw_pref_val(nat,integer(_,V),V). % range checking done in temporary_set_preference |
86 | | %convert_raw_pref_val(nat1,integer(_,V),V). |
87 | | %convert_raw_pref_val(neg,integer(_,V),V). |
88 | | %convert_raw_pref_val(range(_,_),integer(_,V),V). |
89 | | %convert_raw_pref_val(string(_),string(_,S),S). |
90 | | |
91 | | :- use_module(translate,[translate_bexpression/2]). |
92 | | b_get_preferences_from_specification(List) :- |
93 | | findall(set_pref(String,ValS),(get_def_aux(String,TExpr),translate_bexpression(TExpr,ValS)),List). |
94 | | % now a version that does not need to obtain a list with all preferences set: |
95 | | b_get_preferences_from_specification :- get_def_aux(_,_),fail. |
96 | | b_get_preferences_from_specification. |
97 | | |
98 | | get_def_aux(String,TExpr) :- |
99 | ? | b_get_set_pref_definition(_DefName,String,TExpr,DefPos), |
100 | | set_pref_from_machine(String,DefPos,TExpr). |
101 | | |
102 | | b_get_set_pref_definition(DefName,String,TExpr) :- |
103 | | b_get_set_pref_definition(DefName,String,TExpr,_). |
104 | | |
105 | | b_get_set_pref_definition(DefName,String,TExpr,DefPos) :- animation_mode(xtl),!, |
106 | ? | xtl_get_definition_string(DefName,ValString), |
107 | | atom(DefName), |
108 | | atom_concat('SET_PREF_',String,DefName), |
109 | | DefPos=unknown, |
110 | | generate_value(ValString,TExpr). |
111 | | b_get_set_pref_definition(DefName,String,TExpr,DefPos) :- |
112 | ? | b_definition_prefixed(_,'SET_PREF_',String,DefName,DefPos), |
113 | ? | b_get_typed_definition(DefName,[constants],TExpr). % scope=constants allows to use other definitions |
114 | | |
115 | | |
116 | | :- use_module(tools,[safe_number_codes/2]). |
117 | | generate_value(Nr,Res) :- integer(Nr), !, |
118 | | Res = b(integer(Nr),integer,[]). |
119 | | % TO DO: booleans |
120 | | generate_value(ValString,b(string(ValString),string,[])). |
121 | | |
122 | | :- use_module(tools_matching,[get_possible_preferences_matches_msg/2]). |
123 | | set_pref_from_machine(String,DefPos,TExpr) :- |
124 | ? | (eclipse_preference(String,Pref) -> preference_val_type(Pref,PType) |
125 | | ; preference_val_type(String,_) -> Pref=String, % user uses directly internal Prolog Name |
126 | | preference_val_type(Pref,PType) |
127 | | ; deprecated_eclipse_preference(String,PType,Pref,Mapping) |
128 | | ), |
129 | | !, |
130 | | convert_pref_val(PType,TExpr,PVal), |
131 | | (Mapping=[],temporary_set_preference(Pref,PVal) |
132 | | -> add_debug_message(pref_definitions,'Setting DEFINITION preference: ',(String:PVal),DefPos) |
133 | ? | ; member(PVal/NewVal,Mapping), temporary_set_preference(Pref,NewVal) |
134 | | -> add_debug_message(pref_definitions,'Setting deprecated DEFINITION preference: ',(String:NewVal),DefPos) |
135 | | ; add_error(pref_definitions,'Could not set DEFINITION preference: ',(String:PVal),DefPos) |
136 | | ). |
137 | | set_pref_from_machine(String,DefPos,_TExpr) :- obsolete_preference(String),!, |
138 | | add_warning(pref_definitions,'SET_PREF DEFINITION preference is obsolete: ',String,DefPos). |
139 | | set_pref_from_machine(String,DefPos,_TExpr) :- |
140 | ? | get_possible_preferences_matches_msg(String,FuzzyMatches), |
141 | | !, |
142 | | ajoin(['Error in SET_PREF DEFINITION. Preference ',String,' does not exist! Did you mean: '],Msg), |
143 | | add_warning(pref_definitions,Msg,FuzzyMatches,DefPos),fail. |
144 | | set_pref_from_machine(String,DefPos,_TExpr) :- |
145 | | add_warning(pref_definitions,'Error in SET_PREF DEFINITION. Preference does not exist: ',String,DefPos),fail. |
146 | | |
147 | | convert_pref_val(int,TExpr,Val) :- !, |
148 | | check_type(integer,TExpr), |
149 | | compute_expr(TExpr,int(Val)). |
150 | | convert_pref_val(nat,TExpr,Val) :- !, |
151 | | convert_pref_val(int,TExpr,Val), |
152 | | ((ground(Val),Val >= 0) -> true ; error(TExpr,'Value must be a natural (>= 0)')). |
153 | | convert_pref_val(neg,TExpr,Val) :- !, |
154 | | convert_pref_val(int,TExpr,Val), |
155 | | ((ground(Val),Val =< 0) -> true ; error(TExpr,'Value must be non-positive (<= 0)')). |
156 | | convert_pref_val(nat1,TExpr,Val) :- !, |
157 | | convert_pref_val(int,TExpr,Val), |
158 | | ((ground(Val),Val >= 1) -> true ; error(TExpr,'Value must be a natural >= 1')). |
159 | | convert_pref_val(range(Low,Up),TExpr,Val) :-!, |
160 | | convert_pref_val(int,TExpr,Val), |
161 | | ( ground(Val),Val >= Low, Val =< Up -> true |
162 | | ; ajoin(['Value must be in the interval [',Low,',',Up,']'],Msg), |
163 | | error(TExpr,Msg)). |
164 | | convert_pref_val(bool,TExpr,Val) :- !, |
165 | | (get_texpr_type(TExpr,boolean) -> true ; check_type(string,TExpr)), |
166 | | compute_expr(TExpr,BVal), |
167 | | ( BVal = pred_true /* bool_true */ -> Val = true |
168 | | ; BVal = pred_false /* bool_false */ -> Val = false |
169 | | ; BVal=string(Val),member(Val,[false,true]) -> true |
170 | | ; BVal=string(S),member(S/Val,['FALSE'/false,'TRUE'/true]) -> true |
171 | | ; add_error(pref_definitions,'Unexpected preference value (neither TRUE nor FALSE)',BVal,TExpr)). |
172 | | convert_pref_val(axbool,TExpr,Val) :- !, % extended boolean with auto option |
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,full,auto]) -> true |
178 | | ; BVal=string(S),member(S/Val,['FALSE'/false,'TRUE'/true,'FULL'/full,'AUTO'/auto]) -> true |
179 | | ; add_error(pref_definitions,'Unexpected preference value (neither TRUE, FALSE, full nor auto)',BVal,TExpr)). |
180 | | convert_pref_val(xbool,TExpr,Val) :- !, % extended boolean |
181 | | (get_texpr_type(TExpr,boolean) -> true ; check_type(string,TExpr)), |
182 | | compute_expr(TExpr,BVal), |
183 | | ( BVal = pred_true /* bool_true */ -> Val = true |
184 | | ; BVal = pred_false /* bool_false */ -> Val = false |
185 | | ; BVal=string(Val),member(Val,[false,true,full]) -> true |
186 | | ; BVal=string(S),member(S/Val,['FALSE'/false,'TRUE'/true,'FULL'/full]) -> true |
187 | | ; add_error(pref_definitions,'Unexpected preference value (neither TRUE, FALSE nor full)',BVal,TExpr)). |
188 | | convert_pref_val(dbool,TExpr,Val) :- !, % extended boolean |
189 | | (get_texpr_type(TExpr,boolean) -> true ; check_type(string,TExpr)), |
190 | | compute_expr(TExpr,BVal), |
191 | | ( BVal = pred_true /* bool_true */ -> Val = true |
192 | | ; BVal = pred_false /* bool_false */ -> Val = false |
193 | | ; BVal=string(Val),member(Val,[false,true,default]) -> true |
194 | | ; BVal=string(S),member(S/Val,['FALSE'/false,'TRUE'/true,'DEFAULT'/default]) -> true |
195 | | ; add_error(pref_definitions,'Unexpected preference value (neither TRUE, FALSE nor default)',BVal,TExpr)). |
196 | | convert_pref_val(string,TExpr,Val) :- !, |
197 | | check_type(string, TExpr), |
198 | | get_texpr_expr(TExpr,string(Val)). |
199 | | convert_pref_val(path,TExpr,Val) :- !, |
200 | | check_type(string, TExpr), |
201 | | get_texpr_expr(TExpr,string(Val)). |
202 | | convert_pref_val([H|T],TExpr,Val) :- !, |
203 | | check_type(string, TExpr), |
204 | | get_texpr_expr(TExpr,string(Val)), |
205 | ? | (member(Val,[H|T]) -> true |
206 | | ; ajoin_with_sep(['Value must be one of:',H|T],' ',Msg), |
207 | | error(TExpr,Msg)). |
208 | | convert_pref_val(Type,TExpr,Val) :- pref_type_synonym(Type,OtherType),!, |
209 | | convert_pref_val(OtherType,TExpr,Val). |
210 | | convert_pref_val(PrefType,TExpr,Res) :- |
211 | | get_texpr_expr(TExpr,string(Val)), |
212 | | is_of_type(Val,PrefType),!, % the user provided a string which matches exactly a valid preference value |
213 | | Res = Val. |
214 | | convert_pref_val(PrefType,TExpr,_Val) :- |
215 | | add_error(pref_definitions,'Unsupported preference type in DEFINITIONS:',PrefType,TExpr),fail. |
216 | | |
217 | | :- use_module(b_interpreter,[b_compute_expression_nowf/6]). |
218 | | compute_expr(TExpr,Res) :- |
219 | | if( b_compute_expression_nowf(TExpr,[],[],R,'DEFINITION preference',0) , Res=R , |
220 | | add_error_fail(pref_definitions,'Computing expression failed: ',TExpr)). |
221 | | error(TExpr,Msg) :- |
222 | | get_texpr_pos(TExpr,Pos), |
223 | | add_all_perrors([error(Msg,Pos)]), |
224 | | fail. |
225 | | |
226 | | check_type(Type,TExpr) :- |
227 | | get_texpr_type(TExpr,EType), |
228 | | get_texpr_pos(TExpr,Pos), |
229 | | unify_types_werrors(Type,EType,Pos,'PREFERENCE'). |
230 | | |
231 | | % ------------------- |
232 | | |
233 | | |
234 | | :- use_module(tools,[safe_atom_codes/2, string_concatenate/3]). |
235 | | :- use_module(bmachine,[b_definition_prefixed/5,b_get_definition_string_from_machine/3]). |
236 | | :- use_module(specfile,[animation_mode/1]). |
237 | | :- use_module(xtl_interface,[xtl_get_definition_string/2]). |
238 | | |
239 | | /* for tcltk: */ |
240 | | b_get_definition_string_list_from_spec(Def_Name_Prefix,Result) :- |
241 | | atom_codes(Def_Name_Prefix,Codes), append(Codes,_,CodesPrefix), |
242 | | findall(S, (b_get_definition_string_from_spec(Def_Name,_,DS), |
243 | | safe_atom_codes(Def_Name,CodesPrefix), /* check that name begins with the same characters as Def_Name_Prefix */ |
244 | | string_concatenate(DS,';',S)), Result). |
245 | | |
246 | | b_get_definition_string_from_spec(Def_Name,Pos,DS) :- animation_mode(xtl),!, Pos=unknown, |
247 | | xtl_get_definition_string(Def_Name,DS). |
248 | | %TODO: also support CSP |
249 | | b_get_definition_string_from_spec(_,_,_) :- animation_mode(cspm),!,fail. |
250 | | b_get_definition_string_from_spec(Def_Name,Pos,DS) :- |
251 | | b_get_definition_string_from_machine(Def_Name,Pos,DS). |
252 | | |