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 :- module(kernel_tools,[
5 ground_value_check/2,
6 ground_value_opt_check/3, % version with an additional flag to discard check if no longer needed
7 bexpr_variables/2,
8 ground_bexpr/1,
9 ground_bexpr_check/2,
10 value_variables/2, value_variables/3,
11 ground_value/1,
12 ground_value_or_field/1,
13 ground_state_check/2, ground_state/1,
14 ground_typedvals_check/2,
15 %discard_ground_value_check/1,
16 %map_over_bvalue/3,
17 filter_cannot_match/4, get_template_for_filter_cannot_match/2,
18 cannot_match/2, can_match/2,
19 cannot_match_aggressive/2,
20 quick_same_value/2
21 ]).
22
23
24 :- use_module(module_information,[module_info/2]).
25 :- module_info(group,kernel).
26 :- module_info(description,'This module provides utilities for term variables for B expressions and values.').
27
28 :- use_module(self_check).
29 :- use_module(error_manager).
30 :- use_module(bsyntaxtree,[safe_syntaxelement_det/5]).
31
32 % use when ground value check no longer need to instantiate result variable:
33 % seems to have performance issues
34 %discard_ground_value_check(X) :- nonvar(X),!,
35 % (X==ground_value -> true ; print(illegal_ground_value_check(X)),nl).
36 %discard_ground_value_check(ground_value).
37
38 :- assert_must_succeed((kernel_tools:ground_value_check(int(X),V), var(V), X=1, nonvar(V))).
39 :- assert_must_succeed((kernel_tools:ground_value_check(string(X),V), var(V), X=a, nonvar(V))).
40 :- assert_must_succeed((kernel_tools:ground_value_check([int(1),int(X)],V), var(V), X=1, nonvar(V))).
41 % instantiate second argument to atomic-nonvar term if first argument ground B value
42 :- block ground_value_check(-,?).
43 ground_value_check([],R) :- !, R=ground_value.
44 ground_value_check(pred_true,R) :- !, R=ground_value.
45 ground_value_check(pred_false,R) :- !, R=ground_value.
46 ?ground_value_check(int(X),R) :- !, ground_atom(X,R).
47 ground_value_check(global_set(X),R) :- !, ground_atom(X,R).
48 ?ground_value_check(fd(X,_T),R) :- !,ground_atom(X,R). % avoid waking up co-routines with R=X.
49 ?ground_value_check(string(X),R) :- !, ground_atom(X,R).
50 ground_value_check((A,B),R) :- !, ground_value_check(A,GA), ground_value_check_aux(GA,B,R).
51 ?ground_value_check([H|T],R) :- !, ground_value_check(H,GA), ground_value_check_aux(GA,T,R).
52 ground_value_check(avl_set(A),R) :- !, % assume avl_set grounded
53 check_avl_set(A),
54 R = ground_value.
55 ground_value_check(rec(F),R) :- !, ground_fields(F,R).
56 ground_value_check(freeval(ID,Case,Val),R) :- !,
57 ground_freeval_check(ID,Case,Val,R).
58 ground_value_check(closure(_P,_T,B),R) :- !,
59 bexpr_variables(B,Vars),
60 ground_value_check(Vars,R).
61 %when(ground(Vars),R=ground_value).
62 ground_value_check(term(X),R) :- !, ground_term(X,R).
63 ground_value_check(Val,R) :- %print(uncov(Val,R)),nl,trace,
64 (atomic(Val) -> R=ground_value ; when(ground(Val),R=ground_value)).
65
66 :- block ground_term(-,?).
67 ground_term(floating(F),R) :- !, ground_atom(F,R).
68 ground_term(Term,R) :- when(ground(Term),R=ground_value).
69
70 :- block ground_atom(-,?).
71 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).
72 % we use this co-routine rather than direct unification to avoid unnecessarily waking up pending nonvar/ground checks
73 % indeed: if we unify X with another variable Y, this will wake up all when(nonvar(X) checks
74 % in test 1101 for prob_examples/examples/B/Systerel/C578.EML.014/612_001.mch this caused performance problems
75 % we woke up another pending co-routine with the same waitflag priority, it had a check when((nonvar(X);ground(WF1),
76 % WF1 was already ground: this meant we started evaluating another Prolog kernel call before finishing the current one
77
78 :- block ground_value_check_aux(-,?,?).
79 % :- block ground_value_check_aux(-,?,-). % this slows down test 884, 292, 293, 1456, 1737
80 %ground_value_check_aux(_,_,R) :- nonvar(R),!. % groundness check no longer needed
81 ?ground_value_check_aux(_,V,R) :- ground_value_check(V,R).
82
83 :- block ground_fields(-,?).
84 ground_fields([],R) :- !, R=ground_value.
85 ground_fields([field(F,V)|T],R) :- ground_fields_aux(F,V,T,R).
86
87 :- block ground_fields_aux(-,?,?,?).
88 ground_fields_aux(_,V,T,R) :- ground_fields(T,GrT), ground_value_check_aux(GrT,V,R).
89
90 :- block ground_freeval_check(-,?,?,?), ground_freeval_check(?,-,?,?).
91 ground_freeval_check(_ID,_,Val,R) :-
92 % Note: for polymorphic types the ID can contain type variables, but should be ground
93 ground_value_check(Val,R).
94 % -------------------------------
95
96 :- block ground_state_check(-,?).
97 ground_state_check([],R) :- !, R=ground_value.
98 ground_state_check([bind(F,Val)|T],R) :- !, ground_state_check_aux(F,Val,T,R).
99 ground_state_check(BL,R) :- add_internal_error('Illegal bind list:',ground_state_check(BL,R)).
100
101 :- block ground_state_check_aux(-,?,?,?).
102 ground_state_check_aux(_,Val,T,R) :- ground_state_check(T,GrT), ground_value_check_aux(GrT,Val,R).
103
104
105 :- block ground_typedvals_check(-,?).
106 ground_typedvals_check([],R) :- !, R=ground_value.
107 ground_typedvals_check([typedval(Val,_Type,VarID,_EnumWarning)|T],R) :- !, ground_typedvals_check_aux(VarID,Val,T,R).
108 ground_typedvals_check(TL,R) :- add_internal_error('Illegal typedval list:',ground_typedvals_check(TL,R)).
109
110 :- block ground_typedvals_check_aux(-,?,?,?).
111 ground_typedvals_check_aux(_,Val,T,R) :- ground_typedvals_check(T,GrT), ground_value_check_aux(GrT,Val,R).
112
113
114 :- block ground_bexpr_check(-,?).
115 ground_bexpr_check(BExpr,R) :-
116 bexpr_variables(BExpr,Vars),
117 ground_value_check(Vars,R).
118
119 % -------------------------------
120
121
122 % attempt at a more efficient version of term_variables; avoiding traversing big avl_set's
123 %bexpr_variables(T,V) :- !, term_variables(T,V).
124 bexpr_variables(b(P,_,_),Vars) :-
125 bexpr_variables_aux(P,[],Vars), !.
126 bexpr_variables(T,V) :- var(V),
127 add_internal_error('Computation of vars failed: ',bexpr_variables(T,V)),
128 term_variables(T,V).
129
130 % check if a B expression or predicate is ground
131 ground_bexpr(b(P,_,_)) :- !,
132 bexpr_variables_aux(P,[],[]).
133 ground_bexpr(T) :- add_internal_error('Illegal call: ',ground_bexpr(T)),
134 ground(T).
135
136 % get free variables inside a B value
137 value_variables(V,Vars) :- var(V),!, Vars=[V]. % optimize a few frequent cases
138 value_variables(avl_set(A),Vars) :- !, check_avl_set(A),Vars=[].
139 value_variables([],Vars) :- !, Vars=[].
140 value_variables(Val,Vars) :-
141 value_variables(Val,[],Vars).
142
143 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
144
145 % check if a B value is ground
146 %version below seems a bit faster than ground_value(Val) :- value_variables(Val,[],[]).
147
148 :- if(environ(prob_safe_mode,true)).
149 ground_value(Val) :- ground_value1(Val),!,
150 (ground(Val) -> true
151 ; add_internal_error('Value incorrectly marked as ground by:',ground_val(Val)),fail).
152 ground_value(Val) :- ground(Val), !,add_internal_error('Value incorrectly marked as non-ground:',ground_val(Val)).
153 :- else.
154 ground_value(Val) :-ground_value1(Val).
155 :- endif.
156
157 ground_value1(V) :- var(V),!,fail.
158 ground_value1(pred_true) :- !.
159 ground_value1(pred_false) :- !.
160 ground_value1(int(N)) :- !, nonvar(N).
161 ground_value1(global_set(N)) :- !, ground(N).
162 ground_value1(freetype(N)) :- !, ground(N).
163 ground_value1(string(S)) :- !, ground(S).
164 ground_value1(fd(X,T)) :- !, nonvar(X),nonvar(T).
165 ground_value1([]) :- !.
166 ground_value1(avl_set(A)) :- !,check_avl_set(A).
167 ground_value1([H|T]) :- !, ground_value1(H),ground_value1(T).
168 ground_value1((A,B)) :- !, ground_value1(A),ground_value1(B).
169 ground_value1(freeval(ID,Case,Value)) :- !,
170 ground(ID),
171 ground(Case), % Case can be non-ground, ID should be nonvar, but could contain type variables!
172 ground_value1(Value).
173 ground_value1(rec(F)) :- !, ground_fields(F).
174 ground_value1(closure(_P,_T,B)) :- !, ground_bexpr(B). %% DO WE NEED TO CHECK P ? Probably not
175 ground_value1(term(T)) :- !, ground(T).
176 ground_value1(T) :- functor(T,F,N), format('~n*** uncovered term in ground_value ~w/~w~n',[F,N]),
177 ground(T).
178
179 ground_fields(V) :- var(V),!,fail.
180 ground_fields([]).
181 ground_fields([field(Name,Val)|T]) :- ground(Name), ground_value1(Val), ground_fields(T).
182
183 % a version of ground_value that also accepts record fields and lists of record fields without printing warnings
184 ground_value_or_field(V) :- var(V),!,fail.
185 ground_value_or_field(field(F,Value)) :- !, ground(F), ground_value(Value).
186 ground_value_or_field([H|T]) :- !, ground_value_or_field(H),ground_value_or_field(T).
187 ground_value_or_field(V) :- ground_value(V).
188
189 % check if a B state is ground
190 ground_state(V) :- var(V),!,fail.
191 ground_state([]) :- !.
192 ground_state([bind(N,V)|T]) :- !, ground(N),
193 ground_value(V), ground_state(T).
194 ground_state(S) :- add_internal_error('Illegal state: ',ground_state(S)),fail.
195
196 :- use_module(library(aggregate),[term_variables/3]).
197
198 bexpr_variables(b(P,_,_)) --> bexpr_variables_aux(P).
199 % following clause not really needed !?, bexpr_variables_bin/l_bexpr_variables perform propagation
200 %bexpr_variables(b(P,_,_),In,Out) :-
201 % (Out==[] -> In=[] ; true), % useful to propagate empty set to output for ground_bexpr checks
202 % bexpr_variables_aux(P,In,Out).
203
204 value_variables(V) --> {var(V)},!,term_variables_atomic(V). % slightly unnecessary to do two var checks
205 value_variables(avl_set(A)) --> !,{check_avl_set(A)},[].
206 value_variables((A,B)) --> !, value_variables(A),value_variables(B).
207 value_variables([H|T]) --> !, value_variables(H),value_variables(T).
208 value_variables(closure(_P,_T,B)) --> !, bexpr_variables(B). %% DO WE NEED TO CHECK P ? Probably not
209 value_variables(pred_false) --> !,[].
210 value_variables(pred_true) --> !,[].
211 value_variables(fd(X,T)) --> !, {check_nonvar(T)},term_variables_atomic(X).
212 value_variables([]) --> !,[].
213 value_variables(rec(F)) --> !, record_variables(F).
214 value_variables(freeval(ID,Case,Value)) --> !,
215 value_variables(ID),
216 value_variables(Case), % Case can be a variable
217 value_variables(Value).
218 value_variables(string(S)) --> !,term_variables_atomic(S). % not sure this is useful
219 value_variables(int(I)) --> !,term_variables_atomic(I).
220 value_variables(global_set(S)) --> !, term_variables_atomic(S). % normally global_sets should always be ground
221 value_variables(T) --> %{ functor(T,F,N), print(uncov_value_variables(F,N)),nl},
222 term_variables(T).
223
224 check_nonvar(T) :- (var(T) -> add_internal_error('Unexpected variable: ',T) ; true).
225
226 record_variables(V) --> {var(V)},!,term_variables(V).
227 record_variables([]) --> [].
228 record_variables([field(F,V)|T]) -->
229 term_variables_atomic(F), % is this necessary ?
230 value_variables(V), record_variables(T).
231
232 :- use_module(tools, [exact_member/2]).
233 % an optimized version of term_variables/3 which assumes argument is either var or ground
234 term_variables_atomic(VarOrGround,Vars,NewVars) :-
235 var(VarOrGround),
236 \+ exact_member(VarOrGround,Vars),
237 !,
238 NewVars = [VarOrGround|Vars].
239 term_variables_atomic(_,Vars,Vars).
240
241 %bexpr_variables_aux(value(V)) --> !,value_variables(V).
242 bexpr_variables_aux(value(V),In,Out) :- !,
243 (Out==[] -> In=[], ground_value(V) % avoid collecting variables after first variable found, useful for ground_bexpr
244 ; value_variables(V,In,Out)).
245 % 0-ary
246 bexpr_variables_aux(boolean_false) --> !,[].
247 bexpr_variables_aux(boolean_true) --> !,[].
248 bexpr_variables_aux(bool_set) --> !,[].
249 bexpr_variables_aux(empty_set) --> !,[].
250 bexpr_variables_aux(empty_sequence) --> !,[].
251 bexpr_variables_aux(falsity) --> !,[].
252 bexpr_variables_aux(max_int) --> !,[].
253 bexpr_variables_aux(min_int) --> !,[].
254 bexpr_variables_aux(float_set) --> !,[].
255 bexpr_variables_aux(real_set) --> !,[].
256 bexpr_variables_aux(string_set) --> !,[].
257 bexpr_variables_aux(truth) --> !,[].
258 %unary:
259 bexpr_variables_aux(card(A)) --> !, bexpr_variables(A).
260 bexpr_variables_aux(closure(A)) --> !, bexpr_variables(A).
261 %bexpr_variables_aux(closure1(A)) --> !, bexpr_variables(A).
262 bexpr_variables_aux(convert_bool(A)) --> !, bexpr_variables(A).
263 bexpr_variables_aux(convert_real(A)) --> !, bexpr_variables(A).
264 bexpr_variables_aux(convert_int_floor(A)) --> !, bexpr_variables(A).
265 bexpr_variables_aux(convert_int_ceiling(A)) --> !, bexpr_variables(A).
266 bexpr_variables_aux(domain(A)) --> !, bexpr_variables(A).
267 bexpr_variables_aux(identifier(_)) --> !,[].
268 bexpr_variables_aux(integer(_)) --> !,[].
269 bexpr_variables_aux(integer_set(_)) --> !,[].
270 bexpr_variables_aux(first(A)) --> !, bexpr_variables(A).
271 bexpr_variables_aux(first_of_pair(A)) --> !, bexpr_variables(A).
272 bexpr_variables_aux(last(A)) --> !, bexpr_variables(A).
273 bexpr_variables_aux(max(A)) --> !, bexpr_variables(A).
274 bexpr_variables_aux(min(A)) --> !, bexpr_variables(A).
275 bexpr_variables_aux(perm(A)) --> !, bexpr_variables(A).
276 bexpr_variables_aux(pow_subset(A)) --> !, bexpr_variables(A).
277 bexpr_variables_aux(pow1_subset(A)) --> !, bexpr_variables(A).
278 bexpr_variables_aux(range(A)) --> !, bexpr_variables(A).
279 bexpr_variables_aux(real(_)) --> !,[].
280 bexpr_variables_aux(reflexive_closure(A)) --> !, bexpr_variables(A).
281 bexpr_variables_aux(rev(A)) --> !, bexpr_variables(A).
282 bexpr_variables_aux(reverse(A)) --> !, bexpr_variables(A).
283 bexpr_variables_aux(second_of_pair(A)) --> !, bexpr_variables(A).
284 bexpr_variables_aux(seq(A)) --> !, bexpr_variables(A).
285 bexpr_variables_aux(seq1(A)) --> !, bexpr_variables(A).
286 bexpr_variables_aux(size(A)) --> !, bexpr_variables(A).
287 bexpr_variables_aux(string(_)) --> !, [].
288 bexpr_variables_aux(unary_minus(A)) --> !, bexpr_variables(A).
289 bexpr_variables_aux(unary_minus_real(A)) --> !, bexpr_variables(A).
290 % binary:
291 bexpr_variables_aux(add(A,B)) --> !, bexpr_variables_bin(A,B).
292 bexpr_variables_aux(add_real(A,B)) --> !, bexpr_variables_bin(A,B).
293 bexpr_variables_aux(conjunct(A,B)) --> !, bexpr_variables_bin(A,B).
294 bexpr_variables_aux(disjunct(A,B)) --> !, bexpr_variables_bin(A,B).
295 bexpr_variables_aux(div(A,B)) --> !, bexpr_variables_bin(A,B).
296 bexpr_variables_aux(div_real(A,B)) --> !, bexpr_variables_bin(A,B).
297 bexpr_variables_aux(domain_restriction(A,B)) --> !, bexpr_variables_bin(A,B).
298 bexpr_variables_aux(domain_subtraction(A,B)) --> !, bexpr_variables_bin(A,B).
299 bexpr_variables_aux(cartesian_product(A,B)) --> !, bexpr_variables_bin(A,B).
300 %bexpr_variables_aux(comprehension_set(A,B)) --> !, bexpr_variables_bin(A,B).
301 bexpr_variables_aux(couple(A,B)) --> !, bexpr_variables_bin(A,B).
302 bexpr_variables_aux(equal(A,B)) --> !, bexpr_variables_bin(A,B).
303 bexpr_variables_aux(equivalence(A,B)) --> !, bexpr_variables_bin(A,B).
304 bexpr_variables_aux(function(A,B)) --> !, bexpr_variables_bin(A,B).
305 bexpr_variables_aux(greater_equal(A,B)) --> !, bexpr_variables_bin(A,B).
306 bexpr_variables_aux(greater(A,B)) --> !, bexpr_variables_bin(A,B).
307 bexpr_variables_aux(image(A,B)) --> !, bexpr_variables_bin(A,B).
308 bexpr_variables_aux(implication(A,B)) --> !, bexpr_variables_bin(A,B).
309 bexpr_variables_aux(insert_front(A,B)) --> !, bexpr_variables_bin(A,B).
310 bexpr_variables_aux(insert_tail(A,B)) --> !, bexpr_variables_bin(A,B).
311 bexpr_variables_aux(intersection(A,B)) --> !, bexpr_variables_bin(A,B).
312 bexpr_variables_aux(interval(A,B)) --> !, bexpr_variables_bin(A,B).
313 bexpr_variables_aux(lazy_lookup_expr(_)) --> !,[].
314 bexpr_variables_aux(lazy_lookup_pred(_)) --> !,[].
315 bexpr_variables_aux(less_equal(A,B)) --> !, bexpr_variables_bin(A,B).
316 bexpr_variables_aux(less(A,B)) --> !, bexpr_variables_bin(A,B).
317 bexpr_variables_aux(less_equal_real(A,B)) --> !, bexpr_variables_bin(A,B).
318 bexpr_variables_aux(less_real(A,B)) --> !, bexpr_variables_bin(A,B).
319 bexpr_variables_aux(member(A,B)) --> !, bexpr_variables_bin(A,B).
320 bexpr_variables_aux(minus(A,B)) --> !, bexpr_variables_bin(A,B).
321 bexpr_variables_aux(minus_real(A,B)) --> !, bexpr_variables_bin(A,B).
322 bexpr_variables_aux(modulo(A,B)) --> !, bexpr_variables_bin(A,B).
323 bexpr_variables_aux(multiplication(A,B)) --> !, bexpr_variables_bin(A,B).
324 bexpr_variables_aux(multiplication_real(A,B)) --> !, bexpr_variables_bin(A,B).
325 bexpr_variables_aux(negation(A)) --> !, bexpr_variables(A).
326 bexpr_variables_aux(not_equal(A,B)) --> !, bexpr_variables_bin(A,B).
327 bexpr_variables_aux(not_member(A,B)) --> !, bexpr_variables_bin(A,B).
328 bexpr_variables_aux(not_subset(A,B)) --> !, bexpr_variables_bin(A,B).
329 bexpr_variables_aux(not_subset_strict(A,B)) --> !, bexpr_variables_bin(A,B).
330 bexpr_variables_aux(overwrite(A,B)) --> !, bexpr_variables_bin(A,B).
331 bexpr_variables_aux(partial_function(A,B)) --> !, bexpr_variables_bin(A,B).
332 bexpr_variables_aux(partition(A,BL)) --> !, bexpr_variables(A), l_bexpr_variables(BL).
333 bexpr_variables_aux(range_restriction(A,B)) --> !, bexpr_variables_bin(A,B).
334 bexpr_variables_aux(range_subtraction(A,B)) --> !, bexpr_variables_bin(A,B).
335 bexpr_variables_aux(record_field(A,_FieldName)) --> !, bexpr_variables(A).
336 bexpr_variables_aux(restrict_front(A,B)) --> !, bexpr_variables_bin(A,B).
337 bexpr_variables_aux(restrict_tail(A,B)) --> !, bexpr_variables_bin(A,B).
338 bexpr_variables_aux(set_subtraction(A,B)) --> !, bexpr_variables_bin(A,B).
339 bexpr_variables_aux(subset(A,B)) --> !, bexpr_variables_bin(A,B).
340 bexpr_variables_aux(subset_strict(A,B)) --> !, bexpr_variables_bin(A,B).
341 bexpr_variables_aux(union(A,B)) --> !, bexpr_variables_bin(A,B).
342 % ternary
343 bexpr_variables_aux(if_then_else(A,B,C)) --> !, l_bexpr_variables([A,B,C]).
344 % with new local variables:
345 bexpr_variables_aux(comprehension_set(_Ids,A)) --> !, bexpr_variables(A).
346 bexpr_variables_aux(exists(_Ids,A)) --> !, bexpr_variables(A).
347 bexpr_variables_aux(event_b_comprehension_set(_Ids,A,B)) --> !, bexpr_variables_bin(A,B).
348 bexpr_variables_aux(forall(_Ids,A,B)) --> !, bexpr_variables_bin(A,B).
349 bexpr_variables_aux(lambda(_Ids,A,B)) --> !, bexpr_variables_bin(A,B).
350 bexpr_variables_aux(lazy_let_expr(_ID,A,B)) --> !, bexpr_variables_bin(A,B).
351 bexpr_variables_aux(lazy_let_pred(_ID,A,B)) --> !, bexpr_variables_bin(A,B).
352 bexpr_variables_aux(lazy_let_subst(_ID,A,B)) --> !, bexpr_variables_bin(A,B).
353 %bexpr_variables_aux(let_predicate(_Ids,E,A)) --> !, bexpr_variables(E), bexpr_variables(A).
354 %bexpr_variables_aux(let_expression(_Ids,E,A)) --> !, bexpr_variables(E), bexpr_variables(A).
355 bexpr_variables_aux(general_sum(_Ids,A,B)) --> !, bexpr_variables_bin(A,B).
356 bexpr_variables_aux(general_product(_Ids,A,B)) --> !, bexpr_variables_bin(A,B).
357 bexpr_variables_aux(quantified_union(_Ids,A,B)) --> !, bexpr_variables_bin(A,B).
358 bexpr_variables_aux(quantified_intersection(_Ids,A,B)) --> !, bexpr_variables_bin(A,B).
359 % with lists:
360 bexpr_variables_aux(sequence_extension(A)) --> !, l_bexpr_variables(A).
361 bexpr_variables_aux(set_extension(A)) --> !, l_bexpr_variables(A).
362 bexpr_variables_aux(struct(A)) --> !, bexpr_variables(A).
363 bexpr_variables_aux(tail(A)) --> !, bexpr_variables(A).
364 bexpr_variables_aux(total_function(A,B)) --> !, bexpr_variables_bin(A,B).
365 bexpr_variables_aux(external_function_call(_FunName,A)) --> !, l_bexpr_variables(A).
366 bexpr_variables_aux(external_pred_call(_FunName,A)) --> !, l_bexpr_variables(A).
367 % TODO: rec(Fields)
368 % general case (could be used for all above; but is considerably slower)
369 bexpr_variables_aux(Expr) -->
370 %{ functor(Expr,F,N), print(uncov_var_aux(F,N)),nl },
371 {safe_syntaxelement_det(Expr,Subs,_Names,_List,_Constant)},
372 l_bexpr_variables(Subs).
373
374 bexpr_variables_bin(A,B,In,Out) :-
375 (Out==[] -> In=[],Int=[] ; true), % propagate for ground_bexpr use case where Out is []
376 bexpr_variables(A,In,Int), bexpr_variables(B,Int,Out).
377
378 l_bexpr_variables([]) --> [].
379 %l_bexpr_variables([H]) --> !, bexpr_variables(H). % propagate empty result list for ground_bexpr
380 l_bexpr_variables([H|T],In,Out) :-
381 (Out==[] -> In=[], Int=[] ; true), % propagate for ground_bexpr use case where Out is []
382 bexpr_variables(H,In,Int), l_bexpr_variables(T,Int,Out).
383
384
385
386
387 %:- use_module(custom_explicit_sets, [expand_custom_set_to_list_now/2]).
388 % dispatch. TODO: closure/3 and freetype
389 %:- meta_predicate map_over_bvalue(2,?,?).
390 %map_over_bvalue(_,[],[]) :- !.
391 %map_over_bvalue(Pred,[H|T],[Res|Tail]) :- !,
392 % map_over_bvalue(Pred,H,Res),
393 % map_over_bvalue(Pred,T,Tail).
394 %map_over_bvalue(Pred,(A,B),(ResA,ResB)) :- !,
395 % map_over_bvalue(Pred,A,ResA),
396 % map_over_bvalue(Pred,B,ResB).
397 %map_over_bvalue(Pred,rec(L),rec(Res)) :- !,
398 % map_over_bvalue(Pred,L,Res).
399 %map_over_bvalue(Pred,avl_set(A),Res) :- !,
400 % custom_explicit_sets:expand_custom_set_to_list_now(avl_set(A),L),
401 % map_over_bvalue(Pred,L,Res).
402 %map_over_bvalue(Pred,global_set(A), Res) :- !,
403 % custom_explicit_sets:expand_custom_set_to_list_now(global_set(A), L),
404 % map_over_bvalue(Pred,L,Res).
405 %map_over_bvalue(Pred,field(Name,Value),field(Name,TValue)) :- !,
406 % map_over_bvalue(Pred,Value,TValue).
407 %% apply
408 %map_over_bvalue(Pred,BValue,OutValue) :- !,
409 % call(Pred,BValue,OutValue).
410
411 % ----------------------------------
412 :- assert_must_succeed((kernel_tools:filter_cannot_match([int(X),int(11),Y],int(12),R,F), R==[int(X),Y],F==true)).
413
414 % filter out from the set Set (list part) all elements that cannot match X
415 % Filtered=true means at least one element was filtered out
416 filter_cannot_match(Set,X,NewSet,Filtered) :- instantiated_enough(X),!,
417 filter_cannot_match_aux(Set,X,NewSet,Filtered).
418 filter_cannot_match(S,_,S,false).
419
420 :- use_module(library(avl),[avl_domain/2, avl_height/2]).
421 :- use_module(custom_explicit_sets,[sorted_ground_normalised_list_to_avlset/3]).
422 :- use_module(performance_messages,[cond_perfmessage/2]).
423 filter_cannot_match_aux(Var,_,Res,Filtered) :- var(Var),!,Res=Var,Filtered=false.
424 filter_cannot_match_aux([],_,Res,Filtered) :- !, Res=[],Filtered=false.
425 filter_cannot_match_aux([H|T],X,Res,Filtered) :- !,
426 (cannot_match(X,H) -> Filtered=true,filter_cannot_match_aux(T,X,Res,_)
427 ; Res=[H|RT], filter_cannot_match_aux(T,X,RT,Filtered)).
428 filter_cannot_match_aux(avl_set(Avl),X,R,Filtered) :- check_avl_set(Avl),
429 avl_height(Avl,H),
430 (H<8 -> true % TODO: we could add Solver Strength here
431 ; cond_perfmessage([data_validation_mode/false],avl_set_not_filtered(H,X)),fail),
432 !,
433 avl_domain(Avl,List),
434 filter_cannot_match_aux(List,X,L2,Filtered),
435 (Filtered=true
436 -> sorted_ground_normalised_list_to_avlset(L2,R,filter_cannot_match_aux)
437 ; R=avl_set(Avl)).
438 filter_cannot_match_aux(S,_,S,false).
439
440 :- use_module(probsrc(tools_lists),[member_nonvar_list/2]).
441 % does it make sense to filter Set, or will cannot_match always fail
442 instantiated_enough(V) :- var(V),!,fail.
443 instantiated_enough(pred_true) :- !.
444 instantiated_enough(pred_false) :- !.
445 instantiated_enough(int(X)) :- !, nonvar(X).
446 instantiated_enough(fd(X,T)) :- !, nonvar(X),nonvar(T).
447 instantiated_enough(string(X)) :- !, nonvar(X).
448 instantiated_enough((A,B)) :- instantiated_enough(A) -> true ; instantiated_enough(B).
449 instantiated_enough(rec(Fs)) :- (member_nonvar_list(field(N,V),Fs),nonvar(N),instantiated_enough(V) -> true).
450 % TO DO: free-types, ...
451
452
453 %delay_filter_cannot_match(Set,X,NewSet) :-
454 % block_filter_cannot_match_aux(Set,X,NewSet).
455 %
456 %:- block block_filter_cannot_match_aux(-,?,?).
457 %block_filter_cannot_match_aux([],_,Res) :- !, Res=[].
458 %block_filter_cannot_match_aux([H|T],X,Res) :-
459 % (cannot_match(X,H) -> block_filter_cannot_match_aux(T,X,Res)
460 % ; Res=[H|RT], block_filter_cannot_match_aux(T,X,RT)).
461 %block_filter_cannot_match_aux(S,_,S).
462
463
464 % convert a typed expression into a value that can be used to filter a list of values with filter_cannot_match
465 get_template_for_filter_cannot_match(TExpr,ValueForFiltering) :-
466 get_template_for_filter3(TExpr,ValueForFiltering,NonVar), nonvar(NonVar).
467 get_template_for_filter3(b(E,_,_),Val,NonVar) :-
468 get_template_for_filter_aux(E,Val,NonVar).
469 get_template_for_filter_aux(value(Val),Val,NonVar) :- !, (nonvar(Val) -> NonVar=nonvar ; true).
470 get_template_for_filter_aux(couple(A,B),(VA,VB),NonVar) :- !,
471 get_template_for_filter3(A,VA,NonVar),
472 get_template_for_filter3(B,VB,NonVar).
473 %get_template_for_filter_aux(identifier(_),_,_).
474 get_template_for_filter_aux(_,_,_).
475
476
477 :- assert_must_succeed((kernel_tools:can_match(int(1),_V))).
478 :- assert_must_fail((kernel_tools:cannot_match(int(1),_V))).
479 :- assert_must_succeed((kernel_tools:can_match(int(12),int(12)))).
480 :- assert_must_succeed((kernel_tools:cannot_match(int(1),int(2)))).
481 :- assert_must_succeed((kernel_tools:cannot_match(string(a),string(b)))).
482 :- assert_must_succeed((kernel_tools:can_match(string(a),string(a)))).
483 :- assert_must_succeed((kernel_tools:can_match(string(a),string(_)))).
484 :- assert_must_succeed((kernel_tools:can_match(string(_),string(b)))).
485 :- assert_must_succeed((kernel_tools:cannot_match([],[string(b)]))).
486 :- assert_must_succeed((kernel_tools:cannot_match([_],[]))).
487 :- assert_must_succeed((kernel_tools:cannot_match((int(11),string(a)),(int(11),string(b))))).
488 :- assert_must_succeed((kernel_tools:can_match((int(11),string(a)),(int(11),string(_))))).
489 :- assert_must_succeed((kernel_tools:cannot_match(pred_false,pred_true))).
490 :- assert_must_succeed((kernel_tools:can_match(pred_true,pred_true))).
491 :- assert_must_succeed((kernel_tools:can_match(record([field(a,pred_true)]),record([field(a,_)])))).
492 :- assert_must_succeed((kernel_tools:cannot_match(record([field(a,pred_false)]),record([field(a,pred_true)])))).
493
494 % can_match: quick check to see if the (AVL or List) element could match
495
496 can_match(A,B) :- \+ cannot_match(A,B).
497 cannot_match(A,B) :- \+ can_match_aux(A,B). % Note: probably better to wrap can_match into negation to avoid instantiations
498
499 :- use_module(clpfd_interface,[clpfd_can_match/2]).
500
501 can_match_aux(A,_) :- var(A),!. % TO DO: we could check for not_empty_set co-routine if A or B = []?
502 can_match_aux(_,B) :- var(B),!.
503 can_match_aux((A,B),(ElA,ElB)) :- !,can_match_aux(A,ElA), can_match_aux(B,ElB).
504 can_match_aux(int(A),R) :- !,
505 % (\+ 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
506 (var(R) -> true
507 ; R=int(B), clpfd_can_match(A,B)). %,(B=A -> true ; print(ko(A,B)),nl,fail)).%,fail,trace,B=A)).
508 can_match_aux(fd(NrA,GS),R) :- !,
509 %(\+ ground(R) -> true ; R=fd(Nr,GS)). % ditto (see, e.g., test 985 - graph iso)
510 (var(R) -> true ; R=fd(NrB,GS), clpfd_can_match(NrA,NrB)).
511 can_match_aux(pred_false,R) :- !, R=pred_false.
512 can_match_aux(pred_true,R) :- !, R=pred_true.
513 can_match_aux(string(A),R) :- !, %(\+ ground(R) -> true ; R=string(A)). % may instantiate LHS
514 (var(R) -> true ; R=string(B), can_match_atomic(A,B)).
515 can_match_aux(term(A),R) :- !, %(\+ ground(R) -> true ; R=term(A)). % ditto
516 (var(R) -> true ; R=term(B), can_match_term(A,B)).
517 can_match_aux(freeval(ID,Case,Value),R) :- !,
518 (var(R) -> true
519 ; R=freeval(IDR,CaseR,VR),
520 (var(IDR) ; var(CaseR) -> true
521 ; (ID,Case)=(IDR,CaseR),
522 can_match_aux(Value,VR))).
523 can_match_aux([],R) :- !, R \= avl_set(node(_,_,_,_,_)), R\= [_|_].
524 can_match_aux(avl_set(A),R) :- !, check_avl_set(A),
525 can_match_avl_set(R,A).
526 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
527 can_match_aux([_|_],R) :- !, R \= [].
528 can_match_aux(record(Fields1),record(Fields2)) :- !,can_match_fields(Fields1,Fields2).
529 can_match_aux(_,_). % catch-all other types
530
531 can_match_fields(A,B) :- (var(A);var(B)),!.
532 can_match_fields([],[]).
533 can_match_fields([F1|T1],[F2|T2]) :- can_match_field(F1,F2), can_match_fields(T1,T2).
534
535 can_match_field(A,B) :- (var(A);var(B)),!.
536 can_match_field(field(F1,V1),field(F2,V2)) :- F1==F2,!, can_match_aux(V1,V2).
537 can_match_field(F1,F2) :- add_internal_error('Non-matching fields: ',can_match_field(F1,F2)).
538
539 can_match_term(floating(F1),FF2) :- !,
540 (var(FF2) -> true ; FF2=floating(F2), can_match_atomic(F1,F2)). % floating numbers / reals
541 can_match_term(T1,T2) :- can_match_atomic(T1,T2).
542
543 :- use_module(kernel_dif,[frozen_dif/2]).
544 can_match_atomic(A,B) :- var(A),!, \+ frozen_dif(A,B).
545 can_match_atomic(A,B) :- var(B),!, \+ frozen_dif(B,A).
546 can_match_atomic(A,B) :- A=B.
547
548 :- use_module(library(avl),[avl_min/2, avl_max/2, avl_size/2]).
549
550 can_match_avl_set([],A) :- !, A=empty.
551 can_match_avl_set([H|T],A) :- !, list_can_match_avl_set([H|T],0,A).
552 can_match_avl_set(avl_set(B),A) :- !, avl_min(A,Min), avl_min(B,Min), avl_max(A,Max),avl_max(B,Max).
553 can_match_avl_set(_,_).
554
555 list_can_match_avl_set(T,_,_) :- var(T),!.
556 list_can_match_avl_set([],Sze,A) :- !, avl_size(A,Sze).
557 list_can_match_avl_set([H|T],Sze,A) :- !,
558 (custom_explicit_sets:quick_test_avl_membership(A,H,PredRes)
559 -> PredRes=pred_true, S1 is Sze+1,
560 list_can_match_avl_set(T,S1,A)
561 ; true). % TO DO: maybe also check T ?
562 list_can_match_avl_set(_,_,_).
563
564 % ------------------------
565
566 ?cannot_match_aggressive(A,B) :- \+ can_match_aggr(A,B).
567
568 % a more aggressive version; which may trigger co-routines for left-side A
569 can_match_aggr(A,_) :- var(A),!.
570 can_match_aggr(_,B) :- var(B),!.
571 can_match_aggr((A,B),(ElA,ElB)) :- !,can_match_aggr(A,ElA), can_match_aggr(B,ElB).
572 can_match_aggr(int(A),R) :- !, % R=int(A). % can trigger co-routines both sides; causes problem for 985
573 (var(R) -> true
574 ; R=int(B), (var(B) -> clpfd_can_match(A,B) ; A=B)). % only triggers co-routines for left side
575 can_match_aggr(fd(NrA,GS),R) :- !, % R=fd(Nr,GS). % ditto
576 (var(R) -> true
577 ; R=fd(NrB,GS), (var(NrB) -> clpfd_can_match(NrA,NrB) ; NrA=NrB)).
578 can_match_aggr(string(A),R) :- !, %R=string(A). % ditto
579 (var(R) -> true
580 ; R=string(B), (var(B) -> can_match_atomic(A,B) ; A=B)).
581 can_match_aggr(pred_false,R) :- !, R=pred_false.
582 can_match_aggr(pred_true,R) :- !, R=pred_true.
583 can_match_aggr(A,B) :- can_match_aux(A,B).
584
585
586 % ----------------------------------------
587
588
589
590 /* COMPARING TWO CLOSURES */
591
592
593
594 :- use_module(probsrc(avl_tools),[avl_height_less_than/2]).
595 :- use_module(probsrc(btypechecker),[l_unify_types_strict/2, unify_types_strict/2]).
596
597 % a quick check, use instead of == to compare values
598 quick_same_value(V1,V2) :- var(V1),!,V1==V2.
599 quick_same_value(_,V2) :- var(V2),!,fail.
600 quick_same_value(closure(P,T1,B1),closure(P,T2,B2)) :- !,
601 l_unify_types_strict(T1,T2),
602 quick_same_texpr_body(B1,B2).
603 quick_same_value(avl_set(A),AB) :-
604 !, % == for avl_set can be expensive ! triggered e.g. by x = (1..100000) \ {55} & (x \ {33}) <: x
605 % top-level avl_set usually handled by subset_of_explicit_set or similar code
606 AB=avl_set(B),
607 avl_height_less_than(A,3), % what depth value to use? maybe we should simply not compare at all
608 % TODO: what about other values pairs (avl_set(),_), rec(Fields), ...
609 A==B.
610 quick_same_value(V1,V2) :- V1==V2.
611
612 :- use_module(probsrc(custom_explicit_sets),[quick_definitely_maximal_set_avl/1]).
613 inner_quick_same_value(V1,V2) :- var(V1),!,V1==V2.
614 inner_quick_same_value(_,V2) :- var(V2),!,fail.
615 inner_quick_same_value(closure(P,T1,B1),closure(P,T2,B2)) :- !,
616 l_unify_types_strict(T1,T2), % should never fail
617 quick_same_texpr_body(B1,B2).
618 inner_quick_same_value((V1a,V1b),(V2a,V2b)) :- !,
619 inner_quick_same_value(V1a,V2a),
620 inner_quick_same_value(V1b,V2b).
621 inner_quick_same_value(rec(F1),rec(F2)) :- !,
622 inner_quick_same_fields(F1,F2).
623 inner_quick_same_value(avl_set(AVL),global_set(_)) :- !,
624 quick_definitely_maximal_set_avl(AVL).
625 inner_quick_same_value(global_set(_),avl_set(AVL)) :- !,
626 quick_definitely_maximal_set_avl(AVL).
627 inner_quick_same_value(V1,V2) :- % TODO: we could compare avl_sets
628 V1==V2.
629
630 inner_quick_same_fields(V1,V2) :- var(V1),!,V1==V2.
631 inner_quick_same_fields(_,V2) :- var(V2),!,fail.
632 inner_quick_same_fields([],[]).
633 inner_quick_same_fields([F1|T1],[F2|T2]) :- % TODO: check nonvar(Name...)
634 inner_quick_same_field(F1,F2),
635 inner_quick_same_fields(T1,T2).
636
637 inner_quick_same_field(V1,V2) :- var(V1),!,V1==V2.
638 inner_quick_same_field(_,V2) :- var(V2),!,fail.
639 inner_quick_same_field(field(Name1,V1),field(Name2,V2)) :- Name1==Name2,
640 inner_quick_same_value(V1,V2).
641
642 quick_same_texpr_body(b(E1,Type1,_),b(E2,Type2,_)) :-
643 check_unify_types_strict(Type1,Type2), % types should always match
644 qsame_texpr2(E1,E2).
645
646 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
647 :- if(true). %environ(prob_safe_mode,true)).
648 check_unify_types_strict(T1,T2) :- unify_types_strict(T1,T2),!.
649 check_unify_types_strict(T1,T2) :-
650 add_warning(check_unify_types_strict,'Unexpected difference in types: ',T1 \= T2),fail.
651 :- else.
652 check_unify_types_strict(_,_).
653 :- endif.
654
655 qsame_texpr2(value(V1),value(V2)) :- !,
656 inner_quick_same_value(V1,V2).
657 qsame_texpr2(E1,E2) :-
658 functor(E1,F,Arity),
659 functor(E2,F,Arity),
660 safe_syntaxelement_det(E1,Subs1,_Names1,_List1,Constant1),
661 safe_syntaxelement_det(E2,Subs2,_Names2,_List2,Constant2), Constant2==Constant1,
662 quick_same_sub_expressions(Subs1,Subs2).
663
664 quick_same_sub_expressions([],[]).
665 quick_same_sub_expressions([H1|T1],[H2|T2]) :-
666 quick_same_texpr_body(H1,H2),
667 quick_same_sub_expressions(T1,T2).
668
669 % --------------------
670
671 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
672 :- if(environ(prob_safe_mode,true)).
673 :- use_module(avl_tools,[check_is_non_empty_avl/1]).
674 check_avl_set(V) :- check_is_non_empty_avl(V).
675 :- else.
676 check_avl_set(_).
677 :- endif.
678
679 % ------------------------------------------
680
681
682
683 :- assert_must_succeed((kernel_tools:ground_value_opt_check(int(X),_,V), var(V), X=1, nonvar(V))).
684 :- assert_must_succeed((kernel_tools:ground_value_opt_check(string(X),_,V), var(V), X=a, nonvar(V))).
685 :- assert_must_succeed((kernel_tools:ground_value_opt_check([int(1),int(X)],_,V), var(V), X=1, nonvar(V))).
686 % instantiate third argument to atomic-nonvar term if first argument ground B value
687 % if second argument is instantiated the check is no longer required, co-routines should be discarded
688 % useful to ensure e.g. that enumeration_only_fdvar or similar checks work
689
690 % a version with an additional Needed flag that can discard the ground value check if no longer needed
691 :- block ground_value_opt_check(-,-,?).
692 ground_value_opt_check(_,Needed,_) :- nonvar(Needed),!,
693 true. % R=ground_value. Warning: instantiating R can change order of firing co-routines in kernel_mappings
694 % This makes test 1720 fail: int_plus instantiates a variable to int(_) -> which triggers ground_value_opt_check
695 % this in turn instantiates R and then triggers another co-routine (convert_list_of_expressions_into_set_wf)
696 % before finishing int_plus (which should have run until int_plus4, frozen_dif in a subsidiary call sees not pending int_plus4 co-routine)
697 % Other tests which fail: 983, 1380
698 ground_value_opt_check([],_,R) :- !, R=ground_value.
699 ground_value_opt_check(pred_true,_,R) :- !, R=ground_value.
700 ground_value_opt_check(pred_false,_,R) :- !, R=ground_value.
701 ?ground_value_opt_check(int(X),Needed,R) :- !, opt_ground_atom(X,Needed,R).
702 ground_value_opt_check(global_set(X),Needed,R) :- !, opt_ground_atom(X,Needed,R).
703 ground_value_opt_check(fd(X,_T),Needed,R) :- !,opt_ground_atom(X,Needed,R). % avoid waking up co-routines with R=X.
704 ground_value_opt_check(string(X),Needed,R) :- !, opt_ground_atom(X,Needed,R).
705 ground_value_opt_check((A,B),Needed,R) :- !,
706 ? ground_value_opt_check(A,Needed,GA), ground_value_opt_check_aux(GA,B,Needed,R).
707 ground_value_opt_check([H|T],Needed,R) :- !,
708 ground_value_opt_check(H,Needed,GA), ground_value_opt_check_aux(GA,T,Needed,R).
709 ground_value_opt_check(avl_set(A),_,R) :- !, % assume avl_set grounded
710 check_avl_set(A),
711 R = ground_value.
712 ground_value_opt_check(rec(F),Needed,R) :- !, opt_ground_fields(F,Needed,R).
713 ground_value_opt_check(closure(_P,_T,B),Needed,R) :- !,
714 bexpr_variables(B,Vars),
715 ground_value_opt_check(Vars,Needed,R).
716 %when(ground(Vars),R=ground_value).
717 ground_value_opt_check(term(X),Needed,R) :- !, opt_ground_term(X,Needed,R).
718 ground_value_opt_check(Val,Needed,R) :- %print(uncov(Val,R)),nl,trace,
719 (atomic(Val) -> R=ground_value ; when((ground(Val);nonvar(Needed)),R=ground_value)).
720
721
722 :- block opt_ground_term(-,-,?).
723 opt_ground_term(_,Needed,_) :- nonvar(Needed),!.
724 opt_ground_term(floating(F),Needed,R) :- !, opt_ground_atom(F,Needed,R).
725 opt_ground_term(X,Needed,R) :-
726 when((ground(X); nonvar(Needed)),R=ground_value).
727
728 :- block opt_ground_atom(-,-,?).
729 opt_ground_atom(A,_,Res) :- nonvar(A),!, Res=ground_value.
730 opt_ground_atom(_,_,_).
731
732 :- block ground_value_opt_check_aux(-,?,-,?).
733 ?ground_value_opt_check_aux(_,V,Needed,R) :- ground_value_opt_check(V,Needed,R).
734 % :- block ground_value_check_aux(-,?,-). % this slows down test 884, 292, 293, 1456, 1737
735
736
737 :- block opt_ground_fields(-,-,?).
738 opt_ground_fields(_,Needed,_) :- nonvar(Needed),!.
739 opt_ground_fields([],_,R) :- !, R=ground_value.
740 opt_ground_fields([field(F,V)|T],Needed,R) :- opt_ground_fields_aux(F,V,T,Needed,R).
741
742 :- block opt_ground_fields_aux(-,?,?,-,?).
743 opt_ground_fields_aux(_,V,T,Needed,R) :- opt_ground_fields(T,Needed,GrT), ground_value_opt_check_aux(GrT,V,Needed,R).