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