git @ Cat's Eye Technologies Treacle / master src / reduce.scm
master

Tree @master (Download .tar.gz)

reduce.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
;
; Support for reducing terms via context-rewriting
; Chris Pressey, March 2008
;

; SPDX-FileCopyrightText: (c) 2008-2024 Chris Pressey, Cat's Eye Technologies
; This file is distributed under a 2-clause BSD license.  For more information see:
; SPDX-License-Identifier: LicenseRef-BSD-2-Clause-X-Treacle

;
; Given a rule (a pair of a pattern and a map of replacements,)
; apply the rule to the given subject.  If the pattern part of
; the rule matches the subject, replace the subterms that matched
; named subpatterns with the expanded replacement whose key in
; the map is that name.
;
(define apply-rule
  (lambda (subject pattern replacements generation-id)
    (let* ((unifier (match subject subject pattern (mk-empty-unifier) (mk-base-index))))
      (if unifier
        (apply-unifier subject subject unifier unifier replacements generation-id)
        #f))))

;
; Helper function for apply-rule.  For each substitution in the unifier whose
; name is present in some replacement, expand that replacement with values from
; the unifier, and graft it into the subject at the position given in the unifier.
;
(define apply-unifier
  (lambda (complete-subject subject complete-unifier unifier replacements generation-id)
    (if (null? unifier)
      subject
      (let* ((unif-pair         (car unifier))
             (rest-of-unif      (cdr unifier))
             (name              (car unif-pair))
             (index             (cdr unif-pair))
             (repl-pair         (assq name replacements)))
        (if repl-pair
          (let* ((replacement   (cdr repl-pair))
                 (expanded-repl (expand-vars complete-subject replacement complete-unifier generation-id))
                 (new-subject   (term-index-store subject index expanded-repl)))
            (apply-unifier complete-subject new-subject complete-unifier rest-of-unif replacements generation-id))
          (apply-unifier complete-subject subject complete-unifier rest-of-unif replacements generation-id))))))

;
; Given a set of rules, apply repeatedly to subject until none apply.
;
(define reduce
  (lambda (subject complete-rules rules generation-id)
    (if (null? rules)
      subject
      (let* ((rule-pair     (car rules))
             (rest-of-rules (cdr rules))
             (pattern       (car rule-pair))
             (replacements  (cdr rule-pair))
             (new-gen-id    (+ generation-id 1))
             (new-subject   (apply-rule subject pattern replacements generation-id)))
        (if new-subject
          (reduce new-subject complete-rules complete-rules new-gen-id)
          (reduce subject complete-rules rest-of-rules new-gen-id))))))

;
; Useful shortcut for calling reduce.
;
(define toplevel-reduce
  (lambda (subject complete-rules)
    (reduce subject complete-rules complete-rules 0)))