(in-package :vag :use '(lisp util))

;;<declaration> := <sort-decl> | <function-decl> | <subsort-spec> | <filter-spec>

;;<sort-decl> := (declare-sort <sort-name>)

(property-macro sort-name?)
(property-macro noticers)
(property-macro function-name?)
(property-macro arg-sorts)
(property-macro output-sort)
(defvar *component-table* (make-hash-table :test 'equal))
(defmacro components-of-sort (sort)
  `(gethash ',sort *component-table*))
(property-macro supersorts)
(property-macro subsorts)
(property-macro implementation)
(property-macro filter-predicate)
(property-macro vag-definition)
(property-macro production-noticers)

(defvar *production-noticers* nil)
(defvar *value-noticers* nil)

(defvar *using-external-interface* nil)
(defvar imp-package (make-package :imp))
(unuse-package :lisp imp-package)
(unuse-package :lucid-common-lisp imp-package)
(defvar *var-counter* 0)
(defvar *contradiction* nil)
(defvar *infinity* (expt 10 10))
(defvar *minus-infinity* (- (expt 10 10)))
(defvar *infinitetesimal* (expt 10 -10))
(defvar *connection-stack* nil)

(defmacro declare-sort (name)
  `(declare-sort-fun ',name))

(defun declare-sort-fun (name)
  (setf (sort-name? name) t))

;;<sort-exp> := <sort-name> | (list-of <sort-name>)

(defun sort? (exp)
  (if (symbolp exp)
      (sort-name? exp)
      (selectmatch exp
	((list-of ?base)
	 (sort? ?base))
	(:anything nil))))

;;<function-decl> := (declare-function (<function-name> <sort-exp>*) <sort-exp>)

(defmacro declare-function ((name &rest arg-sorts) output-sort)
  `(declare-function-fun ',name ',arg-sorts ',output-sort))

(defun vag-error (string &rest values)
  (if *using-external-interface*
      (throw 'vag-entry `(no ,(format nil string values)))
      (apply 'error string values)))

(defun declare-function-fun (name arg-sorts output-sort)
  (dolist (sort (cons output-sort arg-sorts))
    (unless (sort? sort)
      (vag-error "~s is not a sort" sort)))
  (setf (function-name? name) t)
  (push name (components-of-sort output-sort))
  (setf (arg-sorts name) arg-sorts)
  (setf (output-sort name) output-sort))

;;<subsort-specification> := (subsort <sort-name> <sort-name>)

(defun subsort? (sort1 sort2)
  (or (eq sort2 'anything)
      (selectmatch sort1
	((list-of ?base1)
	 (selectmatch sort2
	   ((list-of ?base2)
	    (subsort? ?base1 ?base2))
	   (:anything
	    nil)))
	(:anything
	 (symbol-subsort? sort1 sort2)))))

(defun symbol-subsort? (sort1 sort2)
  (and (symbolp sort1)
       (symbolp sort2)
       (or (eq sort1 sort2)
	   (some #'(lambda (super)
		     (symbol-subsort? super sort2))
		 (supersorts sort1)))))

;In the following two operations the sort returned is guaranteed
;to be a supersort of the desired sort.;returned is a supersort of the desired sort.

(defun sort-intersection (sort1 sort2)
  (cond ((and (consp sort1)
	      (consp sort2))
	 (let ((combined-arg (sort-intersection (second sort1) (second sort2))))
	   (when combined-arg
	     `(list-of ,combined-arg))))
	((subsort? sort1 sort2)
	 sort1)
	((subsort? sort2 sort1)
	 sort1)
	(t sort1)))

(defun sort-union (sort1 sort2)
  (cond ((and (consp sort1)
	      (consp sort2))
	 `(list-of ,(sort-union (second sort1) (second sort2))))
	((subsort? sort1 sort2)
	 sort2)
	((subsort? sort2 sort1)
	 sort1)
	(t 'anything)))

(defexportmacro subsort (sort1 sort2)
  `(subsort-fun ',sort1 ',sort2))

(defun subsort-fun (sort1 sort2)
  (unless (and (symbolp sort1)
	       (symbolp sort2))
    (error "attempt to declare subsort relation between non symbols"))
  (when (symbol-subsort? sort2 sort1)
    (error "attmept to create circular subtyping"))
  (push sort1 (subsorts sort2))
  (push sort2 (supersorts sort1)))

;;
;;<filter-specification> := (filter (<function-name> <variable>*) <expression>)
;;			  | (filter (<sort-name> <var>) <expression>)
;;
;;<expression> := <var> | <number> | (nil) | (cons <expression> <expression>)
;;                | (list <expression>*) | (<function-name> <expression>*)
;;

(defmacro filter ((name &rest args) boolean)
  `(filter-fun ',name ',args ',boolean))

(defun filter-fun (name args boolean)
  (unless (function-name? name)
    (vag-error "~s is not a sort name"))
  (well-sorted! boolean 'boolean)
  (setf (filter-predicate name) `(lambda ,args ,boolean)))

(defmacro vagprim (name output-sort args filter &rest body)
  (let ((implementation-name (intern (string name) imp-package)))
    `(eval-when (load compile eval)
      (declare-function (,name ,@(mapcar 'second args)) ,output-sort)
      (filter (,name ,@(mapcar 'first args)) ,filter)
      (defun ,implementation-name ,(mapcar 'first args)
	,@body)
      (setf (vag-definition ',name) nil)
      (setf (implementation ',name) ',implementation-name))))

(emacs-indent vagprim 4)

(defmacro vagdef (name output-sort args filter body)
  `(eval-when (load compile eval)
    (declare-function (,name ,@(mapcar 'second args)) ,output-sort)
    (well-sorted! ',body 'anything)
    (filter (,name ,@(mapcar 'first args)) ,filter)
    (setf (implementation ',name) nil)
    (setf (vag-definition ',name)
     '(lambda ,(mapcar 'car args) ,body))))

(emacs-indent vagdef 4)

(defun well-sorted! (expression sort &optional parent)
  (cond ((symbolp expression) t)
	((variablep expression) t)
	((numberp expression)
	 (unless (subsort? (number-sort expression) sort)
	   (vag-error "illegal numerical argument ~s" expression)))
	((and (consp expression) (eq (car expression) 'quote))
	 (unless (subsort? 'expression sort)
	   (vag-error "illegal expression argument ~s" expression)))
	(t (let* ((exp (vag-macro-expand expression))
		  (sort2 (find-sort exp)))
	     (cond ((member (car exp) '(cons car cdr map if))
		    (mapcar #'(lambda (arg) (well-sorted! arg 'anything))
			    (cdr exp)))
		   ((eq (car exp) 'lambda)
		    (unless (= (length exp) 3)
		      (vag-error "ill formed lambda expression ~s" expression))
		    (well-sorted! (third expression) 'anything))
		   (t
		    (unless (subsort? sort2 sort)
		      (if parent
			  (vag-error "ill sorted argument in ~s" parent)
			  (vag-error "~s is not of sort ~s" expression sort)))
		    (unless (function-name? (car exp))
		      (vag-error "undefined-operator ~s" (car exp)))
		    (unless (eq (length (cdr exp)) (length (arg-sorts (car exp))))
		      (vag-error "wrong number of arguments in ~s" expression))
		    (mapc #'(lambda (arg-exp arg-sort)
			      (well-sorted! arg-exp arg-sort expression))
			  (cdr exp)
			  (arg-sorts (car exp)))))))))

(defun number-sort (expression)
  (cond ((integerp expression) 'fixnum)
	((floatp expression) 'float)
	(t 'anything)))

(defun vag-macro-expand (expression)
  (selectmatch expression
    ((list ?first . ?rest)
     `(cons ,?first (list ,@?rest)))
    ((list)
     '(nil))
    ((and ?x ?y ?z . ?rest)
     `(and ,?x (and ,?y ,?z ,@?rest)))
    ((or ?x ?y ?z . ?rest)
     `(or ,?x (or ,?y ,?z ,@?rest)))
    (:anything expression)))

;the following finds a supersort.  In the worst case it just returns the sort anything.

(defun find-sort (exp)
  (cond ((integerp exp)
	 'fixnum)
	((floatp exp)
	 'float)
	((variablep exp) 'anything)
	((and (consp exp) (eq (car exp) 'quote))
	 'expression)
	((symbolp exp) 'anything)
	((not (consp exp)) (vag-error "illegal expression syntax"))
	(t (selectmatch (vag-macro-expand exp)
	     ((lambda . :anything) 'anything)
	     ((cons ?x ?y)
	      (sort-intersection `(list-of ,(find-sort ?x)) (find-sort ?y)))
	     ((car ?x)
	      (let ((xsort (find-sort ?x)))
		(selectmatch xsort
		  ((list-of ?s3)
		   ?s3)
		  (:anything 'anything))))
	     ((cdr ?x)
	      (let ((xsort (find-sort ?x)))
		(selectmatch xsort
		  ((list-of :anything)
		   xsort)
		  (:anything 'anything))))
	     ((map ?f :anything)
	      (setq ?f (if (variablep ?f) (var-value ?f) ?f))
	      (selectmatch ?f
		((lambda (:anything) ?body)
		 `(list-of ,(find-sort ?body)))
		(:anything (vag-error "a first argument to map is not a lambda expression"))))
	     ((if :anything ?x ?y)
	      (sort-union (find-sort ?x) (find-sort ?y)))
	     ((?f . :anything)
	      (or (output-sort ?f)
		  (vag-error "undefined operator ~s" ?f)))))))



;========================================================================
;The basic inference engine with congruence closure
;========================================================================

(defun declare-contradiction ()
  (format t "Contradition!!!!")
  (break)
  (setf-undo *contradiction* t))

(defun contradiction? ()
  *contradiction*)

(defstruct (variable (:predicate variablep)
		     (:conc-name var-)
		     (:print-function print-variable))
  sort
  index
  next-find
  defining-production
  productions-from
  productions-to
  properties
  value
  upper-bound
  lower-bound
  value-flag)

(defvar *var-table* (make-array 10000))

(defmacro var (n)
  `(aref *var-table* ,n))

(defun create-var (sort)
  (let ((var (make-variable :sort sort
			    :upper-bound *infinity*
			    :lower-bound *minus-infinity*))
	(index (incf *var-counter*)))
    (setf (var-index var) index)
    (setf (var index) var)))

(defun print-variable (self stream ignore)
  (declare (ignore ignore))
  (format stream "[~s ~s]" (var-index self) (var-expression self)))

(defun var-expression (var)
  (let ((def (var-defining-production var)))
    (cond ((and def (symbolp def)) def)
	  (def (cons (prod-fun def) (mapcar #'var-expression (prod-rhs def))))
	  ((var-value-flag var)
	   (let ((val (var-value var)))
	     (if (null val)
		 '(nil)
		 val)))
	  (t `(var ,(var-index var))))))

(defun var-find (var)
  (let ((next (var-next-find var)))
    (if next
	(var-find next)
	var)))

(defun list-find (val)
  (when val
    (if (consp val)
	(let* ((car-var (car val))
	       (car-var-find (var-find car-var))
	       (cdr-val (cdr val))
	       (cdr-list-find (list-find cdr-val)))
	  (if (and (eq car-var car-var-find)
		   (eq cdr-val cdr-list-find))
	      val
	      (cons car-var-find cdr-list-find)))
	(var-find val))))

(defvar *exp-table* (make-hash-table :test 'equal))

(defvar *value-table* (make-hash-table :test 'equal))

(defun vag-init ()
  (clrhash *exp-table*)
  (clrhash *value-table*)
  (clear-undo-stack)
  (setq *connection-stack* nil)
  (setq *contradiction* nil)
  (setq *var-counter* 1))

(defstruct (production (:predicate production?)
		       (:print-function print-production)
		       (:conc-name prod-))
  lhs
  fun
  rhs)

(defun print-production (prod stream ignore)
  (declare (ignore ignore))
  (format stream "[prod ~s ~s]" (var-index (prod-lhs prod)) (cons (prod-fun prod) (prod-rhs prod))))
		       
(defun prod-find (prod)
  (let* ((lhs (prod-lhs prod))
	 (rhs (prod-rhs prod))
	 (lhs-find (var-find lhs))
	 (rhs-find (list-find rhs)))
    (if (and (eq lhs lhs-find)
	     (eq rhs rhs-find))
	prod
	(make-production :lhs lhs-find :fun (prod-fun prod) :rhs rhs-find))))

(defun prod-equal (prod1 prod2)
  (and (eq (prod-fun prod1) (prod-fun prod2))
       (eq (prod-lhs prod1) (prod-lhs prod2))
       (equal (prod-rhs prod1) (prod-rhs prod2))))

(defun intern-exp (exp)
  (well-sorted! exp 'anything)
  (var-find (intern-exp2 exp)))

(defun intern-exp2 (exp)
  (cond ((variablep exp) exp)
	((symbolp exp)
	 (or (gethash exp *value-table*)
	     (let ((newvar (create-var 'anything)))
	       (setf-undo (gethash exp *value-table*) newvar)
	       (setf (var-defining-production newvar) exp)
	       newvar)))
	((numberp exp)
	 (or (gethash exp *value-table*)
	     (let* ((sort (cond ((integerp exp) 'fixnum)
				((floatp exp) 'float)
				(t (vag-error "illegal number type ~s" exp))))
		    (newvar (create-var sort)))
		 (set-value newvar exp)
		 (setf-undo (gethash exp *value-table*) newvar)
		 newvar)))
	((and (consp exp) (eq (car exp) 'quote))
	 (or (gethash (second exp) *value-table*)
	     (let ((newvar (create-var 'expression)))
	       (set-value newvar exp)
	       (setf-undo (gethash exp *value-table*) newvar)
	       newvar)))
	((and (consp exp) (eq (car exp) 'lambda))
	 (or (gethash (second exp) *value-table*)
	     (let ((newvar (create-var 'expression)))
	       (set-value newvar exp)
	       (setf-undo (gethash exp *value-table*) newvar)
	       newvar)))
	((consp exp)
	 (setq exp (vag-macro-expand exp))
	 (let ((fun (car exp)))
	   (unless (and (symbolp fun)
			(function-name? fun))
	     (vag-error "attempt to intern non-expression"))
	   (let ((arg-vars (mapcar #'intern-exp (cdr exp))))
	     (let* ((exp2 (cons fun arg-vars))
		    (prod (gethash exp2 *exp-table*)))
	       (if prod
		   (prod-lhs prod)
		   (let ((newvar (create-var (find-sort exp2))))
		     (setq prod (make-production :lhs newvar
						 :fun fun
						 :rhs arg-vars))
		     (setf-undo (gethash exp2 *exp-table*) prod)
		     (setf (var-productions-from newvar) (list prod))
		     (setf (var-defining-production newvar) prod)
		     (dolist (arg (cdr exp2))
		       (push-undo prod (var-productions-to arg)))
		     (notice-production prod)
		     (var-find newvar)))))))
	(t
	 (vag-error "unknown expression type ~s" exp))))

(defun beta-reduction (op args)
  (selectmatch op
    ((lambda ?argvars ?body)
     (let ((subst (mapcar 'cons ?argvars args)))
       (intern-exp (apply-vag-subst subst ?body))))))

(defun apply-vag-subst (subst exp)
  (cond ((symbolp exp)
	 (or (assoc-value exp subst)
	     exp))
	((or (numberp exp) (variablep exp) (and (consp exp) (eq (car exp) 'quote)))
	 exp)
	((consp exp)
	 (selectmatch exp
	   ((lambda ?args ?body)
	    `(lambda ,?args ,(apply-vag-subst
			      (remove-if
			       #'(lambda (cell) (member (car cell) ?args))
			       subst)
			      ?body)))
	   ((?f . ?args)
	    (cons ?f (mapcar #'(lambda (subexp) (apply-vag-subst subst subexp))
			     ?args)))))
	(t
	 (vag-error "unknown subexpression type in beta reduction"))))      

(defun equate-vars (var1 var2)
  (let ((find1 (var-find var1))
	(find2 (var-find var2)))
    (unless (eq find1 find2)
      (if (< (var-index find1) (var-index find2))
	  (set-next-find find2 find1)
	  (set-next-find find1 find2)))))

(defun set-next-find (var1 var2)
  (setf-undo (var-next-find var1) var2)
  (dolist (pcell (var-properties var1))
    (let ((prop (car pcell))
	  (values (cdr pcell)))
      (dolist (val values)
	(add-property var2 prop val))))
  (dolist (prod (var-productions-from var1))
    (add-production-from prod var2))
  (dolist (prod (var-productions-to var1))
    (congruence-check prod)
    (add-production-to prod var2))
  (set-upper-bound var2 (var-upper-bound var1))
  (set-lower-bound var2 (var-lower-bound var1))
  (when (var-value-flag var1)
    (set-value var2 (var-value var1))))

(defun congruence-check (prod)
  (let* ((exp (cons (prod-fun prod) (list-find (prod-rhs prod))))
	 (old-prod (gethash exp *exp-table*)))
    (if (null old-prod)
	(setf-undo (gethash exp *exp-table*) prod)
	(equate-vars (prod-lhs old-prod) (prod-lhs prod)))))

(defun add-production-to (prod var)
  (setq var (var-find var))
  (unless (member prod (var-productions-to var))
    (push prod (var-productions-to var))
    (notice-production prod)))

(defun add-production-from (prod var)
  (setq var (var-find var))
  (unless (member prod (var-productions-from var))
    (push prod (var-productions-from var))
    (notice-production prod)))

(defun notice-production (prod)
  (propagate-value-prod prod)
  (dolist (noticer *production-noticers*)
    (funcall noticer prod))
  (dolist (noticer (production-noticers (prod-fun prod)))
    (funcall noticer prod)))

(defun propagate-value-prod (prod)
  (let ((imp (implementation (prod-fun prod))))
    (when (and imp (every 'var-value-flag (prod-rhs prod)))
      (set-value (prod-lhs prod) (apply imp (mapcar 'var-value (prod-rhs prod)))))))

(defun set-value (var val)
  (setf var (var-find var))
  (if (var-value-flag var)
      (unless (or (equal (var-value var) val)
		  (and (numberp val)
		       (numberp (var-value var))
		       (< (abs (- val (var-value var))) (* 10 *infinitetesimal*))))
	(declare-contradiction))
      (progn
	(setf-undo (var-value-flag var) t)
	(setf-undo (var-value var) val)
	(propagate-value var val))))

(defun propagate-value (var val)
  (dolist (prod (var-productions-to var))
    (propagate-value-prod prod))
  (dolist (noticer *value-noticers*)
    (funcall noticer var val)))

(defvar *improv-req* .05)

(defun set-upper-bound (var bound)
  (setq var (var-find var))
  (if (< bound (var-lower-bound var))
      (declare-contradiction)
      (let* ((old-bound (var-upper-bound var))
	     (delta (- old-bound (var-lower-bound var))))
	(when (and (> delta 0)
		   (> (- old-bound bound) (* *improv-req* delta)))
	  (setf-undo (var-upper-bound var) bound)
	  (dolist (noticer (noticers 'upper-bound))
	    (funcall noticer var bound))))))

(defun set-lower-bound (var bound)
  (setq var (var-find var))
  (if (> bound (var-upper-bound var))
      (declare-contradiction)
      (let* ((old-bound (var-lower-bound var))
	     (delta (- (var-upper-bound var) old-bound)))
	(when (and (> delta 0)
		   (> (- bound old-bound) (* *improv-req* delta)))
	  (setf-undo (var-lower-bound var) bound)
	  (dolist (noticer (noticers 'lower-bound))
	    (funcall noticer var bound))))))

(defun add-property (var prop val)
  (setq var (var-find var))
  (unless (member val (assoc-value prop (var-properties var)))
    (push-undo val (assoc-value prop (var-properties var)))
    (dolist (noticer (noticers prop))
      (funcall noticer var val))))


;========================================================================
;defnoticer
;========================================================================

(defmacro defnoticer (name antecedents &rest body)
  (let ((valvar (gensym "VAR-")))
    (selectmatch (first antecedents)
      ((value ?var ?val)
       `(eval-when (compile load eval)
	 ,(clean-bindings `(defun ,name (,?var ,?val)
			    ,(process-antecedents (rest antecedents) body)))
	 (pushnew ',name *value-noticers*)))
      ((production ?var (?fun . ?args))
       (let ((prodvar (gensym "PROD-")))
	 `(eval-when (compile load eval)
	   ,(clean-bindings `(defun ,name (,prodvar)
			      (when (eq (prod-fun ,prodvar) ',?fun)
				(let ((,?var (var-find (prod-lhs ,prodvar))))
				  (let ((,valvar (prod-rhs ,prodvar)))
				    ,(make-bindings valvar ?args #'(lambda () (process-antecedents (rest antecedents) body))))))))
	   (pushnew ',name (production-noticers ',?fun)))))
      ((upper-bound ?var1 ?var2)
       `(eval-when (compile load eval)
	 ,(clean-bindings `(defun ,name (,?var1 ,?var2)
			    ,(process-antecedents (rest antecedents) body)))
	 (pushnew ',name (noticers 'upper-bound))))
      ((lower-bound ?var1 ?var2)
       `(eval-when (compile load eval)
	 ,(clean-bindings `(defun ,name (,?var1 ,?var2)
			   ,(process-antecedents (rest antecedents) body)))
	 (pushnew ',name (noticers 'lower-bound))))
      ((?var (?prop . ?args))
       `(eval-when (compile load eval)
	 ,(clean-bindings `(defun ,name (,?var ,valvar)
			   ,(make-bindings valvar ?args #'(lambda () (process-antecedents (rest antecedents) body)))))
	 (pushnew ',name (noticers ',?prop)))))))

(emacs-indent defnoticer 2)

(defun make-bindings (source args cont &optional avoid-var)
  (cond ((null args)
	 (funcall cont))
	((eq (car args) avoid-var)
	 (let ((var (gensym "VAR-")))
	   `(let ((,var ,source))
	     (when (eq (var-find (car ,var)) ,avoid-var)
	       ,(make-bindings `(cdr ,var) (cdr args) cont avoid-var)))))
	(t
	 (let ((temp (gensym "TEMP-")))
	   `(let ((,temp ,source))
	     (let ((,(first args) (var-find (car ,temp))))
	     ,(make-bindings `(cdr ,temp) (cdr args) cont avoid-var)))))))

(defun process-antecedents (antecedents body)
  (if (null antecedents)
      `(progn ,@body)
      (selectmatch (first antecedents)
	((value ?var ?val)
	 `(when (var-value-flag ,?var)
	   (let ((,?val (var-value ,?var)))
	     ,(process-antecedents (rest antecedents) body))))
	((production-from ?var (?fun . ?args))
	 (let ((prodvar (gensym "PROD-")))
	   `(dolist (,prodvar (var-productions-from ,?var))
	     (when (eq ',?fun (prod-fun ,prodvar))
	       ,(make-bindings `(prod-rhs ,prodvar) ?args
			       #'(lambda () (process-antecedents (rest antecedents) body)))))))
	((production-to ?var1 ?var2  (?fun . ?args))
	 (let ((prodvar (gensym "PROD-")))
	   `(dolist (,prodvar (var-productions-to ,?var1))
	     (when (eq ',?fun (prod-fun ,prodvar))
	       (let ((,?var2 (var-find (prod-lhs ,prodvar))))
		 ,(make-bindings `(prod-rhs ,prodvar) ?args
				 #'(lambda () (process-antecedents (rest antecedents) body))
				 ?var1))))))
	((upper-bound ?var1 ?var2)
	 `(let ((,?var2 (var-upper-bound ,?var1)))
	   ,(process-antecedents (rest antecedents) body)))
	((lower-bound ?var1 ?var2)
	 `(let ((,?var2 (var-lower-bound ,?var1)))
	   ,(process-antecedents (rest antecedents) body)))
	((when ?test)
	 `(when ,?test
	   ,(process-antecedents (rest antecedents) body)))
	((?var (?prop . ?args))
	 (let ((valvar (gensym "VAR-")))
	   `(dolist (,valvar (assoc-value ',?prop (var-properties ,?var)))
	     ,(make-bindings valvar ?args
	       #'(lambda () (process-antecedents (rest antecedents) body)))))))))

(defun clean-bindings (defun)
  (selectmatch defun
    ((defun ?name ?args . ?body)
     (let ((body2 (mapcar 'clean-bindings-internal ?body)))
       (let ((ignored-args (remove-if #'(lambda (arg) (internal-member arg body2))
				      ?args)))
	 `(defun ,?name ,?args ,@(when ignored-args `((declare (ignore ,@ignored-args)))) ,@body2))))))

(defun clean-bindings-internal (exp)
  (selectmatch exp
    ((let ((?var ?val)) ?exp2)
     (let ((exp3 (clean-bindings-internal ?exp2)))
       (if (internal-member ?var exp3)
	   `(let ((,?var ,?val)) ,exp3)
	   exp3)))
    ((dolist (?var ?val) ?exp2)
     (let ((exp3 (clean-bindings-internal ?exp2)))
       (if (internal-member ?var exp3)
	   `(dolist (,?var ,?val) ,exp3)
	   `(when ,?val ,exp3))))
    ((when ?test . ?body)
     `(when ,?test ,@(mapcar 'clean-bindings-internal ?body)))
    (:anything
     exp)))



;========================================================================
;debugging tools
;========================================================================

(defun pfrom (n)
  (rprint (var-productions-from (var-find (var n)))))

(defun pto (n)
  (rprint (var-productions-to (var-find (var n)))))

(defun value (n)
  (var-value (var-find (var n))))

(defun upper (n)
  (var-upper-bound (var-find (var n))))

(defun lower (n)
  (var-lower-bound (var-find (var n))))

(defun f (n)
  (var-find (var n)))

(defun prop (prop n)
  (rprint (assoc-value prop (var-properties (var-find (var n))))))



;========================================================================
;GLUE interface
;========================================================================

(defmacro vag-catch (&rest body)
  `(let ((*using-external-interface* t))
    (catch 'vag-entry
      ,@body)))

(property-macro glue-definition)

(defun new_instance (comp)
  (vag-catch
   (if (or (numberp comp)
	   (and (consp comp) (eq (car comp) 'quote)))
       (intern-exp comp)
       (progn
	 (unless (function-name? comp)
	   (vag-error "~s is not a component" comp))
	 (let ((argvars (mapcar #'(lambda (arg) (declare (ignore arg)) (gentemp "ARG-"))
				(arg-sorts comp)))
	       (newname (gentemp (string comp))))
	   (setf (glue-definition newname) (cons comp argvars))
	   (unwind-protect (progn (push-undo-frame)
				  (push-undo `(install-var ,newname) *connection-stack*)
				  (equate-vars (intern-exp newname) (intern-exp (cons comp argvars))))
	     (when *contradiction*
	       (pop-undo-frame)
	       (vag-error "comp is inherently inconsistent")))
	   newname)))))

(defun connect_instance (parent position child)
  (vag-catch
   (make-connection parent position child)))

(defun make-connection (parent position child)
  (let ((parent-def (glue-definition parent)))
    (unless (and parent-def (consp parent-def))
      (vag-error "~s is not a node in the structure" parent))
    (let ((argvar (nth position parent-def)))
      (unless argvar
	(vag-error "there is no position ~s" position))
      (unless (glue-subsort?  child (nth (1- position) (arg-sorts (car parent-def))))
	(vag-error "wrong argument sort"))
      (when (glue-definition argvar)
	(vag-error "argument position already filled"))
      (unwind-protect (progn (push-undo-frame)
			     (push-undo `(connect ,parent ,position ,child) *connection-stack*)
			     (setf-undo (glue-definition argvar) child)
			     (equate-vars (intern-exp argvar) (intern-exp child)))
	(when *contradiction*
	  (pop-undo-frame)
	  (vag-error "constraint violation")))
      '(ok))))

(defun glue-subsort? (name sort)
  (cond ((numberp name)
	 (subsort? (number-sort name) sort))
	((and (consp name) (eq (car name) 'quote))
	 (subsort? 'expression sort))
	(t
	 (let ((def (glue-definition name)))
	   (unless (and def (consp def))
	     (vag-error "the node ~s is not defined" name))
	   (cond ((member (car def) '(cons map))
		  (or (eq sort 'anything)
		      (and (consp sort) (eq (car sort) 'list-of))))
		 ((member (car def) '(car cdr))
		  t)
		 (t
		  (subsort? (output-sort (car def)) sort)))))))
  

(defun disconnect_instance (parent position)
  (vag-catch
   (undo-connection parent position)
  '(ok)))

(defun undo-connection (parent position)
  (unless (some #'(lambda (assignment) (and (equal (second assignment) parent)
					    (equal (third assignment) position)))
		*connection-stack*)
    (vag-error "no node exists at desired position"))
  (undo-connection2 parent position *connection-stack*))

(defun undo-connection2 (parent position connection-stack)
  (let ((assignment (car connection-stack)))
    (if (and (equal (second assignment) parent)
	     (equal (third assignment) position))
	(pop-undo-frame)
	(progn (pop-undo-frame)
	       (rprint *connection-stack*)
	       (undo-connection2 parent position (cdr connection-stack))
	       (redo-frame assignment)))))

(defun redo-frame (frame)
  (selectmatch frame
    ((connect ?parent ?position ?child)
     (make-connection ?parent ?position ?child))
    ((install-var ?var)
     (unless (and (glue-definition ?var) (consp (glue-definition ?var)))
       (vag-error "illegal atempt to install a node"))
     (push-undo-frame)
     (push-undo frame *connection-stack*)
     (equate-vars (intern-exp ?var) (intern-exp (glue-definition ?var))))))
  
(defun delete_instance (node)
  (declare (ignore node))
  '(ok))

(property-macro vag-print-name)

(defun rename (name1 name2)
  (setf (vag-print-name name1) name2)
  '(ok))

(defun vag-rename (name)
  (or (vag-print-name name)
      name))

(defun vag-load (filename)
  (vag-catch
   (load filename)))

(defun glue-expression (node)
  (cond ((consp node)
	 (cons (car node) (mapcar #'glue-expression (cdr node))))
	((symbolp node)
	 (let ((def (glue-definition node)))
	   (if def
	       (glue-expression def)
	       node)))
	(t (vag-error "illegal argument to glue-expression"))))