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