;
; Simple support for unification & pattern matching
; Chris Pressey, late January 2006
;
; This work is in the public domain. See the file UNLICENSE for more
; information.
;
;
; Return #t if the given pattern is a variable, #f otherwise.
;
(define pattern-var?
(lambda (pattern)
(vector? pattern))) ; just check that it is a vector
;
; Return the name of the given pattern variable.
;
(define get-pattern-var-name
(lambda (pattern-var)
(vector-ref pattern-var 0))) ; just return the 1st element of the vector
;
; Return the optional predicate associated with the given pattern
; variable, which determines what kind of (Scheme) terms it can
; unify with. If no predicate is associated with the variable,
; a dummy always-true predicate is returned.
;
(define get-pattern-var-pred
(lambda (pattern-var)
(cond ((< (vector-length pattern-var) 2)
(lambda (x) #t))
(else
(let ((term-type (vector-ref pattern-var 1)))
(cond ((eqv? term-type 'num)
(lambda (x) (number? x)))
((eqv? term-type 'sym)
(lambda (x) (symbol? x)))
(else
(lambda (x) #f))))))))
;
; Register that the named pattern variable should be associated with the given
; term in the given unifier. A new unifier containing the new variable-term
; association will be returned if possible; if it is not possible (i.e. the
; variable is already bound to a different term,) #f is returned.
;
(define bind-pattern-var
(lambda (term pattern unifier)
(let* ((var-name (get-pattern-var-name pattern))
(var-pred? (get-pattern-var-pred pattern))
(pair (assq var-name unifier)))
(cond
((not (var-pred? term))
#f)
((not (pair? pair)) ; if it's not in unifier,
(cons (cons var-name term) unifier)) ; add it up front
((eqv? (cdr pair) term) ; already bound to the given term: alright
unifier)
(else ; already bound to something else: not good
#f)))))
;
; Helper function.
; Given a term and a pattern, where we know both are lists,
; fold over both of them, unifying all the corresponding elements.
;
(define unify-lists
(lambda (term pattern unifier)
(cond ((and (null? term) (null? pattern)) ; end of both
unifier)
((or (null? term) (null? pattern)) ; end of one but not the other
#f)
(else
(let ((new-unifier (unify (car term) (car pattern) unifier)))
(if new-unifier
(unify-lists (cdr term) (cdr pattern) new-unifier)
#f))))))
;
; Return #f if the term does not unify with the pattern,
; or a list of substitutions if it does unify.
;
(define unify
(lambda (term pattern unifier)
(cond ((pattern-var? pattern)
(bind-pattern-var term pattern unifier))
((and (list? term) (list? pattern))
(unify-lists term pattern unifier))
((eqv? term pattern)
unifier)
(else
#f))))
;
; Given a pattern and a unifier (set of substitutions,) return a term
; where all the variables in the pattern have been replaced by their
; associated term in the unifier.
;
(define expand-vars
(lambda (pattern unifier)
(cond ((pattern-var? pattern) ; variable - replace if in unifier
(let* ((pair (assq (get-pattern-var-name pattern) unifier)))
(cond ((pair? pair)
(cdr pair))
(else
pattern))))
((list? pattern) ; list - recurse
(map (lambda (subpattern)
(expand-vars subpattern unifier))
pattern))
(else ; ground term - leave it alone.
pattern))))