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

(shadow 'defstruct)
(shadow 'defvar)

(export '(defstruct define defprim subtype-of with-constraint output-type defvar))

;;The above functions are used to install various properties on symbols.
;;The inference rules in vag2.lisp use these properties.

;; --- the definition property of constructor symbols.
;; --- the implementation property of constructor symbols.
;; --- the filter predicate property of function symbols.
;; --- the output sort of function symbols.
;; --- the filter predicate property of sort symbols.
;; --- the supersort of a sort symbol
;; --- the sort of a variable.


;========================================================================
;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)))


(defun vag-expand (exp)
  (let ((exp2 (vag-macro-expand-all exp)))
    (compute-sort exp2 nil)
    exp2))

(setq rules::*vag-expand* 'vag-expand)

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

(defun apply-vag-subst (subst exp)
  (cond ((symbolp exp)
	 (or (assoc-value exp subst)
	     exp))
	((or (not (consp exp))
	     (and (consp exp) (eq (car exp) 'quote)))
	 exp)
	(t
	 (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)))))))


;========================================================================
;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 arg-sorts)
(property-macro output-sort-cache)
(property-macro vag-definition)
(property-macro dependents)
(property-macro implementation)
(property-macro filter-predicate)
(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)))
	((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)))))




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

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