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 | | |