## Tree @master (Download .tar.gz)

## forest-rewrite.scm @master — raw · history · blame

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 | ```
;
; Forest Rewriting
; Chris Pressey, late January 2006
;
; This work is in the public domain. See the file UNLICENSE for more
; information.
;
;
; Given a term, a pattern to look for in that term, a replacement pattern,
; and a unifier (set of substitutions,) determine if the term could be
; rewritten, and if so, return a vector consisting of:
;
; - a partially rewritten term. The replacement pattern is substituted into
; the term but WITHOUT the variables expanded into ground terms.
; - a (possibly new) unifier
;
; The rewrite process first recurses into the term's children (bottom-up
; rewriting.) If the given pattern fails to unify anywhere in the term,
; #f is returned.
;
(define partial-rewrite
(lambda (term pattern replacement unifier)
(cond ((list? term)
(let loop ((subterms term) ; first try to unify with each child
(acc '())) ; keep track of subterms we've seen
(cond ((null? subterms) ; no more children. lament failure.
(direct-partial-rewrite term pattern replacement unifier))
(else
(let* ((subterm (car subterms))
(rest (cdr subterms))
(result (partial-rewrite subterm pattern replacement unifier)))
(cond (result ; this child succeeded. pass along its result
(let* ((result-term (vector-ref result 0))
(result-unifier (vector-ref result 1))
(front (reverse acc))
(back (cons result-term rest))
(spliced-term (append front back)))
(vector spliced-term result-unifier)))
(else ; this child failed,
(loop rest (cons subterm acc))))))))) ; try the next one.
(else
(direct-partial-rewrite term pattern replacement unifier)))))
;
; Essentially a helper function for partial-rewrite; if the given
; pattern unifies with the given term, just return a vector containing
; the replacement and the (updated) unifier, else return #f.
;
(define direct-partial-rewrite
(lambda (term pattern replacement unifier)
(let* ((new-unifier (unify term pattern unifier))) ; try to unify
(cond (new-unifier ; successfully unified, so rewrite
(vector replacement new-unifier))
(else
#f)))))
;
; Given a vector of terms with variable placeholders in them, and
; a unifier, modify the vector so that the variables are replaced
; by their respective replacements (substitutions) in the unifier,
; and return the modified vector.
;
(define expand-forest
(lambda (terms unifier)
(let loop ((terms terms)
(term-num (- (vector-length terms) 1)))
(cond ((< term-num 0)
terms)
(else
(let* ((term (vector-ref terms term-num))
(new-term (expand-vars term unifier))
(new-terms (vector-store terms term-num new-term))
(next-term-num (- term-num 1)))
(loop new-terms next-term-num)))))))
;
; Rewrite a vector of terms in tandem using a list of rules, with a
; shared unifier (so that variable matches are common to all terms.)
; Return a vector of rewritten terms, if the rule list matched, otherwise #f.
;
(define rewrite-terms-with-compound-rule
(lambda (original-terms original-compound-rule)
(let loop ((terms original-terms)
(compound-rule original-compound-rule)
(unifier '()))
(cond ((null? compound-rule) ; when we reach the end of the list,
(expand-forest terms unifier)) ; expand variables in all the new terms
(else
(let* ((rule (car compound-rule))
(rest-rules (cdr compound-rule))
(targ-term-no (vector-ref rule 0))
(pattern (vector-ref rule 1))
(replacement (vector-ref rule 2))
(term (vector-ref terms targ-term-no))
(result (partial-rewrite term pattern replacement unifier)))
(cond (result ; we matched. update term, and try the next rule
(let* ((new-term (vector-ref result 0))
(new-unifier (vector-ref result 1))
(new-terms (vector-store terms targ-term-no new-term)))
(loop new-terms rest-rules new-unifier)))
(else ; no match. abort the entire thing.
#f))))))))
;
; Given a vector(#2) of:
; a vector of terms, and
; a list of compound rules,
; rewrite all terms simultaneously with each of the compound rules.
; Rewriting a set of terms simultaneously means that the variables in the
; compound rule are shared across the terms, and will only unify with subterms
; that are common to all of the terms.
;
; Keep applying compound rules until there are none that apply any longer.
;
; Return a vector of terms so rewritten.
;
(define rewrite-forest
(lambda (everything)
(let* ((original-terms (vector-ref everything 0))
(all-compound-rules (vector-ref everything 1)))
(let loop ((terms original-terms)
(compound-rules all-compound-rules))
(cond ((null? compound-rules)
terms) ; terminate and return new termlist
(else
(let* ((compound-rule (car compound-rules))
(new-terms (rewrite-terms-with-compound-rule
terms compound-rule)))
(cond (new-terms ; successfully rewrote.
(loop new-terms all-compound-rules)) ; try again, using all compound-rules
(else
(loop terms (cdr compound-rules))))))))))) ; try again, using rest of compound-rules
``` |