1 | | % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
2 | | % Heinrich Heine Universitaet Duesseldorf |
3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
4 | | |
5 | | :- module(closures,[construct_closure/4, is_closure/4, %is_closure_x/5, |
6 | | construct_closure_if_necessary/4, |
7 | | is_non_expanded_closure/1, |
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 | | is_lambda_value_domain_closure/5, is_lambda_closure/7, |
16 | | select_equality/6, |
17 | | is_special_infinite_closure/3, |
18 | | is_id_closure_over/5, |
19 | | is_full_id_closure/3, |
20 | | is_closure_or_integer_set/4]). |
21 | | |
22 | | :- use_module(module_information,[module_info/2]). |
23 | | :- module_info(group,kernel). |
24 | | :- module_info(description,'This module provides various utility functions to analyse ProB closures.'). |
25 | | |
26 | | construct_closure(Parameters, ParameterTypes, Body, Res) :- |
27 | | Res = closure(Parameters, ParameterTypes, Body). |
28 | | % Res = closure_x(Parameters, ParameterTypes, Body,_). %% STILL HAS PROBLEMS with delay, e.g. inside b_test_exists !! |
29 | | |
30 | | |
31 | | % an optimized version of construct_closure, which will try to produce explicit values if possible |
32 | | construct_closure_if_necessary(_,_,b(falsity,pred,_),Res) :- !, Res=[]. |
33 | | construct_closure_if_necessary([ID], [T1], b(Pred,pred,_), Res) :- %print(s(ID,T1,Pred)),nl,trace, |
34 | | construct_unary_closure(Pred,ID,T1,SET),!, |
35 | | Res = SET. |
36 | | construct_closure_if_necessary(Parameters, ParameterTypes, Body, Res) :- |
37 | | Res = closure(Parameters, ParameterTypes, Body). |
38 | | |
39 | | :- use_module(b_global_sets,[try_b_type2global_set/2]). |
40 | | :- use_module(custom_explicit_sets,[try_expand_and_convert_to_avl/2]). |
41 | | construct_unary_closure(member(b(identifier(ID),T1,_),b(value(SET),set(T1),_)),ID,T1,Res) :- Res=SET. |
42 | | construct_unary_closure(truth,_,T1,Res) :- try_b_type2global_set(T1,Res). |
43 | | construct_unary_closure(equal(b(identifier(ID),T1,_),b(value(SET),T1,_)),ID,T1,Res) :- |
44 | | try_expand_and_convert_to_avl([SET],Res). |
45 | | |
46 | | |
47 | | :- use_module(self_check). |
48 | | :- assert_must_succeed( closures:is_closure(closure([x],[integer],body),[x],[integer],body)). |
49 | | is_closure(closure_x(Parameters, ParameterTypes, Body, _Exp), Parameters, ParameterTypes, Body). |
50 | | is_closure(closure(Parameters, ParameterTypes, Body), Parameters, ParameterTypes, Body). |
51 | | |
52 | | |
53 | | %is_closure_x(closure_x(Parameters,ParameterTypes,Body,Exp), Parameters,ParameterTypes,Body,Exp). |
54 | | %is_closure_x( closure(Parameters,ParameterTypes,Body), Parameters,ParameterTypes,Body,none). |
55 | | |
56 | | |
57 | | is_non_expanded_closure(closure(_,_,_)). |
58 | | is_non_expanded_closure(closure_x(_,_,_,E)) :- nonvar(E). |
59 | | |
60 | | |
61 | | |
62 | | :- use_module(bsyntaxtree,[create_texpr/4, safe_create_texpr/4, extract_pos_infos/2]). |
63 | | % following not useful: construct_member_closure currently always called where the construction is needed |
64 | | %construct_member_closure(ID,_Type,ClosureSetExpression,Result) :- |
65 | | % nonvar(ClosureSetExpression),ClosureSetExpression = value(S),!, |
66 | | % print(construct_member_closure_value(ID,S)),nl, %% |
67 | | % Result=S. |
68 | | construct_member_closure(ID,Type,Info,ClosureSetExpression,Result) :- |
69 | | check_result_instantiation(Result,construct_member_closure(ID)), |
70 | | create_texpr(identifier(ID),Type,[],TIdentifier), % used to be [generated] |
71 | | extract_pos_infos(Info,PosInfo), % Note: safe_create_texpr will copy WD info |
72 | | safe_create_texpr(ClosureSetExpression,set(Type),PosInfo,TClosureSet), % TODO: we could store whether sub_expression_contains_wd_condition for next call |
73 | | safe_create_texpr(member(TIdentifier,TClosureSet),pred,PosInfo,TPred), |
74 | | construct_closure([ID],[Type],TPred,Result). |
75 | | |
76 | | construct_not_member_closure(ID,Type,Info,ClosureSetExpression,Result) :- |
77 | | check_result_instantiation(Result,construct_not_member_closure(ID)), |
78 | | create_texpr(identifier(ID),Type,[],TIdentifier), % used to be [generated] |
79 | | safe_create_texpr(ClosureSetExpression,set(Type),Info,TClosureSet), |
80 | | safe_create_texpr(not_member(TIdentifier,TClosureSet),pred,Info,TPred), |
81 | | construct_closure([ID],[Type],TPred,Result). |
82 | | |
83 | | :- use_module(error_manager,[add_internal_error/2]). |
84 | | % check that we do not instantiate result to early (rather than using equal_object) |
85 | | check_result_instantiation(X,_) :- var(X),!. |
86 | | check_result_instantiation(closure(_,_,_),_PP) :- !. |
87 | | check_result_instantiation(X,PP) :- |
88 | | add_internal_error('Result already instantiated in incompatible way: ',check_result_instantiation(X,PP)). |
89 | | |
90 | | is_member_closure_with_info([ID],[TYPE],b(PRED,_Pred,Info), TYPE,Info,SET) :- |
91 | | is_member_closure_aux(PRED, ID,TYPE,SET). |
92 | | is_member_closure([ID],[TYPE],b(PRED,_Pred,_), TYPE,SET) :- |
93 | | is_member_closure_aux(PRED, ID,TYPE,SET). |
94 | | |
95 | | is_member_closure_aux(member(b(identifier(ID),TYPE,_),b(SET,set(TYPE),_)), ID,TYPE,SET). |
96 | | is_member_closure_aux(subset(b(identifier(ID),TYPE,_),BSET), ID,TYPE,SET) :- SET = pow_subset(BSET). |
97 | | % can we also detect pow1_subset ? {x| x/= {} & x<: BSET} |
98 | | |
99 | | % detect not_member closures + integerset as special not_member_closures |
100 | | is_not_member_value_closure_or_integerset(global_set(X),TYPE,SET) :- !, |
101 | | is_not_member_global_set(X,TYPE,SET). |
102 | | is_not_member_value_closure_or_integerset(C,TYPE,SET) :- is_not_member_value_closure(C,TYPE,SET). |
103 | | |
104 | | is_not_member_global_set('INTEGER',integer,[]). |
105 | | is_not_member_global_set('NATURAL',integer,X) :- |
106 | | custom_explicit_sets:construct_less_equal_closure(-1,X). % {x|x<0}. |
107 | | is_not_member_global_set('NATURAL1',integer,X) :- |
108 | | custom_explicit_sets:construct_less_equal_closure(0,X). %X = {x|x<1}. |
109 | | |
110 | | is_not_member_value_closure(closure(Par,T,B),TYPE,SET) :- |
111 | | is_not_member_closure(Par,T,B,TYPE,value(SET)). |
112 | | is_not_member_closure([ID],[TYPE],b(PRED,_Pred,_),TYPE,SET) :- |
113 | | is_not_member_closure_aux(PRED,ID,TYPE,SET). |
114 | | |
115 | | is_not_member_closure_aux(not_member(b(identifier(ID),TYPE,_),b(SET,set(TYPE),_)),ID,TYPE,SET). |
116 | | is_not_member_closure_aux(not_equal(b(identifier(ID),TYPE,_),ONE),ID,TYPE,SET) :- |
117 | | (ONE = b(value(Val),_,_) |
118 | | -> custom_explicit_sets:construct_one_element_custom_set(Val,SetVal), SET = value(SetVal) |
119 | | ; SET = set_extension([ONE])). |
120 | | %is_not_member_closure_aux(PRED,ID,TYPE,SET) :- print(check_not_mem(PRED,ID,TYPE,SET)),nl,fail. |
121 | | |
122 | | construct_complement_closure(Delta,Type,Closure) :- |
123 | | % print(generating_complement_closure(GlobalSet,Delta,Type)),nl, |
124 | | construct_not_member_closure('_zzzz_unary',Type,[],value(Delta),Closure). |
125 | | |
126 | | |
127 | | |
128 | | /* lambda abstractions */ |
129 | | :- 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])). |
130 | | :- 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) |
131 | | )). |
132 | | |
133 | | :- use_module(bsyntaxtree,[conjunction_to_list/2,conjunct_predicates/2]). |
134 | | is_lambda_closure(Args,Types,ClosurePred, OtherIDs, OtherTypes, DOMAINPRED,Res) :- |
135 | | % TO DO: do this more efficiently: if LambdaID occurs in any non-equal predicate : stop searching |
136 | | % TO DO: check if is_infinite_equality_closure is not a special case of lambda closure ? |
137 | ? | append(OtherTypes,[LambdaType],Types), OtherTypes \= [], |
138 | ? | append(OtherIDs,[LambdaID],Args), |
139 | | Res=b(EXPR,LambdaType,EXPRINFO), |
140 | | %used to call: b_interpreter:member_conjunct(EQ,ClosurePred,DOMAINPRED), ; but inlined below for efficiency |
141 | | select_equality(ClosurePred,LambdaID,EXPR,LambdaType,EXPRINFO,DOMAINPRED), |
142 | | !. % avoid backtracking member_conjunct |
143 | | % tools:print_bt_message(is_lambda_closure(LambdaID)). |
144 | | % Note: LAMBDA is usually '_lambda_result_' |
145 | | |
146 | | identifier_equality(b(equal(b(LHS,Type,LHSInfo),b(RHS,_TypeRHS,RHSInfo)),pred,_),ID,Type,EXPR,EXPRINFO) :- |
147 | | % no need to unify with TypeRHS; actually Prolog unification could fail due to seq types ? |
148 | | identifier_equality_aux(LHS,LHSInfo,RHS,RHSInfo,ID,EXPR,EXPRINFO). |
149 | | identifier_equality_aux(identifier(ID),_,EXPR,EXPRINFO,ID,EXPR,EXPRINFO) :- !. |
150 | | identifier_equality_aux(EXPR,EXPRINFO,identifier(ID),_,ID,EXPR,EXPRINFO). |
151 | | |
152 | | % find an equality ID = RHSExpr so that ID does not occur in RHSExpr nor in RestPred |
153 | | % the identifier should be provided as input (for the cut below) |
154 | | select_equality(ClosurePred,ID,RHSExpr,Type,Info,RestPred) :- |
155 | | conjunction_to_list(ClosurePred,List), |
156 | ? | select(EQ,List,RestList), |
157 | | identifier_equality(EQ,ID,Type,RHSExpr,Info), |
158 | | !, % once we find a first equality : no need to look for a second one as then does_not_occur in RestPred will always fail ! |
159 | | does_not_occur_in(ID,b(RHSExpr,Type,Info)), |
160 | | conjunct_predicates(RestList,RestPred), |
161 | | does_not_occur_in(ID,RestPred). |
162 | | |
163 | | |
164 | | :- use_module(memoization,[get_memoization_closure_value/4]). |
165 | | |
166 | | % check whether we have a lambda closure and whether we can compute its domain |
167 | | is_lambda_value_domain_closure(P,T,Pred, DomainValue,Expr) :- |
168 | | get_memoization_closure_value(P,T,Pred,Value),!, |
169 | | Value = closure(P2,T2,Pred2), |
170 | | is_lambda_value_domain_closure(P2,T2,Pred2, DomainValue,Expr). |
171 | | is_lambda_value_domain_closure(Args,Types,B, DomainValue, EXPR) :- |
172 | | % tools_printing:print_term_summary(try_is_lambda_domain(Args,Types,B)), % |
173 | | is_lambda_closure(Args,Types,B, OtherIDs,OtherTypes, DomainPred, EXPR),!, |
174 | | %print(lambda_closure(OtherIDs)), translate:print_bexpr(EXPR),nl, |
175 | | construct_closure_if_necessary(OtherIDs,OtherTypes,DomainPred,DomainValue). |
176 | | %print(lambda_domain(Args)),nl, (IDs=[_,_|_] -> trace ; true), |
177 | | %translate:print_bvalue(DomainValue),nl. |
178 | | |
179 | | % LAMBDARES is usually _lambda_result_, LAMBDARES cannot occur in DOMAIN (is value) |
180 | | |
181 | | |
182 | | |
183 | | :- use_module(typing_tools,[is_infinite_type/1]). |
184 | | /* checking for infinite closures */ |
185 | | is_special_infinite_closure(_Par,T,b(truth,_Pred,_)) :- !, |
186 | | member(Type,T), is_infinite_type(Type),!. |
187 | | is_special_infinite_closure(Par,T,Body) :- %print(check_infinite(Par,T,Body)),nl, |
188 | ? | is_infinite_equality_closure(Par,T,Body),!. |
189 | | %is_special_infinite_closure(Par,T,Body) :- is_full_id_closure(Par,T,Body,TYPE), is_infinite_type(TYPE). |
190 | | %is_special_infinite_closure(Par,T,Body) :- is_prj1_closure(Par,T,Body,T1,_T2), is_infinite_type(T1). |
191 | | %is_special_infinite_closure(Par,T,Body) :- is_prj2_closure(Par,T,Body,_T1,T2), is_infinite_type(T2). |
192 | | is_special_infinite_closure(Par,T,Body) :- |
193 | | is_not_member_closure(Par,T,Body,Type,value(_)), is_infinite_type(Type). |
194 | | |
195 | | :- use_module(library(lists)). |
196 | | |
197 | | greater_typing(greater(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP). |
198 | | greater_typing(greater_equal(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP). |
199 | | greater_typing(less(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP). |
200 | | greater_typing(less_equal(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP). |
201 | | |
202 | | less_typing(less(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP). |
203 | | less_typing(less_equal(b(identifier(ID),integer,_),b(VUP,integer,_)),ID,UP) :- is_integer_val(VUP,UP). |
204 | | less_typing(greater(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP). |
205 | | less_typing(greater_equal(b(VUP,integer,_),b(identifier(ID),integer,_)),ID,UP) :- is_integer_val(VUP,UP). |
206 | | |
207 | | is_integer_val(integer(UP),UP). |
208 | | is_integer_val(value(V),UP) :- nonvar(V),V=int(UP). |
209 | | |
210 | ? | infinite_set(value(V)) :- !, % most common case, all other clauses do not seem to get covered |
211 | ? | nonvar(V),infinite_value_set(V). |
212 | | infinite_set(Rel) :- is_relation(Rel,A,B),!, |
213 | | (infinite_set(A) -> true ; infinite_set(B)). |
214 | | infinite_set(cartesian_product(b(A,_,_),b(B,_,_))) :- |
215 | | (infinite_set(A) -> true ; infinite_set(B)). |
216 | | infinite_set(pow_subset(b(A,_,_))) :- infinite_set(A). |
217 | | infinite_set(pow1_subset(b(A,_,_))) :- infinite_set(A). |
218 | | infinite_set(fin_subset(b(A,_,_))) :- infinite_set(A). |
219 | | infinite_set(fin1_subset(b(A,_,_))) :- infinite_set(A). |
220 | | infinite_set(seq(_)). |
221 | | infinite_set(seq1(_)). |
222 | | infinite_set(iseq(b(A,_,_))) :- infinite_set(A). |
223 | | infinite_set(iseq1(b(A,_,_))) :- infinite_set(A). |
224 | | infinite_set(perm(b(A,_,_))) :- infinite_set(A). |
225 | | infinite_set(integer_set(X)) :- |
226 | | X='NATURAL' ; X='NATURAL1' ; X='INTEGER'. |
227 | | infinite_set(string_set). |
228 | | |
229 | | infinite_value_set(global_set(X)) :- |
230 | ? | X='NATURAL' ; X='NATURAL1' ; X='INTEGER'. |
231 | | infinite_value_set(closure(P,T,B)) :- |
232 | | T \= [integer], % otherwise we could intersect with NATURAL,... |
233 | | custom_explicit_sets:is_infinite_closure(P,T,B). |
234 | | infinite_value_set(freetype(ID)) :- kernel_freetypes:is_infinite_freetype(ID). |
235 | | |
236 | | % the following also translates global_set(NATURAL(1)) into closures |
237 | | % TO DO: probably better to remove global_set(INTSET) all together and rewrite in ast_cleanup to closure |
238 | | is_closure_or_integer_set(closure(P,T,B),P,T,B). |
239 | | is_closure_or_integer_set(global_set(INTSET), |
240 | | ['_zzzz_unary'],[integer], |
241 | | b(greater_equal( |
242 | | b(identifier('_zzzz_unary'),integer,[]), |
243 | | b(integer(BOUND),integer,[]) |
244 | | ), |
245 | | pred, |
246 | | [prob_annotation('SYMBOLIC')]) |
247 | | ) :- |
248 | | get_bound(INTSET,BOUND). |
249 | | get_bound('NATURAL',0). |
250 | | get_bound('NATURAL1',1). |
251 | | % TO DO: allow INTEGER / maximal sets ? -> truth; could get rid of complement sets? |
252 | | |
253 | | % to do: extend; could be value(infinite_closure)... |
254 | | |
255 | | is_relation(relations(b(A,_,_),b(B,_,_)),A,B). |
256 | | is_relation(partial_function(b(A,_,_),b(B,_,_)),A,B). |
257 | | is_relation(total_function(b(A,_,_),b(B,_,_)),A,B). |
258 | | is_relation(partial_injection(b(A,_,_),b(B,_,_)),A,B). |
259 | | is_relation(total_injection(b(A,_,_),b(B,_,_)),A,B). |
260 | | is_relation(partial_surjection(b(A,_,_),b(B,_,_)),A,B). |
261 | | is_relation(total_surjection(b(A,_,_),b(B,_,_)),A,B). |
262 | | is_relation(total_bijection(b(A,_,_),b(B,_,_)),A,B). |
263 | | is_relation(partial_bijection(b(A,_,_),b(B,_,_)),A,B). |
264 | | is_relation(total_relation(b(A,_,_),b(B,_,_)),A,B). |
265 | | is_relation(surjection_relation(b(A,_,_),b(B,_,_)),A,B). |
266 | | is_relation(total_surjection_relation(b(A,_,_),b(B,_,_)),A,B). |
267 | | |
268 | | |
269 | | /* Equality closures {x1,x2,...|id=E2}, where id does not occur in E2 and id =xi */ |
270 | | % should cover id, prj1, prj2 |
271 | | % {x,y|y:BOOL & x=f(y) } or %x.(x:NATURAL|Expr(x)) |
272 | | % would not be infinite {x,y|x:BOOL & x=f(g(x)*y)} , g={FALSE|->0, TRUE|->1}, f = ... |
273 | | % we assume Well-Definedness |
274 | | |
275 | | %is_infinite_equality_closure(IDs,TYPES,B) :- IDs = [_,_|_], |
276 | | % print(try(IDs,TYPES,B)),nl,fail. |
277 | | is_infinite_equality_closure(IDs, TYPES, Body) :- |
278 | ? | IDs = [_,_|_], % at least two variables |
279 | | %print(identify_eq(IDs)),nl, |
280 | ? | check_eq_body(Body,[],OutConstrained), |
281 | | %print(out(OutConstrained)),nl, |
282 | ? | (member(_ID/infinite,OutConstrained) -> true |
283 | | ; contains_infinite_type(IDs,TYPES,OutConstrained)). % , print(infinite(IDs)),nl. |
284 | | |
285 | | contains_infinite_type([ID|IT],[H|T],OutConstrained) :- |
286 | ? | ((is_infinite_type(H),\+ member(ID/_,OutConstrained)) |
287 | | -> true ; contains_infinite_type(IT,T,OutConstrained)). |
288 | | |
289 | | :- use_module(b_ast_cleanup,[definitely_not_empty_and_finite/1]). |
290 | | :- use_module(external_functions,[external_pred_always_true/1]). |
291 | ? | check_eq_body(b(B,pred,_),InConstrained,OutConstrained) :- check_eq_body_aux(B,InConstrained,OutConstrained). |
292 | ? | check_eq_body_aux(conjunct(A,B),InConstrained,OutConstrained) :- !, |
293 | ? | check_eq_body(A,InConstrained,OutConstrained1), |
294 | ? | check_eq_body(B,OutConstrained1,OutConstrained). |
295 | | check_eq_body_aux(equal(LHS,RHS), Constrained, [ID/equal|Constrained]) :- |
296 | | LHS=b(identifier(ID),_TYPE,_), |
297 | | \+ member(ID/_,Constrained), % no constraints on ID so far |
298 | | does_not_occur_in(ID,RHS),!. % the equation must have a solution; assuming well-definedness |
299 | | check_eq_body_aux(equal(LHS,RHS), Constrained, [ID/equal|Constrained]) :- % symmetric to case above |
300 | | RHS=b(identifier(ID),_TYPE,_), |
301 | | \+ member(ID/_,Constrained), |
302 | | does_not_occur_in(ID,LHS),!. |
303 | | check_eq_body_aux(member(b(identifier(ID),TYPE,_),SET),Constrained,[ID/INFINITE|Constrained]) :- |
304 | ? | \+ member(ID/_,Constrained), |
305 | | (is_infinite_type(TYPE) |
306 | | -> %check that SET is infinite; otherwise remove from IDs |
307 | | SET = b(S,set(TYPE),_), |
308 | | % print(check_infinite(S)),nl, |
309 | ? | (infinite_set(S) -> INFINITE=infinite; |
310 | | definitely_not_empty_and_finite(SET) -> INFINITE = finite) |
311 | | ; %print(finite(TYPE)),nl, |
312 | | b_ast_cleanup:definitely_not_empty_and_finite(SET), % otherwise we have no solution |
313 | | INFINITE = finite |
314 | | ). |
315 | | check_eq_body_aux(EXPR,Constrained,[ID/infinite|Constrained]) :- |
316 | | %% TO DO: store bounds in ID/... list ! |
317 | | greater_typing(EXPR,ID,_UP), |
318 | ? | \+ member(ID/_,Constrained). |
319 | | check_eq_body_aux(EXPR,Constrained,[ID/infinite|Constrained]) :- |
320 | | less_typing(EXPR,ID,_UP), |
321 | | \+ member(ID/_,Constrained). |
322 | | check_eq_body_aux(truth,Constrained,Constrained). |
323 | | check_eq_body_aux(external_pred_call(FunName,_Args),Constrained,Constrained) :- |
324 | | external_pred_always_true(FunName). |
325 | | |
326 | | |
327 | | :- use_module(bsyntaxtree,[occurs_in_expr/2]). |
328 | | does_not_occur_in(ID,EXPR) :- \+ occurs_in_expr(ID,EXPR). |
329 | | |
330 | | |
331 | | |
332 | | % check if we have a closure of type id(SetValue) |
333 | | |
334 | | is_id_closure_over([ID1,ID2], [TYPE,TYPE],Body, ID_Domain, Full) :- nonvar(Body), |
335 | | Body=b(equal(b(identifier(ID1),TYPE,_),b(identifier(ID2),TYPE,_)),pred,_), |
336 | | !, |
337 | | convert_type_to_value(TYPE,ID_Domain), Full=true. |
338 | | is_id_closure_over(Par,Types,Body,ID_Domain,Full) :- nonvar(Par),nonvar(Body), |
339 | | is_member_closure(Par,Types,Body,_,Set), % print(member_closure(Set)),nl, |
340 | | nonvar(Set), |
341 | | Set = identity(b(VAL,set(_TYPE),_)), |
342 | | nonvar(VAL), VAL=value(ID_Domain), |
343 | | (custom_explicit_sets:is_definitely_maximal_set(ID_Domain) -> Full=true ; Full=false). |
344 | | |
345 | | %:- use_module(kernel_objects,[all_strings/1]). |
346 | | convert_type_to_value(integer,global_set('INTEGER')). |
347 | | convert_type_to_value(global(G),global_set(G)). |
348 | | convert_type_to_value(boolean,BS) :- BS=[pred_true /* bool_true */,pred_false /* bool_false */]. % TO DO: generate AVL ? |
349 | | convert_type_to_value(string,global_set('STRING')). % :- all_strings(S). |
350 | | %convert_type_to_value(Type,closure([x],[Type],TRUTH)) :- ... TO DO |
351 | | |
352 | | |
353 | | |
354 | | /* Event-B id closure over full Type */ |
355 | | |
356 | | is_full_id_closure(P,T,B) :- is_id_closure_over(P,T,B,_,true). |
357 | | |
358 | | |
359 | | % currently commented out in is_special_infinite_closure |
360 | | %is_prj1_closure([ID1,_ID2,RESID],[Type1,Type2,Type1], |
361 | | % b(equal(b(identifier(RESID),Type1,_),b(identifier(ID1),Type1,_)),pred,_),Type1,Type2). |
362 | | %is_prj2_closure([_ID1,ID2,RESID],[Type1,Type2,Type2], |
363 | | % b(equal(b(identifier(RESID),Type2,_),b(identifier(ID2),Type2,_)),pred,_),Type1,Type2). |
364 | | |