Initial population.

1 files changed, 349 insertions, 0 deletions

diff --git a/src/algebra/rule.spad.pamphlet b/src/algebra/rule.spad.pamphlet
new file mode 100644
index 00000000..ce3011bc
--- /dev/null
+++ b/src/algebra/rule.spad.pamphlet
@@ -0,0 +1,349 @@
+\documentclass{article}
+\usepackage{axiom}
+\begin{document}
+\title{\$SPAD/src/algebra rule.spad}
+\author{Manuel Bronstein}
+\maketitle
+\begin{abstract}
+\end{abstract}
+\eject
+\tableofcontents
+\eject
+\section{domain RULE RewriteRule}
+<<domain RULE RewriteRule>>=
+)abbrev domain RULE RewriteRule
+++ Rules for the pattern matcher
+++ Author: Manuel Bronstein
+++ Date Created: 24 Oct 1988
+++ Date Last Updated: 26 October 1993
+++ Keywords: pattern, matching, rule.
+RewriteRule(Base, R, F): Exports == Implementation where
+  Base   : SetCategory
+  R      : Join(Ring, PatternMatchable Base, OrderedSet,
+                                 ConvertibleTo Pattern Base)
+  F      : Join(FunctionSpace R, PatternMatchable Base,
+                                 ConvertibleTo Pattern Base)
+
+  P    ==> Pattern Base
+
+  Exports ==>
+   Join(SetCategory, Eltable(F, F), RetractableTo Equation F) with
+    rule    : (F, F) -> $
+      ++ rule(f, g) creates the rewrite rule: \spad{f == eval(g, g is f)},
+      ++ with left-hand side f and right-hand side g.
+    rule    : (F, F, List Symbol) -> $
+      ++ rule(f, g, [f1,...,fn]) creates the rewrite rule
+      ++ \spad{f == eval(eval(g, g is f), [f1,...,fn])},
+      ++ that is a rule with left-hand side f and right-hand side g;
+      ++ The symbols f1,...,fn are the operators that are considered
+      ++ quoted, that is they are not evaluated during any rewrite,
+      ++ but just applied formally to their arguments.
+    suchThat: ($, List Symbol, List F -> Boolean) -> $
+      ++ suchThat(r, [a1,...,an], f) returns the rewrite rule r with
+      ++ the predicate \spad{f(a1,...,an)} attached to it.
+    pattern : $ -> P
+      ++ pattern(r) returns the pattern corresponding to
+      ++ the left hand side of the rule r.
+    lhs     : $ -> F
+      ++ lhs(r) returns the left hand side of the rule r.
+    rhs     : $ -> F
+      ++ rhs(r) returns the right hand side of the rule r.
+    elt     : ($, F, PositiveInteger) -> F
+      ++ elt(r,f,n) or r(f, n) applies the rule r to f at most n times.
+    quotedOperators: $ -> List Symbol
+      ++ quotedOperators(r) returns the list of operators
+      ++ on the right hand side of r that are considered
+      ++ quoted, that is they are not evaluated during any rewrite,
+      ++ but just applied formally to their arguments.
+
+  Implementation ==> add
+    import ApplyRules(Base, R, F)
+    import PatternFunctions1(Base, F)
+    import FunctionSpaceAssertions(R, F)
+
+    Rep := Record(pat: P, lft: F, rgt: F, qot: List Symbol)
+
+    mkRule      : (P, F, F, List Symbol) -> $
+    transformLhs: P -> Record(plus: F, times: F)
+    bad?        : Union(List P, "failed") -> Boolean
+    appear?     : (P, List P) -> Boolean
+    opt         : F -> P
+    F2Symbol    : F -> F
+
+    pattern x                == x.pat
+    lhs x                    == x.lft
+    rhs x                    == x.rgt
+    quotedOperators x        == x.qot
+    mkRule(pt, p, s, l)      == [pt, p, s, l]
+    coerce(eq:Equation F):$  == rule(lhs eq, rhs eq, empty())
+    rule(l, r)               == rule(l, r, empty())
+    elt(r:$, s:F) == applyRules([r pretend RewriteRule(Base, R, F)], s)
+
+    suchThat(x, l, f) ==
+      mkRule(suchThat(pattern x,l,f),  lhs x, rhs x, quotedOperators x)
+
+    x = y ==
+     (lhs x = lhs y) and (rhs x = rhs y) and
+        (quotedOperators x = quotedOperators y)
+
+    elt(r:$, s:F, n:PositiveInteger) ==
+      applyRules([r pretend RewriteRule(Base, R, F)], s, n)
+
+-- remove the extra properties from the constant symbols in f
+    F2Symbol f ==
+      l := select_!(symbolIfCan #1 case Symbol, tower f)$List(Kernel F)
+      eval(f, l, [symbolIfCan(k)::Symbol::F for k in l])
+
+    retractIfCan r ==
+      constant? pattern r =>
+        (u:= retractIfCan(lhs r)@Union(Kernel F,"failed")) case "failed"
+          => "failed"
+        F2Symbol(u::Kernel(F)::F) = rhs r
+      "failed"
+
+    rule(p, s, l) ==
+      lh := transformLhs(pt := convert(p)@P)
+      mkRule(opt(lh.times) * (opt(lh.plus) + pt),
+             lh.times * (lh.plus + p), lh.times * (lh.plus + s), l)
+
+    opt f ==
+      retractIfCan(f)@Union(R, "failed") case R => convert f
+      convert optional f
+
+-- appear?(x, [p1,...,pn]) is true if x appears as a variable in
+-- a composite pattern pi.
+    appear?(x, l) ==
+      for p in l | p ^= x repeat
+        member?(x, variables p) => return true
+      false
+
+-- a sum/product p1 @ ... @ pn is "bad" if it will not match
+-- a sum/product p1 @ ... @ pn @ p(n+1)
+-- in which case one should transform p1 @ ... @ pn to
+-- p1 @ ... @ ?p(n+1) which does not change its meaning.
+-- examples of "bad" combinations
+--   sin(x) @ sin(y)     sin(x) @ x
+-- examples of "good" combinations
+--   sin(x) @ y
+    bad? u ==
+      u case List(P) =>
+        for x in u::List(P) repeat
+          generic? x and not appear?(x, u::List(P)) => return false
+        true
+      false
+
+    transformLhs p ==
+      bad? isPlus p  => [new()$Symbol :: F, 1]
+      bad? isTimes p => [0, new()$Symbol :: F]
+      [0, 1]
+
+    coerce(x:$):OutputForm ==
+      infix(" == "::Symbol::OutputForm,
+            lhs(x)::OutputForm, rhs(x)::OutputForm)
+
+@
+\section{package APPRULE ApplyRules}
+<<package APPRULE ApplyRules>>=
+)abbrev package APPRULE ApplyRules
+++ Applications of rules to expressions
+++ Author: Manuel Bronstein
+++ Date Created: 20 Mar 1990
+++ Date Last Updated: 5 Jul 1990
+++ Description:
+++   This package apply rewrite rules to expressions, calling
+++   the pattern matcher.
+++ Keywords: pattern, matching, rule.
+ApplyRules(Base, R, F): Exports == Implementation where
+  Base   : SetCategory
+  R      : Join(Ring, PatternMatchable Base, OrderedSet,
+                                 ConvertibleTo Pattern Base)
+  F      : Join(FunctionSpace R, PatternMatchable Base,
+                                 ConvertibleTo Pattern Base)
+
+  P  ==> Pattern Base
+  PR ==> PatternMatchResult(Base, F)
+  RR ==> RewriteRule(Base, R, F)
+  K  ==> Kernel F
+
+  Exports ==> with
+    applyRules  : (List RR, F) -> F
+      ++ applyRules([r1,...,rn], expr) applies the rules
+      ++ r1,...,rn to f an unlimited number of times, i.e. until
+      ++ none of r1,...,rn is applicable to the expression.
+    applyRules  : (List RR, F, PositiveInteger) -> F
+      ++ applyRules([r1,...,rn], expr, n) applies the rules
+      ++ r1,...,rn to f a most n times.
+    localUnquote: (F, List Symbol) -> F
+      ++ localUnquote(f,ls) is a local function.
+
+  Implementation ==> add
+    import PatternFunctions1(Base, F)
+
+    splitRules: List RR -> Record(lker: List K,lval: List F,rl: List RR)
+    localApply  : (List K, List F, List RR, F, PositiveInteger) -> F
+    rewrite     : (F, PR, List Symbol) -> F
+    app         : (List RR, F) -> F
+    applist     : (List RR, List F) -> List F
+    isit        : (F, P) -> PR
+    isitwithpred: (F, P, List P, List PR) -> PR
+
+    applist(lrule, arglist)  == [app(lrule, arg) for arg in arglist]
+
+    splitRules l ==
+      ncr := empty()$List(RR)
+      lk  := empty()$List(K)
+      lv  := empty()$List(F)
+      for r in l repeat
+        if (u := retractIfCan(r)@Union(Equation F, "failed"))
+          case "failed" then ncr := concat(r, ncr)
+          else
+            lk := concat(retract(lhs(u::Equation F))@K, lk)
+            lv := concat(rhs(u::Equation F), lv)
+      [lk, lv, ncr]
+
+    applyRules(l, s) ==
+      rec := splitRules l
+      repeat
+        (new:= localApply(rec.lker,rec.lval,rec.rl,s,1)) = s => return s
+        s := new
+
+    applyRules(l, s, n) ==
+      rec := splitRules l
+      localApply(rec.lker, rec.lval, rec.rl, s, n)
+
+    localApply(lk, lv, lrule, subject, n) ==
+      for i in 1..n repeat
+        for k in lk for v in lv repeat
+          subject := eval(subject, k, v)
+        subject := app(lrule, subject)
+      subject
+
+    rewrite(f, res, l) ==
+      lk := empty()$List(K)
+      lv := empty()$List(F)
+      for rec in destruct res repeat
+        lk := concat(kernel(rec.key), lk)
+        lv := concat(rec.entry, lv)
+      localUnquote(eval(f, lk, lv), l)
+
+    if R has ConvertibleTo InputForm then
+      localUnquote(f, l) ==
+        empty? l => f
+        eval(f, l)
+    else
+      localUnquote(f, l) == f
+
+    isitwithpred(subject, pat, vars, bad) ==
+      failed?(u := patternMatch(subject, pat, new()$PR)) => u
+      satisfy?(u, pat)::Boolean => u
+      member?(u, bad) => failed()
+      for v in vars repeat addBadValue(v, getMatch(v, u)::F)
+      isitwithpred(subject, pat, vars, concat(u, bad))
+
+    isit(subject, pat) ==
+      hasTopPredicate? pat =>
+        for v in (l := variables pat) repeat resetBadValues v
+        isitwithpred(subject, pat, l, empty())
+      patternMatch(subject, pat, new()$PR)
+
+    app(lrule, subject) ==
+      for r in lrule repeat
+        not failed?(u := isit(subject, pattern r)) =>
+          return rewrite(rhs r, u, quotedOperators r)
+      (k := retractIfCan(subject)@Union(K, "failed")) case K =>
+        operator(k::K) applist(lrule, argument(k::K))
+      (l := isPlus  subject) case List(F) => +/applist(lrule,l::List(F))
+      (l := isTimes subject) case List(F) => */applist(lrule,l::List(F))
+      (e := isPower subject) case Record(val:F, exponent:Integer) =>
+        ee := e::Record(val:F, exponent:Integer)
+        f  := app(lrule, ee.val)
+        positive?(ee.exponent) => f ** (ee.exponent)::NonNegativeInteger
+        recip(f)::F ** (- ee.exponent)::NonNegativeInteger
+      subject
+
+@
+\section{domain RULESET Ruleset}
+<<domain RULESET Ruleset>>=
+)abbrev domain RULESET Ruleset
+++ Sets of rules for the pattern matcher
+++ Author: Manuel Bronstein
+++ Date Created: 20 Mar 1990
+++ Date Last Updated: 29 Jun 1990
+++ Description:
+++   A ruleset is a set of pattern matching rules grouped together.
+++ Keywords: pattern, matching, rule.
+Ruleset(Base, R, F): Exports == Implementation where
+  Base   : SetCategory
+  R      : Join(Ring, PatternMatchable Base, OrderedSet,
+                                 ConvertibleTo Pattern Base)
+  F      : Join(FunctionSpace R, PatternMatchable Base,
+                                 ConvertibleTo Pattern Base)
+
+  RR ==> RewriteRule(Base, R, F)
+
+  Exports ==> Join(SetCategory, Eltable(F, F)) with
+    ruleset: List RR -> $
+      ++ ruleset([r1,...,rn]) creates the rule set \spad{{r1,...,rn}}.
+    rules  : $ -> List RR
+      ++ rules(r) returns the rules contained in r.
+    elt    : ($, F, PositiveInteger) -> F
+      ++ elt(r,f,n) or r(f, n) applies all the rules of r to f at most n times.
+
+  Implementation ==> add
+    import ApplyRules(Base, R, F)
+
+    Rep := Set RR
+
+    ruleset l                        == {l}$Rep
+    coerce(x:$):OutputForm           == coerce(x)$Rep
+    x = y                            == x =$Rep y
+    elt(x:$, f:F)                    == applyRules(rules x, f)
+    elt(r:$, s:F, n:PositiveInteger) == applyRules(rules r, s, n)
+    rules x                          == parts(x)$Rep
+
+@
+\section{License}
+<<license>>=
+--Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd.
+--All rights reserved.
+--
+--Redistribution and use in source and binary forms, with or without
+--modification, are permitted provided that the following conditions are
+--met:
+--
+--    - Redistributions of source code must retain the above copyright
+--      notice, this list of conditions and the following disclaimer.
+--
+--    - Redistributions in binary form must reproduce the above copyright
+--      notice, this list of conditions and the following disclaimer in
+--      the documentation and/or other materials provided with the
+--      distribution.
+--
+--    - Neither the name of The Numerical ALgorithms Group Ltd. nor the
+--      names of its contributors may be used to endorse or promote products
+--      derived from this software without specific prior written permission.
+--
+--THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+--IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+--TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+--PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+--OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+--EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+--PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+--PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+--LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+--NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+--SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+@
+<<*>>=
+<<license>>
+
+<<domain RULE RewriteRule>>
+<<package APPRULE ApplyRules>>
+<<domain RULESET Ruleset>>
+@
+\eject
+\begin{thebibliography}{99}
+\bibitem{1} nothing
+\end{thebibliography}
+\end{document}