;;; This file also contains some random globals for the type checker:

(define-walker type ast-td-type-walker)

;;; Some pre-defined types
(define *bool-type* '())
(define *char-type* '())
(define *string-type* '())
(define *int-type* '())
(define *integer-type* '())
(define *rational-type* '())

;;; These two globals are used throughout the typechecker to avoid
;;; passing lots of stuff in each function call.

(define *placeholders* '())
(define *non-generic-tyvars* '())
(define *enclosing-decls* '())

;;; Used by the defaulting mechanism

(define *default-decls* '())

;;; Used in error handling & recovery

(define *type-error-handlers* '())
(define *type-error-recovery* '())


;;; This associates a type checker function with an ast type.  The variable
;;; `object' is bound to the value being types.

(define-syntax (define-type-checker ast-type . cont)
  `(define-walker-method type ,ast-type (object)
     ,@cont))

;;; This recursively type checks a structure slot in the current object.
;;; This updates the ast in the slot (since type checking rewrites the ast)
;;; and binds the computed type to a variable.  The slot must contain an
;;; expression.

(define-syntax (type-check struct slot var . cont)
  `(mlet ((($$$ast$$$ ,var)
	   (dispatch-type-check (struct-slot ',struct ',slot object))))
	 (setf (struct-slot ',struct ',slot object) $$$ast$$$)
	 ,@cont))

;;; This is used to scope decls.

(define-syntax (with-new-tyvars . cont)
  `(dynamic-let ((*non-generic-tyvars* (dynamic *non-generic-tyvars*)))
     ,@cont))


;;; Similar to type-check, the slot must contain a list of decls.
;;; This must be done before any reference to a variable defined in the
;;; decls is typechecked.
		
(define-syntax (type-check/decls struct slot . cont)
  `(with-new-tyvars
    (let (($$$decls$$$
	  (type-decls (struct-slot ',struct ',slot object))))
     (setf (struct-slot ',struct ',slot object) $$$decls$$$)
     ,@cont)))

;;; The type checker returns an expression / type pair.  This
;;; abstracts the returned value.

(define-syntax (return-type object type)
  `(values ,object ,type))

;;; When an ast slot contains a list of expressions, there are two
;;; possibilities: the expressions all share the same type or each has
;;; an independant type.  In the first case, a single type (computed
;;; by unifying all types in the list) is bound to a variable.

(define-syntax (type-check/unify-list struct slot var error-handler . cont)
  `(mlet ((($$$ast$$$ $$$types$$$)
	   (do-type-check/list (struct-slot ',struct ',slot object))))
    (setf (struct-slot ',struct ',slot object) $$$ast$$$)
    (with-type-error-handler ,error-handler ($$$types$$$)
       (unify-list/single-type $$$types$$$)
       (let ((,var (car $$$types$$$)))
	 ,@cont))))

;;; When a list of expressions does not share a common type, the result is
;;; a list of types.

(define-syntax (type-check/list struct slot var . cont)
  `(mlet ((($$$ast$$$ ,var)
	   (do-type-check/list (struct-slot ',struct ',slot object))))
    (setf (struct-slot ',struct ',slot object) $$$ast$$$)
    ,@cont))

;;; This creates a fresh tyvar and binds it to a variable.

(define-syntax (fresh-type var . cont)
  `(let ((,var (**ntyvar)))
     ,@cont))

;;; This drives the unification routine.  Two types are unified and the
;;; context is updated.  Currently no error handling is implemented to
;;; deal with unification errors.

(define-syntax (type-unify type1 type2 error-handler)
  `(with-type-error-handler ,error-handler ()
     (unify ,type1 ,type2)))

;;; This generates a fresh set of monomorphic type variables.

(define-syntax (fresh-monomorphic-types n vars . cont)
  `(with-new-tyvars
     (let ((,vars '()))
       (dotimes (i ,n)
	   (let ((tv (**ntyvar)))
	     (push tv ,vars)
	     (push tv (dynamic *non-generic-tyvars*))))
       ,@cont)))

;;; This creates a single monomorphic type variable.

(define-syntax (fresh-monomorphic-type var . cont)
  `(let* ((,var (**ntyvar)))
     (with-new-tyvars
       (push ,var (dynamic *non-generic-tyvars*))
       ,@cont)))

;;; This is used to rewrite the current ast as a new ast and then
;;; recursively type check the new ast.  The original ast is saved for
;;; error message printouts.

(define-syntax (type-rewrite ast)
  `(mlet (((res-ast type) (dispatch-type-check ,ast))
	  (res (**save-old-exp object res-ast)))
      (return-type res type)))

;;; These are the type error handlers

(define-syntax (recover-type-error error-handler . body)
 (let ((temp (gensym))
       (err-fn (gensym)))
  `(let/cc ,temp
    (let ((,err-fn ,error-handler))
     (dynamic-let ((*type-error-recovery*
		    (cons (lambda ()
			    (funcall ,err-fn ,temp))
			  (dynamic *type-error-recovery*))))
        ,@body)))))

(define-syntax (with-type-error-handler handler extra-args . body)
  (if (eq? handler '#f)
      `(begin ,@body)
      `(dynamic-let ((*type-error-handlers*
		      (cons (lambda ()
			     (,(car handler) ,@extra-args ,@(cdr handler)))
			    (dynamic *type-error-handlers*))))
	    ,@body)))