; a unified matcher

(defpackage :unified-matcher
  (:nicknames :um)
  (:use :cl)
  (:export :unify :fail :subst-bind :if-match :with-bind))
(in-package um)

(defconstant fail (gensym "FAIL"))

(defun var? (symb)
  (and (symbolp symb)
       (eql (char (symbol-name symb) 0)
            #\?)))

; from `Paradigms of Artificial Intelligence Programming'
(defun unify (x y &optional bind)
  "See if x and y match with given bindings."
  (cond ((eql bind fail) fail)
        ((eql x y) bind)
        ((var? x) (unify-variable x y bind))
        ((var? y) (unify-variable y x bind))
        ((and (consp x) (consp y))
         (unify (cdr x) (cdr y)
                (unify (car x) (car y) bind)))
        (t fail)))

(defun unify-variable (var x bind)
  "Unify var with x, using (and maybe extending) bindings."
  (let ((b1 (assoc var bind)))
    (if b1
      (unify (cdr b1) x bind)
      (cons (cons var x) bind))))

(defun subst-bind (bind x)
  "Substitute the value of variables in bindings into x,
  taking recursively bound variables into account."
  (cond ((eql bind fail) fail)
        ((null bind) x)
        ((var? x)
         (let ((b1 (assoc x bind)))
           (if b1 (subst-bind bind (cdr b1)) x)))
        ((atom x) x)
        (t (cons (subst-bind bind (car x))
                 (subst-bind bind (cdr x))))))

(defun vars-in (sexp &optional (atom? #'atom))
  (if (funcall atom? sexp)
    (if (var? sexp) (list sexp))
    (union (vars-in (car sexp) atom?)
           (vars-in (cdr sexp) atom?))))

(defmacro if-match (pat seq then &optional else)
  (let ((gb (gensym))
        (vars (vars-in then)))
    `(let ((,gb (unify ,pat ,seq)))
       (if (eql ,gb fail)
         ,else
         (let ,(mapcar (lambda (v) `(,v (subst-bind ,gb ',v)))
                       vars)
           ,then)))))

(defmacro with-bind (bind &body body)
  (let ((vars (vars-in body))
        (gb (gensym)))
    `(let ((,gb ,bind))
       (let ,(mapcar (lambda (v) `(,v (subst-bind ,gb ',v)))
                     vars)
         ,@body))))
