aboutsummaryrefslogtreecommitdiff
path: root/src/algebra/rule.spad.pamphlet
blob: 98e0ee8d1831afff07449351258c8433cc6be8c8 (plain)
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
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
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}