;
; 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))))