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(equal(LHS,RHS), Constrained, OutConstrained) :- !, |
356 | | (check_bdy_equal(LHS,RHS,Constrained,OutConstrained) -> true |
357 | | ; check_bdy_equal(RHS,LHS,Constrained,OutConstrained)),!. |
358 | | check_bdy_aux(member(b(identifier(ID),TYPE,_),SET),Constrained,[ID/INFINITE|Constrained]) :- !, |
359 | ? | \+ member(ID/_,Constrained), |
360 | | rhs_safe(Constrained,SET), % avoid ID : {ID+1, ID+2} |
361 | | (is_infinite_type(TYPE) |
362 | | -> %check that SET is infinite; otherwise remove from IDs |
363 | ? | (definitely_infinite(SET) -> INFINITE=infinite; |
364 | | definitely_not_empty_and_finite(SET) -> INFINITE = finite |
365 | | ) |
366 | | ; definitely_not_empty_and_finite(SET), % otherwise we may have no solution and the entire closure is empty |
367 | | INFINITE = finite |
368 | | ). |
369 | | check_bdy_aux(member(LHS,RHS),Constrained,[ID/infinite|Constrained]) :- !, % ID'Field : SET |
370 | | record_field_access_with_infinite_rest_type(LHS,RHS,Constrained,ID), % should we also cater for finite rest? |
371 | | definitely_not_empty_set(RHS). |
372 | | check_bdy_aux(not_equal(A,B),Constrained,[ID/infinite|TC]) :- !, |
373 | | (get_texpr_id(A,ID) |
374 | | -> is_static_expr_of_infinite_type(B) % we have to be careful that B does not directly or indirectly reference A |
375 | | ; get_texpr_id(B,ID), |
376 | | is_static_expr_of_infinite_type(A) |
377 | | ), |
378 | ? | (select(ID/Kind,Constrained,TC) |
379 | | -> Kind=infinite % if it was infinite it will remain infinite, we only discard a single static value |
380 | | ; TC=Constrained). |
381 | | check_bdy_aux(truth,Constrained,OutConstrained) :- !, OutConstrained=Constrained. |
382 | | check_bdy_aux(external_pred_call(FunName,_Args),Constrained,Constrained) :- !, |
383 | | external_pred_always_true(FunName). |
384 | | check_bdy_aux(EXPR,Constrained,[ID/infinite|Constrained]) :- |
385 | | %% TO DO: store bounds in ID/... list to check if the domain remains infinite! |
386 | | greater_typing(EXPR,ID,_UP), |
387 | ? | \+ member(ID/_,Constrained). |
388 | | check_bdy_aux(EXPR,Constrained,[ID/infinite|Constrained]) :- |
389 | | less_typing(EXPR,ID,_UP), |
390 | ? | \+ member(ID/_,Constrained). |
391 | | |
392 | | |
393 | | check_bdy_equal(LHS,RHS, Constrained, [ID/equal|Constrained]) :- |
394 | | get_texpr_id(LHS,ID), |
395 | ? | \+ member(ID/_,Constrained), % no constraints on ID so far |
396 | | does_not_occur_in(ID,RHS), |
397 | | rhs_safe(Constrained,RHS), |
398 | | !. % the equation must have a solution; assuming well-definedness |
399 | | check_bdy_equal(LHS,RHS, Constrained, [ID/infinite|Constrained]) :- % ID'FieldName = RHS |
400 | | % detect closures like {x|x:struct(a:INTEGER,b:BOOL) & x'b=FALSE}, see test 2483 |
401 | | record_field_access_with_infinite_rest_type(LHS,RHS,Constrained,ID),!. |
402 | | |
403 | | % check if the RHS is sufficiently unconstrained so that equality with a new variable will succeed |
404 | | % TODO: maybe faster to find_identifier_uses once rather than calling does_not_occur_in repeatedly |
405 | | rhs_safe([],_). |
406 | | rhs_safe([HID/Kind|TConstrained],RHS) :- |
407 | | (Kind=infinite -> true % CHECK! |
408 | | ; %HID could be bound to new ID, e.g., via HID=NewID+1 and equation NewID=HID would have no solution |
409 | | does_not_occur_in(HID,RHS) |
410 | | ), |
411 | | rhs_safe(TConstrained,RHS). |
412 | | |
413 | | % see if we have LHS = ID'FieldName and ID does not occur in RHS and other fields are still infinite |
414 | | record_field_access_with_infinite_rest_type(LHS,RHS,Constrained,ID) :- |
415 | | LHS = b(record_field(TID,FieldName),_,_), |
416 | | get_texpr_id(TID,ID), |
417 | ? | \+ member(ID/_,Constrained), % no constraints on ID so far |
418 | | get_texpr_type(TID,record(FieldTypes)), |
419 | ? | select(field(FieldName,_),FieldTypes,RestTypes), |
420 | | % we now have only a single value for field FieldName |
421 | | is_infinite_type(record(RestTypes)), % there are still infinitely many values left given the other fields |
422 | | does_not_occur_in(ID,RHS), |
423 | | rhs_safe(Constrained,RHS),!. |
424 | | |
425 | | |
426 | | :- use_module(bsyntaxtree,[occurs_in_expr/2]). |
427 | | does_not_occur_in(ID,EXPR) :- \+ occurs_in_expr(ID,EXPR). |
428 | | |
429 | | |
430 | | |
431 | | % check if we have a closure of type id(SetValue) |
432 | | |
433 | | is_id_closure_over([ID1,ID2], [TYPE,TYPE],Body, ID_Domain, Full) :- nonvar(Body), |
434 | | Body=b(equal(b(identifier(ID1),TYPE,_),b(identifier(ID2),TYPE,_)),pred,_), |
435 | | !, |
436 | | convert_type_to_value(TYPE,ID_Domain), Full=true. |
437 | | is_id_closure_over(Par,Types,Body,ID_Domain,Full) :- nonvar(Par),nonvar(Body), |
438 | | is_member_closure(Par,Types,Body,_,Set), % print(member_closure(Set)),nl, |
439 | | nonvar(Set), |
440 | | Set = identity(b(VAL,set(_TYPE),_)), |
441 | | nonvar(VAL), VAL=value(ID_Domain), |
442 | | (custom_explicit_sets:is_definitely_maximal_set(ID_Domain) -> Full=true ; Full=false). |
443 | | |
444 | | %:- use_module(kernel_objects,[all_strings_wf/2]). |
445 | | convert_type_to_value(integer,global_set('INTEGER')). |
446 | | convert_type_to_value(global(G),global_set(G)). |
447 | | convert_type_to_value(boolean,BS) :- BS=[pred_true /* bool_true */,pred_false /* bool_false */]. % TO DO: generate AVL ? |
448 | | convert_type_to_value(string,global_set('STRING')). % :- all_strings_wf(S,WF). |
449 | | %convert_type_to_value(Type,closure([x],[Type],TRUTH)) :- ... TO DO |
450 | | |
451 | | |
452 | | |
453 | | /* Event-B id closure over full Type */ |
454 | | |
455 | | is_full_id_closure(P,T,B) :- is_id_closure_over(P,T,B,_,true). |
456 | | |
457 | | |
458 | | % currently commented out in is_special_infinite_closure |
459 | | %is_prj1_closure([ID1,_ID2,RESID],[Type1,Type2,Type1], |
460 | | % b(equal(b(identifier(RESID),Type1,_),b(identifier(ID1),Type1,_)),pred,_),Type1,Type2). |
461 | | %is_prj2_closure([_ID1,ID2,RESID],[Type1,Type2,Type2], |
462 | | % b(equal(b(identifier(RESID),Type2,_),b(identifier(ID2),Type2,_)),pred,_),Type1,Type2). |
463 | | |
464 | | |
465 | | % ---- SYMBOLIC and RECURSIVE annotations |
466 | | |
467 | | get_recursive_identifier_of_closure(V,RID) :- nonvar(V), V=closure(_P,_T,B), |
468 | | get_recursive_identifier_of_closure_body(B,RID). |
469 | ? | get_recursive_identifier_of_closure_body(b(_,_,BodyInfo),RID) :- member(prob_annotation(recursive(RID)),BodyInfo). |
470 | | |
471 | | is_recursive_closure(V) :- nonvar(V), V=closure(P,T,B), |
472 | | is_recursive_closure(P,T,B). |
473 | | |
474 | | is_recursive_closure(_P,_T,b(_,_,INFO)) :- |
475 | ? | member(prob_annotation('RECURSIVE'),INFO). |
476 | | % we also have prob_annotation(recursive(TID)) annotation |
477 | | |
478 | | is_symbolic_closure(V) :- nonvar(V), V=closure(P,T,B), |
479 | ? | is_symbolic_closure(P,T,B). |
480 | | |
481 | | is_symbolic_closure(_P,_T,b(_,_,INFO)) :- |
482 | ? | member(prob_annotation('SYMBOLIC'),INFO). |
483 | | |
484 | | % see also is_converted_lambda_closure |
485 | | |
486 | | |
487 | | :- use_module(error_manager,[add_internal_error/2, add_error/3]). |
488 | | :- use_module(debug,[debug_println/2]). |
489 | | |
490 | | % mark a closure as symbolic by marking the info field of the body predicate |
491 | | mark_closure_as_symbolic(C,R) :- |
492 | | mark_closure3(C,['SYMBOLIC'],R). |
493 | | mark_closure_as_recursive(C,R) :- |
494 | | mark_closure3(C,['SYMBOLIC','RECURSIVE'],R). |
495 | | mark_closure_as_force(C,R) :- |
496 | | mark_closure3(C,['FORCE'],R). |
497 | | mark_closure3(_,ANN,R) :- nonvar(R), % we could use equal_object |
498 | | add_internal_error('Result already instantiated: ',mark_closure3(_,ANN,R)),fail. |
499 | | mark_closure3(C,ANN,R) :- var(C), % we could use equal_object |
500 | | !, |
501 | | debug_println(19,not_marking_var_closure(C,ANN)), |
502 | | R=C. |
503 | | mark_closure3(C,ANN,R) :- mark_closure(C,ANN,R). |
504 | | %:- block mark_closure(-,?,?). |
505 | | mark_closure(closure(P,T,B),ANN,R) :- !, mark_aux(P,T,B,ANN,R). |
506 | | mark_closure(A,_,Res) :- A=Res. % not a closure |
507 | | %:- block mark_aux(?,?,-,?,?). |
508 | | mark_aux(P,T,b(Pred,pred,INFO),ANN,Res) :- |
509 | | (ground(INFO) |
510 | | -> mark_info(ANN,INFO,RINFO) |
511 | | ; add_error(mark_aux,'Info field not set: ',closure(P,T,b(Pred,pred,INFO))), |
512 | | RINFO=INFO), |
513 | | Res = closure(P,T,b(Pred,pred,RINFO)). |
514 | | |
515 | | mark_info([],INFO,INFO). |
516 | | mark_info([ANN|T],INFO,Res) :- |
517 | ? | (member(prob_annotation(ANN),INFO) -> Res=TRes ; Res = [prob_annotation(ANN)|TRes]), |
518 | | mark_info(T,INFO,TRes). |
519 | | |
520 | | |
521 | | |
522 | | % this will detect prj1/prj2 style functions which project away an infinite number of args |
523 | | % such non-injective functions/relations remain infinite when composed with a finite set |
524 | | is_infinite_non_injective_closure(closure(P,T,Body)) :- |
525 | | %see also bsyntaxtree:get_lambda_equality(Body,LambdaID,RestBody,ResultExpr), |
526 | | Body = b(equal(LHS,RHS),pred,_), |
527 | | get_texpr_id(LHS,LambdaID), |
528 | | get_texpr_id(RHS,ProjID), % TODO: get used ids and see if the rest is infinite |
529 | | append(Args,[LambdaID],P), Args = [_,_|_], |
530 | ? | nth1(Nr,Args,ProjID), |
531 | ? | nth1(Nr2,T,NonProjectedType), |
532 | | Nr2 \= Nr, |
533 | | is_infinite_type(NonProjectedType). |