;;; -*- Syntax: common-lisp; Mode: LISP; Package: (unify :use (common-lisp util)); Base: 10 -*- 

(in-package 'user :use '(lisp))

;basic matching and unification are untyped.

;types, however, are also provided for.

(export '(match
	   apply-match
	   unify
	   apply-subst
	   fail
	   alpha-rename

	   type-declarations
	   make-declaration
	   expression-type
	   combination-type
	   well-typed-subst?
	   typed-match
	   typed-unify))



(defun match (exp1 exp2 &optional subst)
  (cond ((variable? exp1)
	 (let ((new-exp1 (cdr (assoc exp1 subst))))
	   (if new-exp1
	       (if (equal new-exp1 exp2)
		   subst
		   'fail)
	       (extend-subst exp1 exp2 subst))))
	((consp exp1)
	 (if (not (consp exp2))
	     'fail
	     (let ((subst2 (match (car exp1) (car exp2) subst)))
	       (if (eq subst2 'fail)
		   'fail
		   (match (cdr exp1) (cdr exp2) subst2)))))
	((eq exp1 exp2) subst)
	(t 'fail)))

(defun extend-subst (var value subst)
 (if (let ((type (get var 'symbol-type)))
       (and type
	    (not (eq type (expression-type value)))))
     'fail
     (cons (cons var value) subst)))

(defun apply-match (subst exp)
  (cond ((variable? exp)
	 (or (cdr (assoc exp subst))
	     exp))
	((consp exp)
	 (cons (apply-match subst (car exp))
	       (apply-match subst (cdr exp))))
	(t exp)))

(defun unify (exp1 exp2 &optional subst)
  (if (not (variable? exp1))
      (unify2 exp1 exp2 subst)
      (let ((new-exp1 (cdr (assoc exp1 subst))))
	(if new-exp1
	    (unify new-exp1 exp2 subst)
	    (unify2 exp1 exp2 subst)))))

(defun unify2 (clean-exp1 exp2 subst)
  (if (not (variable? exp2))
      (unify3 clean-exp1 exp2 subst)
      (let ((new-exp2 (cdr (assoc exp2 subst))))
	(if new-exp2
	    (unify2 clean-exp1 new-exp2 subst)
	    (unify3 clean-exp1 exp2 subst)))))

(defun unify3 (clean1 clean2 subst)
  (cond ((variable? clean1)
	 (bind clean1 clean2 subst))
	((variable? clean2)
	 (bind clean2 clean1 subst))
	((consp clean1)
	 (if (not (consp clean2))
	     'fail
	     (let ((new-subst (unify (car clean1) (car clean2) subst)))
	       (if (eq new-subst 'fail)
		   'fail
		   (unify (cdr clean1) (cdr clean2) new-subst)))))
	(t
	 (if (not (eq clean1 clean2))
	     'fail
	     subst))))

(defun bind (var value subst)
  (cond ((eq var value)
	 subst)
	((occurs-in? var value subst)
	 'fail)
	(t
	 (let ((new-subst (alpha-rename-subst value subst)))
	   (extend-subst var (apply-subst new-subst value) new-subst)))))

(defun occurs-in? (var value subst)
  (cond ((eq var value) t)
	((variable? value)
	 (let ((new-exp (cdr (assoc value subst))))
	   (if new-exp
	       (occurs-in? var new-exp subst)
	       nil)))
	((consp value)
	 (or (occurs-in? var (car value) subst)
	     (occurs-in? var (cdr value) subst)))
	(t nil)))

(defun alpha-rename-subst (exp &optional subst)
  (cond ((variable? exp)
	 (let ((new-exp (cdr (assoc exp subst))))
	   (if new-exp
	       (alpha-rename-subst new-exp subst)
	       (let ((newvar (gensym (concatenate 'string
						  (subseq (string exp)
							  0 (search "-" (string exp)))
						  "-"))))
		 (make-declaration newvar (get exp 'symbol-type))
		 (cons (cons exp newvar) subst)))))
	((consp exp)
	 (alpha-rename-subst (car exp) (alpha-rename-subst (cdr exp) subst)))
	(t
	 subst)))

(defun alpha-rename (exp)
  (gensym 1)
  (apply-subst (alpha-rename-subst exp) exp))

(defun apply-subst (subst exp)
  (cond ((variable? exp)
	 (let ((new-exp (cdr (assoc exp subst))))
	   (if new-exp
	       (apply-subst subst new-exp)
	       exp)))
	((consp exp)
	 (cons (apply-subst subst (car exp))
	       (apply-subst subst (cdr exp))))
	(t exp)))

(defun tunify (exp1 exp2)
  (let ((subst (unify exp1 exp2)))
    (if (eq subst 'fail)
	'fail
	(apply-subst subst exp1))))


(defmacro type-declarations (&body declarations)
  (let ((decl (gensym "DACEL-")))
    `(dolist (,decl ',declarations)
       (make-declaration (first ,decl) (second ,decl)))))

(defun make-declaration (symbol type)
  (setf (get symbol 'symbol-type) type))

(defun expression-type (expression)
  (if (symbolp expression)
      (let ((type (get expression 'symbol-type)))
	(unless type
	  (error "~s has no declared type" expression))
	type)
      (selectmatch (expression-type (first expression))
	((?input-types ?output-type)
	 (unless (= (length ?input-types) (length (cdr expression)))
	   (error "wrong number of arguments in ~s" expression))
	 (mapc (lambda (input input-type)
		 (unless (equal (expression-type input) input-type)
		   (error "~s is an illegal argument in ~s" input expression)))
	       (cdr expression)
	       ?input-types)
	 ?output-type))))

(defun combination-type (types)
  (selectmatch (first types)
    ((?input-types ?output-type)
     (when (and (= (length ?input-types) (length (cdr types)))
		(every #'equal
		       (cdr types)
		       ?input-types))
       ?output-type))))