;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - NFS Share File - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package :vag :use '(lisp util))

(shadow 'defstruct)
(shadow 'defvar)

(export '(defstruct define defprim subtype-of with-constraint output-type
	  defvar goto-context contradiction? value-of))



;external macros

(lisp:defvar *using-external-interface* nil)

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

(defun vag-error (string &rest values)
  (if nil;;*using-external-interface*
      (throw 'vag-entry (concatenate 'string "error " (apply #'format nil string values)))
      (apply 'error string values)))

(lisp:defvar *lisp-forms* nil)

(emacs-indent defblock 0)

(defmacro defblock (&rest forms)
  (vag-catch
   (let ((*lisp-forms* nil))
     (let ((normalized-forms (mapcan 'normalize-form forms)))
       `(eval-when (load eval compile)
	 ,@*lisp-forms*
	 (vag-catch
	  (defblock-fun ',normalized-forms)))))))

(defmacro define (&rest args)
  `(defblock (define ,@args)))

(emacs-indent define 1)

(defmacro defprim (&rest args)
  `(defblock (defprim ,@args)))

(emacs-indent defprim 1)

(defmacro defstruct (&rest args)
  `(defblock (defstruct ,@args)))

(defmacro defvar (varname sort)
  `(defblock (defvar ,varname ,sort)))

(defmacro sort-name (name)
  `(defblock (declare-sort ,name)))

(defmacro sort-names (&rest names)
  `(defblock ,@(mapcar
		#'(lambda (name) `(declare-sort ,name))
		names)))

(defmacro subsort (name1 name2)
  `(defblock (subsort ,name1 ,name2)))

(defmacro declare-sort-constraint (sort constraint)
  `(defblock (sort-constraint ,sort ,constraint)))

;The normalization process converts the above external forms
;into corresponding "parsed" internal forms, expands all macro
;occurances in VAG expressions, and converts defstructs into the
;internal forms including DECLARE-SORT, SUBSORT, SORT-CONSTRAINT.
;Therefore there are five internal forms, the three sort forms just listed
;plus DEFINE-INTERNAL, DEFPRIM-INTERNAL, and DEFVAR-INTERNAL.

(lisp:defvar imp-package (make-package :imp))
(unuse-package :lisp imp-package)
(unuse-package :lucid-common-lisp imp-package)

(defun normalize-form (form)
  (selectmatch form
    ((define ?self . ?body)
     (mvlet (((constraint body2) (parse-define ?self ?body)))
       `((define-internal ,(car ?self) ,(cdr ?self)
	   ,(vag-macro-expand-all constraint)
	   ,(vag-macro-expand-all body2)))))
    ((defprim ?self . ?body)
     (mvlet (((outtype constraint body2) (parse-defprim ?self ?body)))
       (unless outtype
	 (vag-error "the defprim for ~s does not have a declared output type" (car ?self)))
       (let* ((name1 (car ?self))
	      (args (mapcar 'car (cdr ?self)))
	      (name2 (intern (string name1) imp-package)))
	 (push `(defun ,name2 ,args ,body2)
	       *lisp-forms*)
	 `((defprim-internal ,name1 ,name2 ,outtype ,(cdr ?self) 
			   ,(vag-macro-expand-all (or constraint '(true))))))))
    ((defvar ?name ?sort)
     `((defvar-internal ,?name ,?sort)))
    ((defstruct ?namespec . ?body)
     (unless (well-formed-defstruct? ?namespec ?body)
       (vag-error "illegal defstruct syntax for ~s") (if (listp ?namespec) (car ?namespec) ?namespec))
     (mvlet (((name parent constraint) (parse-name ?namespec)))
       `((defstruct-internal ,name ,parent ,?body)
	 (sort-constraint ,name ,(if constraint
				     (vag-macro-expand-all constraint)
				     '(true))))))
    (:anything (list form))))

(defun symbolic-nth (exp n)
  (if (= n 1)
      `(car ,exp)
      (symbolic-nth `(cdr ,exp) (1- n))))

(lisp:defvar *dependent-functions*)

(defun defblock-fun (forms)
  (let ((*dependent-functions* nil))
    (mapc #'install-definition forms)
    (mapc #'type-check forms)
    (let ((val (vag-catch (mapc 'infered-output-sort *dependent-functions*))))
      (if (stringp val)
	  (vag-error "type error in dependent function: ~s" val)
	  t))))


;The parsing and macro expanding functions

(defun parse-define (self body)
  (unless (well-formed-self? self)
    (vag-error "illegal define syntax ~s" self))
  (selectmatch body
    (((with-constraint ?constraint) ?final-body)
     (values ?constraint ?final-body))
    ((?b)
     (values '(true) ?b))
    (:anything
     (vag-error "illegal define syntax for ~s" self))))

(defun well-formed-self? (self)
  (and (listp self)
       (symbolp (car self))
       (listp (cdr self))
       (every (lambda (arg)
		(selectmatch arg
		  ((?arg ?type)
		   (and (symbolp ?arg) (type-expression? ?type)))))
	      (cdr self))))

(defun type-expression? (exp)
  (or (symbolp exp)
      (selectmatch exp
	((list-of ?type)
	 (type-expression? ?type)))))

;defprim

(defun parse-defprim (self body)
  (unless (well-formed-self? self)
    (vag-error "illegal defprim syntax ~s" self))
  (selectmatch body
    (((with-constraint ?constraint) . ?rest)
     (mvlet (((outtype const final-body)
	      (parse-defprim self ?rest)))
       (when const
	 (vag-error "mulitple constraints in defprim ~s" self))
       (values outtype ?constraint final-body)))
    (((output-type ?outtype) . ?rest)
     (mvlet (((outtype const final-body)
	      (parse-defprim self ?rest)))
       (when outtype
	 (vag-error "mulitple output types in defprim ~s" self))
       (values ?outtype const final-body)))
    ((?b)
     (values nil nil ?b))
    (:anything
     (vag-error "illegal defprim syntax for ~s" self))))

;defstruct

(defun parse-name (namespec)
  (if (symbolp namespec)
      (values namespec nil nil)
      (values (car namespec)
	      (second (assoc 'subtype-of (cdr namespec)))
	      (second (assoc 'with-constraint (cdr namespec))))))

(defun well-formed-defstruct? (namespec body)
    (and (or (symbolp namespec)
	     (and (symbolp (car namespec))
		  (<= (length (cdr namespec)) 2)
		  (every (lambda (spec)
			   (and (member (car spec) '(subtype-of with-constraint))
				(or (not (eq (car spec) 'subtype-of))
				    (symbolp (second  spec)))))
			 (cdr namespec))
		  (or (null (cddr namespec))
		      (not (eq (car (first (cdr namespec)))
			       (car (second (cdr namespec))))))))
	 (every (lambda (slotspec)
		  (selectmatch slotspec
		    ((?sname ?type)
		     (and (symbolp ?sname) (type-expression? ?type)))
		    (:anything nil)))
		body)))

(property-macro polyadic?)

(setf (polyadic? '+) t)
(setf (polyadic? '*) t)
(setf (polyadic? 'and) t)
(setf (polyadic? 'or) t)

(defun vag-macro-expand-all (expression)
  (selectmatch expression
    ((list ?first . ?rest)
     `(cons
       ,(vag-macro-expand-all ?first)
       ,(vag-macro-expand-all `(list ,@?rest))))
    ((list)
     '(nil))
    ((map (lambda (?x) ?body) ?arg)
     `(map (lambda (,?x) ,(vag-macro-expand-all ?body)) ,(vag-macro-expand-all ?arg)))
    ((let ((?x ?e) . ?rest) ?body)
     (apply-vag-subst (acons ?x (vag-macro-expand-all ?e) nil)
		      (vag-macro-expand-all `(let ,?rest ,?body))))
    ((let () ?body)
     (vag-macro-expand-all ?body))
    ((?f . ?args)
     (if (polyadic? ?f)
	 (cond ((> (length ?args) 2)
		`(,?f
		  ,(vag-macro-expand-all (car ?args))
		  ,(vag-macro-expand-all `(,?f ,@(cdr ?args)))))
	       ((= (length ?args) 2)
		(cons ?f (mapcar #'vag-macro-expand-all ?args)))
	       ((= (length ?args) 1)
		(vag-macro-expand-all (first ?args)))
	       (t
		(vag-error "illegal expression ~s" expression)))
	 (cons ?f (mapcar #'vag-macro-expand-all ?args))))
    (?x ?x)))


;installing definitions

;sort name properties

(property-macro sort-name?)
(property-macro sort-noticers)
(property-macro parent-sort)
(property-macro subsorts)
(property-macro sort-constraint)
(property-macro sort-attributes-cache)
(property-macro sort-maker-fun)

;function name properties

(property-macro function-name?)
(property-macro noticers)
(property-macro arg-sorts)
(property-macro output-sort-cache)
(property-macro vag-definition)
(property-macro dependents)
(property-macro implementation)
(property-macro filter-predicate)
(property-macro production-noticers)
(property-macro external?)

;vag variable properties

(property-macro vag-variable?)
(property-macro vag-var-sort)
(property-macro vag-var-dependents)

;indexing variables and components by sort.

(lisp:defvar *functiont-table* (make-hash-table :test 'equal))
(defmacro functions-of-sort (sort)
  `(gethash ',sort *variable-table*))

(lisp:defvar *variable-table* (make-hash-table :test 'equal))
(defmacro variables-of-sort (sort)
  `(gethash ',sort *variable-table*))

(defun install-definition (form)
  (selectmatch form
    ((define-internal ?name ?args ?constraint ?body)
     (define-internal-fun ?name ?args ?constraint ?body))
    ((defprim-internal ?name1 ?name2 ?output-sort ?args ?constraint)
     (defprim-internal-fun ?name1 ?name2 ?output-sort ?args ?constraint))
    ((defvar-internal ?name ?sort)
     (when (vag-variable? ?name)
       (goto-context nil))
     (defvar-internal-fun ?name ?sort))
    ((declare-sort ?name)
     (when (sort-name? ?name)
       (goto-context nil))
     (setf (sort-name? ?name) t))
    ((defstruct-internal ?name ?parent ?body)
     (when (sort-name? ?name)
       (goto-context nil))
     (setf (sort-name? ?name) t)
     (when ?parent
       (subsort-fun ?name ?parent))
     (setf (sort-maker-fun ?name) (create-name 'make ?name))
     (setf (sort-attributes-cache ?name) ?body)
     (recompute-defstruct ?name))
    ((subsort ?name1 ?name2)
     (subsort-fun ?name1 ?name2))
    ((sort-constraint ?name ?constraint)
     (setf (sort-constraint ?name) `(lambda (self) ,?constraint)))))

(defun defvar-internal-fun (?name ?sort)
  (setf (vag-variable? ?name) t)
  (setf (vag-var-sort ?name) ?sort)
  (dolist (dep (vag-var-dependents ?name))
    (clear-output-sort dep)))

(defun define-internal-fun (?name ?args ?constraint ?body)
  (when (function-name? ?name)
    (goto-context nil))
  (setf (function-name? ?name) t)
  (setf (vag-definition ?name) `(lambda ,(mapcar 'car ?args) ,?body))
  (setf (arg-sorts ?name) (mapcar 'second ?args))
  (setf (filter-predicate ?name)
	`(lambda ,(mapcar 'car ?args) ,?constraint))
  (clear-output-sort ?name)
  (setf (external? ?name) nil))

(defun defprim-internal-fun (?name1 ?name2 ?output-sort ?args ?constraint)
  (when (function-name? ?name1)
    (goto-context nil))
  (setf (implementation ?name1) ?name2)
  (setf (arg-sorts ?name1) (mapcar 'cadr ?args))
  (setf (filter-predicate ?name1)
	`(lambda ,(mapcar 'car ?args) ,?constraint))	   
  (clear-output-sort ?name1)
  (setf (output-sort-cache ?name1) ?output-sort)
  (setf (function-name? ?name1) t)
  (setf (external? ?name1) t))

(defun recompute-defstruct (name)
  (mapc #'recompute-defstruct (subsorts name))
  (let ((local-args (sort-attributes-cache name))
	(args (sort-attributes name)))
    (let* ((maker (sort-maker-fun name))
	   (maker-imp (intern (string maker) imp-package))
	   (arg-imps (mapcar #'(lambda (arg) (intern (string (car arg)) imp-package))
			     local-args)))
      (compile maker-imp `(lambda ,(mapcar #'car args)
			   (list ',(intern (string name) imp-package) ,@(mapcar #'car args))))
      (let* ((self (cons maker (mapcar 'car args)))
	     (constraint (if args
			     (vag-macro-expand-all
			      `(and ,@(mapcar (lambda (arg)
						`(= (,(car arg) ,self) ,(car arg)))
				       args)))
			     '(true))))
	(defprim-internal-fun maker maker-imp name args constraint))			    
      (let ((n (1+ (- (length args) (length local-args)))))
	(dolist (arg-imp arg-imps)
	  (incf n)
	  (compile arg-imp `(lambda (x) ,(symbolic-nth 'x n)))))
      (mapc #'(lambda (arg arg-imp)
		(defprim-internal-fun (car arg) arg-imp (second arg) `((x ,name)) '(true)))
	    local-args
	    arg-imps))))

(defun sort-attributes (name)
  (when name
      (values (append (sort-attributes (parent-sort name))
		      (sort-attributes-cache name)))))


(defun clear-output-sort (name)
  (push name *dependent-functions*)
  (when (output-sort-cache name)
    (setf (output-sort-cache name) nil)
    (dolist (dep (dependents name))
      (clear-output-sort dep))))

(defun subsort-fun (sort1 sort2)
  (when (eq sort1 'anything)
    (vag-error "attempt to assign a supertype to the universal type"))
  (unless (and (symbolp sort1)
	       (symbolp sort2))
    (vag-error "attempt to declare subsort relation between non symbols ~s ~s" sort1 sort2))
  (unless (sort-name? sort1)
    (vag-error "~s is not a type in the subtype declaration ~s" sort1 `(subsort ,sort1 ,sort2)))
  (unless (sort-name? sort2)
    (vag-error "~s is not a type in the subtype declaration ~s" sort2 `(subsort ,sort1 ,sort2)))
  (remove-previous-parent sort1)
  (when (symbol-subsort? sort2 sort1)
    (vag-error "attmept to create circular subtyping"))
  (push sort1 (subsorts sort2))
  (setf (parent-sort sort1) sort2))
  
(defun remove-previous-parent (sort)
  (let ((parent (parent-sort sort)))
    (when parent
      (setf (parent-sort sort) nil)
      (setf (subsorts parent) (remove sort (subsorts parent))))))



;type checking.

(defun type-check (form)
  (selectmatch form
    ((define-internal ?name ?args ?constraint :anything)
     (infered-output-sort ?name)
     (dolist (arg ?args)
       (unless (sort? (second arg))
	 (vag-error "~s is not a type" (second arg))))
     (unless (eq (compute-sort ?constraint (mapcar 'cons (mapcar 'car ?args) (mapcar 'second ?args)))
		 'boolean)
       (vag-error "the constraint is not of type Boolean for function ~s" ?name)))
    ((defprim-internal ?name1 :anything ?output-sort ?args ?constraint)
     (unless (sort? ?output-sort)
       (vag-error "~s is not a type" ?output-sort))
     (dolist (arg ?args)
       (unless (sort? (second arg))
	 (vag-error "~s is not a type" (second arg))))
     (unless (eq (compute-sort ?constraint (mapcar 'cons (mapcar 'car ?args) (mapcar 'second ?args)))
		 'boolean)
       (vag-error "the constraint is not of type Boolean for function ~s" ?name1)))
    ((defvar-internal :anything ?sort)
     (unless (sort? ?sort)
       (vag-error "~s is not a type" ?sort)))
    ((declare-sort :anything) t)
    ((defstruct-internal :anything :anything ?body)
     (dolist (arg ?body)
       (unless (sort? (second arg))
	 (vag-error "~s is not a type" (second arg)))))
    ((subsort ?sort1 ?sort2)
     (unless (sort? ?sort1)
       (vag-error "~s is not a type" ?sort1))
     (unless (sort? ?sort2)
       (vag-error "~s is not a type" ?sort2)))
    ((sort-constraint ?name ?constraint)
     (unless (sort? ?name)
       (vag-error "~s is not a type" ?name))
     (unless (eq 'boolean
		 (compute-sort ?constraint (acons 'self ?name nil)))
       (vag-error "the constraint for ~s is not of type boolean" ?name)))))

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

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

(defun symbol-subsort? (sort1 sort2)
  (or (eq sort1 sort2)
      (let ((parent (parent-sort sort1)))
	(and parent
	     (symbol-subsort? parent sort2)))))

;In the following two operations the sort returned is guaranteed
;to be a supersort of the true intersection and union respectively.

(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))))
	((and (symbolp sort1) (symbolp sort2))
	 (symbol-sort-union sort1 sort2))
	(t 'anything)))

;This is the Martin algorithm --- walk up both sides and loop
;to the opposite sort when you reach the root.  The walk has to converge
;to a common point after a number of iterations equal to
;the sum of the paths to the root minus the length of the common path.

(defun symbol-sort-union (sort1 sort2)
  (iterate loop ((parent1 sort1)
		 (parent2 sort2))
    (if (eq parent1 parent2)
	parent1
	(let ((p1 (parent-sort parent1))
	      (p2 (parent-sort parent2)))
	  (cond ((null p1)
		 (if (null p2)
		     'anything
		     (loop sort2 p2)))
		((null p2)
		 (loop p1 sort1))
		(t
		 (loop p1 p2)))))))

(lisp:defvar *current-fun* nil)

(defun infered-output-sort (fname)
  (let ((*current-fun* fname))
    (or (output-sort-cache fname)
	(unwind-protect (progn (setf (output-sort-cache fname) 'anything)
			       (selectmatch (vag-definition fname)
				 ((lambda ?args ?body)
				  (let ((env (mapcar 'cons ?args (arg-sorts fname))))
				    (mvlet (((sort fun-supporters var-supporters) (infer-sort ?body env)))
				      (unless sort
					(vag-error "unable to infer output sort for ~s" fname))
				      (setf (output-sort-cache fname) sort)
				      (dolist (sup fun-supporters)
					(push fname (dependents sup)))
				      (dolist (sup var-supporters)
					(push fname (vag-var-dependents sup)))
				      (let ((sort2 (compute-sort ?body env)))
					(unless (sort? sort2)
					  (vag-error "~s is not a sort" sort2))
					(when (general-sort? sort2)
					  (vag-error "unable to infer output sort for ~s" fname))
					(setf (output-sort-cache fname) sort2)
					sort2))))))
	  (when (eq (output-sort-cache fname) 'anything)
	    (setf (output-sort-cache fname) nil))))))

(defun general-sort? (sort)
  (or (eq sort 'anything)
      (selectmatch sort
	((list-of ?sort2)
	 (general-sort? ?sort2)))))

(defmacro 2val-or (exp1 exp2)
  (let ((val1 (gensym "VAL1-"))
	(val2 (gensym "VAL2-"))
	(val3 (gensym "VAL3-")))
    `(mvlet (((,val1 ,val2 ,val3) ,exp1))
      (if (and ,val1 (not (general-sort? ,val1)))
	  (values ,val1 ,val2 ,val3)
	  ,exp2))))

(defun infer-sort (exp env)
  (or (assoc-value exp env)
      (cond ((symbolp exp)
	     (unless (vag-variable? exp)
	       (vag-error "vag bug --- undeclared variable ~s" exp))
	     (let ((sort (vag-var-sort exp)))
	       (unless (eq sort 'anything)
		 (values sort nil (list exp)))))
	    ((integerp exp) 'fixnum)
	    ((numberp exp) 'number)
	    (t (selectmatch exp
		 ((if :anything ?case1 ?case2)
		  (2val-or (infer-sort ?case1 env)
			   (infer-sort ?case2 env)))
		 ((quote ?x)
		  (when (symbolp ?x)
		    'symbol))
		 ((cons ?x ?y)
		  (mvlet (((s1 sup1 sup2) (infer-sort ?x env)))
		    (if s1
			(values `(list-of ,s1) sup1 sup2)
			(infer-sort ?y env))))
		 ((car ?x)
		  (mvlet (((s sup1 sup2) (infer-sort ?x env)))
		    (selectmatch s
		      ((list-of ?s) (values ?s sup1 sup2)))))
		 ((cdr ?x)
		  (infer-sort ?x env))
		 ((append ?x ?y)
		  (2val-or (infer-sort ?x env) (infer-sort ?y env)))
		 ((map (lambda (?x) ?body) ?y)
		  (mvlet (((s sup1 sup2) (infer-sort ?y env)))
		    (let ((s2 (selectmatch s ((list-of ?s2) ?s2))))
		      (when s2
			(mvlet (((final sup3 sup4) (infer-sort ?body (acons ?x s2 env))))
			  (values `(list-of ,final) (append sup1 sup3) (append sup2 sup4)))))))
		 ((?f . ?args)
		  (cond ((member ?f '(+ * -))
			 (if (every (lambda (arg) (eq (infer-sort arg env) 'fixnum))
				    ?args)
			     'fixnum
			     'number))
			(t
			 (let ((s (infered-output-sort ?f)))
			   (unless (eq s 'anything)
			     (values s (list ?f))))))))))))

;;compute-sort performs type checking on the given argument
;; 
(defun compute-sort (exp env)
  (or (compute-sort2 exp env)
      (sort-error exp)))

(defun sort-error (exp)
  (if *current-fun*
      (vag-error "ill typed expression ~s in definition of ~s" exp *current-fun*)
      (vag-error "ill typed expression ~s" exp)))

(defun compute-sort2 (exp env)
  (cond ((symbolp exp)
	 (or (assoc-value exp env)
	     (vag-var-sort exp)))
	((nodep exp) (var-node-sort exp))
	((integerp exp) 'fixnum)
	((numberp exp) 'number)
	(t
	 (selectmatch exp
	   ((if ?test ?case1 ?case2)
	    (unless (eq (compute-sort ?test env) 'boolean)
	      (vag-error "~s is not of sort boolean" ?test))
	    (sort-unify ?case1 ?case2 env))
	   ((quote ?x)
	    (when (symbolp ?x)
	      'symbol))
	   ((cons ?x ?y)
	    (if (equal ?y '(nil))
		`(list-of ,(compute-sort ?x env))
		(let ((s1 (compute-sort ?x env))
		      (s2 (compute-sort ?y env)))
		  (selectmatch s2
		    ((list-of ?s3)
		     `(list-of ,(sort-union s1 ?s3)))))))
	   ((car ?x)
	    (selectmatch (compute-sort ?x env)
	      ((list-of ?s) ?s)))
	   ((cdr ?x)
	    (let ((s (compute-sort ?x env)))
	      (selectmatch s
		((list-of :anything) s))))
	   ((append ?x ?y)
	    (sort-union ?x ?y))
	   ((null? ?x)
	    (selectmatch (compute-sort ?x env)
	      ((list-of :anything)
	       'boolean)))
	   ((member? ?x ?y)
	    (let ((?s1 (compute-sort ?x env)))
	      (selectmatch (compute-sort ?y env)
		((list-of ?s2)
		 (when (subsort? ?s1 ?s2)
		   'boolean)))))
	   ((map (lambda (?x) ?body) ?y)
	    (selectmatch (compute-sort ?y env)
	      ((list-of ?s1)
	       `(list-of ,(compute-sort ?body (acons ?x ?s1 env))))))
	   ((?f . ?args)
	    (cond ((member ?f '(+ * -))
		   (let ((atypes (mapcar #'(lambda (arg) (compute-sort arg env))
					 ?args)))
		     (when (every #'(lambda (atype) (subsort? atype 'number))
				  atypes)
		       (if (every (lambda (arg) (eq (compute-sort arg env) 'fixnum))
				  ?args)
			   'fixnum
			   'number))))
		  ((eq ?f '=)
		   (when (and (= (length ?args) 2)
			      (let ((s1 (compute-sort (first ?args) env))
				    (s2 (compute-sort (second ?args) env)))
				(or (subsort? s1 s2)
				    (subsort? s2 s1))))
		     'boolean))
		  (t
		   (when (args-check ?args env (arg-sorts ?f))
		     (infered-output-sort ?f)))))))))

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

(defun sort-unify (exp1 exp2 env)
  (cond ((equal exp1 '(nil))
	 (selectmatch (compute-sort exp2 env)
	   ((list-of ?s2)
	    `(list-of ,?s2))
	   (:anything 'anything)))
	((equal exp2 '(nil))
	 (selectmatch (compute-sort exp1 env)
	   ((list-of ?s2)
	    `(list-of ,?s2))
	   (:anything 'anything)))
	(t
	 (sort-union (compute-sort exp1 env) (compute-sort exp2 env)))))

(defun args-check (args env arg-sorts)
  (or (and (null args) (null arg-sorts))
      (and args
	   arg-sorts
	   (subsort? (compute-sort (car args) env) (car arg-sorts))
	   (args-check (cdr args) env (cdr arg-sorts)))))



;;;goto-context
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; A CONTEXT-EXTENSION is either an assumption, an axiom, or a definition. ;;;
;;; A context is defined by a sequence of context extensions.               ;;;
;;; The order of the extensions is important --- for example,               ;;;
;;; if a symbl has two different definitions, only the last is in force.    ;;;
;;; For technical reasons, the order of axioms and assumptions is also      ;;;
;;; significant.                                                            ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(lisp:defvar *context* nil)

(defun current-context ()
  (reverse *context*))

(defun pop-extension ()
  (util::pop-undo-frame)
  (pop *context*))

(defun show-context ()
  (rprint (current-context)))

(defun extend-frame (extension)
  (util::push-undo-frame)
  (unwind-protect (progn
		    (push `(imp::attempt ,extension) *context*)
		    (execute-extension extension)
		    (pop *context*)
		    (push extension *context*))
    (when (eq (car (first *context*))
	      'imp::attempt)
      (pop-extension))))

(defun execute-extension (extension)
  (unless (and (consp extension)
	       (symbolp (car extension)))
    (vag-error "illegal context assumption ~s" extension))
  (unless (contradiction?)
    (let ((fun (get (car extension) 'execution-function)))
      (if fun
	  (apply fun (cdr extension))
	  (set-value (intern-exp (vag-macro-expand-all extension)) 'true)))))

(defun goto-context (new-context)
  (unless (equal new-context (current-context))
    (if (null new-context)
	(dotimes (n (length (current-context)))
	  (pop-extension))
	(let ((tail (current-context)))
	  (dolist (extension new-context)
	    (cond ((and tail
			(equal extension (car tail)))
		   (pop tail))
		  (tail
		    (dotimes (n (length tail))
		      (pop-extension))
		    (setq tail nil)
		    (extend-frame extension))
		  (t
		    (extend-frame extension))))
	  (when tail
	    (dotimes (n (length tail))
	      (pop-extension)))))))

(defun obvious-sequent? (ctxt formula)
  (goto-context ctxt)
  (or (contradiction?)
      (value-from-undo-frame (true-node? (intern-exp formula)))))

(defmacro defextender (extender-name arguments &rest body)
  `(eval-when (eval load compile)
    (setf (get ',extender-name 'execution-function) ',(create-name extender-name 'extender-fun))
    (defun ,(create-name extender-name 'extender-fun) ,arguments
      ,@body)))

(defextender consider-expression (exp)
  (add-property (intern-exp (vag-macro-expand-all exp)) 'consider! nil))


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

(defun new_instance (comp &optional sort)
  (vag-catch
   (cond ((or (numberp comp)
	      (and (consp comp) (eq (car comp) 'quote)))
	  (intern-exp (vag-macro-expand-all comp)))
	 ((eq comp 'cons)
	  (new-cons sort))
	 (t
	  (unless (function-name? comp)
	    (vag-error "~s is not a component" comp))
	  (let ((s2 (infered-output-sort comp)))
	    (if s2
		(progn (unless (or (null sort)
				   (eq sort s2))
			 (vag-error "the sort ~s contradicts the infered sort for ~s" sort comp))
		       (setq sort s2))
		(unless sort
		  (vag-error "~s has no infered sort" comp))))
	  (let ((argvars (mapcar #'newvar (arg-sorts comp)))
		(newname (newvar sort)))
	    (extend-frame `(new-instance ,newname (,comp ,@argvars)))
	    (extend-frame `(consider-expression ,newname))
	    newname)))))

(defun new-cons (sort)
  (selectmatch sort
    ((list-of ?s2)
     (let ((arg1 (newvar ?s2))
	   (arg2 (newvar sort))
	   (node (newvar sort)))
       (extend-frame `(new-instance ,node (cons ,arg1 ,arg2)))
       (extend-frame `(consider-expression ,node))
       node))
    (:anything
     (vag-error "Attempt to create a new instance of a cons with no list type given"))))

(defun newvar (sort)
  (let ((var (gensym "NODE-")))
    (defvar-internal-fun var sort)
    var))

(defextender new-instance (varname app)
  (equate-vars (intern-exp varname)
	       (intern-exp app)))

(defun make-connection (parent position child)
  (vag-catch
   (let ((argvar (child-var parent position)))
     (unless argvar
       (vag-error "the node ~s does not have child ~s" position))
     (when (glue-definition argvar)
       (vag-error "argument position already filled"))
     (extend-frame `(make-connection ,argvar ,child))
     '(ok))))

(defextender make-connection (var1 var2)
  (equate-vars (intern-exp var1)
	       (intern-exp var2)))

(defun child-var (parent position)
  (nth position (glue-definition parent)))

(defun glue-definition (node)
  (dolist (form *context*)
    (selectmatch form
      ((new-instance ?name ?app)
       (when (eq ?name node)
	 (return-from glue-definition ?app)))
      ((make-connection ?name ?name2)
       (when (eq ?name node)
	 (return-from glue-definition (glue-definition ?name2)))))))

(defun undo-connection (parent position)
  (vag-catch
   (let ((argvar (child-var parent position)))
     (goto-context (remove-if #'(lambda (form)
				  (selectmatch form
				    ((make-connection ?var1 :anything)
				     (eq ?var1 argvar))))
			      (current-context)))
     '(ok))))
  
(defun delete_instance (node)
  (goto-context (remove-if #'(lambda (form)
				  (selectmatch form
				    ((new-instance ?var1 :anything)
				     (eq ?var1 node))))
			      (current-context)))
  '(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)
	       (vag-rename node))))
	(t (vag-error "illegal argument to glue-expression"))))


;the inference engine.

(lisp:defvar *production-noticers* nil)
(lisp:defvar *value-noticers* nil)
(lisp:defvar *var-counter* 0)
(lisp:defvar *contradiction* nil)

(lisp:defvar *infinity* (expt 10 10))
(lisp:defvar *minus-infinity* (- (expt 10 10)))
(lisp:defvar *infinitetesimal* (expt 10 -10))

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

(defun contradiction? ()
  *contradiction*)

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

(defun true-node? (n)
  (and (var-value-flag n)
       (var-value n)))

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

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

(defun create-var ()
  (let ((var (make-variable :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))))

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

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

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

(lisp: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 (var-find (prod-lhs prod))) (cons (prod-fun prod) (list-find (prod-rhs prod)))))
		       
(defun intern-exp (exp)
  (compute-sort exp nil)
  (intern-exp2 exp))

(defun value-of (exp)
  (value-from-undo-frame
   (let ((node (intern-exp (vag-macro-expand-all exp))))
     (add-property node 'consider! nil)
     (list (var-value-flag node)
	   (var-value node)))))

(defun intern-exp2 (exp)
  (var-find (intern-exp3 exp)))

(defun intern-exp3 (exp)
  (cond ((nodep exp) exp)
	((symbolp exp)
	 (or (gethash exp *value-table*)
	     (let ((newvar (create-var)))
	       (setf-undo (gethash exp *value-table*) newvar)
	       (setf (var-defining-production newvar) exp)
	       newvar)))
	((numberp exp)
	 (or (gethash exp *value-table*)
	     (let* ((newvar (create-var)))
		 (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)))
	       (set-value newvar (second 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)))
	       (set-value newvar exp)
	       (setf-undo (gethash exp *value-table*) newvar)
	       newvar)))
	((consp exp)
	 (let ((fun (car exp)))
	   (unless (and (symbolp fun)
			(function-name? fun))
	     (vag-error "attempt to intern non-expression"))
	   (let ((arg-vars (mapcar #'intern-exp2 (cdr exp))))
	     (let* ((exp2 (cons fun arg-vars))
		    (prod (gethash exp2 *exp-table*)))
	       (if prod
		   (var-find (prod-lhs prod))
		   (let ((newvar (create-var)))
		     (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-exp2 (apply-vag-subst subst ?body))))))

;;the following can not capture free variables in the subst
;;because the values being substituted in are nodes.

(defun apply-vag-subst (subst exp)
  (cond ((symbolp exp)
	 (or (assoc-value exp subst)
	     exp))
	((or (numberp exp) (nodep 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*)))
    (setf (prod-rhs prod) (cdr exp))
    (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 #'(lambda (arg) (var-value-flag (var-find arg)))
			  (prod-rhs prod)))
      (set-value (prod-lhs prod) (apply imp (mapcar #'(lambda (arg)
							(var-value (var-find arg)))
						    (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)))

(lisp:defvar *improv-req* .05)

(defun set-upper-bound (var bound)
  (setq var (var-find var))
  (if (< bound (- (var-lower-bound var) *infinitetesimal*))
      (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) *infinitetesimal*))
      (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)) :test #'equal)
    (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))
       (unless (and (symbolp ?var)
		    (symbolp ?prop)
		    (listp ?args)
		    (every #'symbolp ?args))
	 (error "illegal noticer head ~s" (first antecedents)))
       `(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))))
      (:anything
       (error "illegal noticer head ~s" (first antecedents))))))

(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))
	 (unless (and (symbolp ?var)
		      (symbolp ?prop)
		      (listp ?args)
		      (every #'symbolp ?args))
	   (error "illegal antecedent ~s" (first antecedents)))
	 (let ((valvar (gensym "VAR-")))
	   `(dolist (,valvar (assoc-value ',?prop (var-properties ,?var)))
	     ,(make-bindings valvar ?args
	       #'(lambda () (process-antecedents (rest antecedents) body))))))
	(:anything
	 (error "illegal antecedent ~s" (first antecedents))))))

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



;primitives

(sort-names boolean symbol fixnum float number anything)
(subsort fixnum number)
(subsort float number)

(defun true? (x)
  (eq x 'true))

(defun truth-value (v)
  (if v 'true 'false))

(shadow 'negation)

(defun negation (x)
  (if (eq x 'true) 'false 'true))

(defun conjunction (x y)
  (if (and (eq x 'true) (eq y 'true))
      'true
      'false))

(defun disjunction (x y)
  (if (or (eq x 'true) (eq y 'true))
      'true
      'false))

(defprim (true)
  (output-type boolean)
  'true)

(defprim (false)
  (output-type boolean)
  'false)

(defprim (and (x boolean) (y boolean))
  (output-type boolean)
  (conjunction x y))

(defprim (or (x boolean) (y boolean))
  (output-type boolean)
  (disjunction x y))

(defprim (not (x boolean))
  (output-type boolean)
  (negation x))

(define (implies (x boolean) (y boolean))
  (or (not x) y))

(define (iff (x boolean) (y boolean))
  (and (implies x y) (implies y x)))

(defprim (+ (x number) (y number))
  (output-type number)
  (progn (unless (and (numberp x) (numberp y))
	   (vag-error "illegal primitive computation ~s" `(+ ,x ,y)))
	 (+ x y)))

(defprim (* (x number) (y number))
  (output-type number)
  (progn (unless (and (numberp x) (numberp y))
	   (vag-error "illegal primitive computation ~s" `(* ,x ,y)))
	 (* x y)))

(defprim (- (x number) (y number))
  (output-type number)
    (progn (unless (and (numberp x) (numberp y))
	     (vag-error "illegal primitive computation ~s" `(- ,x ,y)))
	   (- x y)))

(defprim (/ (x number) (y number))
  (output-type number)
  (progn (unless (and (numberp x) (numberp y))
	   (vag-error "illegal primitive computation ~s" `(/ ,x ,y)))
	 (cond ((not (= y 0))
		(/ x y))
	       ((> x 0) *infinity*)
	       (t *minus-infinity*))))
	 

(dolist (rel '(> >=))
  (setf (output-sort-cache rel) 'boolean)
  (setf (arg-sorts rel) '(number number))
  (setf (function-name? rel) t))

(define (< (x number) (y number))
  (> y x))

(define (<= (x number) (y number))
  (>= y x))

(defprim (= (x number) (y number))
  (output-type boolean)
  (if (and (numberp x) (numberp y))
      (truth-value (< (abs (- x y)) *infinitetesimal*))
      (truth-value (equal x y))))

(dolist (name '(if cons car cdr member? append map))
  (setf (function-name? name) t))
		
(setf (output-sort-cache 'member?) 'boolean)

(setf (implementation 'cons) #'cons)

(defprim (nil)
  (output-type (list-of anything))
  nil)

(defprim (null? (x (list-of anything)))
  (output-type boolean)
  (truth-value (null x)))