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