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		compute_static_expr_for_pref/3]).
11
12		:- use_module(module_information).
13		:- module_info(group,tools).
14		:- module_info(description,'Tools for extracting information from DEFINITIONS.').
15
16		:- use_module(error_manager).
17		:- use_module(self_check).
18		:- use_module(tools,[ajoin/2, ajoin_with_sep/3]).
19		:- use_module(bmachine,[b_definition_prefixed/5,b_get_typed_definition/3]).
20		:- use_module(preferences,[temporary_set_preference/2,eclipse_preference/2,deprecated_eclipse_preference/4,
21		obsolete_preference/1, preference_val_type/2, pref_type_synonym/2, is_of_type/2]).
22		:- use_module(btypechecker,[unify_types_werrors/4]).
23		:- use_module(bsyntaxtree).
24		:- use_module(debug,[debug_println/2]).
25		% get and set important preferences from a raw, untyped machine (as they
26		% may influence type checking,...);
27		% example: IGNORE_PRJ_TYPES, WARN_IF_DEFINITION_HIDES_VARIABLE
28		b_get_important_preferences_from_raw_machine(RawMachine,RawModelType) :-
29		(b_get_important_pref_type(RawModelType,Pref,PVal) ;
30		b_get_important_pref_mach(RawMachine,Pref,PVal)),
31		(temporary_set_preference(Pref,PVal)
32		-> debug_println(9,set_important_pref(Pref,PVal))
33		; add_error(pref_definitions,'Could not set DEFINITION preference to specified value: ',PVal)
34		),
35		fail.
36		b_get_important_preferences_from_raw_machine(_,_).
37
38		b_get_important_pref_mach(RawMachine,Pref,PVal) :-
39	?	member(definitions(_Pos,Defs),RawMachine),
40	?	member(expression_definition(_DPOS,DefName,[],RawVALUE),Defs),
41		(atom(DefName) -> true ; add_internal_error('Non-atomic DEFINITION id:',DefName),fail),
42		atom_concat('SET_PREF_',PREFString,DefName),
43		(eclipse_preference(PREFString,Pref) -> true
44		; additional_important_preference_during_loading(PREFString), Pref=PREFString),
45		preference_val_type(Pref,PType),
46		(PType=bool ; PType=xbool ; PType=dbool; PType=solver_name), % at the moment only boolean preferences supported
47		convert_raw_pref_val(PType,RawVALUE,PVal).
48
49
50		% important preferences that influence type checking, loading, deferred set setup, ...
51		% these preferences should be set before a machine is typechecked and pre-compiled (they are used in ast_cleanup)
52		additional_important_preference_during_loading(convert_comprehension_sets_into_closures).
53		additional_important_preference_during_loading(detect_lambdas).
54		additional_important_preference_during_loading(disprover_mode).
55		additional_important_preference_during_loading(ignore_prj_types).
56		additional_important_preference_during_loading(lift_existential_quantifiers).
57		additional_important_preference_during_loading(normalize_ast).
58		additional_important_preference_during_loading(normalize_ast_sort_commutative).
59		additional_important_preference_during_loading(optimize_ast).
60		%additional_important_preference_during_loading(optimize_enum_set_elems). % hidden, has no eclipse_preference fact
61		additional_important_preference_during_loading(perform_enumeration_order_analysis).
62		additional_important_preference_during_loading(perform_stricter_static_checks).
63		additional_important_preference_during_loading(prob_safe_mode).
64		additional_important_preference_during_loading(remove_implied_constraints).
65		additional_important_preference_during_loading(use_clpfd_solver).
66		additional_important_preference_during_loading(use_common_subexpression_elimination).
67		additional_important_preference_during_loading(use_static_symmetry_detection).
68		additional_important_preference_during_loading(useless_code_elimination).
69		additional_important_preference_during_loading('KODKOD'). % deprecated, but can still be set
70
71		b_get_important_pref_type(system(Pos),Pref,PVal) :-
72		% SET_PREF_ALLOW_NEW_OPERATIONS_IN_REFINEMENT == TRUE;
73		% for Event-B Atelier-B style; alternatively we could set animation_minor_mode ?
74		% TODO: we could have an implementation machine which refines a system model
75		add_message(pref_definitions,'Detected Event-B model; setting ALLOW_NEW_OPERATIONS_IN_REFINEMENT to ','TRUE',Pos),
76		Pref=allow_new_ops_in_refinement, PVal=true.
77		% maybe we should also set SHOW_EVENTB_ANY_VALUES (show_eventb_any_arguments) to TRUE
78
79		convert_raw_pref_val(axbool,Raw,Res) :- convert_raw_pref_val(bool,Raw,Res). % full
80		convert_raw_pref_val(xbool,Raw,Res) :- convert_raw_pref_val(bool,Raw,Res). % full
81		convert_raw_pref_val(dbool,Raw,Res) :- convert_raw_pref_val(bool,Raw,Res). % TODO: support default
82		convert_raw_pref_val(bool,boolean_true(_),true).
83		convert_raw_pref_val(bool,boolean_false(_),false).
84		convert_raw_pref_val(solver_name,string(_,String),String).
85		%convert_raw_pref_val(int,integer(_,V),V).
86		%convert_raw_pref_val(nat,integer(_,V),V). % range checking done in temporary_set_preference
87		%convert_raw_pref_val(nat1,integer(_,V),V).
88		%convert_raw_pref_val(neg,integer(_,V),V).
89		%convert_raw_pref_val(range(_,_),integer(_,V),V).
90		%convert_raw_pref_val(string(_),string(_,S),S).
91
92		:- use_module(translate,[translate_bexpression/2]).
93		b_get_preferences_from_specification(List) :-
94		findall(set_pref(String,ValS),(get_def_aux(String,TExpr),translate_bexpression(TExpr,ValS)),List).
95		% now a version that does not need to obtain a list with all preferences set:
96		b_get_preferences_from_specification :- get_def_aux(_,_),fail.
97		b_get_preferences_from_specification.
98
99		get_def_aux(String,TExpr) :-
100		b_get_set_pref_definition(_DefName,String,TExpr,DefPos),
101		set_pref_from_machine(String,DefPos,TExpr).
102
103		b_get_set_pref_definition(DefName,String,TExpr) :-
104		b_get_set_pref_definition(DefName,String,TExpr,_).
105
106		b_get_set_pref_definition(DefName,String,TExpr,DefPos) :- animation_mode(xtl),!,
107		xtl_get_definition_string(DefName,ValString),
108		atom(DefName),
109		atom_concat('SET_PREF_',String,DefName),
110		DefPos=unknown,
111		generate_value(ValString,TExpr).
112		b_get_set_pref_definition(DefName,String,TExpr,DefPos) :-
113		b_definition_prefixed(_,'SET_PREF_',String,DefName,DefPos),
114		b_get_typed_definition(DefName,[constants],TExpr). % scope=constants allows to use other definitions
115
116
117		:- use_module(tools,[safe_number_codes/2]).
118		generate_value(Nr,Res) :- integer(Nr), !,
119		Res = b(integer(Nr),integer,[]).
120		% TO DO: booleans
121		generate_value(ValString,b(string(ValString),string,[])).
122
123		:- use_module(tools_matching,[get_possible_preferences_matches_msg/2]).
124		set_pref_from_machine(String,DefPos,TExpr) :-
125		(eclipse_preference(String,Pref) -> preference_val_type(Pref,PType)
126		; preference_val_type(String,_) -> Pref=String, % user uses directly internal Prolog Name
127		preference_val_type(Pref,PType)
128		; deprecated_eclipse_preference(String,PType,Pref,Mapping)
129		),
130		!,
131		ajoin(['SET_PREF DEFINITION for ',String],Context),
132		convert_pref_val(PType,Context,TExpr,PVal),
133		(Mapping=[],temporary_set_preference(Pref,PVal)
134		-> add_debug_message(pref_definitions,'Setting DEFINITION preference: ',(String:PVal),DefPos)
135		; member(PVal/NewVal,Mapping), temporary_set_preference(Pref,NewVal)
136		-> add_debug_message(pref_definitions,'Setting deprecated DEFINITION preference: ',(String:NewVal),DefPos)
137		; add_error(pref_definitions,'Could not set DEFINITION preference: ',(String:PVal),DefPos)
138		).
139		set_pref_from_machine(String,DefPos,_TExpr) :- obsolete_preference(String),!,
140		add_warning(pref_definitions,'SET_PREF DEFINITION preference is obsolete: ',String,DefPos).
141		set_pref_from_machine(String,DefPos,_TExpr) :-
142		get_possible_preferences_matches_msg(String,FuzzyMatches),
143		!,
144		ajoin(['Error in SET_PREF DEFINITION. Preference ',String,' does not exist! Did you mean: '],Msg),
145		add_warning(pref_definitions,Msg,FuzzyMatches,DefPos),fail.
146		set_pref_from_machine(String,DefPos,_TExpr) :-
147		add_warning(pref_definitions,'Error in SET_PREF DEFINITION. Preference does not exist: ',String,DefPos),fail.
148
149		convert_pref_val(int,PrefName,TExpr,Val) :- !,
150		check_type(integer,TExpr,PrefName),
151		compute_static_expr_for_pref(TExpr,PrefName,int(Val)).
152		convert_pref_val(nat,PrefName,TExpr,Val) :- !,
153		convert_pref_val(int,PrefName,TExpr,Val),
154		((ground(Val),Val >= 0) -> true ; error(TExpr,'Value must be a natural (>= 0)')).
155		convert_pref_val(neg,PrefName,TExpr,Val) :- !,
156		convert_pref_val(int,PrefName,TExpr,Val),
157		((ground(Val),Val =< 0) -> true ; error(TExpr,'Value must be non-positive (<= 0)')).
158		convert_pref_val(nat1,PrefName,TExpr,Val) :- !,
159		convert_pref_val(int,PrefName,TExpr,Val),
160		((ground(Val),Val >= 1) -> true ; error(TExpr,'Value must be a natural >= 1')).
161		convert_pref_val(range(Low,Up),PrefName,TExpr,Val) :-!,
162		convert_pref_val(int,PrefName,TExpr,Val),
163		( ground(Val),Val >= Low, Val =< Up -> true
164		; ajoin(['Value must be in the interval [',Low,',',Up,']'],Msg),
165		error(TExpr,Msg)).
166		convert_pref_val(bool,PrefName,TExpr,Val) :- !,
167		(get_texpr_type(TExpr,boolean) -> true ; check_type(string,TExpr,PrefName)),
168		compute_static_expr_for_pref(TExpr,PrefName,BVal),
169		( BVal = pred_true /* bool_true */ -> Val = true
170		; BVal = pred_false /* bool_false */ -> Val = false
171		; BVal=string(Val),member(Val,[false,true]) -> true
172		; BVal=string(S),member(S/Val,['FALSE'/false,'TRUE'/true]) -> true
173		; add_error(pref_definitions,'Unexpected preference value (neither TRUE nor FALSE)',BVal,TExpr)).
174		convert_pref_val(axbool,PrefName,TExpr,Val) :- !, % extended boolean with auto option
175		(get_texpr_type(TExpr,boolean) -> true ; check_type(string,TExpr,PrefName)),
176		compute_static_expr_for_pref(TExpr,PrefName,BVal),
177		( BVal = pred_true /* bool_true */ -> Val = true
178		; BVal = pred_false /* bool_false */ -> Val = false
179		; BVal=string(Val),member(Val,[false,true,full,auto]) -> true
180		; BVal=string(S),member(S/Val,['FALSE'/false,'TRUE'/true,'FULL'/full,'AUTO'/auto]) -> true
181		; add_error(pref_definitions,'Unexpected preference value (neither TRUE, FALSE, full nor auto)',BVal,TExpr)).
182		convert_pref_val(xbool,PrefName,TExpr,Val) :- !, % extended boolean
183		(get_texpr_type(TExpr,boolean) -> true ; check_type(string,TExpr,PrefName)),
184		compute_static_expr_for_pref(TExpr,PrefName,Val),
185		( BVal = pred_true /* bool_true */ -> Val = true
186		; BVal = pred_false /* bool_false */ -> Val = false
187		; BVal=string(Val),member(Val,[false,true,full]) -> true
188		; BVal=string(S),member(S/Val,['FALSE'/false,'TRUE'/true,'FULL'/full]) -> true
189		; add_error(pref_definitions,'Unexpected preference value (neither TRUE, FALSE nor full)',BVal,TExpr)).
190		convert_pref_val(dbool,PrefName,TExpr,Val) :- !, % extended boolean
191		(get_texpr_type(TExpr,boolean) -> true ; check_type(string,TExpr,PrefName)),
192		compute_static_expr_for_pref(TExpr,PrefName,BVal),
193		( BVal = pred_true /* bool_true */ -> Val = true
194		; BVal = pred_false /* bool_false */ -> Val = false
195		; BVal=string(Val),member(Val,[false,true,default]) -> true
196		; BVal=string(S),member(S/Val,['FALSE'/false,'TRUE'/true,'DEFAULT'/default]) -> true
197		; add_error(pref_definitions,'Unexpected preference value (neither TRUE, FALSE nor default)',BVal,TExpr)).
198		convert_pref_val(string,PrefName,TExpr,Val) :- !,
199		check_type(string, TExpr,PrefName),
200		get_texpr_expr(TExpr,string(Val)).
201		convert_pref_val(path,PrefName,TExpr,Val) :- !,
202		check_type(string, TExpr,PrefName),
203		get_texpr_expr(TExpr,string(Val)).
204		convert_pref_val([H|T],PrefName,TExpr,Val) :- !,
205		check_type(string, TExpr,PrefName),
206		get_texpr_expr(TExpr,string(Val)),
207		(member(Val,[H|T]) -> true
208		; ajoin_with_sep(['Value must be one of:',H|T],' ',Msg),
209		error(TExpr,Msg)).
210		convert_pref_val(Type,PrefName,TExpr,Val) :- pref_type_synonym(Type,OtherType),!,
211		convert_pref_val(OtherType,PrefName,TExpr,Val).
212		convert_pref_val(PrefType,_PrefName,TExpr,Res) :-
213		get_texpr_expr(TExpr,string(Val)),
214		is_of_type(Val,PrefType),!, % the user provided a string which matches exactly a valid preference value
215		Res = Val.
216		convert_pref_val(PrefType,PrefName,TExpr,_Val) :-
217		ajoin(['Unsupported preference type in SET_PREF DEFINITION for ',PrefName,':'],Msg),
218		add_error(pref_definitions,Msg,PrefType,TExpr),fail.
219
220		:- use_module(bsyntaxtree, [find_identifier_uses/3]).
221		:- use_module(b_interpreter,[b_compute_expression_nowf/6]).
222		compute_static_expr_for_pref(TExpr,PrefName,_Res) :-
223		find_identifier_uses(TExpr,[],Ids),
224		% Note: enumerated sets,... are not yet pre-compiled and evaluation below will fail if any id is used
225		Ids \= [],
226		!,
227		ajoin_with_sep(Ids,',',SIDS),
228		ajoin([PrefName, ' is not static and depends on ',SIDS,':'],Msg),
229		add_error_fail(pref_definitions,Msg,TExpr).
230		compute_static_expr_for_pref(TExpr,PrefName,Res) :-
231		if( b_compute_expression_nowf(TExpr,[],[],R,PrefName,0) , Res=R ,
232		(ajoin(['Computing expression failed for ',PrefName,':'],Msg),
233		add_error_fail(pref_definitions,Msg,TExpr))).
234		error(TExpr,Msg) :-
235		get_texpr_pos(TExpr,Pos),
236		add_all_perrors([error(Msg,Pos)]),
237		fail.
238
239		check_type(Type,TExpr,PrefName) :-
240		get_texpr_type(TExpr,EType),
241		get_texpr_pos(TExpr,Pos),
242		unify_types_werrors(Type,EType,Pos,PrefName).
243
244		% -------------------
245
246
247		:- use_module(tools,[safe_atom_codes/2, string_concatenate/3]).
248		:- use_module(bmachine,[b_definition_prefixed/5,b_get_definition_string_from_machine/3]).
249		:- use_module(specfile,[animation_mode/1]).
250		:- use_module(xtl_interface,[xtl_get_definition_string/2]).
251
252		/* for tcltk: */
253		b_get_definition_string_list_from_spec(Def_Name_Prefix,Result) :-
254		atom_codes(Def_Name_Prefix,Codes), append(Codes,_,CodesPrefix),
255		findall(S, (b_get_definition_string_from_spec(Def_Name,_,DS),
256		safe_atom_codes(Def_Name,CodesPrefix), /* check that name begins with the same characters as Def_Name_Prefix */
257		string_concatenate(DS,';',S)), Result).
258
259		b_get_definition_string_from_spec(Def_Name,Pos,DS) :- animation_mode(xtl),!, Pos=unknown,
260		xtl_get_definition_string(Def_Name,DS).
261		%TODO: also support CSP
262		b_get_definition_string_from_spec(_,_,_) :- animation_mode(cspm),!,fail.
263		b_get_definition_string_from_spec(Def_Name,Pos,DS) :-
264		b_get_definition_string_from_machine(Def_Name,Pos,DS).
265