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