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(closures,[construct_closure/4, is_closure/4, %is_closure_x/5,
6		construct_closure_if_necessary/4,
7		get_domain_range_for_closure_types/3,
8		construct_member_closure/5,
9		%construct_not_member_closure/4,
10		construct_complement_closure/3,
11		is_member_closure/5, is_member_closure_with_info/6,
12		is_not_member_closure/5,
13		is_not_member_value_closure/3,
14		is_not_member_value_closure_or_integerset/3,
15		construct_less_equal_closure/2, construct_greater_equal_closure/2,
16		is_lambda_value_domain_closure/5, % checks for special memoization closure
17		is_lambda_value_domain_normal_closure/5, % performs no check for memoization closures
18		is_lambda_closure/7,
19		is_lambda_comprehension_set/4,
20		select_equality/6,
21		is_special_infinite_closure/3,
22		is_id_closure_over/5,
23		is_full_id_closure/3,
24		is_closure_or_integer_set/4,
25		is_infinite_non_injective_closure/1,
26		is_symbolic_closure/1, is_symbolic_closure/3,
27		is_recursive_closure/1, is_recursive_closure/3,
28		get_recursive_identifier_of_closure/2, get_recursive_identifier_of_closure_body/2,
29		mark_closure_as_symbolic/2, mark_closure_as_recursive/2,
30		mark_closure_as_force/2, mark_closure/3
31		]).
32
33		:- use_module(module_information,[module_info/2]).
34		:- module_info(group,kernel).
35		:- module_info(description,'This module provides various utility functions to analyse ProB closures.').
36
37		construct_closure(Parameters, ParameterTypes, Body, Res) :-
38		Res = closure(Parameters, ParameterTypes, Body).
39		% Res = closure_x(Parameters, ParameterTypes, Body,_). %% STILL HAS PROBLEMS with delay, e.g. inside b_test_exists !!
40
41
42		% an optimized version of construct_closure, which will try to produce explicit values if possible
43		construct_closure_if_necessary(_,_,b(falsity,pred,_),Res) :- !, Res=[].
44		construct_closure_if_necessary([ID], [T1], b(Pred,pred,_), Res) :-
45		construct_unary_closure(Pred,ID,T1,SET),!,
46		Res = SET.
47		construct_closure_if_necessary(Parameters, ParameterTypes, Body, Res) :-
48		Res = closure(Parameters, ParameterTypes, Body).
49
50		:- use_module(b_global_sets,[try_b_type2global_set/2]).
51		:- use_module(custom_explicit_sets,[try_expand_and_convert_to_avl/2]).
52		construct_unary_closure(member(b(identifier(ID),T1,_),b(value(SET),set(T1),_)),ID,T1,Res) :- Res=SET.
53		construct_unary_closure(truth,_,T1,Res) :- try_b_type2global_set(T1,Res).
54		construct_unary_closure(equal(b(identifier(ID),T1,_),b(value(SET),T1,_)),ID,T1,Res) :-
55		try_expand_and_convert_to_avl([SET],Res).
56
57
58		:- use_module(self_check).
59		:- assert_must_succeed( closures:is_closure(closure([x],[integer],body),[x],[integer],body)).
60		%is_closure(closure_x(Parameters, ParameterTypes, Body, _Exp), Parameters, ParameterTypes, Body).
61		is_closure(closure(Parameters, ParameterTypes, Body), Parameters, ParameterTypes, Body).
62
63
64		:- use_module(btypechecker,[couplise_list/2]).
65		get_domain_range_for_closure_types(Types,Domain,Range) :-
66		couplise_list(Types,couple(Domain,Range)).
67
68
69		:- use_module(bsyntaxtree,[create_texpr/4, safe_create_texpr/4, extract_pos_infos/2]).
70		% following not useful: construct_member_closure currently always called where the construction is needed
71		%construct_member_closure(ID,_Type,ClosureSetExpression,Result) :-
72		% nonvar(ClosureSetExpression),ClosureSetExpression = value(S),!,
73		% print(construct_member_closure_value(ID,S)),nl, %%
74		% Result=S.
75		construct_member_closure(ID,Type,Info,ClosureSetExpression,Result) :-
76		check_result_instantiation(Result,construct_member_closure(ID)),
77		create_texpr(identifier(ID),Type,[],TIdentifier), % used to be [generated]
78		extract_pos_infos(Info,PosInfo), % Note: safe_create_texpr will copy WD info
79		safe_create_texpr(ClosureSetExpression,set(Type),PosInfo,TClosureSet), % TODO: we could store whether sub_expression_contains_wd_condition for next call
80		safe_create_texpr(member(TIdentifier,TClosureSet),pred,PosInfo,TPred),
81		construct_closure([ID],[Type],TPred,Result).
82
83		construct_not_member_closure(ID,Type,Info,ClosureSetExpression,Result) :-
84		check_result_instantiation(Result,construct_not_member_closure(ID)),
85		Type==integer,
86	?	interval_up_to_inf(ClosureSetExpression,Limit),
87		!,
88		construct_less_equal_closure(ID,Limit,Info,Result). % construct an interval closure; better support in kernel for it
89		construct_not_member_closure(ID,Type,Info,ClosureSetExpression,Result) :-
90		create_texpr(identifier(ID),Type,[],TIdentifier), % used to be [generated]
91		safe_create_texpr(ClosureSetExpression,set(Type),Info,TClosureSet),
92		safe_create_texpr(not_member(TIdentifier,TClosureSet),pred,Info,TPred),
93		construct_closure([ID],[Type],TPred,Result).
94
95		interval_up_to_inf(global_set('NATURAL'),-1).
96		interval_up_to_inf(global_set('NATURAL1'),0).
97		interval_up_to_inf(value(global_set('NATURAL')),-1).
98		interval_up_to_inf(value(global_set('NATURAL1')),0).
99
100
101		construct_less_equal_closure(X,Res) :-
102		construct_less_equal_closure('_zzzz_unary',X,[],Res).
103		construct_less_equal_closure(ID,X,Info,Res) :-
104		construct_closure([ID],[integer],
105		b(less_equal(b(identifier(ID),integer,[]),
106		b(value(int(X)),integer,[])), pred,Info),Res).
107
108		construct_greater_equal_closure(X,Res) :-
109		construct_closure(['_zzzz_unary'],[integer],
110		b(greater_equal(b(identifier('_zzzz_unary'),integer,[]),
111		b(value(int(X)),integer,[])), pred,[]),Res).
112
113		:- use_module(error_manager,[add_internal_error/2]).
114		% check that we do not instantiate result too early (rather than using equal_object)
115		check_result_instantiation(X,_) :- var(X),!.
116		check_result_instantiation(closure(_,_,_),_PP) :- !.
117		check_result_instantiation(X,PP) :-
118		add_internal_error('Result already instantiated in incompatible way: ',check_result_instantiation(X,PP)).
119
120		is_member_closure_with_info([ID],[TYPE],b(PRED,_Pred,Info), TYPE,Info,SET) :-
121		is_member_closure_aux(PRED, ID,TYPE,SET).
122		is_member_closure([ID],[TYPE],b(PRED,_Pred,_), TYPE,SET) :-
123		is_member_closure_aux(PRED, ID,TYPE,SET).
124
125		:- use_module(bsyntaxtree,[is_set_type/2]).
126		is_member_closure_aux(member(TID,TSET), ID,TYPE,SET) :-
127		TID = b(identifier(ID),TYPE,_),
128		TSET = b(SET,SETTYPE,_),
129		is_set_type(SETTYPE,TYPE).
130		is_member_closure_aux(subset(TID,BSET), ID,TYPE,SET) :-
131		TID = b(identifier(ID),TYPE,_),
132		SET = pow_subset(BSET).
133		% can we also detect pow1_subset ? {x| x/= {} & x<: BSET}
134
135
136		% detect not_member closures + integerset as special not_member_closures
137		is_not_member_value_closure_or_integerset(global_set(X),TYPE,SET) :- !,
138		is_not_member_global_set(X,TYPE,SET).
139		is_not_member_value_closure_or_integerset(C,TYPE,SET) :- is_not_member_value_closure(C,TYPE,SET).
140
141		is_not_member_global_set('INTEGER',integer,[]).
142		is_not_member_global_set('NATURAL',integer,X) :-
143		construct_less_equal_closure(-1,X). % {x|x<0}.
144		is_not_member_global_set('NATURAL1',integer,X) :-
145		construct_less_equal_closure(0,X). %X = {x|x<1}.
146
147		is_not_member_value_closure(closure(Par,T,B),TYPE,SET) :-
148		is_not_member_closure(Par,T,B,TYPE,value(SET)).
149		is_not_member_closure([ID],[TYPE],b(PRED,_Pred,_),TYPE,SET) :-
150		is_not_member_closure_aux(PRED,ID,TYPE,SET).
151
152		:- use_module(kernel_tools,[ground_value/1]).
153		is_not_member_closure_aux(not_member(b(identifier(ID),TYPE,_),b(SET,set(TYPE),_)),ID,TYPE,SET).
154		is_not_member_closure_aux(not_equal(b(identifier(ID),TYPE,_),ONE),ID,TYPE,SET) :-
155		(ONE = b(value(Val),_,_),
156		ground_value(Val)
157		-> custom_explicit_sets:construct_one_element_custom_set(Val,SetVal), SET = value(SetVal)
158		; SET = set_extension([ONE])).
159		%is_not_member_closure_aux(PRED,ID,TYPE,SET) :- print(check_not_mem(PRED,ID,TYPE,SET)),nl,fail.
160
161		construct_complement_closure(Delta,Type,Closure) :-
162		% print(generating_complement_closure(GlobalSet,Delta,Type)),nl,
163		construct_not_member_closure('_zzzz_unary',Type,[],value(Delta),Closure).
164
165
166
167		/* lambda abstractions */
168		:- assert_must_succeed((closures:is_lambda_closure([x,y],[integer,integer],b(conjunct(b(member(b(identifier(x),integer,[nodeid(pos(0,0,0,0,0,0))]),b(value(global_set('NATURAL')),set(integer),[])),pred,[]),b(equal(b(identifier(y),integer,[]),b(multiplication(b(identifier(x),integer,[]),b(identifier(x),integer,[])),integer,[])),pred,[])),pred,[]),OtherIDs,OtherTypes,_DOMAINPRED,_Res), OtherIDs=[x], OtherTypes=[integer])).
169		:- assert_must_fail((closures:is_lambda_closure([x,y],[integer,integer],b(conjunct(b(conjunct(b(member(b(identifier(x),integer,[]),b(value(global_set('NATURAL')),set(integer),[])),pred,[]),b(equal(b(identifier(y),integer,[]),b(multiplication(b(identifier(x),integer,[]),b(identifier(x),integer,[])),integer,[])),pred,[])),pred,[]),b(less(b(identifier(y),integer,[]),b(value(int(10)),integer,[])),pred,[])),pred,[]),_,_,_D,_Res)
170		)).
171
172		:- use_module(bsyntaxtree,[conjunction_to_list/2,conjunct_predicates/2]).
173		is_lambda_closure(Args,Types,ClosurePred, OtherIDs, OtherTypes, DOMAINPRED,Res) :-
174		% TO DO: do this more efficiently: if LambdaID occurs in any non-equal predicate : stop searching
175		% TO DO: check if is_infinite_equality_closure is not a special case of lambda closure ?
176		append(OtherTypes,[LambdaType],Types), OtherTypes \= [],
177		append(OtherIDs,[LambdaID],Args),
178		Res=b(EXPR,LambdaType,EXPRINFO),
179		%used to call: b_interpreter:member_conjunct(EQ,ClosurePred,DOMAINPRED), ; but inlined below for efficiency
180		select_equality(ClosurePred,LambdaID,EXPR,LambdaType,EXPRINFO,DOMAINPRED),
181		!. % avoid backtracking member_conjunct
182		% tools:print_bt_message(is_lambda_closure(LambdaID)).
183		% Note: LAMBDA is usually '_lambda_result_'
184
185		identifier_equality(b(equal(b(LHS,Type,LHSInfo),b(RHS,_TypeRHS,RHSInfo)),pred,_),ID,Type,EXPR,EXPRINFO) :-
186		% no need to unify with TypeRHS; actually Prolog unification could fail due to seq types ?
187		identifier_equality_aux(LHS,LHSInfo,RHS,RHSInfo,ID,EXPR,EXPRINFO).
188		identifier_equality_aux(identifier(ID),_,EXPR,EXPRINFO,ID,EXPR,EXPRINFO) :- !.
189		identifier_equality_aux(EXPR,EXPRINFO,identifier(ID),_,ID,EXPR,EXPRINFO).
190
191		% find an equality ID = RHSExpr so that ID does not occur in RHSExpr nor in RestPred
192		% the identifier should be provided as input (for the cut below)
193		select_equality(ClosurePred,ID,RHSExpr,Type,Info,RestPred) :-
194		conjunction_to_list(ClosurePred,List),
195	?	select(EQ,List,RestList),
196		identifier_equality(EQ,ID,Type,RHSExpr,Info),
197		!, % once we find a first equality : no need to look for a second one as then does_not_occur in RestPred will always fail !
198		(ID='_lambda_result_',EQ=b(_,_,I),
199	?	member(prob_annotation('LAMBDA-EQUALITY'),I)
200		-> true % no need to perform occurs check in RHS, but in RestPred, cf test 1874
201		; %format('Check occurs ~w : ',[ID]), translate:print_bexpr(b(RHSExpr,Type,Info)),nl,
202		does_not_occur_in(ID,b(RHSExpr,Type,Info))
203		),
204		conjunct_predicates(RestList,RestPred),
205		does_not_occur_in(ID,RestPred).
206
207
208		:- use_module(memoization,[is_lambda_value_domain_memoization_closure/5]).
209
210		% check whether we have a lambda closure and whether we can compute its domain
211		is_lambda_value_domain_closure(P,T,Pred, DomainValue,Expr) :-
212	?	is_lambda_value_domain_memoization_closure(P,T,Pred, DV,E),!,
213		DV \= fail, E\= fail,
214		DomainValue=DV, Expr=E.
215		is_lambda_value_domain_closure(Args,Types,B, DomainValue, EXPR) :-
216		is_lambda_value_domain_normal_closure(Args,Types,B, DomainValue, EXPR).
217
218		is_lambda_value_domain_normal_closure(Args,Types,B, DomainValue, EXPR) :-
219		% tools_printing:print_term_summary(try_is_lambda_domain(Args,Types,B)), %
220		is_lambda_closure(Args,Types,B, OtherIDs,OtherTypes, DomainPred, EXPR),!,
221		%print(lambda_closure(OtherIDs)), translate:print_bexpr(EXPR),nl,
222		construct_closure_if_necessary(OtherIDs,OtherTypes,DomainPred,DomClosure),
223	?	(is_symbolic_closure(Args,Types,B)
224		-> mark_closure_as_symbolic(DomClosure,DomainValue)
225		; DomainValue = DomClosure).
226		%print(lambda_domain(Args)),nl, (IDs=[_,_|_] -> trace ; true),
227		%translate:print_bvalue(DomainValue),nl.
228
229		% LAMBDARES is usually _lambda_result_, LAMBDARES cannot occur in DOMAIN (is value)
230
231		:- use_module(library(lists),[maplist/4]).
232		is_lambda_comprehension_set(b(comprehension_set(Parameters,Body),_,_),LambdaParas,DomainPred,EXPR) :-
233		maplist(get_names_and_types,Parameters,Args,Types),
234		is_lambda_closure(Args,Types,Body, OtherIDs,OtherTypes, DomainPred, EXPR),
235		maplist(combine_names_and_types,OtherIDs,OtherTypes,LambdaParas).
236
237		get_names_and_types(b(identifier(ID),Type,_),ID,Type).
238		combine_names_and_types(ID,Type,b(identifier(ID),Type,[])).
239
240		:- assert_must_succeed(closures:is_special_infinite_closure([x],[integer],b(truth,pred,[]))).
241		:- assert_must_succeed((X=b(identifier(x),integer,[]),N=b(integer(3),integer,[]),
242		closures:is_special_infinite_closure([x],[integer],b(greater(X,N),pred,[])))).
243		:- assert_must_succeed((X=b(identifier(x),integer,[]),N=b(integer(3),integer,[]),
244		closures:is_special_infinite_closure([x],[integer],b(greater(X,N),pred,[])))).
245		:- assert_must_succeed((X=b(identifier(x),integer,[]),N=b(integer(3),integer,[]),
246		closures:is_special_infinite_closure([x],[integer],b(less(X,N),pred,[])))).
247		:- assert_must_succeed((X=b(identifier(x),integer,[]),N=b(integer(3),integer,[]),
248		closures:is_special_infinite_closure([x],[integer],b(not_equal(X,N),pred,[])))).
249		:- assert_must_fail((X=b(identifier(x),integer,[]),N=b(integer(3),integer,[]),
250		closures:is_special_infinite_closure([x],[integer],b(equal(X,N),pred,[])))).
251		:- assert_must_succeed((X=b(identifier(x),integer,[]),N=b(integer(3),integer,[]),
252		closures:is_special_infinite_closure([x,y],[integer,integer],b(equal(X,N),pred,[])))).
253		:- assert_must_succeed((Y=b(identifier(y),integer,[]),N=b(integer(3),integer,[]),
254		closures:is_special_infinite_closure([x,y],[integer,integer],b(equal(Y,N),pred,[])))).
255
256		:- use_module(typing_tools,[is_infinite_type/1]).
257		/* checking for infinite closures */
258		%is_special_infinite_closure(_Par,T,b(truth,_Pred,_)) :- !, % now dealt with below
259		% member(Type,T), is_infinite_type(Type),!.
260		is_special_infinite_closure(Par,T,Body) :-
261	?	is_infinite_equality_closure(Par,T,Body),!.
262		%is_special_infinite_closure(Par,T,Body) :- is_full_id_closure(Par,T,Body,TYPE), is_infinite_type(TYPE).
263		%is_special_infinite_closure(Par,T,Body) :- is_prj1_closure(Par,T,Body,T1,_T2), is_infinite_type(T1).
264		%is_special_infinite_closure(Par,T,Body) :- is_prj2_closure(Par,T,Body,_T1,T2), is_infinite_type(T2).
265		is_special_infinite_closure(Par,T,Body) :-
266		is_not_member_closure(Par,T,Body,Type,value(_)), is_infinite_type(Type).
267
268		:- use_module(library(lists)).
269
270		greater_typing(greater(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP).
271		greater_typing(greater_equal(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP).
272		greater_typing(less(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP).
273		greater_typing(less_equal(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP).
274
275		less_typing(less(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP).
276		less_typing(less_equal(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP).
277		less_typing(greater(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP).
278		less_typing(greater_equal(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP).
279
280		is_integer_val(integer(UP),UP).
281		is_integer_val(value(V),UP) :- nonvar(V),V=int(UP).
282
283		is_static_expr_of_infinite_type(b(E,Type,_)) :- is_static_expr_of_infinite_type2(E,Type).
284		is_static_expr_of_infinite_type2(integer(_),_).
285		is_static_expr_of_infinite_type2(string(_),_).
286		is_static_expr_of_infinite_type2(real(_),_).
287		is_static_expr_of_infinite_type2(value(V),Type) :- is_val_of_infinite_type(V,Type).
288		is_static_expr_of_infinite_type2(empty_set,Type) :- is_infinite_type(Type).
289		is_static_expr_of_infinite_type2(empty_sequence,Type) :- is_infinite_type(Type).
290		% TODO: more typical expressions, set/sequence extension pairs
291
292		is_val_of_infinite_type(V,_) :- var(V),!,fail.
293		is_val_of_infinite_type(int(_),_).
294		is_val_of_infinite_type(string(_),_).
295		is_val_of_infinite_type(term(floating(_)),_).
296		is_val_of_infinite_type((A,B),couple(TA,TB)) :- (is_val_of_infinite_type(A,TA) -> true ; is_val_of_infinite_type(B,TB)).
297		is_val_of_infinite_type([],Type) :- is_infinite_type(Type).
298		is_val_of_infinite_type(avl_set(_),Type) :- is_infinite_type(Type).
299
300
301
302
303		% the following also translates global_set(NATURAL(1)) into closures
304		% TO DO: probably better to remove global_set(INTSET) all together and rewrite in ast_cleanup to closure
305		is_closure_or_integer_set(closure(P,T,B),P,T,B).
306		is_closure_or_integer_set(global_set(INTSET),
307		['_zzzz_unary'],[integer],
308		b(greater_equal(
309		b(identifier('_zzzz_unary'),integer,[]),
310		b(integer(BOUND),integer,[])
311		),
312		pred,
313		[prob_annotation('SYMBOLIC')])
314		) :-
315		get_bound(INTSET,BOUND).
316		get_bound('NATURAL',0).
317		get_bound('NATURAL1',1).
318		% TO DO: allow INTEGER / maximal sets ? -> truth; could get rid of complement sets?
319
320		% to do: extend; could be value(infinite_closure)...
321
322
323
324		/* Equality closures {x1,x2,...|id=E2}, where id does not occur in E2 and id =xi */
325		% should cover id, prj1, prj2
326		% {x,y|y:BOOL & x=f(y) } or %x.(x:NATURAL|Expr(x))
327		% would not be infinite {x,y|x:BOOL & x=f(g(x)*y)} , g={FALSE|->0, TRUE|->1}, f = ...
328		% we assume Well-Definedness
329		% we also accept closures without equality now
330
331		is_infinite_equality_closure(IDs, TYPES, Body) :-
332		%IDs = [_,_|_], % we used to require at least at least two variables
333		\+ Body = b(member(_,_),_,_), % simple member closure; we deal with it separately (and avoid blow-up of checks, cf test 2283)
334	?	check_inf_cl_body(Body,[],OutConstrained),
335		% if we arrive here, we know that the body constraint is satisfiable
336	?	(member(_ID/infinite,OutConstrained) -> true
337		; contains_infinite_type(IDs,TYPES,OutConstrained)).
338
339		contains_infinite_type([ID|IT],[H|T],OutConstrained) :-
340		(is_infinite_type(H),
341	?	\+ member(ID/_,OutConstrained)
342		-> true ; contains_infinite_type(IT,T,OutConstrained)).
343
344		:- use_module(b_ast_cleanup,[definitely_not_empty_and_finite/1, definitely_infinite/1]).
345		:- use_module(external_functions,[external_pred_always_true/1]).
346		:- use_module(bsyntaxtree, [get_texpr_id/2, get_texpr_type/2, definitely_not_empty_set/1]).
347		check_inf_cl_body(b(B,pred,_),InConstrained,OutConstrained) :-
348	?	check_bdy_aux(B,InConstrained,OutConstrained).
349		check_bdy_aux(conjunct(A,B),InConstrained,OutConstrained) :- !,
350	?	check_inf_cl_body(A,InConstrained,OutConstrained1),
351	?	check_inf_cl_body(B,OutConstrained1,OutConstrained).
352		check_bdy_aux(disjunct(A,B),InConstrained,OutConstrained) :- !,
353	?	(check_inf_cl_body(A,InConstrained,OutConstrained) -> true
354	?	; check_inf_cl_body(B,InConstrained,OutConstrained)).
355		check_bdy_aux(exists(_Ids,Equal), Constrained, OutConstrained) :- !, % happens in Event-B style compr. sets, cf test 2514
356		% TODO: remove local identifiers from OutConstrained
357		% TODO: we could add identifiers and recursively process Body, even if more complex than simple equality
358		% Example: bap={i,x,y• i:INTEGER & x=y & x:INTEGER|i|->(x|->y)} & bap[{100}][1..2]=res
359		Equal = b(equal(LHS,RHS),pred,_),
360		check_bdy_aux(equal(LHS,RHS), Constrained, OutConstrained). % ID = RHS or ID'field = RHS
361		check_bdy_aux(equal(LHS,RHS), Constrained, OutConstrained) :- !,
362		(check_bdy_equal(LHS,RHS,Constrained,OutConstrained) -> true
363		; check_bdy_equal(RHS,LHS,Constrained,OutConstrained)),!.
364		check_bdy_aux(member(b(identifier(ID),TYPE,_),SET),Constrained,[ID/INFINITE|Constrained]) :- !,
365	?	\+ member(ID/_,Constrained),
366		rhs_safe(Constrained,SET), % avoid ID : {ID+1, ID+2}
367		(is_infinite_type(TYPE)
368		-> %check that SET is infinite; otherwise remove from IDs
369	?	(definitely_infinite(SET) -> INFINITE=infinite;
370		definitely_not_empty_and_finite(SET) -> INFINITE = finite
371		)
372		; definitely_not_empty_and_finite(SET), % otherwise we may have no solution and the entire closure is empty
373		INFINITE = finite
374		).
375		check_bdy_aux(member(LHS,RHS),Constrained,[ID/infinite|Constrained]) :- !, % ID'Field : SET
376		record_field_access_with_infinite_rest_type(LHS,RHS,Constrained,ID), % should we also cater for finite rest?
377		definitely_not_empty_set(RHS).
378		check_bdy_aux(not_equal(A,B),Constrained,[ID/infinite|TC]) :- !,
379		(get_texpr_id(A,ID)
380		-> is_static_expr_of_infinite_type(B) % we have to be careful that B does not directly or indirectly reference A
381		; get_texpr_id(B,ID),
382		is_static_expr_of_infinite_type(A)
383		),
384	?	(select(ID/Kind,Constrained,TC)
385		-> Kind=infinite % if it was infinite it will remain infinite, we only discard a single static value
386		; TC=Constrained).
387		check_bdy_aux(truth,Constrained,OutConstrained) :- !, OutConstrained=Constrained.
388		check_bdy_aux(external_pred_call(FunName,_Args),Constrained,Constrained) :- !,
389		external_pred_always_true(FunName).
390		check_bdy_aux(EXPR,Constrained,[ID/infinite|Constrained]) :-
391		%% TO DO: store bounds in ID/... list to check if the domain remains infinite!
392		greater_typing(EXPR,ID,_UP),
393	?	\+ member(ID/_,Constrained).
394		check_bdy_aux(EXPR,Constrained,[ID/infinite|Constrained]) :-
395		less_typing(EXPR,ID,_UP),
396	?	\+ member(ID/_,Constrained).
397
398
399		check_bdy_equal(LHS,RHS, Constrained, [ID/equal|Constrained]) :-
400		get_texpr_id(LHS,ID),
401	?	\+ member(ID/_,Constrained), % no constraints on ID so far
402		does_not_occur_in(ID,RHS),
403		rhs_safe(Constrained,RHS),
404		!. % the equation must have a solution; assuming well-definedness
405		check_bdy_equal(LHS,RHS, Constrained, [ID/infinite|Constrained]) :- % ID'FieldName = RHS
406		% detect closures like {x|x:struct(a:INTEGER,b:BOOL) & x'b=FALSE}, see test 2483
407		record_field_access_with_infinite_rest_type(LHS,RHS,Constrained,ID),!.
408
409		% check if the RHS is sufficiently unconstrained so that equality with a new variable will succeed
410		% TODO: maybe faster to find_identifier_uses once rather than calling does_not_occur_in repeatedly
411		rhs_safe([],_).
412		rhs_safe([HID/Kind|TConstrained],RHS) :-
413		(Kind=infinite -> true % CHECK!
414		; %HID could be bound to new ID, e.g., via HID=NewID+1 and equation NewID=HID would have no solution
415		does_not_occur_in(HID,RHS)
416		),
417		rhs_safe(TConstrained,RHS).
418
419		% see if we have LHS = ID'FieldName and ID does not occur in RHS and other fields are still infinite
420		record_field_access_with_infinite_rest_type(LHS,RHS,Constrained,ID) :-
421		LHS = b(record_field(TID,FieldName),_,_),
422		get_texpr_id(TID,ID),
423	?	\+ member(ID/_,Constrained), % no constraints on ID so far
424		get_texpr_type(TID,record(FieldTypes)),
425	?	select(field(FieldName,_),FieldTypes,RestTypes),
426		% we now have only a single value for field FieldName
427		is_infinite_type(record(RestTypes)), % there are still infinitely many values left given the other fields
428		does_not_occur_in(ID,RHS),
429		rhs_safe(Constrained,RHS),!.
430
431
432		:- use_module(bsyntaxtree,[occurs_in_expr/2]).
433		does_not_occur_in(ID,EXPR) :- \+ occurs_in_expr(ID,EXPR).
434
435
436
437		% check if we have a closure of type id(SetValue)
438
439		is_id_closure_over([ID1,ID2], [TYPE,TYPE],Body, ID_Domain, Full) :- nonvar(Body),
440		Body=b(equal(b(identifier(ID1),TYPE,_),b(identifier(ID2),TYPE,_)),pred,_),
441		!,
442		convert_type_to_value(TYPE,ID_Domain), Full=true.
443		is_id_closure_over(Par,Types,Body,ID_Domain,Full) :- nonvar(Par),nonvar(Body),
444		is_member_closure(Par,Types,Body,_,Set), % print(member_closure(Set)),nl,
445		nonvar(Set),
446		Set = identity(b(VAL,set(_TYPE),_)),
447		nonvar(VAL), VAL=value(ID_Domain),
448		(custom_explicit_sets:is_definitely_maximal_set(ID_Domain) -> Full=true ; Full=false).
449
450		%:- use_module(kernel_objects,[all_strings_wf/2]).
451		convert_type_to_value(integer,global_set('INTEGER')).
452		convert_type_to_value(global(G),global_set(G)).
453		convert_type_to_value(boolean,BS) :- BS=[pred_true /* bool_true */,pred_false /* bool_false */]. % TO DO: generate AVL ?
454		convert_type_to_value(string,global_set('STRING')). % :- all_strings_wf(S,WF).
455		%convert_type_to_value(Type,closure([x],[Type],TRUTH)) :- ... TO DO
456
457
458
459		/* Event-B id closure over full Type */
460
461		is_full_id_closure(P,T,B) :- is_id_closure_over(P,T,B,_,true).
462
463
464		% currently commented out in is_special_infinite_closure
465		%is_prj1_closure([ID1,_ID2,RESID],[Type1,Type2,Type1],
466		% b(equal(b(identifier(RESID),Type1,_),b(identifier(ID1),Type1,_)),pred,_),Type1,Type2).
467		%is_prj2_closure([_ID1,ID2,RESID],[Type1,Type2,Type2],
468		% b(equal(b(identifier(RESID),Type2,_),b(identifier(ID2),Type2,_)),pred,_),Type1,Type2).
469
470
471		% ---- SYMBOLIC and RECURSIVE annotations
472
473		get_recursive_identifier_of_closure(V,RID) :- nonvar(V), V=closure(_P,_T,B),
474		get_recursive_identifier_of_closure_body(B,RID).
475	?	get_recursive_identifier_of_closure_body(b(_,_,BodyInfo),RID) :- member(prob_annotation(recursive(RID)),BodyInfo).
476
477		is_recursive_closure(V) :- nonvar(V), V=closure(P,T,B),
478		is_recursive_closure(P,T,B).
479
480		is_recursive_closure(_P,_T,b(_,_,INFO)) :-
481	?	member(prob_annotation('RECURSIVE'),INFO).
482		% we also have prob_annotation(recursive(TID)) annotation
483
484		is_symbolic_closure(V) :- nonvar(V), V=closure(P,T,B),
485	?	is_symbolic_closure(P,T,B).
486
487		is_symbolic_closure(_P,_T,b(_,_,INFO)) :-
488	?	member(prob_annotation('SYMBOLIC'),INFO).
489
490		% see also is_converted_lambda_closure
491
492
493		:- use_module(error_manager,[add_internal_error/2, add_error/3]).
494		:- use_module(debug,[debug_println/2]).
495
496		% mark a closure as symbolic by marking the info field of the body predicate
497		mark_closure_as_symbolic(C,R) :-
498		mark_closure3(C,['SYMBOLIC'],R).
499		mark_closure_as_recursive(C,R) :-
500		mark_closure3(C,['SYMBOLIC','RECURSIVE'],R).
501		mark_closure_as_force(C,R) :-
502		mark_closure3(C,['FORCE'],R).
503		mark_closure3(_,ANN,R) :- nonvar(R), % we could use equal_object
504		add_internal_error('Result already instantiated: ',mark_closure3(_,ANN,R)),fail.
505		mark_closure3(C,ANN,R) :- var(C), % we could use equal_object
506		!,
507		debug_println(19,not_marking_var_closure(C,ANN)),
508		R=C.
509		mark_closure3(C,ANN,R) :- mark_closure(C,ANN,R).
510		%:- block mark_closure(-,?,?).
511		mark_closure(closure(P,T,B),ANN,R) :- !, mark_aux(P,T,B,ANN,R).
512		mark_closure(A,_,Res) :- A=Res. % not a closure
513		%:- block mark_aux(?,?,-,?,?).
514		mark_aux(P,T,b(Pred,pred,INFO),ANN,Res) :-
515		(ground(INFO)
516		-> mark_info(ANN,INFO,RINFO)
517		; add_error(mark_aux,'Info field not set: ',closure(P,T,b(Pred,pred,INFO))),
518		RINFO=INFO),
519		Res = closure(P,T,b(Pred,pred,RINFO)).
520
521		mark_info([],INFO,INFO).
522		mark_info([ANN|T],INFO,Res) :-
523	?	(member(prob_annotation(ANN),INFO) -> Res=TRes ; Res = [prob_annotation(ANN)|TRes]),
524		mark_info(T,INFO,TRes).
525
526
527
528		% this will detect prj1/prj2 style functions which project away an infinite number of args
529		% such non-injective functions/relations remain infinite when composed with a finite set
530		is_infinite_non_injective_closure(closure(P,T,Body)) :-
531		%see also bsyntaxtree:get_lambda_equality(Body,LambdaID,RestBody,ResultExpr),
532		Body = b(equal(LHS,RHS),pred,_),
533		get_texpr_id(LHS,LambdaID),
534		get_texpr_id(RHS,ProjID), % TODO: get used ids and see if the rest is infinite
535		append(Args,[LambdaID],P), Args = [_,_|_],
536	?	nth1(Nr,Args,ProjID),
537	?	nth1(Nr2,T,NonProjectedType),
538		Nr2 \= Nr,
539		is_infinite_type(NonProjectedType).