/usr/share/axiom-20170501/src/algebra/APPRULE.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 | )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.
ApplyRules(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
PR ==> PatternMatchResult(Base, F)
RR ==> RewriteRule(Base, R, F)
K ==> Kernel F
SIG ==> with
applyRules : (List RR, F) -> F
++ applyRules([r1,...,rn], expr) applies the rules
++ r1,...,rn to f an unlimited number of times, 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.
CODE ==> 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
|