/usr/share/axiom-20170501/src/algebra/RULE.spad is in axiom-source 20170501-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 | )abbrev domain RULE RewriteRule
++ Author: Manuel Bronstein
++ Date Created: 24 Oct 1988
++ Date Last Updated: 26 October 1993
++ Description:
++ Rules for the pattern matcher
RewriteRule(Base, R, F) : SIG == CODE where
Base : SetCategory
R : Join(Ring, PatternMatchable Base, OrderedSet,ConvertibleTo Pattern Base)
F : Join(FunctionSpace R, PatternMatchable Base, ConvertibleTo Pattern Base)
P ==> Pattern Base
SIG ==> 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.
++
++X logrule := rule log(x) + log(y) == log(x*y)
++X f := log(sin(x)) + log(x)
++X logrule f
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.
CODE ==> 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_!(z+->symbolIfCan z 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)
|