home *** CD-ROM | disk | FTP | other *** search
/ ftp.cs.yorku.ca 2015 / ftp.cs.yorku.ca.tar / ftp.cs.yorku.ca / pub / peter / SVT / SWI / simp.pl < prev    next >
Text File  |  2006-12-25  |  13KB  |  410 lines
  1.  
  2. /*
  3.   SIMPLIFY module
  4.  
  5.   copyright P. H. Roosen-Runge, 1992, 1994, 1998, 2003.
  6.  
  7. % Ver. 1.0:  January 1991.
  8. %      1.2: April 16: trace option added.
  9. %      1.3.1  March 18, 1992: puts A = -B into a canonical order
  10. %                          so that i=-j is recognized as the same as -j=i.
  11. %      1.3.2  July 8, 1992: assigned predicate defined.
  12. %      1.4  November 11, 1993: makes associative expressions left-associative.
  13. %      1.6.1 March 10: theory(Module) now loads rules in lexical order.
  14. %      1.6.2 March 19: handles shift-operators, integer, and float; uses
  15. %            memberchk.
  16. %      1.6.3 September 4: 'or' and 'and' added to associative operators.
  17. %      1.7   December 12, 1997: cancellation repaired. '.pl' changed to 
  18. %            '.prolog'. prove(S) added.
  19. %      1.7.1 December 28, 1998: left-associative cancellation added;
  20. %             trace indents
  21. %      1.8   February 7, 1999: commutative expressions are fully sorted;
  22. %               x+1+y ->> y + x + 1.
  23. %      2.0   Jan 1, 2000: generate associative and commutative rules
  24. %      2.1   March 21: exclude '=' and '<>' from rearrange
  25. %      2.1.1 August 4: but put X=Y and X<>Y into canonical order  
  26. %      3.0   August 20: translate conditions in conditional rules
  27. %      3.1   September 5: circular/1 repaired - handles (X-Y) ->> -(Y-X),
  28. %               pretty printing for circular rules.
  29. %      3.1.1 Nov. 10: circular/1 repaired to handle recursive rules.
  30. %      3.2   Feb. 5, 2001: allow theory references in theory files.
  31. %      3.3   August 6: canonical maps -X to 0-X to allow cancellation
  32. %      3.4   Jan. 28, 2002: recompiled with getTheories 1.3
  33. %      3.5   Feb. 12: replace bound variables with 'Vn'.
  34. %      3.6   Feb. 17: collect commutative terms and their inverses
  35. %             a-b+c+ e-d ->>  a+c+e-b-d
  36. %      3.6SWI  December 22, 2006: SWI Prolog version
  37. ========================================================================
  38.   Load this into any program which needs simplify/2.
  39.  
  40.   The calling program or data should load simplification rules
  41.   by invoking or including terms of the form theory('<file specification>')>
  42.   appropriate for the expressions being simplified.
  43.  
  44. */
  45.  
  46. /* :- initialization(activate).   % gprolog */
  47.  
  48. :- dynamic('tracing/1').
  49.  
  50. error(X) :- write('!! '), write(X), nl.
  51.  
  52. :- ensure_loaded([ /* library(basics) do we need this? */
  53.         qlib(arg), qlib(change_arg), qlib(same_functor),
  54.         qlib(occurs), qlib(unify), qlib(samsort)]).
  55.  
  56. % SWI requires 2nd arg of arg/3 to be compound.
  57. myarg(N, Term, Arg) :- compound(Term), arg(N, Term, Arg).
  58.  
  59.  
  60. % from operators.pl
  61.  
  62. % For consistency, operator declarations used by wang, taut, simp, symbex, and
  63. % quants.
  64.  
  65. :-op(999,xfx, '!'). % used to separate condition from current function.
  66. :-op(995,xfx, '->>').  % simplification
  67. :-op(995,xfy,'>>').    % sequent 
  68. :-op(995,xfy, '::').  % separate parts of a quantified expression
  69. :-op(990, yfx, iff).  % Left-associative (yfx) for consistency with 
  70.                       % commutative arithmetic operators.
  71. :-op(1199, xfx, if).  % separate condition from rule.                      
  72.  
  73. :-op(990,yfx,implies). % for consistency with iff
  74. :-op(980,yfx, [or, cor]).
  75. :-op(970,xfx,xor). % xor isn't associative.  force parenthesization.
  76. :-op(960,yfx,[and, cand, div, mod]).
  77. :-op(950,fy,not).
  78. :-op(700,xfx,assigned).  % used in simplification. A safe 'is' operator.
  79. :-op(700,xfy,['<=','<', '>', '>=', '<>', '==', '!=']).
  80. :-op(200,xfy,'**').
  81. :-op(200,xfy, in).  % used in quants.
  82.  
  83. % path defined in .plrc
  84. :- ensure_loaded([lib(output), lib(condtrans)]).
  85. :- multifile '->>'/2.
  86. :- dynamic '->>'/2.
  87. :- no_style_check(single_var). % to avoid warnings in rules.
  88. :- dynamic tracing/1.  tracing(off). % initialize tracing.
  89.  
  90. :- ensure_loaded(lib('getTheories.pl')).
  91.  
  92. % expects error(X) to be defined in calling module
  93.  
  94. circular(L ->> R) :- 
  95.     copy_term(L, Lnew),
  96.     copy_term(R, Rnew), 
  97.     sub_term(T, Rnew), subsumes_chk(Lnew, T) ->
  98.            nl, 
  99.        write('!! '), prettyRule(L->> R, PR), 
  100.        write(PR), write(' is circular.'), nl. 
  101.  
  102. prettyRule(T, PT ->> PR) :-
  103.     copy_term(T, Pretty),
  104.         numbervars(Pretty, 0, _),    Pretty = (PT ->> PR).
  105.  
  106. addRuleLast((Rule if Condition)) :- 
  107.     transcond(Condition, Translation),!,
  108.     assertz((Rule :- Translation)),
  109.        (makeARules(Rule, ARules),assertRule((ARules :- Translation), z); true),
  110.        (makeCRule(Rule, CRule), assertz((CRule :- Translation)); true).
  111.  
  112. /*                                       
  113. addRuleLast(Rule) :- 
  114.     functor(Rule, '->>', 2), 
  115.        (
  116.          circular(Rule) 
  117.         ;
  118.     assertz(Rule),
  119.        (makeARules(Rule, ARules), assertRule(ARules, z) ; true),
  120.        (makeCRule(Rule, CRule), assertz(CRule) ; true)
  121.        ).
  122. */
  123. addRuleLast(theory(X)) :- theory(X). % if a theory, load it.
  124. addRuleLast(Rule) :- assertz(Rule). % if not a rule or theory, assert it.
  125.  
  126. addRule((Rule if Condition)) :- 
  127.     transcond(Condition, Translation),!,
  128.         asserta((Rule :- Translation)),
  129.        (makeARules(Rule, ARules), assertRule((ARules :- Translation), a)
  130.        ; true),
  131.        (makeCRule(Rule, CRule), asserta((CRule :- Translation)) ; true).
  132.  
  133. /*
  134. addRule(Rule) :- 
  135.         functor(Rule, '->>', 2),  
  136.        (
  137.          circular(Rule)
  138.         ;
  139.         asserta(Rule),
  140.        (makeARules(Rule, ARules), assertRule(ARules, a) ; true),
  141.        (makeCRule(Rule, CRule), asserta(CRule) ; true)
  142.        ). 
  143. */    
  144. addRule(Rule) :- asserta(Rule). % if not a rule, assert it.
  145.  
  146. makeCRule(Rule, CRule) :-
  147.     functor(Rule, '->>', 2),
  148.          arg(1, Rule, LHS), arg(2, Rule, RHS),
  149.          functor(LHS, Op, 2), commutative(Op), !,
  150.      arg(1, LHS, Left), arg(2, LHS, Right),
  151.      CLHS =.. [Op, Right, Left],
  152.      CRule = (CLHS ->> RHS).
  153.  
  154. makeARules(Rule, ARules) :-
  155.     functor(Rule, '->>', 2),
  156.          arg(1, Rule, LHS), arg(2, Rule, RHS),
  157.          functor(LHS, Op, 2), associativeF(Op), !,
  158.          arg(1, LHS, Left), arg(2, LHS, Right),
  159.          A1 =.. [Op, _0, Left],
  160.          ALHS =.. [Op, A1, Right],
  161.      ARHS =.. [Op, _0, RHS],
  162.          ARule = (ALHS ->> ARHS),
  163.         (
  164.          commutative(Op) ->
  165.              AC1 =.. [Op, _0, Right],
  166.          ACLHS =.. [Op, AC1, Left],
  167.          ACRule = (ACLHS ->> ARHS),
  168.          ARules = [ARule, ACRule]
  169.          ;
  170.              ARules = [ARule]
  171.          ).
  172.  
  173. assertRule(([Rule1, Rule2] :- Condition), End) :-
  174.         End = z, assertz((Rule1 :- Condition)), assertz((Rule2 :- Condition))
  175.        ;
  176.     End = a, asserta((Rule1 :- Condition)), asserta((Rule2 :- Condition)).
  177.  
  178. assertRule([Rule1, Rule2], End) :-
  179.         End = z, assertz(Rule1), assertz(Rule2)
  180.        ;
  181.         End = a, asserta(Rule1), asserta(Rule2).  
  182.  
  183. assertRule(([Rule] :- Condition), End) :-
  184.         End = z, assertz((Rule :- Condition))
  185.        ;
  186.         End = a, asserta((Rule :- Condition)).
  187.  
  188. assertRule([Rule], End) :-
  189.         End = z, assertz(Rule)
  190.        ;
  191.         End = a, asserta(Rule).  
  192.  
  193. /*
  194. assertCanonical((LHS ->> RHS :- Condition)) :-
  195.         canonical(LHS, CanLHS), asserta((CanLHS ->> RHS :- Condition)).
  196. assertCanonical((LHS ->> RHS)) :- canonical(LHS, CanLHS),
  197.         asserta((CanLHS ->> RHS)).
  198. */
  199.  
  200. associativeF(F) :- memberchk(F, ['+', '*', or, and]).
  201.  
  202. traceOn ->> true :- turnTraceOn.
  203. traceOff ->> true :- turnTraceOff.
  204. turnTraceOn :- (retract(tracing(off)); true), assert(tracing(on)).
  205. turnTraceOff :- (retract(tracing(on)); true), assert(tracing(off)).
  206.  
  207. quantifier(Q) :- functor(Q, all, 1).
  208. uncanonical(V) :-
  209.     \+ (name(V, VS), append("V",NS, VS), name(N, NS), integer(N)).
  210.  
  211. boundVars(Term, N, Result) :-
  212.         path_arg(Path, Term, Q),
  213.     quantifier(Q), arg(1, Q, V::C::P), uncanonical(V),
  214.         N1 is N + 1, N2 is N + 2,
  215.         boundVars(C, N1, RC), boundVars(P, N2, RQ),
  216.     functor(Q, F, 1),
  217.     New =.. [F, V::RC::RQ],
  218.     change_path_arg(Path, Term, NewTerm, New),
  219.         name(N,NS), append("V",NS, VN), name(BN, VN),
  220.         substitute(BN, NewTerm, V, Modified),
  221.         !,
  222.         boundVars(Modified, N, Result).
  223. boundVars(Term, _, Term).
  224.  
  225. substitute(V, G, R, W) :-   % V for R in G
  226.         setof(Path,path_arg(Path, G, R), Paths),
  227.         changeAll(Paths, V, G, W), !.
  228. substitute(_, G, _, G).
  229.  
  230. changeAll([Path | Rest], V, G, W) :-
  231.         change_path_arg(Path, G, Modified, V), 
  232.         changeAll( Rest, V, Modified, W).
  233. changeAll(_, _, G, G).
  234.  
  235.  
  236. canonical('-'(Term), 0-Term).
  237. canonical(Term, Result) :- nonvar(Term) ->
  238.          (functor(Term, F, 2),
  239.          myarg(1, Term, A1), myarg(2, Term, A2),
  240.          leftAssociative(F, A1, A2, LA1, LA2),
  241.          canonical(LA1, C1), canonical(LA2, C2),
  242.          (
  243.       reverseOp(F, ReverseF) -> Result =.. [ReverseF, C2, C1]      
  244.      ;
  245.           Res =.. [F, C1, C2 ]
  246.      ), 
  247.      checkEq(Res, Res1),
  248.       (
  249.        commutative(F), rearrange(Res1, F, Result)
  250.           ;
  251.            Result = Res1
  252.           )
  253.          ).
  254. canonical(Term, Result) :-
  255.         nonvar(Term) -> 
  256.        Term =.. [F | Args],
  257.        canonicals(Args, CanArgs),
  258.        Result =.. [F | CanArgs].
  259. canonical(X,X).
  260.  
  261. canonicals([], []).
  262. canonicals([Arg | Rest], [CanArg | CanRest]) :-
  263.     canonical(Arg, CanArg),
  264.     canonicals(Rest, CanRest).
  265.  
  266. commutative(F) :- memberchk(F, ['+', '*', and, or, xor, iff, '=', '<>']),!.
  267.  
  268. reverseOp('>', '<').  reverseOp('>=', '<='). reverseOp('=>', '<=').
  269.  
  270. checkEq(Term, (-TH = TL)) :-           
  271.        (Term = (X = -Y) ; Term = (-Y = X)),
  272.         (Y @< X -> TH=X, TL=Y ; TL=X, TH=Y).
  273. checkEq((X = Y), (L = R)) :-
  274.         (Y@< X -> L=X, R=Y ; R=X, L=Y).
  275. checkEq((X <> Y), (L <> R)) :-
  276.         (Y@< X -> L=X, R=Y ; R=X, L=Y).
  277. checkEq(X,X).                
  278.  
  279. leftAssociative(F, A1, A2, LA1, A22) :-
  280.         associativeF(F),
  281.         functor(A2, F, 2), arg(1, A2, A21), arg(2, A2, A22),
  282.         LA1 =.. [F, A1, A21].
  283. leftAssociative(_, A1, A2, A1, A2).
  284.  
  285. simplify(Term, Result) :-
  286.     boundVars(Term, 0, NewTerm),
  287.     simplify0(NewTerm, Simplified),
  288.         canonical(Simplified, Canonical),
  289.         simplify1(Canonical,Result).
  290.  
  291. % based on Quintus Prolog Library Manual, p. 40
  292. simplify1(Expr, Final) :-
  293.         path_arg(Path, Expr, Lhs),
  294.         ( Lhs ->> Rhs ;  cancellator(Lhs, Rhs), Lhs \== Rhs),
  295.         change_path_arg(Path, Expr, Modified, Rhs),
  296.         !,
  297.         (tracing(on) -> indent(1), write(Modified); true),
  298.         canonical(Modified, Canonical),
  299.         simplify1(Canonical, Final).
  300. simplify1(Expr, Expr).
  301. % N. B. simplify is not intended to fail, so prove(P) 
  302. % cannot be just simplify(P, true).
  303.  
  304. simplify0(Expr, Final) :-
  305.         path_arg(Path, Expr, Lhs),
  306.         Lhs ->> Rhs ,
  307.         change_path_arg(Path, Expr, Modified, Rhs),
  308.         !,
  309.         (tracing(on) -> indent(1), write(Modified); true),
  310.         simplify0(Modified, Final).
  311. simplify0(Expr, Expr).                               
  312.  
  313. assocInv('-', '+'). assocInv('/', '*').
  314.  
  315. cancellator(Expr, Result) :-
  316.         functor(Expr, F, 2), assocInv(F, Inv),
  317.         arg(1, Expr, Left), arg(2, Expr, A),
  318.         canonical(Left, CL), canonical(A, CA),
  319.         cancel(Inv, CL, CA, Expr, Result),!.
  320. cancellator(Expr, Result) :- laCancel(Expr, Result).
  321.  
  322. laCancel(Expr, Result) :-
  323.     Expr =.. [F, Left, Right],
  324.      assocInv(Inv, F),
  325.       laCancel( Left, Right, Inv, Result).
  326. laCancel(Expr, Expr).
  327.  
  328. laCancel(Left, Right, Inv,  Result) :-
  329.        Left =.. [Inv, Next, Right], Result = Next 
  330.       ;
  331.        Left =.. [Op, NextLeft, NextRight], 
  332.        (Op = Inv ; assocInv(Inv, Op)),
  333.        laCancel(NextLeft, Right, Inv, NextResult),
  334.        (
  335.         NextLeft \== NextResult -> Result =.. [Op, NextResult, NextRight]
  336.        ;
  337.         assocInv(Inv, F),
  338.             Result =.. [F, Left, Right]
  339.        ).
  340.  
  341. listify(Term, F, Result) :-
  342.    commutative(F),
  343.    listify(Term, F, [], Result).
  344. listify(Term, _, Term).
  345.  
  346. listify(Term, Op, SoFar, Result) :-
  347.    (
  348.     Term =.. [Op, A1, A2],
  349.     listify(A1, Op, SoFar, New),
  350.     listify(A2, Op, New, Result)
  351.    ;
  352.      append(SoFar, [Term], Result)
  353.            ).
  354.  
  355. listify(Term, F, Inv, Commutatives, Inverses) :-
  356.    commutative(F), assocInv(Inv, F),
  357.    listify(Term, F, Inv, [], [], Commutatives, Inverses).
  358. listify(Term, _, _, Term, []).
  359.  
  360. listify(Term, F, Inv, SoFarComm, SoFarInv, Commutatives, Inverses) :-
  361.    (
  362.     Term =.. [F, A1, A2],
  363.     listify(A1, F, Inv, SoFarCom, SoFarInv, NewComm, SoFarInv),
  364.     listify(A2, F, Inv, NewComm, SoFarInv, Commutatives, Inverses)  
  365.    ;
  366.     Term =.. [Inv, A1, A2],
  367.     listify(A1, F, Inv, SoFarComm, SoFarInv, SoFarComm, NewInv),
  368.     listify(A2, F, Inv, SoFarCom, NewInv, Commutatives, Inverses)
  369.    ;
  370.      append(SoFarCom, [Term], Commutatives), Inverses = SoFarInv
  371.    ).
  372.  
  373. rearrange(Term, F, Result) :-
  374.    listify(Term, F,  List),
  375.   (
  376.    List = [_| _],
  377.    samsort(List, Sorted),
  378.    treeify(Sorted, F, Result)
  379.   ;
  380.    Result = List
  381.  ).
  382.  
  383. treeify([T], _, T) .
  384. treeify([T | Rest], F, Result) :- 
  385.    treeify(Rest, F, Sofar),
  386.    Result =.. [F, Sofar, T].
  387.      
  388. cancel('+', Expr, Expr, _, 0).  cancel('*', Expr, Expr, _, 1).
  389. cancel(F, Left, A, _, Result) :-
  390.         functor(Left, F, 2),
  391.         (
  392.          arg(1, Left, A) -> arg(2, Left, Result)
  393.         ;
  394.          arg(2, Left, A) -> arg(1, Left, Result)
  395.         ;
  396.          arg(1, Left, Left1), arg(2, Left, Left2),
  397.          cancel(F, Left1, A, Left, Result1),
  398.          (
  399.           Result1 \== Left -> Result =..[F, Result1, Left2]
  400.           ;
  401.           cancel(F, Left2, A, Left, Result2),
  402.           Result2 \== Left -> Result =.. [F, Left1, Result2]
  403.          )
  404.         ).
  405. cancel(_, _, _, Expr, Expr).
  406.  
  407. prove(X=Y) :- number(X), number(Y), X == Y.
  408. prove(X<>Y) :- number(X), number(Y), X =\= Y.
  409. prove(Term) :- simplify(Term, STerm), !, STerm = true.
  410.