1 % (c) 2009-2026 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 % detect closures like {x | x : SET } or {x,y | x |-> y : SET }
121 is_member_closure_with_info(Par,Types,b(PRED,_Pred,Info), TYPE,Info,SET) :-
122 is_member_closure_aux(PRED, Par,Types,TYPE,SET).
123 is_member_closure(Par,Types,b(PRED,_Pred,_), TYPE,SET) :-
124 is_member_closure_aux(PRED, Par,Types,TYPE,SET).
125
126 :- use_module(bsyntaxtree,[is_set_type/2]).
127 is_member_closure_aux(member(TID,TSET), Par,Types,ElementTYPE,SET) :-
128 tid_matches_paras(TID,Par,Types,ElementTYPE),
129 TSET = b(SET,_SETTYPE,_),
130 (paras_do_not_occur_in(Par,TSET) -> true).
131 is_member_closure_aux(subset(TID,BSET), Par,Types,ElementTYPE,SET) :-
132 tid_matches_paras(TID,Par,Types,ElementTYPE),
133 (paras_do_not_occur_in(Par,BSET) -> true),
134 SET = pow_subset(BSET).
135 % can we also detect pow1_subset ? {x| x/= {} & x<: BSET}
136
137
138
139 % check if the LHS of a member or subset expression exactly matches the closure parameters
140 tid_matches_paras(b(Expr,IDTYPE,Info),Par,Types,TYPE) :-
141 tid_matches_paras_aux(Expr,IDTYPE,Info,Par,Types,TYPE).
142 tid_matches_paras_aux(identifier(ID),IDTYPE,Info,[ID],[TYPE],TYPE) :-
143 (check_types_unify(IDTYPE,TYPE,Info) -> true ; write(type_mismatch_in_paras(ID)),nl,fail).
144 % used to be relevant for test 1948
145 tid_matches_paras_aux(couple(A,B),IDTYPE,_Info,[ID1,ID2],[T1,T2],IDTYPE) :-
146 IDTYPE = couple(IDTYPE1,IDTYPE2),
147 tid_matches_paras(A,[ID1],[T1],IDTYPE1),
148 tid_matches_paras(B,[ID2],[T2],IDTYPE2).
149 % TODO: treat nested couple(couple(A,B),C) using DCGs
150
151 % detect not_member closures + integerset as special not_member_closures
152 is_not_member_value_closure_or_integerset(global_set(X),TYPE,SET) :- !,
153 is_not_member_global_set(X,TYPE,SET).
154 is_not_member_value_closure_or_integerset(C,TYPE,SET) :- is_not_member_value_closure(C,TYPE,SET).
155
156 is_not_member_global_set('INTEGER',integer,[]).
157 is_not_member_global_set('NATURAL',integer,X) :-
158 construct_less_equal_closure(-1,X). % {x|x<0}.
159 is_not_member_global_set('NATURAL1',integer,X) :-
160 construct_less_equal_closure(0,X). %X = {x|x<1}.
161
162 is_not_member_value_closure(closure(Par,T,B),TYPE,SET) :-
163 is_not_member_closure(Par,T,B,TYPE,value(SET)).
164 is_not_member_closure([ID],[TYPE],b(PRED,_Pred,_),TYPE,SET) :-
165 is_not_member_closure_aux(PRED,ID,TYPE,SET).
166
167 :- use_module(kernel_tools,[ground_value/1]).
168 is_not_member_closure_aux(not_member(b(identifier(ID),IDType,Info),b(SET,SType,_)),ID,TYPE,SET)
169 :-
170 check_types_unify(IDType,TYPE,Info),
171 is_set_type(SType,IDType).
172 is_not_member_closure_aux(not_equal(b(identifier(ID),IDType,Info),ONE),ID,TYPE,SET) :-
173 (ONE = b(value(Val),_,_),
174 ground_value(Val)
175 -> custom_explicit_sets:construct_one_element_custom_set(Val,SetVal), SET = value(SetVal)
176 ; SET = set_extension([ONE])),
177 check_types_unify(IDType,TYPE,Info).
178 %is_not_member_closure_aux(PRED,ID,TYPE,SET) :- print(check_not_mem(PRED,ID,TYPE,SET)),nl,fail.
179
180 :- use_module(btypechecker, [unify_types_strict/2]).
181 :- use_module(error_manager, [add_error/4]).
182 check_types_unify(IDType,TYPE,_) :- unify_types_strict(IDType,TYPE),!.
183 check_types_unify(IDType,TYPE,Info) :- add_error(closures,'Types do not match:',IDType-TYPE,Info),fail.
184
185
186 construct_complement_closure(Delta,Type,Closure) :-
187 % print(generating_complement_closure(GlobalSet,Delta,Type)),nl,
188 construct_not_member_closure('_zzzz_unary',Type,[],value(Delta),Closure).
189
190
191
192 /* lambda abstractions */
193 :- 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])).
194 :- 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)
195 )).
196
197 :- use_module(bsyntaxtree,[conjunction_to_list/2,conjunct_predicates/2]).
198 is_lambda_closure(Args,Types,ClosurePred, OtherIDs, OtherTypes, DOMAINPRED,Res) :-
199 % TO DO: do this more efficiently: if LambdaID occurs in any non-equal predicate : stop searching
200 % TO DO: check if is_infinite_equality_closure is not a special case of lambda closure ?
201 append(OtherTypes,[LambdaType],Types), OtherTypes \= [],
202 append(OtherIDs,[LambdaID],Args),
203 Res=b(EXPR,LambdaType,EXPRINFO),
204 %used to call: b_interpreter:member_conjunct(EQ,ClosurePred,DOMAINPRED), ; but inlined below for efficiency
205 select_equality(ClosurePred,LambdaID,EXPR,LambdaType,EXPRINFO,DOMAINPRED),
206 !. % avoid backtracking member_conjunct
207 % tools:print_bt_message(is_lambda_closure(LambdaID)).
208 % Note: LAMBDA is usually '_lambda_result_'
209
210 identifier_equality(b(equal(b(LHS,Type,LHSInfo),b(RHS,_TypeRHS,RHSInfo)),pred,_),ID,Type,EXPR,EXPRINFO) :-
211 % no need to unify with TypeRHS; actually Prolog unification could fail due to seq types ?
212 identifier_equality_aux(LHS,LHSInfo,RHS,RHSInfo,ID,EXPR,EXPRINFO).
213 identifier_equality_aux(identifier(ID),_,EXPR,EXPRINFO,ID,EXPR,EXPRINFO) :- !.
214 identifier_equality_aux(EXPR,EXPRINFO,identifier(ID),_,ID,EXPR,EXPRINFO).
215
216 % find an equality ID = RHSExpr so that ID does not occur in RHSExpr nor in RestPred
217 % the identifier should be provided as input (for the cut below)
218 select_equality(ClosurePred,ID,RHSExpr,Type,Info,RestPred) :-
219 conjunction_to_list(ClosurePred,List),
220 ? select(EQ,List,RestList),
221 identifier_equality(EQ,ID,Type,RHSExpr,Info),
222 !, % once we find a first equality : no need to look for a second one as then does_not_occur in RestPred will always fail !
223 (ID='_lambda_result_',EQ=b(_,_,I),
224 ? member(prob_annotation('LAMBDA-EQUALITY'),I)
225 -> true % no need to perform occurs check in RHS, but in RestPred, cf test 1874
226 ; %format('Check occurs ~w : ',[ID]), translate:print_bexpr(b(RHSExpr,Type,Info)),nl,
227 does_not_occur_in(ID,b(RHSExpr,Type,Info))
228 ),
229 conjunct_predicates(RestList,RestPred),
230 does_not_occur_in(ID,RestPred).
231
232
233 :- use_module(memoization,[is_lambda_value_domain_memoization_closure/5]).
234
235 % check whether we have a lambda closure and whether we can compute its domain
236 is_lambda_value_domain_closure(P,T,Pred, DomainValue,Expr) :-
237 ? is_lambda_value_domain_memoization_closure(P,T,Pred, DV,E),!,
238 DV \= fail, E\= fail,
239 DomainValue=DV, Expr=E.
240 is_lambda_value_domain_closure(Args,Types,B, DomainValue, EXPR) :-
241 is_lambda_value_domain_normal_closure(Args,Types,B, DomainValue, EXPR).
242
243 is_lambda_value_domain_normal_closure(Args,Types,B, DomainValue, EXPR) :-
244 % tools_printing:print_term_summary(try_is_lambda_domain(Args,Types,B)), %
245 is_lambda_closure(Args,Types,B, OtherIDs,OtherTypes, DomainPred, EXPR),!,
246 %print(lambda_closure(OtherIDs)), translate:print_bexpr(EXPR),nl,
247 construct_closure_if_necessary(OtherIDs,OtherTypes,DomainPred,DomClosure),
248 ? (is_symbolic_closure(Args,Types,B)
249 -> mark_closure_as_symbolic(DomClosure,DomainValue)
250 ; DomainValue = DomClosure).
251 %print(lambda_domain(Args)),nl, (IDs=[_,_|_] -> trace ; true),
252 %translate:print_bvalue(DomainValue),nl.
253
254 % LAMBDARES is usually _lambda_result_, LAMBDARES cannot occur in DOMAIN (is value)
255
256 :- use_module(library(lists),[maplist/4]).
257 is_lambda_comprehension_set(b(comprehension_set(Parameters,Body),_,_),LambdaParas,DomainPred,EXPR) :-
258 maplist(get_names_and_types,Parameters,Args,Types),
259 is_lambda_closure(Args,Types,Body, OtherIDs,OtherTypes, DomainPred, EXPR),
260 maplist(combine_names_and_types,OtherIDs,OtherTypes,LambdaParas).
261
262 get_names_and_types(b(identifier(ID),Type,_),ID,Type).
263 combine_names_and_types(ID,Type,b(identifier(ID),Type,[])).
264
265 :- assert_must_succeed(closures:is_special_infinite_closure([x],[integer],b(truth,pred,[]))).
266 :- assert_must_succeed((X=b(identifier(x),integer,[]),N=b(integer(3),integer,[]),
267 closures:is_special_infinite_closure([x],[integer],b(greater(X,N),pred,[])))).
268 :- assert_must_succeed((X=b(identifier(x),integer,[]),N=b(integer(3),integer,[]),
269 closures:is_special_infinite_closure([x],[integer],b(greater(X,N),pred,[])))).
270 :- assert_must_succeed((X=b(identifier(x),integer,[]),N=b(integer(3),integer,[]),
271 closures:is_special_infinite_closure([x],[integer],b(less(X,N),pred,[])))).
272 :- assert_must_succeed((X=b(identifier(x),integer,[]),N=b(integer(3),integer,[]),
273 closures:is_special_infinite_closure([x],[integer],b(not_equal(X,N),pred,[])))).
274 :- assert_must_fail((X=b(identifier(x),integer,[]),N=b(integer(3),integer,[]),
275 closures:is_special_infinite_closure([x],[integer],b(equal(X,N),pred,[])))).
276 :- assert_must_succeed((X=b(identifier(x),integer,[]),N=b(integer(3),integer,[]),
277 closures:is_special_infinite_closure([x,y],[integer,integer],b(equal(X,N),pred,[])))).
278 :- assert_must_succeed((Y=b(identifier(y),integer,[]),N=b(integer(3),integer,[]),
279 closures:is_special_infinite_closure([x,y],[integer,integer],b(equal(Y,N),pred,[])))).
280
281 :- use_module(typing_tools,[is_infinite_type/1]).
282 /* checking for infinite closures */
283 %is_special_infinite_closure(_Par,T,b(truth,_Pred,_)) :- !, % now dealt with below
284 % member(Type,T), is_infinite_type(Type),!.
285 is_special_infinite_closure(Par,T,Body) :-
286 ? is_infinite_equality_closure(Par,T,Body),!.
287 %is_special_infinite_closure(Par,T,Body) :- is_full_id_closure(Par,T,Body,TYPE), is_infinite_type(TYPE).
288 %is_special_infinite_closure(Par,T,Body) :- is_prj1_closure(Par,T,Body,T1,_T2), is_infinite_type(T1).
289 %is_special_infinite_closure(Par,T,Body) :- is_prj2_closure(Par,T,Body,_T1,T2), is_infinite_type(T2).
290 is_special_infinite_closure(Par,T,Body) :-
291 is_not_member_closure(Par,T,Body,Type,value(_)), is_infinite_type(Type).
292
293 :- use_module(library(lists)).
294
295 greater_typing(greater(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP).
296 greater_typing(greater_equal(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP).
297 greater_typing(less(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP).
298 greater_typing(less_equal(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP).
299
300 less_typing(less(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP).
301 less_typing(less_equal(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP).
302 less_typing(greater(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP).
303 less_typing(greater_equal(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP).
304
305 is_integer_val(integer(UP),UP).
306 is_integer_val(value(V),UP) :- nonvar(V),V=int(UP).
307
308 is_static_expr_of_infinite_type(b(E,Type,_)) :- is_static_expr_of_infinite_type2(E,Type).
309 is_static_expr_of_infinite_type2(integer(_),_).
310 is_static_expr_of_infinite_type2(string(_),_).
311 is_static_expr_of_infinite_type2(real(_),_).
312 is_static_expr_of_infinite_type2(value(V),Type) :- is_val_of_infinite_type(V,Type).
313 is_static_expr_of_infinite_type2(empty_set,Type) :- is_infinite_type(Type).
314 is_static_expr_of_infinite_type2(empty_sequence,Type) :- is_infinite_type(Type).
315 % TODO: more typical expressions, set/sequence extension pairs
316
317 is_val_of_infinite_type(V,_) :- var(V),!,fail.
318 is_val_of_infinite_type(int(_),_).
319 is_val_of_infinite_type(string(_),_).
320 is_val_of_infinite_type(term(T),_) :- nonvar(T), T=floating(_). % term(floating(_))
321 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)).
322 is_val_of_infinite_type([],Type) :- is_infinite_type(Type).
323 is_val_of_infinite_type(avl_set(_),Type) :- is_infinite_type(Type).
324
325
326
327
328 % the following also translates global_set(NATURAL(1)) into closures
329 % TO DO: probably better to remove global_set(INTSET) all together and rewrite in ast_cleanup to closure
330 is_closure_or_integer_set(closure(P,T,B),P,T,B).
331 is_closure_or_integer_set(global_set(INTSET),
332 ['_zzzz_unary'],[integer],
333 b(greater_equal(
334 b(identifier('_zzzz_unary'),integer,[]),
335 b(integer(BOUND),integer,[])
336 ),
337 pred,
338 [prob_annotation('SYMBOLIC')])
339 ) :-
340 get_bound(INTSET,BOUND).
341 get_bound('NATURAL',0).
342 get_bound('NATURAL1',1).
343 % TO DO: allow INTEGER / maximal sets ? -> truth; could get rid of complement sets?
344
345 % to do: extend; could be value(infinite_closure)...
346
347
348
349 /* Equality closures {x1,x2,...|id=E2}, where id does not occur in E2 and id =xi */
350 % should cover id, prj1, prj2
351 % {x,y|y:BOOL & x=f(y) } or %x.(x:NATURAL|Expr(x))
352 % would not be infinite {x,y|x:BOOL & x=f(g(x)*y)} , g={FALSE|->0, TRUE|->1}, f = ...
353 % we assume Well-Definedness
354 % we also accept closures without equality now
355
356 is_infinite_equality_closure(IDs, TYPES, Body) :-
357 %IDs = [_,_|_], % we used to require at least at least two variables
358 \+ Body = b(member(_,_),_,_), % simple member closure; we deal with it separately (and avoid blow-up of checks, cf test 2283)
359 ? check_inf_cl_body(Body,[],OutConstrained),
360 % if we arrive here, we know that the body constraint is satisfiable
361 ? (member(_ID/infinite(_Bounds),OutConstrained) -> true
362 ; contains_infinite_type(IDs,TYPES,OutConstrained)).
363
364 contains_infinite_type([ID|IT],[H|T],OutConstrained) :-
365 (is_infinite_type(H),
366 ? \+ member(ID/_,OutConstrained)
367 -> true ; contains_infinite_type(IT,T,OutConstrained)).
368
369 :- use_module(library(ordsets),[ord_member/2]).
370 is_quantified(SIds,ID/_) :- ord_member(ID,SIds).
371 ?is_lambda_equality(b(equal(_,_),_,Infos)) :- member(prob_annotation('LAMBDA-EQUALITY'),Infos).
372
373 :- use_module(b_ast_cleanup,[definitely_not_empty_and_finite/1, definitely_infinite/1]).
374 :- use_module(external_functions,[external_pred_always_true/1]).
375 :- use_module(bsyntaxtree, [get_texpr_id/2, get_texpr_type/2, definitely_not_empty_set/1]).
376 check_inf_cl_body(b(B,pred,_),InConstrained,OutConstrained) :-
377 ? check_bdy_aux(B,InConstrained,OutConstrained).
378
379 l_check_inf_cl_body([]) --> [].
380 ?l_check_inf_cl_body([H|T]) --> check_inf_cl_body(H), l_check_inf_cl_body(T).
381
382 :- use_module(probsrc(tools),[split_list/4]).
383
384 check_bdy_aux(conjunct(A,B),InConstrained,OutConstrained) :- !,
385 conjunction_to_list(b(conjunct(A,B),pred,[]),List),
386 split_list(is_lambda_equality,List,LambdaEq,Rest),
387 l_check_inf_cl_body(LambdaEq,InConstrained,OutConstrained1), % treat lambda equalities first
388 % reason: avoid failing due to rhs_safe checks; ideally we should do topological sorting
389 % or keep track of really used ids in each equality
390 ? l_check_inf_cl_body(Rest,OutConstrained1,OutConstrained).
391 check_bdy_aux(disjunct(A,B),InConstrained,OutConstrained) :- !,
392 ? (check_inf_cl_body(A,InConstrained,OutConstrained) -> true
393 ? ; check_inf_cl_body(B,InConstrained,OutConstrained)). % TODO: union bounds
394 check_bdy_aux(exists(TIds,ExistsBody), Constrained, OutConstrained) :- !,
395 bsyntaxtree:get_texpr_ids(TIds,Ids), sort(Ids,SIds),
396 % happens in Event-B style compr. sets, cf test 2514
397 % Example: bap={i,x,y• i:INTEGER & x=y & x:INTEGER|i|->(x|->y)} & bap[{100}][1..2]=res
398 exclude(is_quantified(SIds),Constrained,C1), % remove any var that is clashing with exists ids
399 ? check_inf_cl_body(ExistsBody,C1,C2),
400 exclude(is_quantified(SIds),C2,OutConstrained).
401 % remove quantified ids; should not count towards outer infinity, unless linked via equal to an outer id
402 % example, UNION(x,y,z).(x:INTEGER & y=x*x & z=x+x|{x|->(y|->z)}) = s & not(s:FIN(s))
403 % or {i•i:NATURAL|i*i}; but we need to prove that expression in RHS is injective, {i•i:NATURAL|i*0} is finite
404
405 check_bdy_aux(equal(LHS,RHS), Constrained, OutConstrained) :- !,
406 (check_bdy_equal(LHS,RHS,Constrained,OutConstrained) -> true
407 ; check_bdy_equal(RHS,LHS,Constrained,OutConstrained)),!.
408 check_bdy_aux(member(b(identifier(ID),TYPE,_),SET),Constrained,[ID/INFINITE|Constrained]) :- !,
409 ? \+ member(ID/_,Constrained),
410 rhs_safe(Constrained,SET), % avoid ID : {ID+1, ID+2}
411 (is_infinite_type(TYPE)
412 -> %check that SET is infinite; otherwise remove from IDs
413 (definitely_infinite_with_bounds(SET,BB) -> INFINITE=infinite(BB);
414 definitely_not_empty_and_finite(SET) -> INFINITE = finite
415 )
416 ; definitely_not_empty_and_finite(SET), % otherwise we may have no solution and the entire closure is empty
417 INFINITE = finite
418 ).
419 check_bdy_aux(member(LHS,RHS),Constrained,[ID/infinite(bounds_unknown)|Constrained]) :- !, % ID'Field : SET
420 record_field_access_with_infinite_rest_type(LHS,RHS,Constrained,ID), % should we also cater for finite rest?
421 definitely_not_empty_set(RHS).
422 check_bdy_aux(not_equal(A,B),Constrained,[ID/infinite(bounds_unknown)|TC]) :- !,
423 (get_texpr_id(A,ID)
424 -> is_static_expr_of_infinite_type(B) % we have to be careful that B does not directly or indirectly reference A
425 ; get_texpr_id(B,ID),
426 is_static_expr_of_infinite_type(A)
427 ),
428 ? (select(ID/Kind,Constrained,TC)
429 -> Kind=infinite(_) % if it was infinite it will remain infinite, we only discard a single static value
430 % TODO: update bounds
431 ; TC=Constrained).
432 check_bdy_aux(truth,Constrained,OutConstrained) :- !, OutConstrained=Constrained.
433 check_bdy_aux(external_pred_call(FunName,_Args),Constrained,Constrained) :- !,
434 external_pred_always_true(FunName).
435 check_bdy_aux(EXPR,Constrained,[ID/infinite(Bounds)|Constrained]) :-
436 greater_typing(EXPR,ID,UP), % TODO: also allow symbolic bounds like {x,y|x > 2 & y > x}
437 B1 = bounds_greater(UP),
438 ? (member(ID/BI,Constrained)
439 -> BI=infinite(B2), intersect_bounds(B1,B2,Bounds) ; Bounds = B1).
440 check_bdy_aux(EXPR,Constrained,[ID/infinite(Bounds)|Constrained]) :-
441 less_typing(EXPR,ID,DOWN),
442 B1 = bounds_less(DOWN),
443 ? (member(ID/BI,Constrained)
444 -> BI=infinite(B2), intersect_bounds(B1,B2,Bounds) ; Bounds = B1).
445
446 % check if a set is definitely infinite, and try and return bounds information
447 definitely_infinite_with_bounds(b(SET,_,_),Bounds) :- definitely_infinite_wbounds2(SET,B),!,Bounds=B.
448 definitely_infinite_with_bounds(SET,bounds_unknown) :- definitely_infinite(SET).
449
450 definitely_infinite_wbounds2(integer_set(GS),Bounds) :- get_int_set_bounds(GS,Bounds).
451 definitely_infinite_wbounds2(value(V),Bounds) :- nonvar(V), definitely_infinite_wbounds3(V,Bounds).
452
453 definitely_infinite_wbounds3(global_set(GS), Bounds) :- get_int_set_bounds(GS,Bounds).
454
455 get_int_set_bounds('NATURAL',bounds_greater(-1)).
456 get_int_set_bounds('NATURAL1',bounds_greater(0)).
457
458 intersect_bounds(bounds_greater(N1),bounds_greater(N2),bounds_greater(Max)) :- number(N1), number(N2),
459 Max is max(N1,N2).
460 intersect_bounds(bounds_less(N1),bounds_less(N2),bounds_less(Min)) :- number(N1), number(N2),
461 Min is min(N1,N2).
462
463 :- use_module(bsyntaxtree,[get_integer/2]).
464 % check if a given value is in the bounds
465 value_in_bounds(bounds_greater(Bound),Value) :- !, get_integer(Value,ValNr), ValNr > Bound.
466 value_in_bounds(bounds_less(Bound),Value) :- !, get_integer(Value,ValNr), ValNr < Bound.
467 %value_in_bounds(Bounds,Value) :- write(value_in_bounds(Bounds,Value)),nl,fail.
468
469 check_bdy_equal(LHS,RHS, Constrained, [ID/equal|C2]) :-
470 get_texpr_id(LHS,ID),
471 ? (select(ID/INFINITE,Constrained,C2)
472 -> INFINITE = infinite(Bounds), % there are some constraints
473 value_in_bounds(Bounds,RHS) % check value satisfies constraints, eg: {b,a|a:NATURAL1 & b:NATURAL & b=0}
474 ; C2=Constrained % no constraints on ID so far
475 ),
476 % TODO: store bounds for /infinite and check if RHS is in set?
477 does_not_occur_in(ID,RHS), % we have no direct equation like ID=ID+1
478 rhs_safe(Constrained,RHS),
479 !. % the equation must have a solution; assuming well-definedness
480 check_bdy_equal(LHS,RHS, Constrained, [ID/infinite(bounds_unknown)|Constrained]) :- % ID'FieldName = RHS
481 % detect closures like {x|x:struct(a:INTEGER,b:BOOL) & x'b=FALSE}, see test 2483
482 record_field_access_with_infinite_rest_type(LHS,RHS,Constrained,ID),!.
483
484 % check if the RHS is sufficiently unconstrained so that equality with a new variable will succeed
485 % see test 2483, card({x,y,v|x:INTEGER & y:{v+1,v+2} & v=y}) = 0
486 % TODO: maybe faster to find_identifier_uses once rather than calling does_not_occur_in repeatedly
487 % TODO: detect if an identifier is used only once, then we do not need to check RHS (LAMBDA-EQUALITY)
488 rhs_safe([],_).
489 rhs_safe([HID/Kind|TConstrained],RHS) :-
490 (Kind=infinite(_) -> true % CHECK! happens for HID=b in 2283
491 ; %HID could be bound to new ID, e.g., via HID=NewID+1 and equation NewID=HID would have no solution
492 does_not_occur_in(HID,RHS)
493 ),
494 rhs_safe(TConstrained,RHS).
495
496 % see if we have LHS = ID'FieldName and ID does not occur in RHS and other fields are still infinite
497 record_field_access_with_infinite_rest_type(LHS,RHS,Constrained,ID) :-
498 LHS = b(record_field(TID,FieldName),_,_),
499 get_texpr_id(TID,ID),
500 ? \+ member(ID/_,Constrained), % no constraints on ID so far
501 get_texpr_type(TID,record(FieldTypes)),
502 ? select(field(FieldName,_),FieldTypes,RestTypes),
503 % we now have only a single value for field FieldName
504 is_infinite_type(record(RestTypes)), % there are still infinitely many values left given the other fields
505 does_not_occur_in(ID,RHS),
506 rhs_safe(Constrained,RHS),!.
507
508
509 :- use_module(bsyntaxtree,[occurs_in_expr/2]).
510 does_not_occur_in(ID,EXPR) :- \+ occurs_in_expr(ID,EXPR).
511
512 :- use_module(bsyntaxtree,[some_id_occurs_in_expr/2]).
513 paras_do_not_occur_in([ID],TExpr) :- !, does_not_occur_in(ID,TExpr).
514 paras_do_not_occur_in(Ids,TExpr) :- sort(Ids,SIds), \+ some_id_occurs_in_expr(SIds,TExpr).
515
516
517 % check if we have a closure of type id(SetValue)
518
519 is_id_closure_over([ID1,ID2], [TYPE,TYPE],Body, ID_Domain, Full) :- nonvar(Body),
520 Body=b(equal(b(identifier(ID1),TYPE,_),b(identifier(ID2),TYPE,_)),pred,_),
521 !,
522 convert_type_to_value(TYPE,ID_Domain), Full=true.
523 is_id_closure_over(Par,Types,Body,ID_Domain,Full) :- nonvar(Par),nonvar(Body),
524 is_member_closure(Par,Types,Body,_,Set), % print(member_closure(Set)),nl,
525 nonvar(Set),
526 Set = identity(b(VAL,SType,_)),
527 is_set_type(SType,_),
528 nonvar(VAL), VAL=value(ID_Domain),
529 (custom_explicit_sets:is_definitely_maximal_set(ID_Domain) -> Full=true ; Full=false).
530
531 %:- use_module(kernel_objects,[all_strings_wf/2]).
532 convert_type_to_value(integer,global_set('INTEGER')).
533 convert_type_to_value(global(G),global_set(G)).
534 convert_type_to_value(boolean,BS) :- BS=[pred_true /* bool_true */,pred_false /* bool_false */]. % TO DO: generate AVL ?
535 convert_type_to_value(string,global_set('STRING')). % :- all_strings_wf(S,WF).
536 %convert_type_to_value(Type,closure([x],[Type],TRUTH)) :- ... TO DO
537
538
539
540 /* Event-B id closure over full Type */
541
542 is_full_id_closure(P,T,B) :- is_id_closure_over(P,T,B,_,true).
543
544
545 % currently commented out in is_special_infinite_closure
546 %is_prj1_closure([ID1,_ID2,RESID],[Type1,Type2,Type1],
547 % b(equal(b(identifier(RESID),Type1,_),b(identifier(ID1),Type1,_)),pred,_),Type1,Type2).
548 %is_prj2_closure([_ID1,ID2,RESID],[Type1,Type2,Type2],
549 % b(equal(b(identifier(RESID),Type2,_),b(identifier(ID2),Type2,_)),pred,_),Type1,Type2).
550
551
552 % ---- SYMBOLIC and RECURSIVE annotations
553
554 get_recursive_identifier_of_closure(V,RID) :- nonvar(V), V=closure(_P,_T,B),
555 get_recursive_identifier_of_closure_body(B,RID).
556 ?get_recursive_identifier_of_closure_body(b(_,_,BodyInfo),RID) :- member(prob_annotation(recursive(RID)),BodyInfo).
557
558 is_recursive_closure(V) :- nonvar(V), V=closure(P,T,B),
559 is_recursive_closure(P,T,B).
560
561 is_recursive_closure(_P,_T,b(_,_,INFO)) :-
562 ? member(prob_annotation('RECURSIVE'),INFO).
563 % we also have prob_annotation(recursive(TID)) annotation
564
565 is_symbolic_closure(V) :- nonvar(V), V=closure(P,T,B),
566 ? is_symbolic_closure(P,T,B).
567
568 is_symbolic_closure(_P,_T,b(_,_,INFO)) :-
569 ? member(prob_annotation('SYMBOLIC'),INFO).
570
571 % see also is_converted_lambda_closure
572
573
574 :- use_module(error_manager,[add_internal_error/2, add_error/3]).
575 :- use_module(debug,[debug_println/2]).
576
577 % mark a closure as symbolic by marking the info field of the body predicate
578 mark_closure_as_symbolic(C,R) :-
579 mark_closure3(C,['SYMBOLIC'],R).
580 mark_closure_as_recursive(C,R) :-
581 mark_closure3(C,['SYMBOLIC','RECURSIVE'],R).
582 mark_closure_as_force(C,R) :-
583 mark_closure3(C,['FORCE'],R).
584 mark_closure3(_,ANN,R) :- nonvar(R), % we could use equal_object
585 add_internal_error('Result already instantiated: ',mark_closure3(_,ANN,R)),fail.
586 mark_closure3(C,ANN,R) :- var(C), % we could use equal_object
587 !,
588 debug_println(19,not_marking_var_closure(C,ANN)),
589 R=C.
590 mark_closure3(C,ANN,R) :- mark_closure(C,ANN,R).
591 %:- block mark_closure(-,?,?).
592 mark_closure(closure(P,T,B),ANN,R) :- !, mark_aux(P,T,B,ANN,R).
593 mark_closure(A,_,Res) :- A=Res. % not a closure
594 %:- block mark_aux(?,?,-,?,?).
595 mark_aux(P,T,b(Pred,pred,INFO),ANN,Res) :-
596 (ground(INFO)
597 -> mark_info(ANN,INFO,RINFO)
598 ; add_error(mark_aux,'Info field not set: ',closure(P,T,b(Pred,pred,INFO))),
599 RINFO=INFO),
600 Res = closure(P,T,b(Pred,pred,RINFO)).
601
602 mark_info([],INFO,INFO).
603 mark_info([ANN|T],INFO,Res) :-
604 ? (member(prob_annotation(ANN),INFO) -> Res=TRes ; Res = [prob_annotation(ANN)|TRes]),
605 mark_info(T,INFO,TRes).
606
607
608
609 % this will detect prj1/prj2 style functions which project away an infinite number of args
610 % such non-injective functions/relations remain infinite when composed with a finite set
611 is_infinite_non_injective_closure(closure(P,T,Body)) :-
612 %see also bsyntaxtree:get_lambda_equality(Body,LambdaID,RestBody,ResultExpr),
613 Body = b(equal(LHS,RHS),pred,_),
614 get_texpr_id(LHS,LambdaID),
615 get_texpr_id(RHS,ProjID), % TODO: get used ids and see if the rest is infinite
616 append(Args,[LambdaID],P), Args = [_,_|_],
617 ? nth1(Nr,Args,ProjID),
618 ? nth1(Nr2,T,NonProjectedType),
619 Nr2 \= Nr,
620 is_infinite_type(NonProjectedType).