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

Tree @master (Download .tar.gz)

unifier.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
;
; Support for matching of patterns containing contexts (holes)
; 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

;
; A traditional unifier is a set of (variable name, value) pairs indicating
; what value is bound to each variable name.  In our case, unifiers contain
; (name, term index) pairs which bind named to indices into the subject term.
; In a sense, conventional unifiers are unifiers "by value" while Treacle's
; are unifiers "by reference".
;
; Note also that in these unifiers, the same name can be bound to *multiple*
; positions within the subject, since the name may occur in any number of
; positions in the pattern, and will match as long as those subterms are
; equivalent.
;

;
; Create and return a new, empty unifier.
;
(define mk-empty-unifier
  (lambda ()
    '()))

;
; Extend the given unifier to one where the given name is associated with
; the given term index in the given subject term.  If such an extension is
; not possible (i.e. the name is already bound to an inequivalent term at
; a different index in the subject,) then #f is returned.
;
(define bind-name
  (lambda (subject index name unifier)
    (if (scour-unifier? subject index name unifier)
      (cons (cons name index) unifier)
      #f)))

;
; Helper function for bind-name.  Returns #t if it's OK to extend the
; unifier with the given name->index association, #f otherwise
;
(define scour-unifier?
  (lambda (subject index name unifier)
    (cond
      ((null? unifier)
        #t)
      (else
        (let* ((pair        (car unifier))
               (bound-name  (car pair))
               (bound-index (cdr pair)))
          (cond
            ((not (eq? name bound-name))
              (scour-unifier? subject index name (cdr unifier)))
            ((eqv? index bound-index) ; already bound to same place: ok
              (scour-unifier? subject index name (cdr unifier)))
            ((eqv? (term-index-fetch subject index) ; already bound to equiv
                   (term-index-fetch subject (cdr pair))) ; term: alright
              (scour-unifier? subject index name (cdr unifier)))
            (else                ; already bound to something else: not good
              #f)))))))

;
; Given a subject, a replacement, and a unifier, return a term which is like
; the replacement except where where each of the placeholders in the replacement
; has been replaced by the associated term referenced in the unifier.
;
(define expand-vars
  (lambda (subject replacement unifier generation-id)
    (cond ((is-named? replacement)      ; variable - replace if in unifier
            (let* ((pair (assq (get-name replacement) unifier)))
              (cond ((pair? pair)
                      (term-index-fetch subject (cdr pair)))
                    (else
                      replacement))))
          ((is-newref? replacement)
            (string->symbol (string-append "unique-ref-" (number->string generation-id))))
          ((list? replacement)          ; list - recurse
            (map (lambda (subpattern)
                   (expand-vars subject subpattern unifier generation-id))
                 replacement))
          (else                         ; ground term - leave it alone.
            replacement))))