1		% (c) 2009-2019 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
6		:- module(b_compiler,[b_compile/6, b_optimize/6]).
7
8		:- use_module(library(lists)).
9
10		:- use_module(self_check).
11		:- use_module(bsyntaxtree).
12		:- use_module(error_manager).
13		:- use_module(btypechecker,[fasttype/2]).
14		:- use_module(b_interpreter).
15		:- use_module(custom_explicit_sets).
16		%:- use_module(bmachine,[b_operation_reads_output_variables/3]).
17
18		:- use_module(module_information,[module_info/2]).
19		:- module_info(group,interpreter).
20		:- module_info(description,'This module compiles set comprehensions into closures; making them independent of the state of the B machine.').
21
22		/* compile boolean expression into a closure where the local state and the global
23		state has been incorporated, but any parameter is left in the closure */
24
25		:- public test_bexpr/3, test_bexpr2/3.
26		test_bexpr(Expr,[bind(cc,int(1)),bind(nn,int(2))], [bind(db,[(int(1),int(2))])]) :-
27		fasttype( +conjunct( +conjunct( +member( global('Name')<<identifier(nn), +identifier('Name')),
28		+member( global('Code')<<identifier(cc), +identifier('Code'))),
29		+not_member( global('Name')<<identifier(nn),
30		+domain(set(couple(global('Name'),global('Code')))<<identifier(db)))), Expr).
31
32		test_bexpr2(Expr,[],[]) :-
33		fasttype( +implication( +equal( seq(any)<<identifier(ss), +empty_sequence),
34		+equal( set(any)<<identifier(res), +empty_set)), Expr).
35
36
37		% difference with b_compile: the states LS, S will not be thrown away by the interpreter
38		% thus: we do not have to compile all accesses, in particular lazy lookups !
39		%b_optimize(TExpr,Parameters,_LS,_S,NTExpr,_WF) :- TExpr=b(_,_,Infos), member(already_optimized,Infos),
40		% !, NTExpr=TExpr.
41		b_optimize(TExpr,Parameters,LS,S,NTExpr,WF) :- %print('OPTIMIZE: '),translate:print_bexpr(TExpr),nl, trace,
42		append(LS,[bind('$do_not_force_lazy_lookups',pred_true)],NewLS),
43		b_compile(TExpr,Parameters,NewLS,S,NTExpr,WF).
44		%bsyntaxtree:add_texpr_info_if_new(NTExpr,already_optimized,ResTExpr).
45
46		b_compile(TExpr,Parameters,NewLS,S,NTExpr) :-
47		b_compile(TExpr,Parameters,NewLS,S,NTExpr,no_wf_available). % for unit tests
48
49		:- assert_must_succeed(( b_compiler:test_bexpr(E,L,S),
50		b_compiler:b_compile(E,[nn],L,S,_R) )).
51		:- assert_must_succeed(( b_compiler:test_bexpr2(E,L,S),
52		b_compiler:b_compile(E,[ss,res],L,S,_R) )).
53
54		%:- assert_pre(b_compiler:b_compile_boolean_expression(E,Parameters,LS,S,_),
55		% (type_check(E,boolean_expression),type_check(Parameters,list(variable_id)),
56		% type_check(LS,store),type_check(S,store))).
57		%:- assert_post(b_compiler:b_compile_boolean_expression(_,_,_,_,E), type_check(E,boolean_expression)).
58
59		/* probably not worthwhile:
60		b_compile(TExpr,Parameters,LS,S,NTExpr) :- get_texpr_info(TExpr,Info),
61		(memberchk(compiled(Parameters),Info) -> NTExpr = TExpr ,print(already_compiled(Parameters)),nl, translate:print_bexpr(TExpr),nl
62		; b_compile0(TExpr,Parameters,LS,S,b(E,T,I)), translate:print(compiling(Parameters)),nl, translate:print_bexpr(TExpr),nl,
63		NTExpr = b(E,T,[compiled(Parameters)|I])).
64		*/
65
66		b_compile(TExpr,Parameters,LS,S,NTExpr,WF) :- check_is_id_list(Parameters,Parameters1),
67		% print('compile : '),translate:print_bexpr(TExpr),nl, statistics(runtime,[Start,_]),%%
68		if(b_compile1(TExpr,Parameters1,LS,S,NTExpr0,eval,_FullyKnown,WF),
69		copy_pos_infos(TExpr,NTExpr0,NTExpr), % ensure position info is not deleted if full expression compiled away, see PROB-412
70		(add_internal_error('Compilation failed: ',b_compile(TExpr,Parameters,LS,S,NTExpr,WF)),
71		%b_compile1(TExpr,Parameters1,LS,S,NTExpr0,eval,_FullyKnown,WF),
72		NTExpr = TExpr)
73		). %, check_infos(TExpr,NTExpr).
74		%, print('compiled: '), translate:print_bexpr(NTExpr), print(' '),statistics(runtime,[Stop,_]), T is Stop-Start, print(T), print(' ms '),nl, bsyntaxtree:check_ast(NTExpr). % , print(NTExpr),nl. check_ast
75
76		/*
77		check_infos(Old,New) :- bsyntaxtree:get_texpr_info(Old,IO),
78		bsyntaxtree:get_texpr_info(New,IN),
79		member(X,IO), \+ member(X,IN),
80		bsyntaxtree:important_info(X),
81		print(check_infos(Old,New)),nl,
82		print('Not copied: '), print(X),fail.
83		check_infos(_,_). */
84
85		:- use_module(bsyntaxtree,[always_well_defined/1]).
86		:- use_module(translate,[translate_bexpression_with_limit/2]).
87		%:- use_module(hit_profiler,[add_profile_hit/1]).
88		b_compile1(TExpr,Parameters,LS,S,ResultTExpr,Eval,FullyKnown1,WF) :-
89		TExpr = b(Expr,Type,Infos),
90		NTExpr = b(NewUntypedExpr,Type,NewInfos),
91		%remove_bt(TExpr,Expr,NewUntypedExpr,NTExpr), % remove top-level Type Information
92		%hit_profiler:add_profile_hit(Expr),
93		b_compile1_infos(Expr,Infos,Parameters,LS,S,NewUntypedExpr,NewInfos,Eval,FullyKnown,WF),
94		% print(' compiled : '),translate:print_bexpr_or_subst(NTExpr),nl,
95		% print(res(FullyKnown,Eval,NTExpr)),nl,
96		(FullyKnown=true, evaluate_this(Eval,NewUntypedExpr,Type,NewInfos)
97		-> % print('eval : '),translate:print_bexpr(NTExpr),nl, %
98		(nonvar(NewUntypedExpr),
99		b_interpreter:b_compute_expression_nowf(NTExpr,LS,S,ResultValue) % if( would be more prudent !?
100		-> %print(result(ResultValue)),nl,
101		%remove_bt(TExpr,Expr,value(ResultValue),ResultTExpr)
102		get_texpr_type(TExpr,TT),ResultTExpr = b(value(ResultValue),TT,[]),
103		FullyKnown1 = FullyKnown
104		%, print(compiled_value(ResultTExpr)),nl
105		; translate_bexpression_with_limit(NTExpr,TTS),
106		add_internal_error('Undefined Value: ',b_compile1(TTS,Parameters,LS,S,_,_,_,WF)),
107		%trace, b_interpreter:b_compute_expression_nowf(NTExpr,LS,S,ResultValue),
108		ResultTExpr=NTExpr, FullyKnown1=false
109		)
110		; % ((FullyKnown=true, NTExpr\=b(value(_),_,_)) -> format('not eval: ~w (~w)~n',[NTExpr,Eval]) ; true),
111		ResultTExpr=NTExpr,
112		(ResultTExpr = b(value(_),_,_) -> FullyKnown1=FullyKnown ; FullyKnown1=false)
113		).
114
115
116		:- use_module(bsyntaxtree,[create_exists_or_let_predicate/3]).
117		b_compile1_infos(exists(ExistsPara,Pred),OldInfos,Parameters,LS,S,NExpr,NewInfos,Eval,FullyKnown,WF) :- !,
118		FullyKnown=false, % predicates never automatically evaluated in b_compile1
119		get_texpr_ids(ExistsPara,AtomicIds),
120		append(Parameters,AtomicIds,NParameters),
121		b_compile1(Pred,NParameters,LS,S,NPred,Eval,_FullyKnown1,WF),
122		(is_falsity(NPred) -> NExpr = falsity, NewInfos = OldInfos
123		; is_truth(NPred) -> NExpr = truth, NewInfos = OldInfos
124		; create_exists_or_let_predicate(ExistsPara,NPred,b(NExpr,pred,NI)),
125		%print('COMPILED EXISTS: '), translate:print_bexpr(b(NExpr,pred,NI)),nl,
126	?	(delete(OldInfos,used_ids(_),I1),
127	?	member(used_ids(NewUsedIds),NI) -> NewInfos = [used_ids(NewUsedIds)|I1]
128		; %nl,print(missing_used_ids(OldInfos,NI)),nl, % can happen when we construt a let_predicate above
129		update_infos(NExpr,OldInfos,Parameters,NewInfos))
130		).
131		b_compile1_infos(identifier(Id),OldInfos,Parameters,LS,S,NExpr,NewInfos,Eval,FullyKnown,WF) :- !,
132		( memberchk(Id,Parameters) ->
133		NExpr = identifier(Id), FullyKnown=false, NewInfos = OldInfos
134		; Id=op(_) ->
135		NExpr = identifier(Id), FullyKnown=false, NewInfos = OldInfos
136		; b_interpreter:lookup_value_in_store_and_global_sets(Id,LS,S,Value) ->
137		NExpr = value(Value), (known_value(Value) -> FullyKnown=true ; FullyKnown=false),
138		NewInfos = [was_identifier(Id)|OldInfos]
139		% TO DO: store in info field the identifier
140		; add_internal_error('Compilation of identifier failed: ',
141		b_compile2(identifier(Id),Parameters,LS,S,NExpr,Eval,FullyKnown,WF)),
142		NExpr = identifier(Id), FullyKnown=false, NewInfos = OldInfos
143		).
144		b_compile1_infos(Expr,OldInfos,_Parameters,_LS,_S,NewUntypedExpr,NewInfos,_Eval,FullyKnown,_WF) :-
145		b_ast_cleanup:is_integer_set(Expr,_Set),!,
146		NewUntypedExpr=Expr, NewInfos=OldInfos,FullyKnown=true.
147		b_compile1_infos(operation_call_in_expr(Operation,OpCallParas),OldInfos,Parameters,LS,S,
148		Compiled,NewInfos,Eval,FullyKnown,WF) :- !,
149		def_get_texpr_id(Operation,op(OperationName)),
150		FullyKnown = false,
151		b_compile_l(OpCallParas,Parameters,LS,S,OpCallParaValues,Eval,_,WF),
152		b_get_operation_normalized_read_write_info(OperationName,Read,Modified),
153		exclude(operation_identifier,Read,ReadVars), % Read also contains operations; TO DO: check if this is ok in other places of source code of ProB; see test 1957
154		(Modified=[] -> true ; add_error(b_compiler,'Calling operation that modifies state in expression:',OperationName)),
155		% print(compile_call_op(OperationName,ReadVars,Modified,OpCallParaValues)),nl,
156		(ReadVars=[]
157		-> Compiled = operation_call_in_expr(Operation,OpCallParaValues),
158		NewInfos = OldInfos
159		; maplist(create_value_for_read_variable(LS,S),ReadVars,TRead,TValues),
160		NewInfos = [generated_by_b_compiler],
161		Compiled = let_expression_global(TRead,TValues,
162		b(operation_call_in_expr(Operation,OpCallParaValues),any,OldInfos))
163		).
164		b_compile1_infos(Expr,OldInfos,Parameters,LS,S,NewUntypedExpr,NewInfos,Eval,FullyKnown,WF) :-
165		b_compile2(Expr,Parameters,LS,S,NewUntypedExpr,Eval,FullyKnown,WF),
166		update_infos(NewUntypedExpr,OldInfos,Parameters,NewInfos).
167
168		:- use_module(bmachine,[b_get_operation_normalized_read_write_info/3]).
169
170		operation_identifier(op(_)).
171		create_value_for_read_variable(LS,S,Variable,TVariable,TValue) :-
172		b_interpreter:lookup_value_in_store_and_global_sets(Variable,LS,S,Value),!, % TO DO: try and find type?
173		TVariable = b(identifier(Variable),any,[]),
174		TValue = b(value(Value),any,[]).
175		create_value_for_read_variable(_LS,_S,Variable,TVariable,b(value(term(undefined)),any,[])) :-
176		TVariable = b(identifier(Variable),any,[]),
177		add_internal_error('Cannot find variable (read) while compiling operation:',Variable),fail.
178
179		:- use_module(library(ordsets)).
180		update_infos(forall(EParas,LHS,RHS),Infos,Parameters,NewInfos) :-
181		% forall also has used_ids field as it may call exists in negative context
182		conjunct_predicates([LHS,RHS],Cond),
183		update_infos_aux(EParas,Cond,Infos,Parameters,NewInfos),!.
184		update_infos(exists(EParas,Cond),Infos,Parameters,NewInfos) :- % we create_exists_or_let_predicate above, but other transformations may generate an exists below:
185		update_infos_aux(EParas,Cond,Infos,Parameters,NewInfos),!.
186		update_infos(BOP,Infos,_,NewInfos) :- bsyntaxtree:syntaxelement(BOP, [A,B],[], [], [], _),
187		wd_and_efficient(BOP), % should not generate WD errors itself
188	?	select(contains_wd_condition,Infos,NewInfos), % there is a WD condition attached
189		fast_check_wd(A), fast_check_wd(B),
190		%print(removing_wd_condition(BOP)),nl,
191		!.
192		update_infos(_,I,_,I).
193
194		update_infos_aux(EParas,Cond,Infos,Parameters,NewInfos) :-
195		select_used_ids(UsedIds,Infos,I1,EParas,Cond),
196		UsedIds \= [],!,
197		% remove those used identifiers which will be compiled into the predicate
198		sort(Parameters,SParas),
199		ord_intersection(UsedIds,SParas,NewUsedIds),
200		%print(update(Parameters,UsedIds,I1,new(NewUsedIds))),nl,
201		NewInfos = [used_ids(NewUsedIds)|I1].
202
203		:- use_module(bsyntaxtree,[find_identifier_uses/3]).
204	?	select_used_ids(UsedIds,Infos,I1,_,_) :- select(used_ids(UsedIds),Infos,I1),!.
205		% check_used_ids_info(Parameters,Condition,UsedIds,b_compiler)
206		select_used_ids(UsedIds,Infos,Infos,_Parameters,Condition) :-
207		%add_error(bcompiler,'Expected information of used identifiers in exists operation information : ',Parameters:Infos), %% missing info can happen due to simplifcation rules below !
208		find_identifier_uses(Condition, [], UsedIds). % ,print(used(UsedIds,in_exist(Parameters))),nl.
209		% TO DO: avoid re-computing used-ids; we should refactor b_compile2 to return new Info field
210
211		%is_pred(b(_,pred,_)).
212
213
214		evaluate_this(eval,X,Type,Info) :- !, worth_it_type(Type,X,Info).
215		evaluate_this(_,X,_Type,_Info) :- wd_and_efficient(X).
216
217
218		% things which are very quick to compute
219		wd_and_efficient(sequence_extension(_)) :- !.
220		wd_and_efficient(integer_set(_)) :- !. % will be converted into value(global_set(_))
221		%% wd_and_efficient(value(_)) :- !. % is already computed
222		% the following will reduce the size of the representation; usually a good thing;
223		% we assume only avl_sets apprear here; inner set comprehensions are never computed into symbolic form by b_compile (see known_value below):
224		%wd_and_efficient(identity(_)) :- !.
225		wd_and_efficient(range(_)) :- !.
226		wd_and_efficient(domain(_)) :- !.
227		wd_and_efficient(domain_restriction(_,_)) :- !.
228		wd_and_efficient(domain_subtraction(_,_)) :- !.
229		wd_and_efficient(range_restriction(_,_)) :- !.
230		wd_and_efficient(range_subtraction(_,_)) :- !.
231		wd_and_efficient(intersection(_,_)) :- !.
232		wd_and_efficient(set_subtraction(_,_)) :- !.
233		wd_and_efficient(image(_,_)) :- !.
234		% what about union: usually the union of two avl_sets will be smaller than keeping them separate
235		% some other efficient operators:
236		wd_and_efficient(X) :- worth_it_int(X),!.
237		wd_and_efficient(X) :- worth_it_other(X).
238
239		fast_check_wd(b(E,_,Infos)) :-
240		(nonmember(contains_wd_condition,Infos) -> true ; nonvar(E), E= value(_)).
241
242		check_wd(NTExpr) :- bsyntaxtree:always_well_defined(NTExpr). % ,print(wd(NTExpr)),nl.
243		%(bsyntaxtree:always_well_defined(NTExpr) -> true ; print(not_guaranteed_wd(NTExpr)),nl).
244
245		% (worth_it_type(Type,X,Info) -> true ; X=value(_) -> true ; print(not_evaluating(X)),nl,fail).
246		worth_it_type(integer,X,Info) :- worth_it_int_wd(X),!, check_wd(b(X,integer,Info)).
247		worth_it_type(T,function(A,B),Info) :- !,
248		(check_wd(b(function(A,B),T,Info)) -> true
249		; fail). %print('not_precompiling_function '),translate:print_bexpr(A), print(' @ '), translate:print_bexpr(B),nl,fail).
250		worth_it_type(integer,X,_) :- worth_it_int(X),!.
251		worth_it_type(T,X,Info) :- worth_it_wd(X),!, check_wd(b(X,T,Info)).
252		worth_it_type(set(_),X,_) :- worth_it_set(X),!.
253		worth_it_type(seq(_),X,_) :- worth_it_set(X),!.
254		worth_it_type(_,X,_) :- worth_it_other(X).
255
256		% TO DO: we should use the predicate has_wd_condition from b_ast_cleanup
257
258		% integer operations that could generate WD-errors
259		worth_it_int_wd(div(_,_)).
260		worth_it_int_wd(max(_)).
261		worth_it_int_wd(min(_)).
262		worth_it_int_wd(mod(_,_)).
263		worth_it_int_wd(power_of(_,_)).
264		worth_it_int_wd(card(_)). % has WD condition !!
265		worth_it_int_wd(size(_)).
266
267		% other operations that could generate WD-errors
268		worth_it_wd(first(_)).
269		worth_it_wd(last(_)).
270		worth_it_wd(tail(_)).
271		worth_it_wd(front(_)).
272		worth_it_wd(restrict_front(_,_)).
273		worth_it_wd(restrict_tail(_,_)).
274		worth_it_wd(rel_iterate(_,_)). %% could be expensive
275		worth_it_wd(general_intersection(_)).
276		worth_it_wd(general_concat(_)).
277
278		% to do: check other operators that could be not well-defined !
279
280		worth_it_int(unary_minus(_)).
281		worth_it_int(add(_,_)).
282		worth_it_int(minus(_,_)).
283		worth_it_int(multiplication(_,_)).
284		worth_it_int(max_int).
285		worth_it_int(min_int).
286
287		%worth_it_set(empty_set). % treated below
288		%worth_it_set(empty_sequence). % treated below
289		%worth_it_set(closure(_)). % this is closure1; it is currently always kept symbolic and can be counterproductive to compile; e.g., card(closure1(%x.(x : 1 .. 200|x + 1)))
290		%% ?? need to be more careful here; can be expensive --> need to keep track which parts need definitely to be evaluated
291		worth_it_set(integer_set(_)). % will be converted into value(global_set(_))
292		worth_it_set(comprehension_set(A,B)) :- b_ast_cleanup:is_integer_set(comprehension_set(A,B),_).
293		worth_it_set(interval(_,_)).
294		worth_it_set(reflexive_closure(_)).
295		worth_it_set(reverse(_)).
296		worth_it_set(domain(_)). worth_it_set(range(_)).
297		worth_it_set(union(_,_)). worth_it_set(intersection(_,_)). worth_it_set(set_subtraction(_,_)).
298		worth_it_set(image(_,_)). worth_it_set(composition(_,_)).
299		worth_it_set(domain_restriction(_,_)). worth_it_set(domain_subtraction(_,_)).
300		worth_it_set(range_restriction(_,_)). worth_it_set(range_subtraction(_,_)).
301		worth_it_set(direct_product(_,_)). worth_it_set(parallel_product(_,_)).
302		worth_it_set(iteration(_,_)).
303		worth_it_set(set_extension(_)).
304		worth_it_set(sequence_extension(_)).
305		worth_it_set(rev(_)).
306		worth_it_set(concat(_,_)).
307		worth_it_set(seq(_)). % will be kept symbolic anyway
308		worth_it_set(seq1(_)). % will be kept symbolic anyway
309		worth_it_set(iseq(_)). % will be kept symbolic anyway
310		worth_it_set(iseq1(_)). % will be kept symbolic anyway
311		worth_it_set(perm(_)). % will be kept symbolic anyway
312		worth_it_set(pow_subset(_)). % will be kept symbolic anyway
313		worth_it_set(pow1_subset(_)). % will be kept symbolic anyway
314		worth_it_set(fin_subset(_)). % will be kept symbolic anyway
315		worth_it_set(fin1_subset(_)). % will be kept symbolic anyway
316		worth_it_set(general_union(_)).
317		worth_it_set(identity(_)).
318		worth_it_set(first_of_pair(_)). % can also produce set
319		worth_it_set(second_of_pair(_)). % can also produce set
320		worth_it_set(cartesian_product(_,_)). % will usually be kept symbolic
321		worth_it_set(string_set). % ensure we have values inside compiled closures, e.g., for custom_explicit_set card computations
322		worth_it_set(bool_set).
323
324		:- use_module(external_functions,[not_declarative/1,external_fun_has_wd_condition/1]).
325		worth_it_other(boolean_true).
326		worth_it_other(boolean_false).
327		worth_it_other(string(_)).
328		worth_it_other(first_of_pair(_)).
329		worth_it_other(second_of_pair(_)).
330		worth_it_other(couple(_,_)).
331		worth_it_other(record_field(_,_)).
332		worth_it_other(external_function_call(FunName,_)) :-
333		\+ not_declarative(FunName),
334		\+ external_fun_has_wd_condition(FunName). %print(compile(FunName)),nl.
335		worth_it_other(rec(_)).
336		worth_it_other(struct(_)).
337		%worth_it_other(value(_)). % does not have to be evaluted; already a value
338
339		/*
340		% To do: distinguish which parts definitely need to be evaluated
341		%dont_eval_subexpressions(member). % special membership code can be used
342		%dont_eval_subexpressions(not_member). % special membership code can be used
343		dont_eval_subexpressions(disjunct(_,_)). % it may not be necessary to eval RHS
344		dont_eval_subexpressions(implication(_,_)). % it may not be necessary to eval RHS
345		*/
346
347		:- use_module(kernel_objects,[equal_object/3]).
348		:- use_module(kernel_mappings,[binary_boolean_operator/3]).
349		:- use_module(kernel_tools,[filter_cannot_match/4, get_template_for_filter_cannot_match/2]).
350		b_compile2(Exp,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- var(Exp), !,
351		add_internal_error('Variable Expression: ',b_compile2(Exp,Parameters,LS,S,NExpr,Eval,FullyKnown,WF)),
352		NExpr=Exp, FullyKnown=false.
353		b_compile2(truth,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=truth, FullyKnown=false. % predicates never fully known
354		b_compile2(falsity,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=falsity, FullyKnown=false. % predicates never fully known
355		b_compile2(empty_set,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value([]), FullyKnown=true.
356		b_compile2(empty_sequence,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value([]), FullyKnown=true.
357		b_compile2(value(Val),_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !,
358		NExpr=value(Val),
359		(known_value(Val) -> % ground(Val) -> known_value ?
360		FullyKnown=true ; FullyKnown=false).
361		b_compile2(integer(Val),_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !,
362		NExpr=value(int(Val)), (number(Val) -> FullyKnown=true ; FullyKnown=false).
363		b_compile2(lazy_lookup_pred(Id),Parameters,LS,S,NExpr,_Eval,FullyKnown,_WF) :- !,
364		( memberchk(Id,Parameters) -> %print(lazy_lookup_pred_id_as_parameter(Id,Parameters)),nl,
365		NExpr = lazy_lookup_pred(Id), FullyKnown=false
366		; otherwise -> compute_lazy_lookup(Id,lazy_lookup_pred(Id),LS,S,NExpr,FullyKnown)
367		).
368		b_compile2(lazy_lookup_expr(Id),Parameters,LS,S,NExpr,_Eval,FullyKnown,_WF) :- !,
369		( memberchk(Id,Parameters) -> %print(lazy_lookup_expr_id_as_parameter(Id,Parameters)),nl,
370		NExpr = lazy_lookup_expr(Id), FullyKnown=false
371		; otherwise -> compute_lazy_lookup(Id,lazy_lookup_expr(Id),LS,S,NExpr,FullyKnown)
372		).
373		% treat a few common cases, more efficiently than syntaxtransformation
374		b_compile2(equal(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
375		FullyKnown=false, % predicates never evaluated in b_compile1
376		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
377		b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
378		( FullyKnownA=true, FullyKnownB=true,
379		NExprA = b(value(VA),_,_), NExprB = b(value(VB),_,_)
380		-> %print(computing_eq(VA,VB)),nl,
381		(equal_object(VA,VB,b_compile2_1) -> NExpr = truth ; NExpr = falsity)
382		%, print(result(NExpr)),nl
383		; generate_equality(NExprA,NExprB,NExpr)
384		).
385		b_compile2(not_equal(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
386		FullyKnown=false, % predicates never evaluated in b_compile1
387		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
388		b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
389		( FullyKnownA=true, FullyKnownB=true,
390		NExprA = b(value(VA),_,_), NExprB = b(value(VB),_,_)
391		-> %print(computing_neq(VA,VB)),nl,
392		(kernel_objects:equal_object(VA,VB,b_compile2_2) -> NExpr = falsity ; NExpr = truth)
393		%, print(result(NExpr)),nl
394		; NExpr = not_equal(NExprA,NExprB)
395		).
396		b_compile2(member(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
397		FullyKnown=false, % predicates never evaluated in b_compile1
398		b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF),
399		(NExprB = b(value(X),BT,BI)
400		-> (X==[], always_well_defined(A) -> NExpr = falsity
401		; b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
402		% check if we can decide membership (e.g., 1:{1})
403	?	(quick_test_membership1(NExprA,X,PRes)
404		-> convert_pred_res(PRes,NExpr)
405		% TO DO: maybe optimize x: {y|P(y)} --> P(x) ; by commenting in code below
406		% However, ensure test 273 succeeds and closure equality correctly detected (e.g., for BV16 = {bt|bt : BIT_VECTOR & bv_size(bt) = 16})
407		% ; (get_texpr_id(NExprA,IDA),
408		% get_comprehension_set(NExprB,IDB,Pred), get_texpr_info(NExprB,Info),
409		% print(rename(IDB,IDA,Info)),nl,
410		% bsyntaxtree:rename_bt(Pred,[rename(IDB,IDA)],PredA)) -> get_texpr_expr(PredA,NExpr)
411		; custom_explicit_sets:singleton_set(X,El) % replace x:{El} -> x=El
412		-> get_texpr_type(NExprA,TA), NExpr = equal(NExprA,b(value(El),TA,[]))
413		; get_template_for_filter_cannot_match(NExprA,VA)
414		-> filter_cannot_match(X,VA,NewX,Filtered),
415		% (Filtered=false -> true ; print(filtered(NewX,VA,X)),nl),
416		(Filtered=false -> NExpr = member(NExprA,NExprB)
417		; (NewX==[], always_well_defined(A)) -> NExpr = falsity
418		; custom_explicit_sets:singleton_set(NewX,El)
419		-> get_texpr_type(NExprA,TA), NExpr = equal(NExprA,b(value(El),TA,[]))
420		; otherwise -> NExpr = member(NExprA, b(value(NewX),BT,BI))
421		)
422		% end fo filtering
423		; NExpr = member(NExprA,NExprB)
424		)
425		% , print('compile: '),print(NExpr),nl
426		)
427		; NExpr = member(NExprA,NExprB),
428		b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF)
429		).
430		% TO DO: also optimize things like: (ev1 |-> 0) |-> eg : #221:{((1|->0)|->3),((2|->0)|->0),...,((233|->0)|->218),((234|->0)|->228)}
431
432		b_compile2(not_member(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
433		FullyKnown=false, % predicates never evaluated in b_compile1
434		b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF),
435		(NExprB = b(value(X),_,_)
436		-> (X==[], always_well_defined(A) -> NExpr = truth
437		; b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
438		(quick_test_membership1(NExprA,X,PRes)
439		-> convert_neg_pred_res(PRes,NExpr)
440		; NExpr = not_member(NExprA,NExprB))
441		)
442		; NExpr = not_member(NExprA,NExprB),
443		b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF)
444		).
445		b_compile2(function(Fun,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
446		(is_extension_function_gt1(Fun) -> Eval1=false % extension function applications treated lazily
447		% TO DO: first evaluate B, if known then only evaluate relevant part of extension function
448		; Eval1=Eval),
449		b_compile1(Fun,Parameters,LS,S,NExprA,Eval1,FullyKnown1,WF),
450		combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown12),
451		b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF),
452		%tools_printing:print_term_summary(compiled_function(FullyKnown1,FullyKnown2,NExprA,NExprB)),nl,
453		(FullyKnown2=true, preferences:preference(find_abort_values,false),
454		% check if we have enough information to apply a partially specified function as a list
455		% e.g. if the function is [(int(1),A),(int(2),B)] and the argument is int(2): we can apply the function without knowing A or B; can have a dramatic importance when expanding unversal quantifiers !
456		can_apply_partially_specified_function(NExprA,NExprB,ResultExpr,WF)
457		-> NExpr = ResultExpr,
458		(FullyKnown12=true -> FullyKnown=true
459		; ResultExpr=value(ResultValue),known_value(ResultValue) -> FullyKnown=true
460		; FullyKnown = false)
461		; % print(cannot_apply_function(NExprA,NExprB,FullyKnown2)),nl,
462		NExpr = function(NExprA,NExprB), FullyKnown = FullyKnown12).
463
464		b_compile2(conjunct(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
465		FullyKnown=false, % predicates never automatically evaluated in b_compile1
466		b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
467		(is_falsity(NExprA) -> NExpr = falsity
468		;
469		% TO DO: propagate static information from A to B, e.g. if A :: x=10 -> add x=10 to LS/Parameters
470		% also: try and detect unsatisfiable predicates beforehand
471		b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF),
472		(is_falsity(NExprB) -> NExpr = falsity
473		; is_truth(NExprB) -> get_texpr_expr(NExprA,NExpr)
474		; is_truth(NExprA) -> get_texpr_expr(NExprB,NExpr)
475		; NExpr = conjunct(NExprA,NExprB))
476		).
477		b_compile2(disjunct(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
478		FullyKnown=false, % predicates never automatically evaluated in b_compile1
479		b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
480		(is_truth(NExprA) -> NExpr = truth
481		; b_compile1(B,Parameters,LS,S,NExprB,false,_,WF), % does not have to be executed in a successful branch: set Eval to false to avoid computing expensive expressions which may not be needed
482		(is_truth(NExprB) -> NExpr = truth
483		; is_falsity(NExprA) -> get_texpr_expr(NExprB,NExpr)
484		; is_falsity(NExprB) -> get_texpr_expr(NExprA,NExpr)
485		; NExpr = disjunct(NExprA,NExprB))
486		).
487		b_compile2(implication(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
488		FullyKnown=false, % predicates never automatically evaluated in b_compile1
489		b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
490		(is_falsity(NExprA) -> NExpr = truth
491		; is_truth(NExprA) -> b_compile1(B,Parameters,LS,S,NExprB,false,_,WF), get_texpr_expr(NExprB,NExpr)
492		; NExpr = implication(NExprA,NExprB),
493		b_compile1(B,Parameters,LS,S,NExprB,false,_,WF) % does not have to be executed in a succesful branch: set Eval to false to avoid computing expensive expressions which may not be needed
494		).
495		b_compile2(negation(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
496		FullyKnown=false, % predicates never automatically evaluated in b_compile1
497		b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
498		( get_negated_expr(NExprA,NegatedA) -> NExpr = NegatedA
499		; NExpr = negation(NExprA)
500		).
501
502		/* b_compile2(comprehension_set(CParas,Body),Parameters,LS,S,NExpr,_Eval,FullyKnown,WF) :-
503		sort(Parameters,SParas),
504		b_ast_cleanup:not_occurs_in_predicate(SParas,Body), %can only be applied if Body does not reference Parameters
505		!,
506		b_generate_inner_closure_if_necessary(Parameters,CParas,Body,LS,S,Result), % will itself call b_compile
507		NExpr = value(Result),
508		(ground(Result) -> FullyKnown=true ; FullyKnown=false). */
509		b_compile2(forall(ForallPara,A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
510		FullyKnown=false, % predicates never automatically evaluated in b_compile1
511		get_texpr_ids(ForallPara,AtomicIds),
512		append(Parameters,AtomicIds,NParameters),
513		b_compile1(A,NParameters,LS,S,NA,Eval,_FullyKnownA,WF),
514		(is_falsity(NA) -> NExpr = truth
515		; b_compile1(B,NParameters,LS,S,NB,Eval,_FullyKnownB,WF),
516		(is_truth(NB) -> NExpr = truth
517		; NExpr = forall(ForallPara,NA,NB)
518		% TO DO ??: if we have an equality -> replace Body by value and remove quantifier
519		%,print('COMPIlED: '),translate:print_bexpr(b(NExpr,pred,[])),nl
520		)
521		).
522		% some special cases to avoid calling syntaxtransformation
523		b_compile2(record_field(A,FieldName),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
524		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
525		% First: we can try compute even if value not fully known !, we just need record field list
526		(get_record_field(NExprA,FieldName,NExpr,FullyKnown) -> true
527		; NExpr = record_field(NExprA,FieldName), FullyKnown=FullyKnownA).
528		%((FullyKnown=false,NExprA=b(VV,_,_),nonvar(VV),VV=value(V)) , trace, known_value(V) ; true).
529		b_compile2(couple(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
530		%NExpr = couple(NExprA,NExprB),
531		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
532		combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown),
533		b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF),
534		(FullyKnown \== true, % evaluation will already combine the result
535		NExprA=b(value(VA),_,_),NExprB=b(value(VB),_,_)
536		-> NExpr = value((VA,VB))
537		; NExpr = couple(NExprA,NExprB)).
538		b_compile2(image(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
539		%NExpr = image(NExprA,NExprB),
540		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
541		combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown),
542		b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF),
543		(FullyKnown \= true, NExprA=b(value(VA),BT,BI),
544		NExprB=b(value(VB),_,_), nonvar(VB),
545		custom_explicit_sets:singleton_set(VB,VBX)
546		-> filter_cannot_match(VA,(VBX,_),NewVA,_Filtered), %nl,print(filtered_image(VBX,VA,NewVA)),nl,
547		NExpr = image(b(value(NewVA),BT,BI),NExprB)
548		% TO DO: add case where VB==[] or VA==[] are the empty set
549		; NExpr = image(NExprA,NExprB)
550		). %, print('compile image: '),translate:print_bexpr(NExpr),nl.
551		% TO DO: do something like can_apply_partially_specified_function; or filter_can_match
552		b_compile2(domain(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
553		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
554		(FullyKnown1=false,get_texpr_expr(NExprA,NA),evaluate_domain(NA,Domain) % try and compute domain even if not fully known
555		-> FullyKnown = true, NExpr = value(Domain)
556		; FullyKnown = FullyKnown1, NExpr = domain(NExprA)).
557		b_compile2(range(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
558		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
559		(FullyKnown1=false,evaluate_range(NExprA,Range) % try and compute range even if not fully known
560		-> FullyKnown = true, NExpr = value(Range)
561		; FullyKnown = FullyKnown1, NExpr = range(NExprA)).
562		b_compile2(assign(LHS_List,RHS_List),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
563		%print(compile_assign(LHS_List)),nl,
564		NExpr = assign(New_LHS_List,NewRHS_List), FullyKnown = false,
565		maplist(b_compile_lhs(Parameters,LS,S,Eval,WF),LHS_List,New_LHS_List),
566		b_compile_l(RHS_List,Parameters,LS,S,NewRHS_List,Eval,_FullyKnown2,WF).
567		b_compile2(assign_single_id(ID,B),Parameters,LS,S,assign_single_id(ID,NExprB),Eval,FullyKnown,WF) :- !,
568		FullyKnown = false,
569		b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF).
570		b_compile2(operation_call(Operation,OpCallResults,OpCallParas),Parameters,LS,S,InlinedOpCall,Eval,FullyKnown,WF) :-
571		%print(opcall(Operation,OpCallResults,OpCallParas)),nl,
572		% TO DO: evaluate if we should also use the let_expression_global approach used for operation_call_in_expr
573		!,
574		def_get_texpr_id(Operation,op(OperationName)),
575		FullyKnown = false,
576		b_compile_l(OpCallParas,Parameters,LS,S,OpCallParaValues,Eval,_,WF),
577		TopLevel=false,
578		b_get_machine_operation_for_animation(OperationName,OpResults,OpFormalParameters,Body,_OType,TopLevel),
579		bsyntaxtree:replace_ids_by_exprs(Body,OpResults,OpCallResults,Body2),
580		get_texpr_ids(OpFormalParameters,OpIds),
581		append(OpIds,Parameters,InnerParas),
582		b_compile1(Body2,InnerParas,[],S,NBody,Eval,FullyKnown,WF), % do not pass local state: this may override constants,... from the called machine
583		% Note: global state S should be valid for all machines in currently loaded specification
584		get_texpr_ids(OpCallResults,OpRIds),
585		append(OpRIds,Parameters,LocalKnownParas),
586		simplify_assignment(OpFormalParameters,OpCallParaValues,LHSFormalParas,RHSCallVals), %%
587		split_formal_parameters(LHSFormalParas,RHSCallVals,LocalKnownParas,
588		FreshOpParas,FreshCallVals,
589		ClashOpParas, ClashCallVals), % only set up VAR for fresh Paras
590		% print(split(LHSFormalParas,LocalKnownParas,fresh(FreshOpParas),clash(ClashOpParas))),nl,
591		(FreshOpParas=[] -> get_texpr_expr(NBody,Let1)
592		; create_equality_for_let(FreshOpParas,FreshCallVals,Equality1),
593		Let1 = let(FreshOpParas,Equality1,NBody)),
594		(ClashOpParas = []
595		-> InlinedOpCall = Let1
596		; %nl,print(clash(ClashOpParas)),nl,
597		maplist(create_fresh_id,ClashOpParas,FreshCopy),
598		create_equality_for_let(ClashOpParas,FreshCopy,Equality2), % copy Values from Fresh Ids
599		create_equality_for_let(FreshCopy,ClashCallVals,Equality3), % assign Parameter Vals to Fresh Ids
600		get_texpr_pos(Body,BodyPos), BodyPosInfo = [nodeid(BodyPos)],
601		Let2 = let(ClashOpParas,Equality2,b(Let1,subst,[BodyPosInfo])),
602		InlinedOpCall = let(FreshCopy,Equality3,b(Let2,subst,[BodyPosInfo]))
603		).
604		%, print('Compiled operation call: '), translate:print_subst(b(InlinedOpCall,subst,BodyPosInfo)),nl,nl.
605		% Maybe this version is faster when no OpCallResults:
606		%b_compile2(operation_call(Operation,OpCallResults,OpCallParas),Parameters,LS,S,InlinedOpCall,Eval,FullyKnown,WF) :-
607		% OpCallResults=[],
608		% !,
609		% def_get_texpr_id(Operation,op(OperationName)),
610		% FullyKnown = false,
611		%% b_compile_l(Results,Parameters,LS,S,NResults,Eval,_,WF),
612		% b_compile_l(OpCallParas,Parameters,LS,S,OpCallParaValues,Eval,_,WF),
613		% TopLevel=false,
614		% b_get_machine_operation_for_animation(OperationName,OpResults,OpParameters,Body,_OType,TopLevel),
615		% % Note: input parameters cannot be assigned to: so replace ids is ok
616		% % However, we cannot replace output parameters: these can be assigned to and we can have aliasing
617		% % Note: no aliasing is allowed in OpCallResults (cf Atelier-B handbook x,x <-- op not allowed)
618		% bsyntaxtree:replace_ids_by_exprs(Body,OpParameters,OpCallParaValues,Body2),
619		% get_texpr_ids(OpResults,OpIds),
620		% append(OpIds,Parameters,InnerParas),
621		% b_compile1(Body2,InnerParas,LS,S,NBody,Eval,FullyKnown,WF),
622		% FinalBody = NBody.
623		b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :-
624		functor(Expr,BOP,2),
625		binary_boolean_operator(BOP,_,_),!, % from kernel_mappings, slightly more efficient than syntaxtransformation
626		arg(1,Expr,A),
627		FullyKnown=false, % predicates never evaluated in b_compile1
628		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
629		arg(2,Expr,B),
630		b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
631		(eval_binary_bool(FullyKnownA,NExprA,FullyKnownB,NExprB,BOP,Result)
632		-> NExpr = Result
633		; functor(NExpr,BOP,2), arg(1,NExpr,NExprA), arg(2,NExpr,NExprB)
634		).
635		b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :-
636		functor(Expr,BOP,2),
637		kernel_mappings:binary_function(BOP,_,_),!, % slightly more efficient than syntaxtransformation
638		arg(1,Expr,A),
639		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
640		combine_fully_known(FullyKnownA,FullyKnownB,FullyKnown),
641		arg(2,Expr,B),
642		b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
643		functor(NExpr,BOP,2), arg(1,NExpr,NExprA), arg(2,NExpr,NExprB).
644		b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :-
645		functor(Expr,UOP,1),
646		kernel_mappings:unary_function(UOP,_,_),!, % slightly more efficient than syntaxtransformation
647		arg(1,Expr,A),
648		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown,WF),
649		functor(NExpr,UOP,1), arg(1,NExpr,NExprA).
650		b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- % GENERAL CASE
651		%hit_profiler:add_profile_hit(Expr),
652		syntaxtransformation(Expr,Subs,Names,NSubs,NExpr),
653		get_texpr_ids(Names,Ids), append(Parameters,Ids,NParameters),
654		b_compile_l(Subs,NParameters,LS,S,NSubs,Eval,FullyKnown,WF).
655
656		b_compile_l([],_,_,_,[],_Eval,true,_WF).
657		b_compile_l([Expr|ExprRest],P,LS,S,[NExpr|NExprRest],Eval,FullyKnown,WF) :-
658		b_compile1(Expr,P,LS,S,NExpr,Eval,FullyKnown1,WF),
659		combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown),
660		b_compile_l(ExprRest,P,LS,S,NExprRest,Eval,FullyKnown2,WF).
661
662		% detecth when a parameter clashes with existing known ids
663		id_clash(LocalKnownParas,TID) :- def_get_texpr_id(TID,ID), member(ID,LocalKnownParas).
664
665		/* comment in if we want to compile inner comprehension sets:
666		:- use_module(closures,[construct_closure_if_necessary/4]).
667		b_generate_inner_closure_if_necessary(OuterParameters,ClosureParas,Condition,LocalState,State,Result) :-
668		split_names_and_types(ClosureParas,Names,Types),
669		append(OuterParameters,Names,FullNames),
670		b_compile(Condition,FullNames,LocalState,State,ClosurePred),
671		print('INNER COMPILE: '), translate:print_bexpr(ClosurePred),nl,
672		construct_closure_if_necessary(Names,Types,ClosurePred,Result).
673		*/
674
675
676		% the LHS contains l-values which should not be looked up in the environment
677		% however, we need to deal with things like f(i) := RHS and compile i
678		b_compile_lhs(Parameters,LS,S,Eval,WF,TExpr,NewTExpr) :-
679		TExpr = b(Expr,Type,Info), NewTExpr = b(NewExpr,Type,Info),
680		b_compile_lhs_aux(Expr,Parameters,LS,S,NewExpr,Eval,WF).
681
682		b_compile_lhs_aux(function(A,B),Parameters,LS,S,function(NewA,NewB),Eval,WF) :- !,
683		b_compile_lhs(Parameters,LS,S,Eval,WF,A,NewA), % we can have nexted function calls f(e)(g) :=
684		b_compile1(B,Parameters,LS,S,NewB,Eval,_,WF).
685		b_compile_lhs_aux(E,_,_,_,E,_,_WF). % other LHS should be identifier -> just copy
686
687		get_record_field(b(value(Val),_,_),FieldName,value(Field),FullyKnown) :- !,
688		nonvar(Val), Val=rec(Fields),
689		safe_get_field(Fields,FieldName,Field),
690		known_value(Field,FullyKnown).
691		get_record_field(b(function(FUN,ARG),_Type,_Info),FieldName,function(ReducedFUN,ARG),false) :-
692		% {1|->rec(a:1,b:2),...}(x)'b --> {1|->2,...}(x)
693		%nl,print(get_field(FUN,ARG,FieldName)),nl,
694		% TO DO: also allow nested functions calls {1|->rec(a:1,b:2),...}(x)(y)'b or other reduction operators
695		get_field_in_range(FUN,FieldName,ReducedFUN).
696		safe_get_field(V,_,_) :- var(V),!,fail.
697		safe_get_field([field(N,V)|T],FieldName,Result) :- nonvar(N),
698		(N=FieldName -> Result=V ; safe_get_field(T,FieldName,Result)).
699
700		:- use_module(probsrc(custom_explicit_sets),[expand_custom_set_to_list/4, convert_to_avl/2]).
701		:- use_module(probsrc(avl_tools),[avl_height_less_than/2]).
702		get_field_in_range(b(value(OldVal),set(couple(Dom,OldRange)),Info),FieldName,
703		b(value(NewVal),set(couple(Dom,NewRange)),Info)) :-
704		nonvar(OldVal), OldVal=avl_set(AVL),
705		avl_height_less_than(AVL,10),
706		OldRange = record(Fields),
707		member(field(FieldName,NewRange),Fields),!,
708		expand_custom_set_to_list(avl_set(AVL),List,_,get_field_in_range),
709		maplist(safe_get_range_field(FieldName),List,NewList),
710		%print(reduced_get_field_in_range(NewList)),nl,
711		convert_to_avl(NewList,NewVal).
712
713		% compute the field access for the range elements:
714		safe_get_range_field(FieldName,(Dom,rec(Fields)),(Dom,Field)) :- safe_get_field(Fields,FieldName,Field).
715
716
717		eval_binary_bool(true,b(value(ValA),_,_),true,b(value(ValB),_,_),BOP,Result) :-
718		eval_binary_aux(BOP,ValA,ValB,Result).
719		%print(eval(BOP,ValA,ValB,Result)),nl,nl.
720		eval_binary_aux(less,int(A),int(B),Result) :-
721		(A < B -> Result = truth ; Result = falsity).
722		eval_binary_aux(greater,int(A),int(B),Result) :-
723		(A > B -> Result = truth ; Result = falsity).
724		eval_binary_aux(less_equal,int(A),int(B),Result) :-
725		(A =< B -> Result = truth ; Result = falsity).
726		eval_binary_aux(greater_equal,int(A),int(B),Result) :-
727		(A >= B -> Result = truth ; Result = falsity).
728		% TO DO: other operators are subset, strict_subset, ...
729
730		get_negated_expr(b(E,pred,_),Res) :- negate_expr_aux(E,Res).
731		negate_expr_aux(falsity,truth).
732		negate_expr_aux(truth,falsity).
733		negate_expr_aux(member(X,S),not_member(X,S)).
734		negate_expr_aux(not_member(X,S),member(X,S)).
735		negate_expr_aux(subset(X,S),not_subset(X,S)).
736		negate_expr_aux(not_subset(X,S),subset(X,S)).
737		negate_expr_aux(subset_strict(X,S),not_subset_strict(X,S)).
738		negate_expr_aux(not_subset_strict(X,S),subset_strict(X,S)).
739		negate_expr_aux(equal(X,S),not_equal(X,S)).
740		negate_expr_aux(not_equal(X,S),equal(X,S)).
741		negate_expr_aux(less(X,S),greater_equal(X,S)).
742		negate_expr_aux(greater_equal(X,S),less(X,S)).
743		negate_expr_aux(less_equal(X,S),greater(X,S)).
744		negate_expr_aux(greater(X,S),less_equal(X,S)).
745
746		:- use_module(store,[lookup_value_for_existing_id/4]).
747		compute_lazy_lookup(Id,Expr,LS,S,NExpr,FullyKnown) :-
748		lookup_value_for_existing_id(Id,LS,S,(Evaluated,Value)),
749		!,
750		known_value(Value,FullyKnown),
751		(Evaluated==pred_true -> NExpr = value(Value)
752		; FullyKnown==true -> NExpr = value(Value)
753		; memberchk('$do_not_force_lazy_lookups',LS) -> NExpr = Expr % we do not force lookup: there could be WD issues ! TO DO: examine Infos for wd_condition
754		%, print(not_forcing(Id,Value)),nl
755		; if(Evaluated = pred_true, % will force evaluation ! Note: this means shared expression inside a compiled expression must be well-defined
756		NExpr = value(Value),
757		(add_internal_error('Compilation failed: ',compute_lazy_lookup(Id,Expr,LS,S,NExpr,FullyKnown) ),
758		fail))
759		).
760		compute_lazy_lookup(Id,E,LS,S,LazyValue,_) :-
761		add_internal_error('Compilation failed, illegal lazy_lookup_value: ',compute_lazy_lookup(Id,E,LS,S,LazyValue,_)),
762		fail.
763
764		combine_fully_known(true,A,A).
765		combine_fully_known(false,_,false).
766
767		% is an extension function with at least two elements
768		is_extension_function_gt1(b(A,_,_Info)) :- is_extension_function_aux(A).
769		is_extension_function_aux(set_extension([_,_|_])).
770		is_extension_function_aux(sequence_extension([_,_|_])).
771
772		:- use_module(bsyntaxtree,[is_set_type/2]).
773		% check if we can apply an argument to a partially specified function (as a list)
774		%can_apply_partially_specified_function(Fun,X,_) :- print(fun(Fun)),nl,print(val(X)),nl,fail.
775		can_apply_partially_specified_function(b(Expr,TYPE,_), b(value(X),TA,_),ResultExpr,WF) :-
776		can_apply_aux(Expr,TYPE,X,TA,ResultExpr,WF).
777
778		can_apply_aux(value(VAL),TYPE,X,TA,value(ResultValue),WF) :-
779		is_set_type(TYPE,couple(TA,_TB)),
780		lookup_result(VAL,X,ResultValue,WF).
781		can_apply_aux(sequence_extension(List),_,X,integer,ResultExpr,_WF) :- % important, e.g., for solving test 1551: {b|[a,b,c](2)=333} =res & a : res & b:res
782		nonvar(X), X=int(Index), number(Index),
783		% this will prevent computing rest of sequence extension: can hide WD issues !
784		% print(apply_seq_extension(Index,List)),nl,
785		nth1(Index,List,b(ResultExpr,_,_)).
786
787		:- use_module(kernel_equality,[equality_objects_wf/4]).
788		%lookup_result(VAR,ArgValue,Result,WF) :- var(VAR),!,kernel_mappings:kernel_call_apply_to(VAR,ArgValue,Result,unknown,unknown,WF).
789		% the clause above is unsound; as apply_to CAN RAISE WD ERRORS !! what if we have IF 1:dom(f) THEN f(1) ELSE f(0) END; we do not want to compute f(1) ! it can also instantiate unbound variables !
790		% the idea was to avoid that we wait on the full function, before compiled closure can be evaluated; test 1552
791		% important for e.g. a = {(1, {([]|->2)} ), (2, const(1, [a(1)]))}
792		% or: a = {1 |-> {[] |-> 2}, 2 |-> (dom({pi,ff,p|((pi : seq(INTEGER) & ff : INTEGER) & p : seq(INTEGER)) & (p |-> ff : [a(1)](1) & pi = 1 -> p)}) \/ {[] |-> 1})}
793		% test 1552 is currently skipped
794		% TO DO: think whether there are other deterministic computations that can be done in b_compile: prj1,prj2, record-field access ? this would ensure that closures,... can be computed earlier
795		lookup_result(VAR,_,_,_WF) :- var(VAR),!,fail.
796		lookup_result([(HFrom,HTo)|T],X,Result,WF) :-
797		equality_objects_wf(HFrom,X,PredRes,WF), %print(compare(PredRes,HFrom,X)),nl,
798		nonvar(PredRes), % only proceed if we have enough information to determine the result of the comparison
799		(PredRes = pred_true -> Result = HTo % we have found the value; we assume there is no other value later
800		% TO DO: if find_abort_values=true: look later in the list if for all other HFrom PredRes=pred_false
801		; lookup_result(T,X,Result,WF)).
802
803		% get_comprehension_set(b(SET,_,_),ID,PRED) :- get_comprehension_set_aux(SET,ID,PRED).
804		% get_comprehension_set_aux(comprehension_set([TID],PRED),ID,PRED) :-
805		% get_texpr_id(TID,ID).
806		% get_comprehension_set_aux(value(V),ID,PRED) :- nonvar(V), V = closure([ID],_,PRED).
807
808
809
810
811		quick_test_membership1(b(value(VA),_,_),VB,Result) :-
812	?	quick_test_membership_aux(VB,VA,Result).
813		quick_test_membership_aux(VAR,_,_) :- var(VAR),!,fail.
814		quick_test_membership_aux([],_,pred_false).
815		quick_test_membership_aux(avl_set(AVL),X,Result) :-
816		custom_explicit_sets:quick_test_avl_membership(AVL,X,Result). % we could also check that in case X is not ground but partially instantiated, whether there is a possible match in AVL (if not Result = pred_false)
817		quick_test_membership_aux(global_set(GS),X,Result) :- nonvar(X), X=int(IX), nonvar(IX),
818		custom_explicit_sets:membership_global_set(GS,X,R,_WF),
819		nonvar(R), Result=R.
820		quick_test_membership_aux(closure(P,T,B),X,Result) :- nonvar(X), X=int(IX), nonvar(IX),
821		custom_explicit_sets:is_interval_closure(P,T,B,LOW,UP), number(LOW),number(UP),
822		kernel_equality:in_nat_range_test(X,int(LOW),int(UP),R),
823		nonvar(R), Result=R.
824		quick_test_membership_aux(closure(P,T,B),X,Result) :- X==[], % check {} : POW(_) / FIN(_) and {} : POW1(_) / FIN1(_)
825		custom_explicit_sets:is_powerset_closure(closure(P,T,B),Kind,_),
826		(contains_empty_set(Kind) -> Result = pred_true ; Result=pred_false).
827
828		contains_empty_set(pow).
829		contains_empty_set(fin).
830
831		convert_pred_res(pred_false,falsity).
832		convert_pred_res(pred_true,truth).
833		convert_neg_pred_res(pred_true,falsity).
834		convert_neg_pred_res(pred_false,truth).
835
836		generate_equality(b(A,_,_),b(B,_,_),Res) :-
837		( generate_equality_aux(A,B,Res) ;
838		generate_equality_aux(B,A,Res) ),
839		!.
840		generate_equality(A,B,equal(A,B)).
841
842		generate_equality_aux(convert_bool(AA),value(PT),Res) :-
843		PT==pred_true,
844		get_texpr_expr(AA,TA),
845		!,
846		%print(simplify_bool(AA,PT)),nl,
847		Res = TA.
848		generate_equality_aux(convert_bool(AA),value(PF),Res) :-
849		PF==pred_false,!,
850		%print(simplify_bool(AA,PF)),nl,
851		Res = negation(AA).
852
853		known_value(X,FullyKnown) :- (known_value(X) -> FullyKnown=true ; FullyKnown=false).
854		known_value(X) :- nonvar(X), known_value2(X).
855		known_value2(global_set(GS)) :- nonvar(GS).
856		known_value2(freetype(GS)) :- nonvar(GS).
857		known_value2(closure(P,T,B)) :- known_closure(P,T,B).
858		%Note: for other closures: they still may have to be computed; some of the computations in wd_and_efficient could be expensive for closures
859		known_value2(avl_set(_)). % already fully normalised
860		known_value2((X,Y)) :- known_value(X),known_value(Y).
861		known_value2(fd(A,B)) :- number(A),atomic(B).
862		known_value2(int(N)) :- number(N).
863		known_value2([]).
864		known_value2(pred_true).
865		known_value2(pred_false).
866		known_value2(string(S)) :- atomic(S).
867		known_value2([H|T]) :- known_value(H), known_value(T).
868		%known_value2(record(Fields)) :- known_fields(Fields).
869		known_value2(rec(Fields)) :- known_fields(Fields).
870
871
872		known_closure(P,T,B) :- custom_explicit_sets:is_interval_closure(P,T,B,Low,Up), !,
873		number(Low), number(Up),
874		Up < Low+1000.
875		known_closure(P,T,B) :-
876		is_cartesian_product_closure(closure(P,T,B),A1,A2),
877		!,% we could call is_cartesian_product_closure_aux(P,T,B,A1,A2)
878		known_value(A1), known_value(A2).
879
880		known_fields(X) :- var(X),!,fail.
881		known_fields([]).
882		known_fields([field(N,V)|T]) :- ground(N),known_value(V),known_fields(T).
883
884		%b_evaluate1(TExpr,Parameters,LS,S,ResultTExpr,FullyKnown) :-
885
886		check_is_id_list([],[]).
887		check_is_id_list([H|T],Res) :-
888		(H=b(identifier(_),_,_)
889		-> add_internal_error('Typed id list as argument: ',check_is_id_list([H|T],Res)), % use get_texpr_ids or maplist(def_get_texpr_id,P,PIDs)
890		maplist(def_get_texpr_id,[H|T],Res)
891		; Res=[H|T]).
892
893		:- use_module(kernel_frozen_info,[kfi_domain/2]).
894
895		:- use_module(custom_explicit_sets,[construct_interval_closure/3]).
896		% try and evaluate domain of a list (avl_set already dealt with separately)
897		%evaluate_domain(X,_) :- print(dom(X)),nl,fail.
898		evaluate_domain(sequence_extension(L),Domain) :- length(L,Len),
899		% this will prevent computing range of sequence extension: can hide WD issues ! TO DO: check wd info and/or preference
900		construct_interval_closure(1,Len,Domain).
901		% TO DO: set_extension when possible ?
902		evaluate_domain(value(L),Domain) :-
903		get_domain(L,Domain).
904
905		get_domain(V,Dom) :- var(V),!,kfi_domain(V,Dom). % try infer domain from attached co-routines
906		get_domain([],[]).
907		get_domain([V|VT],Result) :- nonvar(V), V=(D,_),
908		known_value(D),get_list_domain(VT,DT),
909		sort([D|DT],Result).
910		% we could also do this:
911		%get_domain(closure(Par,Typ,Body),Result) :-
912		% is_lambda_value_domain_closure(Par,Typ,Body, DomainValue,Expr), check_wd(Expr),
913		% Result=DomainValue.
914		get_list_domain(V,_) :- var(V),!,fail.
915		get_list_domain([],[]).
916		get_list_domain([V|VT],[D|DT]) :- nonvar(V), V=(D,_),
917		known_value(D),get_list_domain(VT,DT).
918
919
920		:- use_module(kernel_frozen_info,[kfi_range/2]).
921
922		% try and evaluate range of a list (avl_set already dealt with separately)
923		evaluate_range(b(value(L),_T,_),Range) :-
924		get_range(L,Range).
925		get_range(V,Dom) :- var(V),!,kfi_range(V,Dom). % try infer range from attached co-routines
926		get_range([],[]).
927		get_range([V|VT],Result) :- nonvar(V), V=(_,D),
928		known_value(D),
929		get_list_range(VT,DT),
930		sort([D|DT],Result).
931
932		get_list_range(V,_) :- var(V),!,fail.
933		get_list_range([],[]).
934		get_list_range([V|VT],[D|DT]) :-
935		nonvar(V), V=(_,D),
936		known_value(D),
937		get_list_range(VT,DT).
938
939		create_equality_for_let(LHS,RHS,Conj) :-
940		maplist(create_eq,LHS,RHS,CL),
941		conjunct_predicates(CL,Conj).
942		create_eq(Id,Expr,TPred) :- safe_create_texpr(equal(Id,Expr),pred,TPred).
943
944		% split formal operation call parameters into those which clash and those that do not:
945		split_formal_parameters([],[],_,[],[],[],[]).
946		split_formal_parameters([Formal1|FormalT],[Val1|VT],LocalKnownParas,Fresh,FV,Clash,CV) :-
947		(id_clash(LocalKnownParas,Formal1)
948		-> Fresh = FreshT, FV=FVT, Clash = [Formal1|ClashT], CV = [Val1|CVT]
949		; Fresh = [Formal1|FreshT], FV = [Val1|FVT], Clash = ClashT, CV = CVT
950		), split_formal_parameters(FormalT,VT,LocalKnownParas,FreshT,FVT,ClashT,CVT).
951
952		:- use_module(gensym,[gensym/2]).
953		create_fresh_id(b(identifier(_),T,I),b(identifier(FRESHID),T,I)) :-
954		gensym('__COMPILED_ID__',FRESHID).
955
956		:- use_module(bsyntaxtree, [get_texpr_pos/2,same_id/3]).
957		% compute which assignments are really necessary, remove skip assignments x := x
958		simplify_assignment([],[],[],[]).
959		simplify_assignment([ID1|T1],[ID2|T2],Res1,Res2) :-
960		(same_id(ID1,ID2,_) -> Res1=TR1, Res2=TR2 ; Res1=[ID1|TR1], Res2=[ID2|TR2]),
961		simplify_assignment(T1,T2,TR1,TR2).