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
    8% reduce/[3,4]  by rules
    9% ?- reduce:reduce(math:desugar, -(a-b), X).
   10%@ X = -1* (a+ -1*b).
   11% ?- reduce:term_write(math:desugar, [],  -(+(a)-b), X).
   12%@ X = -1* (a+ -1*b).
   13% ?- reduce:term_write(math:desugar, (-);(+),  -(+(a)-b), X).
   14% ?- reduce:term_write(math:desugar, {-,+},  -(a), X).
   15
   16		/******************************************************************
   17		*     [2016/03/20]                                                *
   18		*     Regular expressions over signatures (S-Regex).              *
   19		*                                                                 *
   20		*     <S-Regex> -->                                               *
   21		*	  []                                                          *
   22		*     |	<atom>                                                    *
   23		*     |	<S-Regex>; <S-Regex>                                      *
   24		*     |	<S-Regex>, <S-Regex>                                      *
   25		*     |	\+ <S-Regex>                                              *
   26		*     |	<S-Regex>/N                                               *
   27		*     |	[N, N, ..., N]		(non-empty list)                      *
   28		*                                                                 *
   29		*     where <atom> is a prollog atom and N a positive integer.    *
   30		******************************************************************/
   31
   32:- meta_predicate reduce_one(2, 4, ?, ?).   33reduce_one(R, P, X, Y):- call(P, X, Y, S, S0),
   34	nonvar(S),				% [2010/03/05]
   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).
   43%
   44reduce(R, P, X, Y):- reduce_one(R, P, X, X0), !,
   45					 reduce(R, P, X0, Y).
   46reduce(_, _, X, X).
   47
   48%
   49term_rewrite(R, X, Y):- term_rewrite(R, [], X,Y).
   50%
   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
   55%%% The subtree relation is the transtive closure of child relation.
   56% subtree/[2,3,4,5]
   57% ?- reduce:subtree(a+b, X).
   58% ?- reduce:subtree(+, a*b+ c*d, X).
   59% ?- reduce:subtree(\+ (+), a*b+ c*d, X).
   60%@ X = a*b+c*d ;
   61% ?- reduce:subtree(\+ (-), a*b+ c*d, X).
   62% ?- reduce:subtree((+); (*)/2, a*b + c*d, X).
   63% ?- reduce:subtree(\+ ((+); []/2), a*b + c*d, X).
   64% ?- reduce:subtree({+, *}, a*b + c*d, X).
   65% ?- reduce:subtree(f(a,b), T, S, S0).
   66% ?- reduce:subtree(f, f(a, f(b,c)), X, Y, Z).
   67% ?- reduce:subtree(([], \+g),  f(a,g(b)), X, Y, Z).
   68% ?- reduce:subtree(\+g,  f(a,g(b)), X, Y, Z).
   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
   81% ?- reduce:subtree((f,[1,2]) ; (g, [1]), f(b,g(a)), X, Y, Z).
   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
   88% Get a child (backtrackable)
   89% ?- reduce:child([], a+b, X0, Y, Y0).
   90% ?- reduce:child(*, a+b, X0, Y, Y0).
   91
   92% ?- reduce:child((+)/1;(+)/2, a+b, X0, Y, Y0).
   93% ?- reduce:child((+)/1;(+)/2, a+b, X0, Y, Y0).
   94% ?- reduce:child((+)/3, a+b, X0, Y, Y0).
   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(+,+,+,+)).  107%  sng_index_chk(+Sgn, +F, +N,  +I): det.
  108%	True if (F, N, I) is an instance of Signature Sgn.
  109
  110% ?- reduce:sgn_index_chk(*, f, 3, 2).
  111% ?- reduce:sgn_index_chk([], f, 3, 2).
  112% ?- reduce:sgn_index_chk([], *, 3, 2).
  113% ?- reduce:sgn_index_chk(f, f, 3, 2).
  114% ?- reduce:sgn_index_chk(f, g, 3, 2).
  115% ?- reduce:sgn_index_chk((f/3,[1,3]), f, 3, 1).
  116% ?- reduce:sgn_index_chk(((g/2;f/3), [1,3]), f, 3, 1).
  117% ?- reduce:sgn_index_chk(\+ [], f, 3, 1).
  118% ?- reduce:sgn_index_chk(\+ ((*)/2), f, 3, 1).
  119% ?- reduce:sgn_index_chk(\+ ([]/2), f, 3, 1).
  120% ?- reduce:sgn_index_chk((*)/2, *, 2, 1).
  121% ?- reduce:sgn_index_chk([]/2, *, 2, 1).
  122
  123sgn_index_chk(X,Y,Z,U):- once(sgn_index(X,Y,Z,U)).
  124
  125:- meta_predicate(sgn_index(+,+,+,+)).  126
  127% '*' is a wild-card
  128% The null list [] is '*'-functor
  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
  143%
  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
  148% copy_args(J, I, X, T, T0) :-  T and T0 have the same children
  149% up to the J-th child except that the I-th child of T0 is X.
  150% ?- copy_args(3, 2, X, f(a,b,c), f(A,B,C)).
  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).
  161%
  162term_complete([], G, G):-!.
  163term_complete(A, G, G0):- G =.. H,
  164	append(H, A, H0),
  165	G0 =.. H0.
  166
  167% ?- complete_args(f(a), [b,c], X).
  168% ?- complete_args(user:m:F,[a,b], R).
  169% ?- complete_args([]:[]:F,[a,b], R).
  170% ?- complete_args([]:M:[]:F,[a,b], R).
  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		/***************************
  190		*     Simplifying Goals    *
  191		***************************/
  192
  193% some tiny.
  194%  C is safely supposed to be without a module prefix.
  195canonical_prefix_form(M:C, M, C).
  196canonical_prefix_form(C, [], C).
  197
  198% ?-  prefix_var(_:_).
  199prefix_var(X):- var(X),!.
  200prefix_var(_:X):- prefix_var(X).
  201
  202% ?-  prefix_nonvar(_:_).
  203prefix_nonvar(X):- nonvar(X), !,
  204				( X = _:Y  -> prefix_nonvar(Y)
  205				; true
  206				).
  207
  208% ?- module(reduce).
  209% Goal simplification for Prolog *operational* semantics !!
  210% ?- slim_goal((true, (fail-> X)), R).
  211% ?- slim_goal((true, (true-> X)), R).
  212% ?- slim_goal((A,true), R).
  213% ?- slim_goal((A,false), R).
  214% ?- slim_goal(true, R).
  215% ?- listing(slim_goal).
  216
  217
  218slim_goal(X, Y):- boole_rule(X, X0), !, slim_goal(X0, Y).
  219slim_goal(X, X).
  220
  221% Pseudo truth tables for goal simplification.
  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).
  236% boole_rule((_, false), false).		% Disabled.
  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
  257%
  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
  265%
  266% prefix_cancellable(=(_,_)).  % attributes unify_hook
  267prefix_cancellable(!).
  268prefix_cancellable(true).
  269prefix_cancellable(false).
  270
  271%
  272optimize_call_N(X, Y):- slim_call(X, Y).
  273optimize_call_N(X, X).
  274
  275%
  276slim_call(X, Y) :-	canonical_prefix_form(X, M, X0),
  277					reducible_call(X0),
  278					slim_call(X0, M, Y).
  279
  280%
  281reducible_call(X) :- X=..[F, A|_],
  282				  (F == call; F == apply),
  283				  prefix_nonvar(A).
  284
  285% ?- slim_call(apply(a(b), [c,d]), [], R).
  286% ?- slim_call(apply(F, [a,b]), [], R).
  287% ?- slim_call(call(call(p(a), b)), m, X).
  288% ?- slim_call(a, [], Y).
  289% ?- slim_call(A, M, Y).
  290% ?- slim_call(call(f, a, b), m, Y).
  291% ?- slim_call(call(call(f), a, b), m, Y).
  292% ?- slim_call(apply(call(f), [a,b]), m, Y).
  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
  307% [2015/03/04] various attach-prefixes integrated.
  308%%  attach_prefix(M, X, Y) is det.
  309%	Y is unified with X attached prefix M.
  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
  323% Let E be a system of equations:
  324%	m1 = t1
  325%	m2 = t2
  326%	...
  327%	mr  = tr
  328% The following conditions are equivalent.
  329% 1.  E has a solution such that no variable x that appears in some
  330%	ti is not affected by the unification.
  331% 2.  The list [m1,...,mr] subsumes the list [t1,...,tr]
  332
  333% ?- reduce_subsumes(f(a, b), f(a,  Q), R).
  334%@ R = (a==a,b==Q,true).
  335% ?- reduce_subsumes(f(a, b), f(a,  Q), R), call(R).
  336%@ false.
  337% ?- reduce_subsumes(f(a, B), f(a,  b), R), call(R).
  338%@ B = b,
  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
  352%
  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
  371% ?- unzip_equality((a=b, c=d), P, Q).
  372%@ P = [c,a],
  373%@ Q = [d,b].
  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)