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