;;; This file contains typecheckers for all expressions except vars and
;;; declarations.

;;; From valdef-structs:
;;;   valdef, single-fun-def are in type-decls

(define-type-checker guarded-rhs
  (type-check guarded-rhs rhs rhs-type
    (type-check guarded-rhs guard guard-type
      (type-unify guard-type *bool-type*
          (type-mismatch/fixed (guarded-rhs-guard object)
	   "Guards must be of type Bool" guard-type))
      (return-type object rhs-type))))

;;; These type checkers deal with patterns.

(define-type-checker as-pat
  (type-check as-pat pattern as-type
    (setf (var-type (var-ref-var (as-pat-var object))) as-type)
    (return-type object as-type)))

(define-type-checker irr-pat
  (type-check irr-pat pattern pattern-type
    (return-type object pattern-type)))

(define-type-checker var-pat
  (fresh-type var-type
    (setf (var-type (var-ref-var (var-pat-var object))) var-type)
    (return-type object var-type)))

(define-type-checker wildcard-pat
 (fresh-type pat-type
    (return-type object pat-type)))

;;; Constant patterns create a piece of code to actually to the
;;; match: ((==) k), where k is the constant.  This code is placed in the
;;; match-fn slot of the const-pat and is used by the cfn.

(define-type-checker const-pat
 (let* ((val (const-pat-value object))
	(match-fn (**app (**var/def (core-symbol "==")) val)))
   (setf (const-pat-match-fn object) match-fn)
   (type-check const-pat match-fn match-type
     (fresh-type res-type
       (type-unify match-type (**arrow res-type *bool-type*) #f)
       (return-type object res-type)))))

(define-type-checker plus-pat
  (let* ((kp (**int (plus-pat-k object)))
	 (km (**int (- (plus-pat-k object))))
	 (match-fn (**app (**var/def (core-symbol "<=")) kp))
	 (bind-fn (**app (**var/def (core-symbol "+")) km)))
    (setf (plus-pat-match-fn object) match-fn)
    (setf (plus-pat-bind-fn object) bind-fn)
    (fresh-type res-type
      (setf (ntyvar-context res-type) (list (core-symbol "Integral")))
      (type-check plus-pat match-fn match-type
        (type-check plus-pat bind-fn bind-type
          (type-check plus-pat pattern pat-type
	    (type-unify match-type (**arrow pat-type *bool-type*) #f)
	    (type-unify bind-type (**arrow pat-type pat-type) #f)
	    (type-unify res-type pat-type #f)
	    (return-type object res-type)))))))

(define-type-checker pcon
 (type-check/list pcon pats arg-types
   (fresh-type res-type
     (let ((con-type (instantiate-gtype (con-signature (pcon-con object)))))
       (type-unify con-type (**arrow/l-2 arg-types res-type) #f)
       (return-type object res-type)))))

(define-type-checker list-pat
  (if (null? (list-pat-pats object))
      (return-type object (instantiate-gtype
			     (algdata-signature (core-symbol "List"))))
      (type-check/unify-list list-pat pats element-type
	   (type-mismatch/list object
	     "List elements have different types")
	(return-type object (**list-of element-type)))))

;;; These are in the order defined in exp-structs.scm

(define-type-checker lambda
 (with-new-tyvars
  (fresh-monomorphic-types (length (lambda-pats object)) arg-vars
    (type-check/list lambda pats arg-types
     (unify-list arg-types arg-vars)
     (type-check lambda body body-type
      (return-type object (**arrow/l-2 arg-vars body-type)))))))

(define-type-checker let
  (type-check/decls let decls
    (type-check let body let-type
      (return-type object let-type))))

(define-type-checker if
  (type-check if test-exp test-type
    (type-unify test-type *bool-type*
        (type-mismatch/fixed object
	 "The test in an if statement must be of type Bool"
	 test-type))
    (type-check if then-exp then-type
      (type-check if else-exp else-type
        (type-unify then-type else-type
              (type-mismatch object
		   "then and else clauses have different types"
		   then-type else-type))
	(return-type object then-type)))))

(define-type-checker case
 (with-new-tyvars
  (let ((case-exp object))  ; needed since object is rebound later
   (fresh-monomorphic-type arg-type
    (type-check case exp exp-type
      (type-unify arg-type exp-type #f) ; just to make it monomorphic
      (fresh-type res-type
	(dolist (object (case-alts object))
	  (recover-type-error ;;; %%% Needs work
	   (type-check alt pat pat-type
	     (type-unify pat-type arg-type
                 (type-mismatch case-exp
		  "Case patterns type conflict."
		  pat-type arg-type))
	     (type-check/decls alt where-decls
	       (type-check/unify-list alt rhs-list rhs-type
                 (type-mismatch/list case-exp
		     "Guarded expressions must have the same type")
		 (type-unify rhs-type res-type
			      (type-mismatch case-exp
		   "Case expression alternatives must have the same type"
		                 rhs-type res-type)))))))
	(return-type case-exp res-type)))))))

;;; Expressions with signatures are transformed into let expressions
;;; with signatures.  

;;;    exp :: type   is rewritten as
;;;    let temp = exp
;;;        temp :: type
;;;     in temp

(define-type-checker exp-sign
 (type-rewrite
  (let* ((temp-var (create-temp-var "TC"))
	 (decl (**valdef (**var-pat/def temp-var) '() (exp-sign-exp object)))
	 (let-exp (**let (list decl) (**var/def temp-var)))
	 (signature (exp-sign-signature object)))
      (setf (var-signature temp-var)
	    (ast->gtype (signature-context signature)
			(signature-type signature)))
      let-exp)))

;;; Rather than complicate the ast structure with a new node for dictSel
;;; we recognize the dictSel primitive as an application and treat it
;;; specially.

(define-type-checker app
 (if (and (var-ref? (app-fn object))
	  (eq? (var-ref-var (app-fn object)) (core-symbol "dictSel")))
  (type-check-dict-sel (app-arg object))
  (type-check app fn fn-type
    (type-check app arg arg-type
      (fresh-type res-type
        (fresh-type arg-type-1
          (type-unify fn-type (**arrow arg-type-1 res-type)
              (type-mismatch/fixed object
		       "Attempt to call a non-function"
		       fn-type))
	  (type-unify arg-type-1 arg-type
              (type-mismatch object
		 "Argument type mismatch" arg-type-1 arg-type))
	  (return-type object res-type)))))))

;;; This is a special hack for typing dictionary selection as used in
;;; generic tuple functions.  This extracts a dictionary from a TupleDict
;;; object and uses is to resolve the overloading of a designated
;;; expression.  The expresion must generate exactly one new context.

(define (type-check-dict-sel arg)
  (when (or (not (app? arg))
	    (not (app? (app-fn arg))))
     (dict-sel-error))
  (let* ((exp (app-fn (app-fn arg)))
	 (dict-var (app-arg (app-fn arg)))
	 (i (app-arg arg))
	 (p (dynamic *placeholders*)))
    (mlet (((object exp-type) (dispatch-type-check exp)))
	  ; check for exactly one new context
      (when (or (eq? (dynamic *placeholders*) p)
		(not (eq? (cdr (dynamic *placeholders*)) p)))
	 (dict-sel-error))
	(mlet ((placeholder (car (dynamic *placeholders*)))
	       (tyvar (placeholder-tyvar placeholder))
	       ((dict-var-ast dict-var-type) (dispatch-type-check dict-var))
	       ((index-ast index-type) (dispatch-type-check i)))
	   (setf (ntyvar-context tyvar) '())  ; prevent context from leaking out
	   (setf (dynamic *placeholders*) p)
           (type-unify dict-var-type
			  (**ntycon (core-symbol "TupleDicts") '()) #f)
	   (type-unify index-type *int-type* #f)
	   (cond ((method-placeholder? placeholder)
		  (dict-sel-error))  ; I am lazy.  This means that
		 ; dictSel must not be passed a method
		 (else
		  (setf (placeholder-exp placeholder)
			(**app (**var/def (core-symbol "dictSel"))
			       dict-var-ast index-ast))))
	   (return-type object exp-type)))))

(define (dict-sel-error)
  (fatal-error 'dict-sel-error "Bad dictSel usage."))

(define-type-checker con-ref
  (return-type object (instantiate-gtype (con-signature (con-ref-con object)))))

(define-type-checker integer-const
  (cond ((const-overloaded? object)
	 (setf (const-overloaded? object) '#f)
	 (type-rewrite (**fromInteger object)))
	(else
	 (return-type object *Integer-type*))))

(define-type-checker float-const
  (cond ((const-overloaded? object)
	 (setf (const-overloaded? object) '#f)
	 (type-rewrite (**fromRational object)))
	(else
	 (return-type object *Rational-type*))))

(define-type-checker char-const
  (return-type object *char-type*))

(define-type-checker string-const
  (return-type object *string-type*))

(define-type-checker list-exp
  (if (null? (list-exp-exps object))
      (return-type object (instantiate-gtype
			     (algdata-signature (core-symbol "List"))))
      (type-check/unify-list list-exp exps element-type
	      (type-mismatch/list object
		 "List elements do not share a common type")
	(return-type object (**list-of element-type)))))

(define-type-checker sequence
  (type-rewrite (**enumFrom (sequence-from object))))

(define-type-checker sequence-to
  (type-rewrite (**enumFromTo (sequence-to-from object)
			      (sequence-to-to object))))

(define-type-checker sequence-then
  (type-rewrite (**enumFromThen (sequence-then-from object)
				(sequence-then-then object))))

(define-type-checker sequence-then-to
  (type-rewrite (**enumFromThenTo (sequence-then-to-from object)
				  (sequence-then-to-then object)
				  (sequence-then-to-to object))))

(define-type-checker list-comp
 (with-new-tyvars
  (dolist (object (list-comp-quals object))
    (if (is-type? 'qual-generator object)
	(fresh-type pat-type
	 (push pat-type (dynamic *non-generic-tyvars*))
	 (type-check qual-generator pat pat-type-1
	   (type-unify pat-type pat-type-1 #f)
	   (type-check qual-generator exp qual-exp-type
	     (type-unify (**list-of pat-type) qual-exp-type
                            (type-mismatch/fixed object
		 "Generator expression is not a list" qual-exp-type)))))
	 (type-check qual-filter exp filter-type
	   (type-unify filter-type *bool-type*
              (type-mismatch/fixed object
		"Filter must have type Bool" filter-type)))))
  (type-check list-comp exp exp-type
     (return-type object (**list-of exp-type)))))

(define-type-checker section-l
  (type-check section-l op op-type
    (type-check section-l exp exp-type
      (fresh-type a-type
        (fresh-type b-type
          (fresh-type c-type
            (type-unify op-type (**arrow a-type b-type c-type)
                (type-mismatch/fixed object
		     "Binary function required in section" op-type))
	    (type-unify b-type exp-type
                  (type-mismatch object
		      "Argument type mismatch" b-type exp-type))
	    (return-type object (**arrow a-type c-type))))))))

(define-type-checker section-r
  (type-check section-r op op-type
    (type-check section-r exp exp-type
      (fresh-type a-type
        (fresh-type b-type
          (fresh-type c-type
            (type-unify op-type (**arrow a-type b-type c-type)
                  (type-mismatch/fixed object
			 "Binary function required" op-type))
	    (type-unify exp-type a-type
                    (type-mismatch object
			 "Argument type mismatch" a-type exp-type))
	    (return-type object (**arrow b-type c-type))))))))

(define-type-checker omitted-guard
  (return-type object *bool-type*))

(define-type-checker con-number
  (let ((arg-type (instantiate-gtype
		   (algdata-signature (con-number-type object)))))
    (type-check con-number value arg-type1
      (type-unify arg-type arg-type1 #f)
      (return-type object *int-type*))))

(define-type-checker sel
  (let ((con-type (instantiate-gtype
		   (con-signature (sel-constructor object)))))
    (mlet (((res-type exp-type1) (get-ith-type con-type (sel-slot object))))
      (type-check sel value exp-type
        (type-unify exp-type exp-type1 #f)
	(return-type object res-type)))))

(define (get-ith-type type i)
 (let ((args (ntycon-args type)))  ; must be an arrow
  (if (eq? i 0)
      (values (car args) (get-ith-type/last (cadr args)))
      (get-ith-type (cadr args) (1- i)))))

(define (get-ith-type/last type)
  (if (eq? (ntycon-tycon type) (core-symbol "Arrow"))
      (get-ith-type/last (cadr (ntycon-args type)))
      type))

(define-type-checker is-constructor
  (let ((alg-type (instantiate-gtype
		   (algdata-signature
		    (con-alg (is-constructor-constructor object))))))
    (type-check is-constructor value arg-type
      (type-unify arg-type alg-type #f)
      (return-type object *bool-type*))))

(define-type-checker cast
  (type-check cast exp _
    (fresh-type res
      (return-type object res))))

;;; This is used for overloaded methods.  The theory is to avoid supplying
;;; the context at the class level.  This type checks the variable as if it had
;;; the supplied signature.

(define-type-checker overloaded-var-ref
  (let* ((var (overloaded-var-ref-var object))
	 (gtype (overloaded-var-ref-sig object))
	 (ovar-type (var-type var)))
    (when (recursive-type? ovar-type)
	 (error
	  "Implementation error: overloaded method found a recursive type"))
    (mlet (((ntype new-vars) (instantiate-gtype/newvars gtype))
	   (object1 (insert-dict-placeholders
		     (**var/def var) new-vars object)))
	  (return-type object1 ntype))))