/usr/lib/open-axiom/src/algebra/rule.spad is in open-axiom-source 1.4.1+svn~2626-2ubuntu2.
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 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 | --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.
)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,
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)
)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,
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 =>
l : List P
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
)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,
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
|