
/*
  SIMPLIFY module

  copyright P. H. Roosen-Runge, 1992, 1994, 1998, 2003.

% Ver. 1.0:  January 1991.
%      1.2: April 16: trace option added.
%      1.3.1  March 18, 1992: puts A = -B into a canonical order
%                          so that i=-j is recognized as the same as -j=i.
%      1.3.2  July 8, 1992: assigned predicate defined.
%      1.4  November 11, 1993: makes associative expressions left-associative.
%      1.6.1 March 10: theory(Module) now loads rules in lexical order.
%      1.6.2 March 19: handles shift-operators, integer, and float; uses
%            memberchk.
%      1.6.3 September 4: 'or' and 'and' added to associative operators.
%      1.7   December 12, 1997: cancellation repaired. '.pl' changed to 
%            '.prolog'. prove(S) added.
%      1.7.1 December 28, 1998: left-associative cancellation added;
%             trace indents
%      1.8   February 7, 1999: commutative expressions are fully sorted;
%               x+1+y ->> y + x + 1.
%      2.0   Jan 1, 2000: generate associative and commutative rules
%      2.1   March 21: exclude '=' and '<>' from rearrange
%      2.1.1 August 4: but put X=Y and X<>Y into canonical order  
%      3.0   August 20: translate conditions in conditional rules
%      3.1   September 5: circular/1 repaired - handles (X-Y) ->> -(Y-X),
%               pretty printing for circular rules.
%      3.1.1 Nov. 10: circular/1 repaired to handle recursive rules.
%      3.2   Feb. 5, 2001: allow theory references in theory files.
%      3.3   August 6: canonical maps -X to 0-X to allow cancellation
%      3.4   Jan. 28, 2002: recompiled with getTheories 1.3
%      3.5   Feb. 12: replace bound variables with 'Vn'.
%      3.6   Feb. 17: collect commutative terms and their inverses
%             a-b+c+ e-d ->>  a+c+e-b-d
%      3.6SWI  December 22, 2006: SWI Prolog version
========================================================================
  Load this into any program which needs simplify/2.

  The calling program or data should load simplification rules
  by invoking or including terms of the form theory('<file specification>')>
  appropriate for the expressions being simplified.

*/

/* :- initialization(activate).   % gprolog */

:- dynamic('tracing/1').

error(X) :- write('!! '), write(X), nl.

:- ensure_loaded([ /* library(basics) do we need this? */
        qlib(arg), qlib(change_arg), qlib(same_functor),
        qlib(occurs), qlib(unify), qlib(samsort)]).

% SWI requires 2nd arg of arg/3 to be compound.
myarg(N, Term, Arg) :- compound(Term), arg(N, Term, Arg).


% from operators.pl

% For consistency, operator declarations used by wang, taut, simp, symbex, and
% quants.

:-op(999,xfx, '!'). % used to separate condition from current function.
:-op(995,xfx, '->>').  % simplification
:-op(995,xfy,'>>').    % sequent 
:-op(995,xfy, '::').  % separate parts of a quantified expression
:-op(990, yfx, iff).  % Left-associative (yfx) for consistency with 
                      % commutative arithmetic operators.
:-op(1199, xfx, if).  % separate condition from rule.                      

:-op(990,yfx,implies). % for consistency with iff
:-op(980,yfx, [or, cor]).
:-op(970,xfx,xor). % xor isn't associative.  force parenthesization.
:-op(960,yfx,[and, cand, div, mod]).
:-op(950,fy,not).
:-op(700,xfx,assigned).  % used in simplification. A safe 'is' operator.
:-op(700,xfy,['<=','<', '>', '>=', '<>', '==', '!=']).
:-op(200,xfy,'**').
:-op(200,xfy, in).  % used in quants.

% path defined in .plrc
:- ensure_loaded([lib(output), lib(condtrans)]).
:- multifile '->>'/2.
:- dynamic '->>'/2.
:- no_style_check(single_var). % to avoid warnings in rules.
:- dynamic tracing/1.  tracing(off). % initialize tracing.

:- ensure_loaded(lib('getTheories.pl')).

% expects error(X) to be defined in calling module

circular(L ->> R) :- 
	copy_term(L, Lnew),
	copy_term(R, Rnew), 
	sub_term(T, Rnew), subsumes_chk(Lnew, T) ->
           nl, 
	   write('!! '), prettyRule(L->> R, PR), 
	   write(PR), write(' is circular.'), nl. 

prettyRule(T, PT ->> PR) :-
	copy_term(T, Pretty),
        numbervars(Pretty, 0, _),    Pretty = (PT ->> PR).

addRuleLast((Rule if Condition)) :- 
	transcond(Condition, Translation),!,
	assertz((Rule :- Translation)),
       (makeARules(Rule, ARules),assertRule((ARules :- Translation), z); true),
       (makeCRule(Rule, CRule), assertz((CRule :- Translation)); true).

/*                                       
addRuleLast(Rule) :- 
	functor(Rule, '->>', 2), 
       (
         circular(Rule) 
        ;
	assertz(Rule),
       (makeARules(Rule, ARules), assertRule(ARules, z) ; true),
       (makeCRule(Rule, CRule), assertz(CRule) ; true)
       ).
*/
addRuleLast(theory(X)) :- theory(X). % if a theory, load it.
addRuleLast(Rule) :- assertz(Rule). % if not a rule or theory, assert it.

addRule((Rule if Condition)) :- 
	transcond(Condition, Translation),!,
        asserta((Rule :- Translation)),
       (makeARules(Rule, ARules), assertRule((ARules :- Translation), a)
       ; true),
       (makeCRule(Rule, CRule), asserta((CRule :- Translation)) ; true).

/*
addRule(Rule) :- 
        functor(Rule, '->>', 2),  
       (
         circular(Rule)
        ;
        asserta(Rule),
       (makeARules(Rule, ARules), assertRule(ARules, a) ; true),
       (makeCRule(Rule, CRule), asserta(CRule) ; true)
       ). 
*/	
addRule(Rule) :- asserta(Rule). % if not a rule, assert it.

makeCRule(Rule, CRule) :-
	functor(Rule, '->>', 2),
         arg(1, Rule, LHS), arg(2, Rule, RHS),
         functor(LHS, Op, 2), commutative(Op), !,
	 arg(1, LHS, Left), arg(2, LHS, Right),
	 CLHS =.. [Op, Right, Left],
	 CRule = (CLHS ->> RHS).

makeARules(Rule, ARules) :-
	functor(Rule, '->>', 2),
         arg(1, Rule, LHS), arg(2, Rule, RHS),
         functor(LHS, Op, 2), associativeF(Op), !,
         arg(1, LHS, Left), arg(2, LHS, Right),
         A1 =.. [Op, _0, Left],
         ALHS =.. [Op, A1, Right],
	 ARHS =.. [Op, _0, RHS],
         ARule = (ALHS ->> ARHS),
        (
         commutative(Op) ->
             AC1 =.. [Op, _0, Right],
	     ACLHS =.. [Op, AC1, Left],
	     ACRule = (ACLHS ->> ARHS),
	     ARules = [ARule, ACRule]
         ;
             ARules = [ARule]
         ).

assertRule(([Rule1, Rule2] :- Condition), End) :-
        End = z, assertz((Rule1 :- Condition)), assertz((Rule2 :- Condition))
       ;
	End = a, asserta((Rule1 :- Condition)), asserta((Rule2 :- Condition)).

assertRule([Rule1, Rule2], End) :-
        End = z, assertz(Rule1), assertz(Rule2)
       ;
        End = a, asserta(Rule1), asserta(Rule2).  

assertRule(([Rule] :- Condition), End) :-
        End = z, assertz((Rule :- Condition))
       ;
        End = a, asserta((Rule :- Condition)).

assertRule([Rule], End) :-
        End = z, assertz(Rule)
       ;
        End = a, asserta(Rule).  

/*
assertCanonical((LHS ->> RHS :- Condition)) :-
        canonical(LHS, CanLHS), asserta((CanLHS ->> RHS :- Condition)).
assertCanonical((LHS ->> RHS)) :- canonical(LHS, CanLHS),
        asserta((CanLHS ->> RHS)).
*/

associativeF(F) :- memberchk(F, ['+', '*', or, and]).

traceOn ->> true :- turnTraceOn.
traceOff ->> true :- turnTraceOff.
turnTraceOn :- (retract(tracing(off)); true), assert(tracing(on)).
turnTraceOff :- (retract(tracing(on)); true), assert(tracing(off)).

quantifier(Q) :- functor(Q, all, 1).
uncanonical(V) :-
	\+ (name(V, VS), append("V",NS, VS), name(N, NS), integer(N)).

boundVars(Term, N, Result) :-
        path_arg(Path, Term, Q),
	quantifier(Q), arg(1, Q, V::C::P), uncanonical(V),
        N1 is N + 1, N2 is N + 2,
        boundVars(C, N1, RC), boundVars(P, N2, RQ),
	functor(Q, F, 1),
	New =.. [F, V::RC::RQ],
	change_path_arg(Path, Term, NewTerm, New),
        name(N,NS), append("V",NS, VN), name(BN, VN),
        substitute(BN, NewTerm, V, Modified),
        !,
        boundVars(Modified, N, Result).
boundVars(Term, _, Term).

substitute(V, G, R, W) :-   % V for R in G
        setof(Path,path_arg(Path, G, R), Paths),
        changeAll(Paths, V, G, W), !.
substitute(_, G, _, G).

changeAll([Path | Rest], V, G, W) :-
        change_path_arg(Path, G, Modified, V), 
        changeAll( Rest, V, Modified, W).
changeAll(_, _, G, G).


canonical('-'(Term), 0-Term).
canonical(Term, Result) :- nonvar(Term) ->
         (functor(Term, F, 2),
         myarg(1, Term, A1), myarg(2, Term, A2),
         leftAssociative(F, A1, A2, LA1, LA2),
         canonical(LA1, C1), canonical(LA2, C2),
         (
	  reverseOp(F, ReverseF) -> Result =.. [ReverseF, C2, C1]      
	 ;
          Res =.. [F, C1, C2 ]
	 ), 
	 checkEq(Res, Res1),
	  (
	   commutative(F), rearrange(Res1, F, Result)
          ;
           Result = Res1
          )
         ).
canonical(Term, Result) :-
        nonvar(Term) -> 
	   Term =.. [F | Args],
	   canonicals(Args, CanArgs),
	   Result =.. [F | CanArgs].
canonical(X,X).

canonicals([], []).
canonicals([Arg | Rest], [CanArg | CanRest]) :-
	canonical(Arg, CanArg),
	canonicals(Rest, CanRest).

commutative(F) :- memberchk(F, ['+', '*', and, or, xor, iff, '=', '<>']),!.

reverseOp('>', '<').  reverseOp('>=', '<='). reverseOp('=>', '<=').

checkEq(Term, (-TH = TL)) :-           
       (Term = (X = -Y) ; Term = (-Y = X)),
        (Y @< X -> TH=X, TL=Y ; TL=X, TH=Y).
checkEq((X = Y), (L = R)) :-
        (Y@< X -> L=X, R=Y ; R=X, L=Y).
checkEq((X <> Y), (L <> R)) :-
        (Y@< X -> L=X, R=Y ; R=X, L=Y).
checkEq(X,X).                

leftAssociative(F, A1, A2, LA1, A22) :-
        associativeF(F),
        functor(A2, F, 2), arg(1, A2, A21), arg(2, A2, A22),
        LA1 =.. [F, A1, A21].
leftAssociative(_, A1, A2, A1, A2).

simplify(Term, Result) :-
	boundVars(Term, 0, NewTerm),
	simplify0(NewTerm, Simplified),
        canonical(Simplified, Canonical),
        simplify1(Canonical,Result).

% based on Quintus Prolog Library Manual, p. 40
simplify1(Expr, Final) :-
        path_arg(Path, Expr, Lhs),
        ( Lhs ->> Rhs ;  cancellator(Lhs, Rhs), Lhs \== Rhs),
        change_path_arg(Path, Expr, Modified, Rhs),
        !,
        (tracing(on) -> indent(1), write(Modified); true),
        canonical(Modified, Canonical),
        simplify1(Canonical, Final).
simplify1(Expr, Expr).
% N. B. simplify is not intended to fail, so prove(P) 
% cannot be just simplify(P, true).

simplify0(Expr, Final) :-
        path_arg(Path, Expr, Lhs),
        Lhs ->> Rhs ,
        change_path_arg(Path, Expr, Modified, Rhs),
        !,
        (tracing(on) -> indent(1), write(Modified); true),
        simplify0(Modified, Final).
simplify0(Expr, Expr).                               

assocInv('-', '+'). assocInv('/', '*').

cancellator(Expr, Result) :-
        functor(Expr, F, 2), assocInv(F, Inv),
        arg(1, Expr, Left), arg(2, Expr, A),
        canonical(Left, CL), canonical(A, CA),
        cancel(Inv, CL, CA, Expr, Result),!.
cancellator(Expr, Result) :- laCancel(Expr, Result).

laCancel(Expr, Result) :-
	Expr =.. [F, Left, Right],
	 assocInv(Inv, F),
	  laCancel( Left, Right, Inv, Result).
laCancel(Expr, Expr).

laCancel(Left, Right, Inv,  Result) :-
	   Left =.. [Inv, Next, Right], Result = Next 
	  ;
	   Left =.. [Op, NextLeft, NextRight], 
	   (Op = Inv ; assocInv(Inv, Op)),
	   laCancel(NextLeft, Right, Inv, NextResult),
	   (
	    NextLeft \== NextResult -> Result =.. [Op, NextResult, NextRight]
	   ;
	    assocInv(Inv, F),
            Result =.. [F, Left, Right]
	   ).

listify(Term, F, Result) :-
   commutative(F),
   listify(Term, F, [], Result).
listify(Term, _, Term).

listify(Term, Op, SoFar, Result) :-
   (
    Term =.. [Op, A1, A2],
    listify(A1, Op, SoFar, New),
    listify(A2, Op, New, Result)
   ;
     append(SoFar, [Term], Result)
           ).

listify(Term, F, Inv, Commutatives, Inverses) :-
   commutative(F), assocInv(Inv, F),
   listify(Term, F, Inv, [], [], Commutatives, Inverses).
listify(Term, _, _, Term, []).

listify(Term, F, Inv, SoFarComm, SoFarInv, Commutatives, Inverses) :-
   (
    Term =.. [F, A1, A2],
    listify(A1, F, Inv, SoFarCom, SoFarInv, NewComm, SoFarInv),
    listify(A2, F, Inv, NewComm, SoFarInv, Commutatives, Inverses)  
   ;
    Term =.. [Inv, A1, A2],
    listify(A1, F, Inv, SoFarComm, SoFarInv, SoFarComm, NewInv),
    listify(A2, F, Inv, SoFarCom, NewInv, Commutatives, Inverses)
   ;
     append(SoFarCom, [Term], Commutatives), Inverses = SoFarInv
   ).

rearrange(Term, F, Result) :-
   listify(Term, F,  List),
  (
   List = [_| _],
   samsort(List, Sorted),
   treeify(Sorted, F, Result)
  ;
   Result = List
 ).

treeify([T], _, T) .
treeify([T | Rest], F, Result) :- 
   treeify(Rest, F, Sofar),
   Result =.. [F, Sofar, T].
     
cancel('+', Expr, Expr, _, 0).  cancel('*', Expr, Expr, _, 1).
cancel(F, Left, A, _, Result) :-
        functor(Left, F, 2),
        (
         arg(1, Left, A) -> arg(2, Left, Result)
        ;
         arg(2, Left, A) -> arg(1, Left, Result)
        ;
         arg(1, Left, Left1), arg(2, Left, Left2),
         cancel(F, Left1, A, Left, Result1),
         (
          Result1 \== Left -> Result =..[F, Result1, Left2]
          ;
          cancel(F, Left2, A, Left, Result2),
          Result2 \== Left -> Result =.. [F, Left1, Result2]
         )
        ).
cancel(_, _, _, Expr, Expr).

prove(X=Y) :- number(X), number(Y), X == Y.
prove(X<>Y) :- number(X), number(Y), X =\= Y.
prove(Term) :- simplify(Term, STerm), !, STerm = true.
