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). |