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 :- module(kernel_tools,[
5 ground_value_check/2,
6 bexpr_variables/2,
7 ground_bexpr/1,
8 ground_bexpr_check/2,
9 value_variables/2,
10 ground_value/1,
11 ground_state_check/2, ground_state/1,
12 ground_typedvals_check/2,
13 %discard_ground_value_check/1,
14 %map_over_bvalue/3,
15 filter_cannot_match/4, get_template_for_filter_cannot_match/2,
16 cannot_match/2, can_match/2,
17 cannot_match_aggressive/2,
18 quick_same_value/2
19 ]).
20
21
22 :- use_module(module_information,[module_info/2]).
23 :- module_info(group,kernel).
24 :- module_info(description,'This module provides utilities for term variables for B expressions and values.').
25
26 :- use_module(self_check).
27 :- use_module(error_manager).
28 :- use_module(bsyntaxtree,[safe_syntaxelement/5]).
29
30 % use when ground value check no longer need to instantiate result variable:
31 % seems to have performance issues
32 %discard_ground_value_check(X) :- nonvar(X),!,
33 % (X==ground_value -> true ; print(illegal_ground_value_check(X)),nl).
34 %discard_ground_value_check(ground_value).
35
36 :- assert_must_succeed((kernel_tools:ground_value_check(int(X),V), var(V), X=1, nonvar(V))).
37 :- assert_must_succeed((kernel_tools:ground_value_check(string(X),V), var(V), X=a, nonvar(V))).
38 :- assert_must_succeed((kernel_tools:ground_value_check([int(1),int(X)],V), var(V), X=1, nonvar(V))).
39 % instantiate second argument to atomic-nonvar term if first argument ground B value
40 :- block ground_value_check(-,?).
41 ?ground_value_check([],R) :- !, R=ground_value.
42 ground_value_check(pred_true,R) :- !, R=ground_value.
43 ground_value_check(pred_false,R) :- !, R=ground_value.
44 ?ground_value_check(int(X),R) :- !, ground_atom(X,R).
45 ground_value_check(fd(X,_T),R) :- !,ground_atom(X,R). % avoid waking up co-routines with R=X.
46 ?ground_value_check(string(X),R) :- !, ground_atom(X,R).
47 ground_value_check((A,B),R) :- !, ground_value_check(A,GA), ground_value_check_aux(GA,B,R).
48 ?ground_value_check([H|T],R) :- !, ground_value_check(H,GA), ground_value_check_aux(GA,T,R).
49 ?ground_value_check(avl_set(_),R) :- !, % assume avl_set grounded
50 ? R = ground_value.
51 ground_value_check(rec(F),R) :- !, ground_fields(F,R).
52 ?ground_value_check(closure(_P,_T,B),R) :- !,
53 ? bexpr_variables(B,Vars),
54 ? ground_value_check(Vars,R).
55 %when(ground(Vars),R=ground_value).
56 ground_value_check(term(X),R) :- !, when(ground(X),R=ground_value).
57 ground_value_check(Val,R) :- %print(uncov(Val,R)),nl,trace,
58 ? (atomic(Val) -> R=ground_value ; when(ground(Val),R=ground_value)).
59
60 :- block ground_atom(-,?).
61 ground_atom(_,ground_value). %we could do a check ground_atom(X,R) :- (nonvar(R) -> nl,print(illegal_grval(X,R)),nl,nl ; R=X).
62 % we use this co-routine rather than direct unification to avoid unnecessarily waking up pending nonvar/ground checks
63 % indeed: if we unify X with another variable Y, this will wake up all when(nonvar(X) checks
64 % in test 1101 for prob_examples/examples/B/Systerel/C578.EML.014/612_001.mch this caused performance problems
65 % we woke up another pending co-routine with the same waitflag priority, it had a check when((nonvar(X);ground(WF1),
66 % WF1 was already ground: this meant we started evaluating another Prolog kernel call before finishing the current one
67
68 :- block ground_value_check_aux(-,?,?).
69 % :- block ground_value_check_aux(-,?,-). % this slows down test 884, 292, 293, 1456, 1737
70 %ground_value_check_aux(_,_,R) :- nonvar(R),!. % groundness check no longer needed
71 ?ground_value_check_aux(_,V,R) :- ground_value_check(V,R).
72
73 :- block ground_fields(-,?).
74 ground_fields([],R) :- !, R=ground_value.
75 ground_fields([field(F,V)|T],R) :- ground_fields_aux(F,V,T,R).
76
77 :- block ground_fields_aux(-,?,?,?).
78 ground_fields_aux(_,V,T,R) :- ground_fields(T,GrT), ground_value_check_aux(GrT,V,R).
79
80
81 :- block ground_state_check(-,?).
82 ground_state_check([],R) :- !, R=ground_value.
83 ground_state_check([bind(F,Val)|T],R) :- !, ground_state_check_aux(F,Val,T,R).
84 ground_state_check(BL,R) :- add_internal_error('Illegal bind list:',ground_state_check(BL,R)).
85
86 :- block ground_state_check_aux(-,?,?,?).
87 ground_state_check_aux(_,Val,T,R) :- ground_state_check(T,GrT), ground_value_check_aux(GrT,Val,R).
88
89
90 :- block ground_typedvals_check(-,?).
91 ground_typedvals_check([],R) :- !, R=ground_value.
92 ground_typedvals_check([typedval(Val,_Type,VarID,_EnumWarning)|T],R) :- !, ground_typedvals_check_aux(VarID,Val,T,R).
93 ground_typedvals_check(TL,R) :- add_internal_error('Illegal typedval list:',ground_typedvals_check(TL,R)).
94
95 :- block ground_typedvals_check_aux(-,?,?,?).
96 ground_typedvals_check_aux(_,Val,T,R) :- ground_typedvals_check(T,GrT), ground_value_check_aux(GrT,Val,R).
97
98
99 :- block ground_bexpr_check(-,?).
100 ground_bexpr_check(BExpr,R) :-
101 bexpr_variables(BExpr,Vars),
102 ground_value_check(Vars,R).
103
104 % -------------------------------
105
106
107 % attempt at a more efficient version of term_variables; avoiding traversing big avl_set's
108 %bexpr_variables(T,V) :- !, term_variables(T,V).
109 bexpr_variables(b(P,_,_),Vars) :-
110 bexpr_variables_aux(P,[],Vars), ! . %, print(vars(P,Vars)),nl.
111 bexpr_variables(T,V) :- add_internal_error('Illegal call: ',bexpr_variables(T,V)),
112 %trace, bexpr_variables(T,V),
113 term_variables(T,V).
114
115 % check if a B expression or predicate is ground
116 ground_bexpr(b(P,_,_)) :- !,
117 bexpr_variables_aux(P,[],[]).
118 ground_bexpr(T) :- add_internal_error('Illegal call: ',ground_bexpr(T)),
119 ground(T).
120
121 % get free variables inside a B value
122 value_variables(V,Vars) :- var(V),!, Vars=[V]. % optimize a few frequent cases
123 value_variables(avl_set(_),Vars) :- !, Vars=[].
124 value_variables([],Vars) :- !, Vars=[].
125 value_variables(Val,Vars) :- %print(val(Val)),nl,
126 value_variables(Val,[],Vars).
127
128 % check if a B value is ground
129 %version below seems a bit faster than ground_value(Val) :- value_variables(Val,[],[]).
130 ground_value(V) :- var(V),!,fail.
131 ground_value(pred_true) :- !.
132 ground_value(pred_false) :- !.
133 ground_value(int(N)) :- !, nonvar(N).
134 ground_value(global_set(N)) :- !, ground(N).
135 ground_value(freetype(N)) :- !, ground(N).
136 ground_value(string(S)) :- !, ground(S).
137 ground_value(fd(X,T)) :- !, nonvar(X),nonvar(T).
138 ground_value([]) :- !.
139 ground_value(avl_set(_)) :- !.
140 ground_value([H|T]) :- !, ground_value(H),ground_value(T).
141 ground_value((A,B)) :- !, ground_value(A),ground_value(B).
142 ground_value(freeval(ID,Case,Value)) :- !,
143 ground(ID), ground(Case), % necessary ?
144 ground_value(Value).
145 ground_value(rec(F)) :- !, record_variables(F,[],[]).
146 ground_value(closure(_P,_T,B)) :- !, ground_bexpr(B). %% DO WE NEED TO CHECK P ? Probably not
147 ground_value(term(T)) :- !, ground(T).
148 ground_value(T) :- functor(T,F,N), format('~n*** uncovered value ~w/~w~n',[F,N]),
149 ground(T).
150
151
152 % check if a B state is ground
153 ground_state(V) :- var(V),!,fail.
154 ground_state([]) :- !.
155 ground_state([bind(N,V)|T]) :- !, ground(N),
156 ground_value(V), ground_state(T).
157 ground_state(S) :- add_internal_error('Illegal state: ',ground_state(S)),fail.
158
159 :- use_module(library(aggregate),[term_variables/3]).
160
161 bexpr_variables(b(P,_,_)) --> bexpr_variables_aux(P).
162
163 value_variables(V) --> {var(V)},!,term_variables_atomic(V). % slightly unnecessary to do two var checks
164 value_variables(avl_set(_)) --> !,[].
165 value_variables((A,B)) --> !, value_variables(A),value_variables(B).
166 value_variables([H|T]) --> !, value_variables(H),value_variables(T).
167 value_variables(closure(_P,_T,B)) --> !, bexpr_variables(B). %% DO WE NEED TO CHECK P ? Probably not
168 value_variables(pred_false) --> !,[].
169 value_variables(pred_true) --> !,[].
170 value_variables(fd(X,T)) --> !, {check_nonvar(T)},term_variables_atomic(X).
171 value_variables([]) --> !,[].
172 value_variables(rec(F)) --> !, record_variables(F).
173 value_variables(freeval(ID,Case,Value)) --> !,
174 value_variables(ID), value_variables(Case), % necessary ?
175 value_variables(Value).
176 value_variables(string(S)) --> !,term_variables_atomic(S). % not sure this is useful
177 value_variables(int(I)) --> !,term_variables_atomic(I).
178 value_variables(global_set(S)) --> !, term_variables_atomic(S). % normally global_sets should always be ground
179 % TO DO: support freevals
180 value_variables(T) --> %{ functor(T,F,N), print(uncov_value_variables(F,N)),nl},
181 term_variables(T).
182
183 check_nonvar(T) :- (var(T) -> add_internal_error('Unexpected variable: ',T) ; true).
184
185 record_variables(V) --> {var(V)},!,term_variables(V).
186 record_variables([]) --> [].
187 record_variables([field(F,V)|T]) -->
188 term_variables_atomic(F), % is this necessary ?
189 value_variables(V), record_variables(T).
190
191 :- use_module(tools, [exact_member/2]).
192 % an optimized version of term_variables/3 which assumes argument is either var or ground
193 term_variables_atomic(VarOrGround,Vars,NewVars) :-
194 var(VarOrGround),
195 \+ exact_member(VarOrGround,Vars),
196 !,
197 NewVars = [VarOrGround|Vars].
198 term_variables_atomic(_,Vars,Vars).
199
200 bexpr_variables_aux(value(V)) --> !,value_variables(V).
201 % 0-ary
202 bexpr_variables_aux(boolean_false) --> !,[].
203 bexpr_variables_aux(boolean_true) --> !,[].
204 bexpr_variables_aux(bool_set) --> !,[].
205 bexpr_variables_aux(empty_set) --> !,[].
206 bexpr_variables_aux(empty_sequence) --> !,[].
207 bexpr_variables_aux(falsity) --> !,[].
208 bexpr_variables_aux(integer_set) --> !,[].
209 bexpr_variables_aux(max_int) --> !,[].
210 bexpr_variables_aux(min_int) --> !,[].
211 bexpr_variables_aux(string_set) --> !,[].
212 bexpr_variables_aux(truth) --> !,[].
213 %unary:
214 bexpr_variables_aux(card(A)) --> !, bexpr_variables(A).
215 bexpr_variables_aux(closure(A)) --> !, bexpr_variables(A).
216 %bexpr_variables_aux(closure1(A)) --> !, bexpr_variables(A).
217 bexpr_variables_aux(convert_bool(A)) --> !, bexpr_variables(A).
218 bexpr_variables_aux(domain(A)) --> !, bexpr_variables(A).
219 bexpr_variables_aux(identifier(_)) --> !,[].
220 bexpr_variables_aux(integer(_)) --> !,[].
221 bexpr_variables_aux(first(A)) --> !, bexpr_variables(A).
222 bexpr_variables_aux(last(A)) --> !, bexpr_variables(A).
223 bexpr_variables_aux(max(A)) --> !, bexpr_variables(A).
224 bexpr_variables_aux(min(A)) --> !, bexpr_variables(A).
225 bexpr_variables_aux(perm(A)) --> !, bexpr_variables(A).
226 bexpr_variables_aux(pow_subset(A)) --> !, bexpr_variables(A).
227 bexpr_variables_aux(pow1_subset(A)) --> !, bexpr_variables(A).
228 bexpr_variables_aux(range(A)) --> !, bexpr_variables(A).
229 bexpr_variables_aux(reflexive_closure(A)) --> !, bexpr_variables(A).
230 bexpr_variables_aux(rev(A)) --> !, bexpr_variables(A).
231 bexpr_variables_aux(reverse(A)) --> !, bexpr_variables(A).
232 bexpr_variables_aux(second_of_pair(A)) --> !, bexpr_variables(A).
233 bexpr_variables_aux(seq(A)) --> !, bexpr_variables(A).
234 bexpr_variables_aux(seq1(A)) --> !, bexpr_variables(A).
235 bexpr_variables_aux(size(A)) --> !, bexpr_variables(A).
236 bexpr_variables_aux(string(_)) --> !, [].
237 bexpr_variables_aux(unary_minus(A)) --> !, bexpr_variables(A).
238 % binary:
239 bexpr_variables_aux(add(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
240 bexpr_variables_aux(conjunct(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
241 bexpr_variables_aux(disjunct(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
242 bexpr_variables_aux(domain_restriction(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
243 bexpr_variables_aux(domain_subtraction(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
244 bexpr_variables_aux(cartesian_product(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
245 %bexpr_variables_aux(comprehension_set(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
246 bexpr_variables_aux(couple(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
247 bexpr_variables_aux(equal(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
248 bexpr_variables_aux(equivalence(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
249 bexpr_variables_aux(function(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
250 bexpr_variables_aux(greater_equal(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
251 bexpr_variables_aux(greater(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
252 bexpr_variables_aux(image(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
253 bexpr_variables_aux(implication(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
254 bexpr_variables_aux(insert_front(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
255 bexpr_variables_aux(insert_tail(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
256 bexpr_variables_aux(intersection(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
257 bexpr_variables_aux(interval(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
258 bexpr_variables_aux(lazy_lookup_expr(_)) --> !,[].
259 bexpr_variables_aux(lazy_lookup_pred(_)) --> !,[].
260 bexpr_variables_aux(less_equal(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
261 bexpr_variables_aux(less(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
262 bexpr_variables_aux(member(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
263 bexpr_variables_aux(minus(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
264 bexpr_variables_aux(modulo(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
265 bexpr_variables_aux(multiplication(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
266 bexpr_variables_aux(negation(A)) --> !, bexpr_variables(A).
267 bexpr_variables_aux(not_equal(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
268 bexpr_variables_aux(not_member(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
269 bexpr_variables_aux(not_subset(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
270 bexpr_variables_aux(not_subset_strict(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
271 bexpr_variables_aux(overwrite(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
272 bexpr_variables_aux(partial_function(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
273 bexpr_variables_aux(range_restriction(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
274 bexpr_variables_aux(range_subtraction(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
275 bexpr_variables_aux(record_field(A,_FieldName)) --> !, bexpr_variables(A).
276 bexpr_variables_aux(restrict_front(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
277 bexpr_variables_aux(restrict_tail(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
278 bexpr_variables_aux(set_subtraction(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
279 bexpr_variables_aux(subset(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
280 bexpr_variables_aux(subset_strict(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
281 bexpr_variables_aux(union(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
282 % ternary
283 bexpr_variables_aux(if_then_else(A,B,C)) --> !, bexpr_variables(A), bexpr_variables(B), bexpr_variables(C).
284 % with new local variables:
285 bexpr_variables_aux(comprehension_set(_Ids,A)) --> !, bexpr_variables(A).
286 bexpr_variables_aux(exists(_Ids,A)) --> !, bexpr_variables(A).
287 bexpr_variables_aux(event_b_comprehension_set(_Ids,A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
288 bexpr_variables_aux(forall(_Ids,A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
289 bexpr_variables_aux(lambda(_Ids,A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
290 bexpr_variables_aux(lazy_let_expr(_ID,A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
291 bexpr_variables_aux(lazy_let_pred(_ID,A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
292 bexpr_variables_aux(lazy_let_subst(_ID,A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
293 %bexpr_variables_aux(let_predicate(_Ids,E,A)) --> !, bexpr_variables(E), bexpr_variables(A).
294 %bexpr_variables_aux(let_expression(_Ids,E,A)) --> !, bexpr_variables(E), bexpr_variables(A).
295 bexpr_variables_aux(general_sum(_Ids,A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
296 bexpr_variables_aux(general_product(_Ids,A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
297 bexpr_variables_aux(quantified_union(_Ids,A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
298 bexpr_variables_aux(quantified_intersection(_Ids,A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
299 % with lists:
300 bexpr_variables_aux(sequence_extension(A)) --> !, l_bexpr_variables(A).
301 bexpr_variables_aux(set_extension(A)) --> !, l_bexpr_variables(A).
302 bexpr_variables_aux(struct(A)) --> !, bexpr_variables(A).
303 bexpr_variables_aux(tail(A)) --> !, bexpr_variables(A).
304 bexpr_variables_aux(total_function(A,B)) --> !, bexpr_variables(A), bexpr_variables(B).
305 bexpr_variables_aux(external_function_call(_FunName,A)) --> !, l_bexpr_variables(A).
306 bexpr_variables_aux(external_pred_call(_FunName,A)) --> !, l_bexpr_variables(A).
307 % general case (could be used for all above; but is considerably slower)
308 bexpr_variables_aux(Expr) -->
309 %{ functor(Expr,F,N), print(uncov_var_aux(F,N)),nl },
310 {bsyntaxtree:safe_syntaxelement(Expr,Subs,_Names,_List,_Constant)},
311 l_bexpr_variables(Subs).
312
313 l_bexpr_variables([]) --> [].
314 l_bexpr_variables([H|T]) --> bexpr_variables(H), l_bexpr_variables(T).
315
316
317
318
319 %:- use_module(custom_explicit_sets, [expand_custom_set_to_list_now/2]).
320 % dispatch. TODO: closure/3 and freetype
321 %:- meta_predicate map_over_bvalue(2,?,?).
322 %map_over_bvalue(_,[],[]) :- !.
323 %map_over_bvalue(Pred,[H|T],[Res|Tail]) :- !,
324 % map_over_bvalue(Pred,H,Res),
325 % map_over_bvalue(Pred,T,Tail).
326 %map_over_bvalue(Pred,(A,B),(ResA,ResB)) :- !,
327 % map_over_bvalue(Pred,A,ResA),
328 % map_over_bvalue(Pred,B,ResB).
329 %map_over_bvalue(Pred,rec(L),rec(Res)) :- !,
330 % map_over_bvalue(Pred,L,Res).
331 %map_over_bvalue(Pred,avl_set(A),Res) :- !,
332 % custom_explicit_sets:expand_custom_set_to_list_now(avl_set(A),L),
333 % map_over_bvalue(Pred,L,Res).
334 %map_over_bvalue(Pred,global_set(A), Res) :- !,
335 % custom_explicit_sets:expand_custom_set_to_list_now(global_set(A), L),
336 % map_over_bvalue(Pred,L,Res).
337 %map_over_bvalue(Pred,field(Name,Value),field(Name,TValue)) :- !,
338 % map_over_bvalue(Pred,Value,TValue).
339 %% apply
340 %map_over_bvalue(Pred,BValue,OutValue) :- !,
341 % call(Pred,BValue,OutValue).
342
343 % ----------------------------------
344 :- assert_must_succeed((kernel_tools:filter_cannot_match([int(X),int(11),Y],int(12),R,F), R==[int(X),Y],F==true)).
345
346 % filter out from the set Set (list part) all elements that cannot match X
347 % Filtered=true means at least one element was filtered out
348 filter_cannot_match(Set,X,NewSet,Filtered) :- instantiated_enough(X),!,
349 filter_cannot_match_aux(Set,X,NewSet,Filtered).
350 filter_cannot_match(S,_,S,false).
351
352 :- use_module(library(avl),[avl_domain/2, avl_height/2]).
353 :- use_module(custom_explicit_sets,[sorted_ground_normalised_list_to_avlset/3]).
354 :- use_module(performance_messages,[perfmessage/1]).
355 filter_cannot_match_aux(Var,_,Res,Filtered) :- var(Var),!,Res=Var,Filtered=false.
356 filter_cannot_match_aux([],_,Res,Filtered) :- !, Res=[],Filtered=false.
357 filter_cannot_match_aux([H|T],X,Res,Filtered) :- !,
358 (cannot_match(X,H) -> Filtered=true,filter_cannot_match_aux(T,X,Res,_)
359 ; Res=[H|RT], filter_cannot_match_aux(T,X,RT,Filtered)).
360 filter_cannot_match_aux(avl_set(Avl),X,R,Filtered) :- avl_height(Avl,H), %print(avl(H)),nl,
361 (H<8 -> true ; perfmessage(avl_set_not_filtered(H,X)),fail),
362 !,
363 avl_domain(Avl,List),
364 filter_cannot_match_aux(List,X,L2,Filtered),
365 (Filtered=true
366 -> sorted_ground_normalised_list_to_avlset(L2,R,filter_cannot_match_aux)
367 ; R=avl_set(Avl)).
368 filter_cannot_match_aux(S,_,S,false).
369
370 % does it make sense to filter Set, or will cannot_match always fail
371 instantiated_enough(V) :- var(V),!,fail.
372 instantiated_enough(pred_true) :- !.
373 instantiated_enough(pred_false) :- !.
374 instantiated_enough(int(X)) :- !, nonvar(X).
375 instantiated_enough(fd(X,T)) :- !, nonvar(X),nonvar(T).
376 instantiated_enough(string(X)) :- !, nonvar(X).
377 instantiated_enough((A,B)) :- instantiated_enough(A) -> true ; instantiated_enough(B).
378 instantiated_enough(rec(Fs)) :- (member(field(N,V),Fs),nonvar(N),instantiated_enough(V) -> true).
379 % TO DO: free-types, ...
380
381
382 %delay_filter_cannot_match(Set,X,NewSet) :-
383 % block_filter_cannot_match_aux(Set,X,NewSet).
384 %
385 %:- block block_filter_cannot_match_aux(-,?,?).
386 %block_filter_cannot_match_aux([],_,Res) :- !, Res=[].
387 %block_filter_cannot_match_aux([H|T],X,Res) :-
388 % (cannot_match(X,H) -> block_filter_cannot_match_aux(T,X,Res)
389 % ; Res=[H|RT], block_filter_cannot_match_aux(T,X,RT)).
390 %block_filter_cannot_match_aux(S,_,S).
391
392
393 % convert a typed expression into a value that can be used to filter a list of values with filter_cannot_match
394 get_template_for_filter_cannot_match(TExpr,ValueForFiltering) :- %print(getT(TExpr)),nl,
395 get_template_for_filter3(TExpr,ValueForFiltering,NonVar), nonvar(NonVar).
396 get_template_for_filter3(b(E,_,_),Val,NonVar) :-
397 get_template_for_filter_aux(E,Val,NonVar).
398 get_template_for_filter_aux(value(Val),Val,NonVar) :- !, (nonvar(Val) -> NonVar=nonvar ; true).
399 get_template_for_filter_aux(couple(A,B),(VA,VB),NonVar) :- !,
400 get_template_for_filter3(A,VA,NonVar),
401 get_template_for_filter3(B,VB,NonVar).
402 %get_template_for_filter_aux(identifier(_),_,_).
403 get_template_for_filter_aux(_,_,_).
404
405
406 :- assert_must_succeed((kernel_tools:can_match(int(1),_V))).
407 :- assert_must_fail((kernel_tools:cannot_match(int(1),_V))).
408 :- assert_must_succeed((kernel_tools:can_match(int(12),int(12)))).
409 :- assert_must_succeed((kernel_tools:cannot_match(int(1),int(2)))).
410 :- assert_must_succeed((kernel_tools:cannot_match(string(a),string(b)))).
411 :- assert_must_succeed((kernel_tools:can_match(string(a),string(a)))).
412 :- assert_must_succeed((kernel_tools:can_match(string(a),string(_)))).
413 :- assert_must_succeed((kernel_tools:can_match(string(_),string(b)))).
414 :- assert_must_succeed((kernel_tools:cannot_match([],[string(b)]))).
415 :- assert_must_succeed((kernel_tools:cannot_match([_],[]))).
416 :- assert_must_succeed((kernel_tools:cannot_match((int(11),string(a)),(int(11),string(b))))).
417 :- assert_must_succeed((kernel_tools:can_match((int(11),string(a)),(int(11),string(_))))).
418 :- assert_must_succeed((kernel_tools:cannot_match(pred_false,pred_true))).
419 :- assert_must_succeed((kernel_tools:can_match(pred_true,pred_true))).
420 :- assert_must_succeed((kernel_tools:can_match(record([field(a,pred_true)]),record([field(a,_)])))).
421 :- assert_must_succeed((kernel_tools:cannot_match(record([field(a,pred_false)]),record([field(a,pred_true)])))).
422
423 % can_match: quick check to see if the (AVL or List) element could match
424
425 can_match(A,B) :- \+ cannot_match(A,B).
426 cannot_match(A,B) :- \+ can_match_aux(A,B). % Note: probably better to wrap can_match into negation to avoid instantiations
427
428 :- use_module(clpfd_interface,[clpfd_can_match/2]).
429
430 can_match_aux(A,_) :- var(A),!. % TO DO: we could check for not_empty_set co-routine if A or B = []?
431 can_match_aux(_,B) :- var(B),!.
432 can_match_aux((A,B),(ElA,ElB)) :- !,can_match_aux(A,ElA), can_match_aux(B,ElB).
433 can_match_aux(int(A),R) :- !,
434 % (\+ ground(R) -> true,print(ok(int(A),R)),nl ; print(unify(R,int(A))),nl,R=int(A)). % unification could trigger other constraint propagations and be expensive; we could just check that A is in domain
435 (var(R) -> true
436 ; R=int(B), clpfd_can_match(A,B)). %,(B=A -> true ; print(ko(A,B)),nl,fail)).%,fail,trace,B=A)).
437 can_match_aux(fd(NrA,GS),R) :- !,
438 %(\+ ground(R) -> true ; R=fd(Nr,GS)). % ditto (see, e.g., test 985 - graph iso)
439 (var(R) -> true ; R=fd(NrB,GS), clpfd_can_match(NrA,NrB)).
440 can_match_aux(pred_false,R) :- !, R=pred_false.
441 can_match_aux(pred_true,R) :- !, R=pred_true.
442 can_match_aux(string(A),R) :- !, %(\+ ground(R) -> true ; R=string(A)). % may instantiate LHS
443 (var(R) -> true ; R=string(B), can_match_atomic(A,B)).
444 can_match_aux(term(A),R) :- !, %(\+ ground(R) -> true ; R=term(A)). % ditto
445 (var(R) -> true ; R=term(B), can_match_atomic(A,B)).
446 can_match_aux(freeval(ID,Case,Value),R) :- !,
447 (var(R) -> true
448 ; R=freeval(IDR,CaseR,VR),
449 (var(IDR) ; var(CaseR) -> true
450 ; (ID,Case)=(IDR,CaseR),
451 can_match_aux(Value,VR))).
452 can_match_aux([],R) :- !, R \= avl_set(node(_,_,_,_,_)), R\= [_|_].
453 can_match_aux(avl_set(A),R) :- !, can_match_avl_set(R,A).
454 can_match_aux(global_set(_),R) :- !, R \= []. % global sets must be non-empty; TO DO: maybe quick check in case global_set is infinite; TO DO: check if two global_sets are identical
455 can_match_aux([_|_],R) :- !, R \= [].
456 can_match_aux(record(Fields1),record(Fields2)) :- !,can_match_fields(Fields1,Fields2).
457 can_match_aux(_,_). % catch-all other types
458
459 can_match_fields(A,B) :- (var(A);var(B)),!.
460 can_match_fields([],[]).
461 can_match_fields([F1|T1],[F2|T2]) :- can_match_field(F1,F2), can_match_fields(T1,T2).
462
463 can_match_field(A,B) :- (var(A);var(B)),!.
464 can_match_field(field(F1,V1),field(F2,V2)) :- F1==F2,!, can_match_aux(V1,V2).
465 can_match_field(F1,F2) :- add_internal_error('Non-matching fields: ',can_match_field(F1,F2)).
466
467 :- use_module(kernel_dif,[frozen_dif/2]).
468 can_match_atomic(A,B) :- var(A),!, \+ frozen_dif(A,B).
469 can_match_atomic(A,B) :- var(B),!, \+ frozen_dif(B,A).
470 can_match_atomic(A,B) :- A=B.
471
472 :- use_module(library(avl),[avl_min/2, avl_max/2, avl_size/2]).
473
474 can_match_avl_set([],A) :- !, A=empty.
475 can_match_avl_set([H|T],A) :- !, list_can_match_avl_set([H|T],0,A).
476 can_match_avl_set(avl_set(B),A) :- !, avl_min(A,Min), avl_min(B,Min), avl_max(A,Max),avl_max(B,Max).
477 can_match_avl_set(_,_).
478
479 list_can_match_avl_set(T,_,_) :- var(T),!.
480 list_can_match_avl_set([],Sze,A) :- !, avl_size(A,Sze).
481 list_can_match_avl_set([H|T],Sze,A) :- !,
482 (custom_explicit_sets:quick_test_avl_membership(A,H,PredRes)
483 -> PredRes=pred_true, S1 is Sze+1,
484 list_can_match_avl_set(T,S1,A)
485 ; true). % TO DO: maybe also check T ?
486 list_can_match_avl_set(_,_,_).
487
488 % ------------------------
489
490 cannot_match_aggressive(A,B) :- \+ can_match_aggr(A,B).
491
492 % a more aggressive version; which may trigger co-routines for left-side A
493 can_match_aggr(A,_) :- var(A),!.
494 can_match_aggr(_,B) :- var(B),!.
495 can_match_aggr((A,B),(ElA,ElB)) :- !,can_match_aggr(A,ElA), can_match_aggr(B,ElB).
496 can_match_aggr(int(A),R) :- !, % R=int(A). % can trigger co-routines both sides; causes problem for 985
497 (var(R) -> true
498 ; R=int(B), (var(B) -> clpfd_can_match(A,B) ; A=B)). % only triggers co-routines for left side
499 can_match_aggr(fd(NrA,GS),R) :- !, % R=fd(Nr,GS). % ditto
500 (var(R) -> true
501 ; R=fd(NrB,GS), (var(NrB) -> clpfd_can_match(NrA,NrB) ; NrA=NrB)).
502 can_match_aggr(string(A),R) :- !, %R=string(A). % ditto
503 (var(R) -> true
504 ; R=string(B), (var(B) -> can_match_atomic(A,B) ; A=B)).
505 can_match_aggr(pred_false,R) :- !, R=pred_false.
506 can_match_aggr(pred_true,R) :- !, R=pred_true.
507 can_match_aggr(A,B) :- can_match_aux(A,B).
508
509
510 % ----------------------------------------
511
512
513
514 /* COMPARING TWO CLOSURES */
515
516
517
518
519 % a quick check, use instead of == to compare values
520 quick_same_value(V1,V2) :- var(V1),!,V1==V2.
521 quick_same_value(_,V2) :- var(V2),!,fail.
522 quick_same_value(closure(P,T,B1),closure(P,T,B2)) :- !, quick_same_texpr_body(B1,B2).
523 quick_same_value(V1,V2) :- V1==V2.
524
525
526 quick_same_texpr_body(b(E1,Type,_),b(E2,Type,_)) :- qsame_texpr2(E1,E2).
527
528 :- use_module(bsyntaxtree,[safe_syntaxelement/5]).
529 qsame_texpr2(value(V1),value(V2)) :- !,quick_same_value(V1,V2).
530 qsame_texpr2(E1,E2) :-
531 functor(E1,F,Arity),
532 functor(E2,F,Arity),
533 safe_syntaxelement(E1,Subs1,_Names1,_List1,Constant1),
534 safe_syntaxelement(E2,Subs2,_Names2,_List2,Constant2), Constant2==Constant1,
535 same_sub_expressions(Subs1,Subs2).
536
537 same_sub_expressions([],[]).
538 same_sub_expressions([H1|T1],[H2|T2]) :- quick_same_texpr_body(H1,H2),
539 same_sub_expressions(T1,T2).