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