1:- module(reduce, [attach_prefix/3, complete_args/3,
2 optimize_call_N/2,
3 slim_goal/2,
4 subtree/4, subtree/5,
5 reduce/3, reduce/4, reduce_one/4,
6 term_rewrite/3, term_rewrite/4]). 7
15
16 31
32:- meta_predicate reduce_one(2, 4, ?, ?). 33reduce_one(R, P, X, Y):- call(P, X, Y, S, S0),
34 nonvar(S), 35 call(R, S, S0).
36
37:- meta_predicate reduce(2, ?, ?),
38 reduce(2, 4, ?, ?). 39:- meta_predicate term_rewrite(2, ?, ?),
40 term_rewrite(2, ?, ?, ?). 41
42reduce(R, A, B):- reduce(R, subtree([]), A, B).
44reduce(R, P, X, Y):- reduce_one(R, P, X, X0), !,
45 reduce(R, P, X0, Y).
46reduce(_, _, X, X).
47
49term_rewrite(R, X, Y):- term_rewrite(R, [], X,Y).
51term_rewrite(R, E, X, Y):- reduce_one(R, subtree(E), X, X0), !,
52 term_rewrite(R, E, X0, Y).
53term_rewrite(_, _, X, X).
54
69
70subtree(T, S):- child([], T, S).
71
72subtree(_, T, T).
73subtree(Sgn, T, S):- child(Sgn, T, U), subtree(Sgn, U, S).
74
75child(S, X, Y):- compound(X),
76 functor(X, F, N),
77 between(1, N, I),
78 sgn_index_chk(S, F, N, I),
79 arg(I, X, Y).
80
82subtree(T, T0, S, S0):- subtree([], T, T0, S, S0).
83
84subtree(_, T, T0, T, T0).
85subtree(Sgn, T, T0, S, S0):- child(Sgn, T, T0, U, U0),
86 subtree(Sgn, U, U0, S, S0).
87
91
95
96child(T, T0, A, A0):- child([], T, T0, A, A0).
97
98child(S, X, X0, Y, Y0):- compound(X),
99 functor(X, F, N),
100 functor(X0, F, N),
101 between(1, N, I),
102 sgn_index_chk(S, F, N, I),
103 arg(I, X, Y),
104 copy_args(N, I, Y0, X, X0).
105
106:- meta_predicate(sgn_index_chk(+,+,+,+)). 109
122
123sgn_index_chk(X,Y,Z,U):- once(sgn_index(X,Y,Z,U)).
124
125:- meta_predicate(sgn_index(+,+,+,+)). 126
129sgn_index([], _, _, _).
130sgn_index(F, G, _, _):- atom(F), G==F.
131sgn_index(A;B, F, N, I):-
132 ( sgn_index(A, F, N, I)
133 ; sgn_index(B, F, N, I)).
134sgn_index((A,B), F, N, I):-
135 sgn_index(A, F, N, I),
136 sgn_index(B, F, N, I).
137sgn_index(\+(A), F, N, I):- \+ sgn_index(A, F, N, I).
138sgn_index(S/N, F, N, I):- sgn_index(S, F, N, I).
139sgn_index([I|_], _, _, I).
140sgn_index([_|L], _, _, I):- memberchk(I, L).
141sgn_index({A}, F, N, I):- sgn_index_brace(A, F, N, I).
142
144sgn_index_brace((A, B), F, N, I):- sgn_index_brace(A, F, N, I), !
145 ; sgn_index_brace(B, F, N, I).
146sgn_index_brace(A, F, N, I):- sgn_index(A, F, N, I).
147
151
152copy_args(0, _, _, _, _):-!.
153copy_args(J, I, A, T, T0):-
154 ( J==I
155 -> arg(J, T0, A)
156 ; arg(J, T, X),
157 arg(J, T0, X)
158 ),
159 J1 is J-1,
160 copy_args(J1, I, A, T, T0).
162term_complete([], G, G):-!.
163term_complete(A, G, G0):- G =.. H,
164 append(H, A, H0),
165 G0 =.. H0.
166
171complete_args(X, As, Y):- var(X), !,
172 Y=..[call, X|As].
173complete_args(M:X, As, Y):- !,
174 ( M == []
175 -> complete_args(X, As, Y)
176 ; complete_args(X, As, Y0),
177 Y = M:Y0
178 ).
179complete_args(X, As, Y):- var(As), !,
180 Y =.. [call, X|As].
181complete_args(X, [], X):- !.
182complete_args(G, As, G0):- atom(G), !,
183 G0 =.. [G|As].
184complete_args(G, As, G0):-
185 G =.. H,
186 append(H, As, H0),
187 G0 =.. H0.
188
189 192
195canonical_prefix_form(M:C, M, C).
196canonical_prefix_form(C, [], C).
197
199prefix_var(X):- var(X),!.
200prefix_var(_:X):- prefix_var(X).
201
203prefix_nonvar(X):- nonvar(X), !,
204 ( X = _:Y -> prefix_nonvar(Y)
205 ; true
206 ).
207
216
217
218slim_goal(X, Y):- boole_rule(X, X0), !, slim_goal(X0, Y).
219slim_goal(X, X).
220
222boole_rule(A, call(A)) :- var(A).
223boole_rule((A, B), (A0, B)) :- boole_rule(A, A0).
224boole_rule((A, B), (A, B0)) :- boole_rule(B, B0).
225boole_rule((A; B), (A0; B)) :- boole_rule(A, A0).
226boole_rule((A; B), (A; B0)) :- boole_rule(B, B0).
227boole_rule((A -> B), (A0->B)) :- boole_rule(A, A0).
228boole_rule((A -> B), (A->B0)) :- boole_rule(B, B0).
229boole_rule(\+(A), \+(A0)) :- boole_rule(A, A0).
230boole_rule(M:A, M:B) :- boole_rule(A, B).
231boole_rule(once(A), once(B)) :- boole_rule(A, B).
232boole_rule(once(A), A) :- ( A == true; A == false ).
233boole_rule((true, A), A).
234boole_rule((A, true), A).
235boole_rule((false, _), false).
237boole_rule((true; true), true).
238boole_rule((A; false), A).
239boole_rule((false; A), A).
240boole_rule((false -> _), false).
241boole_rule((true -> A), A).
242boole_rule(\+(false), true).
243boole_rule(\+(true), false).
244boole_rule(X=Y, true) :- X == Y.
245boole_rule(X=Y, false) :- X \== Y, ground((X,Y)).
246boole_rule(X==Y, true) :- X == Y.
247boole_rule(X==Y, false) :- X \== Y, ground((X,Y)).
248boole_rule(nonvar(X), true) :- nonvar(X).
249boole_rule(var(X), false) :- nonvar(X).
250boole_rule(fail, false).
251boole_rule(_:(M:A), M:A).
252boole_rule(_:E, E) :- prefix_cancellable(E).
253boole_rule(M:A, A) :- M == [].
254boole_rule(M:E, ME) :- propagate_prefix(M, E, ME).
255boole_rule(X, Y) :- slim_call(X, Y).
256
258propagate_prefix(M, X, X):- M==[], !.
259propagate_prefix(M, once(X), once(M:X)).
260propagate_prefix(M, (X, Y), (M:X, M:Y)).
261propagate_prefix(M, (X; Y), (M:X; M:Y)).
262propagate_prefix(M, (X -> Y), (M:X -> M:Y)).
263propagate_prefix(M, \+(X), \+(M:X)).
264
267prefix_cancellable(!).
268prefix_cancellable(true).
269prefix_cancellable(false).
270
272optimize_call_N(X, Y):- slim_call(X, Y).
273optimize_call_N(X, X).
274
276slim_call(X, Y) :- canonical_prefix_form(X, M, X0),
277 reducible_call(X0),
278 slim_call(X0, M, Y).
279
281reducible_call(X) :- X=..[F, A|_],
282 (F == call; F == apply),
283 prefix_nonvar(A).
284
293
294slim_call(X, M, call(Y)):- var(X), !,
295 attach_prefix(M, X, Y).
296slim_call(M:X, _, Y):-!, slim_call(X, M, Y).
297slim_call(X, M, Y):- X =..[call, F|As], !,
298 slim_call(F, M, F0),
299 complete_args(F0, As, Y).
300slim_call(apply(F, As), M, Y):-
301 slim_call(F, M, F0),
302 complete_args(F0, As, Y).
303slim_call(apply(F), M, Y):-
304 slim_call(F, M, Y).
305slim_call(X, M, Y):- attach_prefix(M, X, Y).
306
310
311attach_prefix(M, X, Y):- var(X), !,
312 ( var(M), Y = M:X
313 ; M == [], Y = X
314 ; Y = M:X
315 ),
316 !.
317attach_prefix(_, X, X) :- integer(X), !.
318attach_prefix(_, X, X) :- string(X), !.
319attach_prefix(_, X, X) :- X = (_:_), !.
320attach_prefix(M, X, X) :- M == [], !.
321attach_prefix(M, X, M:X).
322
332
339
340reduce_subsumes(X, Y, G):- collect_subsumes(X, Y, G),
341 check_subsumes_throw(G).
342
343reduce_subsumes(N, X, Y, G):- collect_subsumes(N, X, Y,true,G),
344 check_subsumes_throw(G).
345
346check_subsumes_throw(G):- unzip_equality(G, L, R),
347 ( subsumes_term(L, R)
348 -> true
349 ; throw(error('reduce_subsumes rule'))
350 ).
351
353collect_subsumes(X, Y, X = Y):- var(X), !.
354collect_subsumes(X, Y, X == Y):- atomic(X), !.
355collect_subsumes(X, Y, (nonvar(Y), Y=Y0, G)):- var(Y), !,
356 functor(X, F, N),
357 functor(Y0, F, N),
358 collect_subsumes(N, X, Y0, true, G).
359collect_subsumes(X, Y, G):- functor(X, F, N),
360 functor(Y, F, N),
361 !,
362 collect_subsumes(N, X, Y, true, G).
363
364collect_subsumes(0, _, _, G, G):-!.
365collect_subsumes(J, X, T, G0, G):- arg(J, X, A),
366 arg(J, T, B),
367 collect_subsumes(A, B, H),
368 K is J - 1,
369 collect_subsumes(K, X, T, (H, G0), G).
370
374
375unzip_equality(E, P, Q):- unzip_equal_dlist(E, []-P, []-Q), !.
376
377unzip_equal_dlist((E,F), P-Q, R-S):- unzip_equal_dlist(E, P-T, R-U),
378 unzip_equal_dlist(F, T-Q, U-S).
379unzip_equal_dlist(X=Y, A-[X|A], B-[Y|B]).
380unzip_equal_dlist(_, P-P, Q-Q)