1-- Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd. 2-- All rights reserved. 3-- 4-- Redistribution and use in source and binary forms, with or without 5-- modification, are permitted provided that the following conditions are 6-- met: 7-- 8-- - Redistributions of source code must retain the above copyright 9-- notice, this list of conditions and the following disclaimer. 10-- 11-- - Redistributions in binary form must reproduce the above copyright 12-- notice, this list of conditions and the following disclaimer in 13-- the documentation and/or other materials provided with the 14-- distribution. 15-- 16-- - Neither the name of The Numerical ALgorithms Group Ltd. nor the 17-- names of its contributors may be used to endorse or promote products 18-- derived from this software without specific prior written permission. 19-- 20-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS 21-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED 22-- TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A 23-- PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER 24-- OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, 25-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, 26-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR 27-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF 28-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING 29-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS 30-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 31 32 33)package "BOOT" 34 35)if false 36Algorithms for Term Reduction 37 38The following assumptions are made: 39 40a term rewrite system is represented by a pair (varlist,varRules) where 41 varlist is the list of rewrite variables (test by MEMQ) and varRules 42 is an alist (no variables may occur in varRules) 43 44the following rewrite functions are available: 45 term1RW applies the first rule 46 47subCopy uses an alist (calls of ASSQ) to substitute a list structure 48 no left side of a pair of alist may appear on a righthand side 49 this means, subCopy is an idempotent function 50 51in both cases copying is only done if necessary to avoid destruction 52this means, EQ can be used to check whether something was done 53)endif 54 55term1RW(t,R) == 56 -- tries to reduce t at the top node 57 [vars,:varRules]:= R 58 for r in varRules until not (SL='failed) repeat 59 SL := termMatch(first r, t, NIL, vars) 60 not (SL='failed) => 61 t := subCopy(copy rest r, SL) 62 t 63 64term1RWall(t,R) == 65 -- same as term1RW, but returns a list 66 [vars,:varRules]:= R 67 [not (SL = 'failed) and subCopy(copy rest r, SL) for r in varRules | 68 not EQ(SL := termMatch(first r, t, NIL, vars), 'failed)] 69 70termMatch(tp,t,SL,vars) == 71 -- t is a term pattern, t a term 72 -- then the result is the augmented substitution SL or 'failed 73 tp=t => SL 74 atom tp => 75 MEMQ(tp,vars) => 76 p := assoc(tp, SL) => (rest p = t) 77 CONS(CONS(tp,t),SL) 78 'failed 79 atom t => 'failed 80 [tp1,:tp2]:= tp 81 [t1,:t2]:= t 82 SL:= termMatch(tp1,t1,SL,vars) 83 SL='failed => 'failed 84 tp2 and t2 => termMatch(tp2,t2,SL,vars) 85 tp2 or t2 => 'failed 86 SL 87 88 89--% substitution handling 90 91augmentSub(v,t,SL) == 92 -- destructively adds the pair (v,t) to the substitution list SL 93 -- t doesn't contain any of the variables of SL 94 q:= CONS(v,t) 95 null SL => [q] 96-- for p in SL repeat RPLACD(p, SUBSTQ(t, v, rest p)) 97 CONS(q,SL) 98 99mergeSubs(S1,S2) == 100 -- augments S2 by each pair of S1 101 -- S1 doesn't contain any of the variables of S2 102 null S1 => S2 103 null S2 => S1 104 S3 := [p for p in S2 | not ASSQ(first p, S1)] 105-- for p in S1 repeat S3 := augmentSub(first p, rest p, S3) 106 APPEND(S1,S3) 107 108subCopy(t,SL) == 109 -- t is any LISP structure, SL a substitution list for sharp variables 110 -- then t is substituted and copied if necessary 111 SL=NIL => t 112 subCopy0(t,SL) 113 114subCopy0(t, SL) == 115 p := subCopyOrNil(t, SL) => rest p 116 t 117 118subCopyOrNil(t,SL) == 119 -- the same as subCopy, but the result is NIL if nothing was copied 120 p:= assoc(t,SL) => p 121 atom t => NIL 122 [t1,:t2]:= t 123 t0:= subCopyOrNil(t1,SL) => 124 t2 => CONS(t, CONS(rest t0, subCopy0(t2, SL))) 125 CONS(t, CONS(rest t0, t2)) 126 t2 and (t0 := subCopyOrNil(t2, SL)) => CONS(t, CONS(t1, rest t0)) 127 NIL 128 129 130deepSubCopy(t,SL) == 131 -- t is any LISP structure, SL a substitution list for sharp variables 132 -- then t is substituted and copied if necessary 133 SL=NIL => t 134 deepSubCopy0(t,SL) 135 136deepSubCopy0(t, SL) == 137 p := deepSubCopyOrNil(t, SL) => rest p 138 t 139 140deepSubCopyOrNil(t,SL) == 141 -- the same as subCopy, but the result is NIL if nothing was copied 142 p := assoc(t, SL) => CONS(t, deepSubCopy0(rest p, SL)) 143 atom t => NIL 144 [t1,:t2]:= t 145 t0:= deepSubCopyOrNil(t1,SL) => 146 t2 => CONS(t, CONS(rest t0, deepSubCopy0(t2, SL))) 147 CONS(t, CONS(rest t0, t2)) 148 t2 and (t0 := deepSubCopyOrNil(t2, SL)) => CONS(t, CONS(t1, rest t0)) 149