1:- module(reduce,
    2		  [attach_prefix/3, complete_args/3,
    3		   optimize_call_N/2,
    4		   slim_goal/2,
    5		   subtree/4, subtree/5, subterm/4, subterm/5,
    6		   reduce/3, reduce/4, reduce_one/4, copy_args_with_hole/4
    7		]).    8
    9% reduce/[3,4]  by rules
   10% ?- reduce(math:desugar, -(a-b), X).
   11% ?- term_rewrite(math:desugar, [],  -(+(a)-b), X).
   12% ?- term_rewrite(math:desugar, (-);(+),  -(+(a)-b), X).
   13% ?- term_rewrite(math:desugar, {-,+},  -(a), X).
   14
   15		/******************************************************************
   16		*     [2016/03/20]                                                *
   17		*     Regular expressions over signatures (S-Regex).              *
   18		*                                                                 *
   19		*     <S-Regex> -->                                               *
   20		*	  []                                                          *
   21		*     |	<atom>                                                    *
   22		*     |	<S-Regex>; <S-Regex>                                      *
   23		*     |	<S-Regex>, <S-Regex>                                      *
   24		*     |	\+ <S-Regex>                                              *
   25		*     |	<S-Regex>/N                                               *
   26		*     |	[N, N, ..., N]		(non-empty list)                      *
   27		*                                                                 *
   28		*     where <atom> is a prollog atom and N a positive integer.    *
   29		******************************************************************/
   30
   31:- meta_predicate reduce_one(2, 4, ?, ?).   32reduce_one(R, P, X, Y):- call(P, X, Y, S, S0),
   33	nonvar(S),				% [2010/03/05]
   34	call(R, S, S0).
   35
   36:- meta_predicate reduce(2, ?, ?), reduce(2, 4, ?, ?).   37:- meta_predicate term_rewrite(2, ?, ?), term_rewrite(2, ?, ?, ?).   38
   39reduce(R, A, B):-  reduce(R, subterm([]), A, B).
   40%
   41reduce(R, P, X, Y):- reduce_one(R, P, X, X0), !,
   42	reduce(R, P, X0, Y).
   43reduce(_, _, X, X).
   44
   45% sutree/[2,3] deprecated ==> renamed to subterm.
   46% The subtree relation is the transtive closure of direct-child relation.
   47% subtree/[2,3,4,5]
   48% ?- subtree(a+b, X).
   49% ?- subtree(+, a*b, X).
   50% ?- subtree(+, a*b+ c*d, X).
   51% ?- subtree(\+ (+), a*b+ c*d, X).
   52% ?- subtree(\+ (-), a*b+ c*d, X).
   53% ?- subtree((+); (*)/2, a*b + c*d, X).
   54% ?- subtree(\+ ((+); []/2), a*b + c*d, X).
   55% ?- subtree({+, *}, a*b + c*d, X).
   56% ?- subtree(f(a,b), T, S, S0).
   57% ?- subtree(f, f(a, f(b,c)), X, Y, Z).
   58% ?- subtree(([], \+g),  f(a,g(b)), X, Y, Z).
   59% ?- subtree(\+g,  f(a,g(b)), X, Y, Z).
   60% ?- subtree(+, a*b + c*d,  Z).
   61subtree(T, S):- subterm(T, S).
   62%
   63subtree(Sgn, T, S):- subterm(Sgn, T, S).
   64
   65% ?- subtree(a+b, X, Y, Z).
   66subtree(T, T0, S, S0):- subterm(T, T0, S, S0).
   67%
   68subtree(Sgn, T, T0, S, S0):- subterm(Sgn, T, T0, S, S0).

Y is unified with a subterm of X. ?- subterm(X, Y). % false ?- subterm(a, Y). ?- subterm([a,b,c], Y). ?- subterm([a,B,c], Y).

   77subterm(X, Y) :- nonvar(X),
   78		functor(X, F, N),
   79		(	Y = X
   80		;	functor(X, F, N),
   81			between(1, N, I),
   82			arg(I, X, A),
   83			subterm(A, Y)
   84		).

Y is unified with a subterm of X satisfying filter S.

   90% ?- subterm(+, a*b, Y).	% false
   91% ?- subterm((+)/2, a+f(b), Y).
   92% ?- subterm((+)/2, a+f(b)+c, Y).
   93% ?- subterm((+)/2, a+ b +c, Y).
   94% ?- subterm((+)/2, a+ (b +c), Y).
   95% ?- subterm([], a+ (b +c), Y).
   96subterm(S, X, Y) :- nonvar(X),
   97		functor(X, F, N),
   98		(	sgn_boole_chk(S, F, N, *) ->   % * for the whole term.
   99			(	Y = X
  100			;	functor(X, F, N),
  101				between(1, N, I),
  102				arg(I, X, A),
  103				subterm(S, A, Y)
  104			)
  105		).

Z is unified with a subterm of Y, and Y is unified with a term with a leaf U such that if Y is unified with U then X == Y.

  111% ?- subterm(f(g(a)), X, Y, Z).
  112subterm(X, Y, X, Y) :- nonvar(X).
  113subterm(X, X0, Y, Y0):- compound(X),
  114	functor(X, F, N),
  115	functor(X0, F, N),
  116	between(1, N, I),
  117	arg(I, X, A),
  118	copy_args_with_hole(1, I, V, X, X0),
  119	subterm(A, V, Y, Y0).

Z is unified with a subterm of Y satisfying filter S and Y is unified with a term with a leaf U such that if Y is unified with U then X == Y.

  126% ?- subterm(((+)/2; f/1), a+f(b), A, B, C).
  127subterm(S, X, Y, X, Y) :- nonvar(X),
  128	functor(X, F, N),
  129	sgn_boole_chk(S, F, N, *).   % * for the whole term
  130subterm(S, X, X0, Y, Y0):- compound(X),
  131	functor(X, F, N),
  132	functor(X0, F, N),
  133	between(1, N, I),
  134	sgn_boole_chk(S, F, N, I),
  135	arg(I, X, A),
  136	copy_args_with_hole(1, I, V, X, X0),
  137	subterm(S, A, V, Y, Y0).

True if (F, N, I) is an instance satisfying signature filter Sgn. ?- sgn_boole_chk([], f, 3, 2). ?- sgn_boole_chk([], *, 3, 2). ?- sgn_boole_chk(f, f, 3, 2). ?- sgn_boole_chk(f, g, 3, 2). % false ?- sgn_boole_chk((f/3, [1,3]), f, 3, 1). ?- sgn_boole_chk(([]/3, [1,3]), f, 3, 1). ?- sgn_boole_chk(((g/2;f/3), [1,3]), f, 3, 1). ?- sgn_boole_chk(\+ [], f, 3, 1). % false ?- sgn_boole_chk(\+ ((*)/2), f, 3, 1). ?- sgn_boole_chk(\+ ([]/2), f, 3, 1). ?- sgn_boole_chk((*)/2, *, 2, 1). ?- sgn_boole_chk([]/2, *, 2, 1). ?- sgn_boole_chk('[|]'/2, *, 2, 1). % false ?- sgn_boole_chk('[|]'/2, '[|]', 2, 1). ?- sgn_boole_chk('[|]', '[|]', 2, 1).

  158sgn_boole_chk(X, Y, Z, U):-
  159	once(eval_sgn_boole(X, Y, Z, U)).
  160
  161% - The null list [] is for wild card
  162% - [...] works as disj for arg pos.
  163% - 0 as pos for the whole term.
  164% - S/N indicate arity is N in addition (and) S
  165% - Sgn works as constraint on given triple (F, N, I)
  166eval_sgn_boole([], _, _, _).			% wild card
  167eval_sgn_boole([J|Js], _, _, I):-	% filter on arg position
  168	(	I = 0 -> true
  169	;	memberchk(I, [J|Js])
  170	).
  171eval_sgn_boole(S/N, F, N, I):- eval_sgn_boole(S, F, N, I).
  172eval_sgn_boole((A,B), F, N, I):-		% conjunctive
  173	eval_sgn_boole(A, F, N, I),
  174	eval_sgn_boole(B, F, N, I).
  175eval_sgn_boole((A;B), F, N, I):-		% disjuntive
  176	(	eval_sgn_boole(A, F, N, I)
  177	;	eval_sgn_boole(B, F, N, I)
  178	).
  179eval_sgn_boole(\+(A), F, N, I):-		% negative.
  180	\+ eval_sgn_boole(A, F, N, I).
  181eval_sgn_boole(G, F, _, _):-
  182	(	atomic(G) -> G == F
  183	;	G = [_|_] -> memberchk(F, G)
  184	).

T0 is a copy of T but the I-th arg of T0 unified with A.

  191% ?- copy_args_with_hole(1, d, f(a,b,c), f(A,B,C)).
  192copy_args_with_hole(I, A, T, T0):- copy_args_with_hole(1, I, A, T, T0).
  193%
  194copy_args_with_hole(J, I, A, T, T0):- arg(J, T, X), !,
  195	(   J == I 	->  arg(I, T0, A)
  196	;   arg(J, T0, X)
  197	),
  198	J1 is J + 1,
  199	copy_args_with_hole(J1, I, A, T, T0).
  200copy_args_with_hole(_, _, _, _, _).
  201%
  202term_complete([], G, G):-!.
  203term_complete(A, G, G0):- G =.. H,
  204	append(H, A, H0),
  205	G0 =.. H0.
  206
  207% ?- complete_args(f(a), [b,c], X).
  208% ?- complete_args(user:m:F,[a,b], R).
  209% ?- complete_args([]:[]:F,[a,b], R).
  210% ?- complete_args([]:M:[]:F,[a,b], R).
  211complete_args(X,  As,  Y):- var(X), !,
  212	Y=..[call, X|As].
  213complete_args(M:X, As, Y):- !,
  214	(	M == []
  215	-> 	complete_args(X, As, Y)
  216	;	complete_args(X, As, Y0),
  217		Y = M:Y0
  218	).
  219complete_args(X, As, Y):- var(As), !,
  220	Y =.. [call, X|As].
  221complete_args(X, [], X):- !.
  222complete_args(G, As, G0):- atom(G), !,
  223 	G0 =.. [G|As].
  224complete_args(G, As, G0):-
  225	G =.. H,
  226 	append(H, As, H0),
  227 	G0 =.. H0.
  228
  229		/***************************
  230		*     Simplifying Goals    *
  231		***************************/
  232
  233% some tiny.
  234%  C is safely supposed to be without a module prefix.
  235canonical_prefix_form(M:C, M, C).
  236canonical_prefix_form(C, [], C).
  237
  238% ?-  prefix_var(_:_).
  239prefix_var(X):- var(X),!.
  240prefix_var(_:X):- prefix_var(X).
  241
  242% ?-  prefix_nonvar(_:_).
  243prefix_nonvar(X):- nonvar(X), !,
  244				( X = _:Y  -> prefix_nonvar(Y)
  245				; true
  246				).
  247
  248% Goal simplification for Prolog *operational* semantics !!
  249% ?- slim_goal((true, (fail-> X)), R).
  250% ?- slim_goal((true, (true-> X)), R).
  251% ?- slim_goal((A,true), R).
  252% ?- slim_goal((A,false), R).
  253% ?- slim_goal(true, R).
  254
  255slim_goal(X, Y):- boole_rule(X, X0), !, slim_goal(X0, Y).
  256slim_goal(X, X).
  257
  258% Pseudo truth tables for goal simplification.
  259boole_rule(A, call(A))		 :- var(A).
  260boole_rule((A, B), (A0, B))	 :- boole_rule(A, A0).
  261boole_rule((A, B), (A, B0))	 :- boole_rule(B, B0).
  262boole_rule((A; B), (A0; B))	 :- boole_rule(A, A0).
  263boole_rule((A; B), (A; B0))	 :- boole_rule(B, B0).
  264boole_rule((A -> B), (A0->B)) :- boole_rule(A, A0).
  265boole_rule((A -> B), (A->B0)) :- boole_rule(B, B0).
  266boole_rule(\+(A), \+(A0))	 :- boole_rule(A, A0).
  267boole_rule(M:A, M:B)			 :- boole_rule(A, B).
  268boole_rule(once(A), once(B))	 :- boole_rule(A, B).
  269boole_rule(once(A), A)		 :- ( A == true; A == false ).
  270boole_rule((true, A), A).
  271boole_rule((A, true), A).
  272boole_rule((false, _), false).
  273% boole_rule((_, false), false).		% Disabled.
  274boole_rule((true; true), true).
  275boole_rule((A; false), A).
  276boole_rule((false; A), A).
  277boole_rule((false -> _), false).
  278boole_rule((true -> A), A).
  279boole_rule(\+(false), true).
  280boole_rule(\+(true), false).
  281boole_rule(X=Y, true)		 :- X == Y.
  282boole_rule(X=Y, false)		 :- X \== Y, ground((X,Y)).
  283boole_rule(X==Y, true)		 :- X == Y.
  284boole_rule(X==Y, false)		 :- X \== Y, ground((X,Y)).
  285boole_rule(nonvar(X), true)	 :- nonvar(X).
  286boole_rule(var(X), false)	 :- nonvar(X).
  287boole_rule(fail, false).
  288boole_rule(_:(M:A), M:A).
  289boole_rule(_:E, E)			 :- prefix_cancellable(E).
  290boole_rule(M:A, A)			 :- M == [].
  291boole_rule(M:E, ME)			 :- propagate_prefix(M, E, ME).
  292boole_rule(X, Y)				 :- slim_call(X, Y).
  293
  294%
  295propagate_prefix(M, X, X):- M==[], !.
  296propagate_prefix(M, once(X), once(M:X)).
  297propagate_prefix(M, (X, Y), (M:X, M:Y)).
  298propagate_prefix(M, (X; Y), (M:X; M:Y)).
  299propagate_prefix(M, (X -> Y), (M:X -> M:Y)).
  300propagate_prefix(M, \+(X), \+(M:X)).
  301
  302%
  303% prefix_cancellable(=(_,_)).  % attributes unify_hook
  304prefix_cancellable(!).
  305prefix_cancellable(true).
  306prefix_cancellable(false).
  307
  308%
  309optimize_call_N(X, Y):- slim_call(X, Y).
  310optimize_call_N(X, X).
  311
  312%
  313slim_call(X, Y) :-	canonical_prefix_form(X, M, X0),
  314					reducible_call(X0),
  315					slim_call(X0, M, Y).
  316
  317%
  318reducible_call(X) :- X=..[F, A|_],
  319				  (F == call; F == apply),
  320				  prefix_nonvar(A).
  321
  322% ?- slim_call(apply(a(b), [c,d]), [], R).
  323% ?- slim_call(apply(F, [a,b]), [], R).
  324% ?- slim_call(call(call(p(a), b)), m, X).
  325% ?- slim_call(a, [], Y).
  326% ?- slim_call(A, M, Y).
  327% ?- slim_call(call(f, a, b), m, Y).
  328% ?- slim_call(call(call(f), a, b), m, Y).
  329% ?- slim_call(apply(call(f), [a,b]), m, Y).
  330
  331slim_call(X, M, call(Y)):- var(X), !,
  332	attach_prefix(M, X, Y).
  333slim_call(M:X, _, Y):-!, slim_call(X, M, Y).
  334slim_call(X, M, Y):- X =..[call, F|As], !,
  335	slim_call(F, M, F0),
  336	complete_args(F0, As, Y).
  337slim_call(apply(F, As), M, Y):-
  338	slim_call(F, M, F0),
  339	complete_args(F0, As, Y).
  340slim_call(apply(F), M, Y):-
  341	slim_call(F, M, Y).
  342slim_call(X, M, Y):- attach_prefix(M, X, Y).
  343
  344% [2015/03/04] various attach-prefixes integrated.
  345%%  attach_prefix(M, X, Y) is det.
  346%	Y is unified with X attached prefix M.
  347
  348attach_prefix(M, X, Y):- var(X), !,
  349		( var(M), Y = M:X
  350		; M == [], Y = X
  351		; Y = M:X
  352		),
  353		!.
  354attach_prefix(_, X, X)  :- integer(X), !.
  355attach_prefix(_, X, X)  :- string(X), !.
  356attach_prefix(_, X, X)	:- X = (_:_), !.
  357attach_prefix(M, X, X)	:- M == [], !.
  358attach_prefix(M, X, M:X).
  359
  360% Let E be a system of equations:
  361%	m1 = t1
  362%	m2 = t2
  363%	...
  364%	mr  = tr
  365% The following conditions are equivalent.
  366% 1.  E has a solution such that no variable x that appears in some
  367%	ti is not affected by the unification.
  368% 2.  The list [m1,...,mr] subsumes the list [t1,...,tr]
  369
  370% ?- reduce_subsumes(f(a, b), f(a,  Q), R).
  371%@ R = (a==a,b==Q,true).
  372% ?- reduce_subsumes(f(a, b), f(a,  Q), R), call(R).
  373%@ false.
  374% ?- reduce_subsumes(f(a, B), f(a,  b), R), call(R).
  375%@ B = b,
  376
  377reduce_subsumes(X, Y, G):- collect_subsumes(X, Y, G),
  378	check_subsumes_throw(G).
  379
  380reduce_subsumes(N, X, Y, G):- collect_subsumes(N, X, Y,true,G),
  381	check_subsumes_throw(G).
  382
  383check_subsumes_throw(G):- unzip_equality(G, L, R),
  384	(	subsumes_term(L, R)
  385	->	true
  386	;	throw(error('reduce_subsumes rule'))
  387	).
  388
  389%
  390collect_subsumes(X, Y, X = Y):- var(X), !.
  391collect_subsumes(X, Y, X == Y):- atomic(X), !.
  392collect_subsumes(X, Y, (nonvar(Y), Y=Y0, G)):- var(Y), !,
  393	functor(X, F, N),
  394	functor(Y0, F, N),
  395	collect_subsumes(N, X, Y0, true, G).
  396collect_subsumes(X, Y, G):- functor(X, F, N),
  397	functor(Y, F, N),
  398	!,
  399	collect_subsumes(N, X, Y, true, G).
  400
  401collect_subsumes(0, _, _, G, G):-!.
  402collect_subsumes(J, X, T, G0, G):- arg(J, X, A),
  403	arg(J, T, B),
  404	collect_subsumes(A, B, H),
  405	K is J - 1,
  406	collect_subsumes(K, X, T, (H, G0), G).
  407
  408% ?- unzip_equality((a=b, c=d), P, Q).
  409unzip_equality(E, P, Q):- unzip_equal_dlist(E, []-P, []-Q), !.
  410%
  411unzip_equal_dlist((E,F), P-Q, R-S):- unzip_equal_dlist(E, P-T, R-U),
  412	unzip_equal_dlist(F, T-Q, U-S).
  413unzip_equal_dlist(X=Y, A-[X|A], B-[Y|B]).
  414unzip_equal_dlist(_, P-P, Q-Q)