;; $Id: tc-type-helpers.scm,v 1.117 2005/05/12 20:06:05 dorn Exp $
;; 
;; Some helpful functions for type checking with type environments.
;; 
;; AUTHOR: Brian Dorn, Gary T. Leavens
;; 

(module tc-type-helpers (lib "typedscm.ss" "lib342")

(provide tc:set-current-subst-list!
	 tc:judgement tc:judgement?
	 : :?- <: <:> :- :-d
	 tc:atree-of
	 tc:axiom-helper tc:rule-helper tc:rule-or-helper
	 tc:rule-if-helper tc:rule-seq-helper
	 tc:mixed tc:hyp tc:when tc:def
	 tc:annotation->type)

(require-for-syntax mzscheme)
(require (lib "tc-util.scm" "lib342")
         (lib "tc-subst.scm" "lib342")
         (lib "tc-environments.scm" "lib342")
	 (lib "tc-tracing.scm" "lib342"))

;; NOTE: The calling code must properly initalize the subst list 
;;       with the null subsititution or no type checking will occur
(define *tc:current-subst-list* (list))

(define tc:set-current-subst-list!
  (lambda (sl) (set! *tc:current-subst-list* sl)))

(define tc:get-current-subst (lambda () (car *tc:current-subst-list*)))

(define tc:get-current-subst-list (lambda () *tc:current-subst-list*))

;; Procedures which help deal with the substitution list
(define tc:error-noted?
  (lambda () (null? *tc:current-subst-list*)))

(define tc:note-error!
  (lambda () (set! *tc:current-subst-list* '())))

;;        TYPE JUDGEMENTS
;; 
;; Typing judgements with inherited attributes that are type environments
;; are defined by the following.
;; The second form allows the inherited attribute to be a logical variable.
;; This is only useful in certain declaration forms; normally the first
;; kind of judgement would be used.
;; 
(define-datatype tc:judgement tc:judgement?
  (:-d (env tc:environment?) (attr-pair (tc:attrib-pair-of datum? datum?)))
  (:?- (lvar tc:logicalvar?) (attr-pair (tc:attrib-pair-of datum? datum?)))
  (<: (subtype datum?) (supertype datum?))  
  (<:> (t1 datum?) (t2 datum?)
       (subtype-var tc:logicalvar?) (supertype-var tc:logicalvar?)))

(define-syntax :-
  (syntax-rules (:)
    ((:- pi (: s t))
     (:-d pi (: s (delay t))))))

;;                  ATREES
;;
;; ATrees are attributed syntax pairs where the attributes are trees of
;; primitive attributes.
;; This allows the attributes of subtrees to be recovered if needed.

;(defrep
;  (forall (syn) (tc:atc:tree-of syn) (pair-of syn (tc:tree-of tc:type-expr))))

(deftype tc:atree-of (type-predicate-for tc:atree))
(define tc:atree-of
  (forall (Syn?)
    (tc:attrib-pair-of Syn? (tc:tree-of datum?))))

;; 
;; 	HELPERS FOR WRITING
;;         TYPE CHECKING RULES
;; 
;; Note: the functions below have different interfaces than the ones in
;; CoreTypeHelpers.
;; 
;;          Examples
;; 
;; The following are examples of how to use the functions defined below.
;; The horizontal lines are simply Haskell comments, but they look nice (:->).
;; 
;; The following are examples of the basic helpers; you can do almost
;; everything with these two.
;; 
;;   annotate pi Skip =
;;    axiom (pi :- Skip ::: Acomm)
;;
;;   

;; ;;    (rule (lis

;;   annotate pi d@(Fun i e) =
;;    rule [pi :- Expr e ::: Aexp (Avar tau)]
;;         ----------------------------------------------
;;         (pi :- d ::: Adec (Api [(i, Aexp (cdrAvar tau))]))
;;                 where tau = (0, "tau")
;;
;;
;; The rule example also shows how to use logical variables to express
;; simple dependencies of the resulting type on the types of parts of
;; the hypothesis.  Often you won't need even this complication.  But
;; note the use of Aexp (Avar tau) instead of just the type attribute (Avar tau).
;; A type error (Aerr) will not unify with Aexp (Avar tau),
;; hence if an error is detected in the hypothesis, the rule as a whole
;; will generate an error, as desired.
;; 
;; A convenience that allows more fine-grained splitting of rules
;; into cases is the ruleOr combinator. This combines two rules.
;; (The rules combined don't have to be programmed with "rule", it just happens
;; to work that way in common examples.)
;; 
;;   annotate pi e@(e1 `Equals` e2) =
;;      (rule [pi :- e1 ::: Aexp Aint,
;;             pi :- e2 ::: Aexp Aint]
;;            --------------------------
;;            (pi :- e ::: (Aexp Abool)))
;;    `ruleOr`
;;      (rule [pi :- e1 ::: Aexp Abool,
;;             pi :- e2 ::: Aexp Abool]
;;            --------------------------
;;            (pi :- e ::: (Aexp Abool)))
;; 
;; For rules with side conditions the ruleIf form usually suffices.
;; The following is an example (of how to use it for sequential declarations).
;; More explanation follows the example.
;; 
;;   annotate pi d@(d1 `Also` d2) =
;;    ruleIf [pi :- Decl d1 ::: Adec (Avar pi1),
;;            pi :- Decl d2 ::: Adec (Avar pi2)]  (\[t1, t2] -> isDisjoint t1 t2)
;;                                                (\[Adec (Api ff1),
;;                                                   Adec (Api ff2)] ->
;;                                                  (pi3 ->- Api
;;                                                    (uniondisjoint ff1 ff2)))
;;           ----------------------------------
;;           (pi :- d ::: Adec (Avar pi3))
;;               where pi1 = (1, "pi")
;;                     pi2 = (2, "pi")
;;                     pi3 = (3, "pi")
;;                     isDisjoint t1 t2 = ...
;;                     uniondisjoint ff1 ff2 = ...
;; 
;; Notice that the ruleIf helper takes two functions as side conditions.
;; The first is a function from the type attributes to a boolean value.
;; If this returns True, then the type attributes are passed to the second,
;; which is to retur n a substitution.  This substitution can define the values
;; of logical variables used in the conclusion, based on the values of
;; the logical variables that result from checking the hypotheses.
;; Note that the substitution returned by the second side condition function
;; is computed last, so it can't affect the checking of the hypotheses
;; or the type attributes passed to the first side condition function.
;; 
;; You are guaranteed that the argument passed to the first side condition
;; function in ruleIf is a list with the same number of elements as
;; the list of hypotheses, and that the type attributes unify with
;; expected attributes.  Thus, if errors are detected, the first function
;; is not even called.  You are also guaranteed that the second side condition
;; function is only called if the first returns True.
;; 
;; On thing you can't do with the helpers shown above
;; is sequential declarations.  For this you need a specialized form, ruleSeq.
;; This processes its first argument list sequentially (see example below).
;; Each element of this list is tagged.
;; Ones with the tag "Hyp" are hypotheses, and do checking for expected type
;; attributes, but the judgement form (pi :?- s :::t)
;; allows the type environment (pi) to be a logical variable,
;; which is substituted for before the checking is done.
;; Ones with the tag "Def" and "When" are side condition functions
;; that are passed the list of attributes so far.
;; The "Def" functions return a substitution, which can be used to define the
;; values of logical variables to be used later.
;; Ones with the tag "When" are tests that return booleans; these stop
;; most checking if they return False.
;; 
;;   annotate pi d@(d1 `Then` d2) = 
;;    ruleSeq;;    (rule (lis

;;      [Hyp (pi :- Decl d1 ::: Adec (Avar pi1)),  Def (\[Adec (Api ff1)] ->
;;                                                      (pi4 ->- Api
;;                                                       (pi `unionMinus` ff1))),
;;       Hyp (pi4 :?- Decl d2 ::: Adec (Avar pi2)), When (\[t1, t2] ->
;;                                                        isDisjoint t1 t2),
;;                                                  Def (\[Adec (Api ff1),
;;                                                         Adec (Api ff2)] ->
;;                                                       (pi3 ->- Api
;;                                                        (uniondisjoint ff1 ff2)
;;                                                       ))]
;;      ------------------------------------------
;;      (pi :- d ::: Adec (Avar pi3))
;;               where pi1 = (1, "pi")
;;                     pi2 = (2, "pi")
;;                     pi3 = (3, "pi")
;;                     pi4 = (4, "pi")
;; 
;; 
;;        Implementations
;; 
;; A rule without hypotheses is an axiom.
;; We make this strict in its type environment, to allow better error handling.

(deftype tc:axiom-helper
  (-> (tc:unifiable-md)
      (-> (tc:judgement)
	   (tc:atree-of datum))))
(define tc:axiom-helper
  (lambda (md)
    (cases tc:unifiable-md md
	   (tc:unifiable-md-dict
	    (to-term get-var subterms same-kind nullSubst bind app
		     contravar-subterms covar-subterms invar-subterms
		     subtype-replace intersection-type? find-intersection-subtyping find-intersection-supertyping
		     is-bottom? is-top? is-error? gen-error-mismatch gen-error-rule
		     is-dec-type-expr? dec-type-expr->env)
	      (lambda (judgement)
		(cases tc:judgement judgement
		       (:-d (env attr-pair)
			    (let ((type (tc:force-if-promise (tc:attrib-pair->type attr-pair))))
			      (if (is-error? type)
				  (tc:note-error!))				 
			      (: (tc:attrib-pair->syn attr-pair) (tc:node type '()))))
		       (else (error "Judgment cannot contain logicalvars or subtypes"))))))))

;; The "rule" helper doesn't allow side conditions.
;; It is implemented by just calling the "rule-seq" form with
;; vacuous side conditions.
;; 

(deftype tc:rule-helper
  (forall (syn)
    (-> (tc:unifiable-md (-> (tc:type-env syn) (tc:atree-of syn)))
	(-> ((list-of tc:judgement) tc:judgement)
	    (tc:atree-of datum)))))
(define tc:rule-helper
  (lambda (md annotate)
    (lambda (hs conc)
      ((tc:rule-seq-helper md annotate) (map tc:hyp hs) conc))))

;; 
;; A sequential case analysis is provided by rule-or
;; 

(deftype tc:rule-or-helper
  (forall (syn)
    (-> (tc:unifiable-md (-> (tc:type-env syn) (tc:atree-of syn)))
	(-> ((list-of
	      (tc:atree-of datum)))
	    (tc:atree-of datum)))))
(define tc:rule-or-helper
  (lambda (md annotate)
    (cases
	tc:unifiable-md md
	(tc:unifiable-md-dict
	 (to-term get-var subterms same-kind nullSubst bind app
		  contravar-subterms covar-subterms invar-subterms
		  subtype-replace intersection-type? find-intersection-subtyping find-intersection-supertyping
		  is-bottom? is-top? is-error? gen-error-mismatch gen-error-rule
		  is-dec-type-expr? dec-type-expr->env)
	 (lambda ts
	   ;; REQUIRES: ts is a non-empty list of rules whose
	   ;;           execution has been delayed
	   (letrec
	       ;; Save the current subst list so we don't destroy it
	       ((saved-subst-list (tc:get-current-subst-list))
		(recur
		 (lambda (rules)
		   (if (null? (cdr rules))
		       (force (car rules))
		       (let ((result (force (car rules))))
			 (if (not (is-error? 
				   (tc:root (tc:attrib-pair->type result))))
			     result
			     ;; If it is an error, we need to fix the current subst
			     (begin
			       (tc:set-current-subst-list! saved-subst-list)
			       (recur (cdr rules)))))))))
	     (recur ts)))))))

;; Rules with side conditions are handled in rule-if.
;; Note that it actually takes two side condition functions,
;; as described above.

(deftype tc:rule-if-helper
  (forall (syn)
    (-> (tc:unifiable-md (-> (tc:type-env syn) (tc:atree-of syn)))
	(-> ((list-of tc:judgement)
	     (-> (list-of tc:type-expr) bool)
	     (-> (list-of tc:type-expr) (tc:subst-of tc:type-expr))
	     tc:judgement)
	    (tc:atree-of daum)))))
(define tc:rule-if-helper
  (lambda (md annotate)
    (lambda (hs side_cond side_defs conc)
      ((tc:rule-seq-helper md annotate)
       (append (map tc:hyp hs)
	       (list (tc:when side_cond) (tc:def side_defs)))
       conc))))

;; The following helper function is used in the next form.

(deftype tc:map-tops
  (forall (a)
    (-> ((-> (a) a) (list-of (tc:tree-of a)))
	(list-of (tc:tree-of a)))))
(define tc:map-tops
  (lambda (f ts)
    (map (lambda (n) (tc:node (f (tc:root n)) (tc:leaves n)))
	 ts)))

;; 
;; The form rule-seq is for sequentially processing hypotheses
;; and side conditions, as occurs in sequential declarations.
;; It also allows the type environment computed in one hypothesis
;; to be used in the next.
;; 
;; The data type tc:mixed is for mixing true hypotheses with
;; side conditions and side definitions
;; that are to be executed to define new substitutions
;; or to test for some correctness condition
;; before going on to the next hypothesis.
;; 

(define-datatype tc:mixed tc:mixed?
  (tc:hyp (judgement tc:judgement?))
  (tc:when (f (-> (list-of datum?) boolean?)))
  (tc:def (f (-> (list-of datum?) (tc:subst-of datum?)))))


(deftype tc:rule-seq-helper
  (forall (syn)
    (-> (tc:unifiable-md (-> (tc:type-env syn) (tc:atree-of syn)))
	(-> ((list-of tc:mixed) tc:judgement)
	    (tc:atree-of datum)))))
(define tc:rule-seq-helper
  (lambda (md annotate)
    (cases tc:unifiable-md md
	   (tc:unifiable-md-dict
	    (to-term get-var subterms same-kind nullSubst bind app
		     contravar-subterms covar-subterms invar-subterms
		     subtype-replace intersection-type?
		     find-intersection-subtyping find-intersection-supertyping
		     is-bottom? is-top? is-error? gen-error-mismatch gen-error-rule
		     is-dec-type-expr? dec-type-expr->env)
	      (lambda (hs conc)
		(cases tc:judgement conc
		       (:-d (env attr-pair)
			    (let ((result_trees
				   ((tc:sequence md annotate) hs '() ))
				  (syn (tc:attrib-pair->syn attr-pair))
				  (tau (tc:attrib-pair->type attr-pair)))
			      ;;Current will be updated by recusion
			      (if (not (tc:error-noted?))
				  (let* ((s (tc:get-current-subst))
					 (ts (tc:map-tops (app s) result_trees)))
				    (: syn (tc:node ((app s)
						     (tc:force-if-promise tau))
						    ts)))
				  ;; Type error
				  (: syn (tc:node
					  (gen-error-rule syn result_trees)
					  result_trees)))))
		       (else (error "Conclusion judgement must be a :- judgement")))
		)))))

;; [[[FIxME:  make deftype oblivious to type-expr]]]		     
(deftype tc:sequence
  (forall (syn)
    (-> (tc:unifiable-md (-> (tc:type-env syn) (tc:atree-of syn)))
	(-> ((list-of tc:mixed)
	     (list-of (tc:tree-of tc:type-expr)))
	    (list-of (tc:tree-of tc:type-expr))))))
(define tc:sequence
  (lambda (md annotate)
    (cases tc:unifiable-md
      md
      (tc:unifiable-md-dict
       (to-term get-var subterms same-kind nullSubst bind app
		contravar-subterms covar-subterms invar-subterms
		subtype-replace intersection-type? find-intersection-subtyping find-intersection-supertyping
		is-bottom? is-top? is-error? gen-error-mismatch gen-error-rule
		is-dec-type-expr? dec-type-expr->env)
       (lambda (hs attrs)
	 (letrec ((recurse (tc:sequence md annotate))
		  (vars-in (tc:vars-in md)))
	   (let ((check-subtype-judgement
		  (tc:check-subtype-judgement hs md app bind attrs recurse)))
	     (if (null? hs)
		 ;; Case 1
		   attrs
		 (cases tc:mixed
		   (tc:force-if-promise (car hs))
		   (tc:def (f)
			   (if (tc:error-noted?)
			       ;; Case 2, already working on a type error, so ignore this
			       (recurse (cdr hs) attrs)
				  
			       ;; Case 3
			       (let ((delta_subst (f (map tc:root attrs))))
				 ;; Update the current environment
				 (tc:set-current-subst-list!
				       (list
					(tc:subst-compose
					 (tc:get-current-subst)
					 delta_subst)))
				 (recurse (cdr hs) attrs))))
		   (tc:when (p)
			    (if (tc:error-noted?)
				;; Case 4, already working on a type error, so ignore this
				(recurse (cdr hs) attrs)
				   
				;; Case 5			   
				(if (p (map tc:root attrs))
				    (recurse (cdr hs) attrs)
				    (begin
				      ;; Update unification env with error
				      (tc:note-error!)
				      (recurse (cdr hs) attrs)))))
		   (tc:hyp
		    (judgement)
		    (cases tc:judgement
		      judgement
		      (:-d (env attr-pair)
			   (if (tc:error-noted?)
			       ;; Case 6
			       (recurse (cdr hs) attrs)
			       
			       ;;(let* ((recur-result (annotate env (tc:attrib-pair->syn attr-pair)))
			;;	      (attr (tc:attrib-pair->type recur-result)))
			;;	 (recurse (cdr hs)
			;;		  (append attrs (list attr))))

			       ;; Case 7
			       (let* ((syn (tc:attrib-pair->syn attr-pair))
				      (recur-result (annotate env syn)))
				 (if (tc:error-noted?)
				     ;; Unification error on sub annotation
				     (recurse (cdr hs)
					      (append attrs (list (tc:attrib-pair->type recur-result))))
				     ;; So far so good...
				     (let* ((result-attr (tc:attrib-pair->type recur-result))
					    (attr
					     (tc:node
					      ((app (tc:get-current-subst)) (tc:root result-attr))
					      (tc:leaves result-attr)))
					    (expected
					     ((app (tc:get-current-subst))  
					      (tc:force-if-promise (tc:attrib-pair->type attr-pair)))) )

				       (if (> (type-tracing-level) 3)
					   (begin
					     (displayln "Expected type: " expected)
					     (displayln "Inferred type: " (tc:root attr))))

				       (let* ((renaming
					       (if (null? (tc:intersect (vars-in (tc:root attr)) (vars-in expected)))
						   (lambda (trm) trm)
						   ((tc:rename-vars md)
						    (+ 1 (tc:max-list (map cdr (vars-in expected)))))))
					      (rt (renaming (tc:root attr)))
					      (delta-substl ((tc:mgu md) expected rt)))
					 (if (null? delta-substl)
					     ;; no result substitution
					     (begin
					       (tc:note-error!)
					       (recurse (cdr hs)
							(append attrs
								(list (tc:node (gen-error-mismatch syn expected rt)
									       '())))))
					     (begin						 
					       (tc:set-current-subst-list!
						(list 
						 (tc:subst-compose
						  (tc:get-current-subst)
						  (car delta-substl))))
					       (let ((t2 ((app (tc:get-current-subst)) rt)))
						 (recurse (cdr hs)
							  (append attrs
								  (list (tc:node t2 (tc:leaves attr))))))))))))))
		      (:?- (lvar attr-pair)
			   (if (tc:error-noted?)
			       ;; Case 8
			       (recurse (cdr hs) attrs)
				;;	(append attrs
				;;		(list (tc:node (tc:attrib-pair->type attr-pair) '()))))
					   
			       ;; Case 9
			       (let ((te ((app (tc:get-current-subst))
					  (to-term lvar))))
				 (cond				
				  ((is-dec-type-expr? te)
				   (recurse (cons (tc:hyp (:-d (dec-type-expr->env te) attr-pair))
						  (cdr hs))
					    attrs))
				  (else (error "tc:sequence: Bad binding for logical var: " lvar))))))

		      (<: (subtype supertype)
			  ;; Case 10
			  (check-subtype-judgement subtype supertype
						   (tc:new-logicalvar) (tc:new-logicalvar)))

		      (<:> (t1 t2 subtype-var supertype-var)
			   ;; Case 11
			   (let ((saved-subst-list (tc:get-current-subst-list))
				 (t1-sub-result (check-subtype-judgement t1 t2 subtype-var supertype-var)))
			     (if (not (tc:error-noted?))
				 ;; t1 <: t2 passed, pass along answer
				 t1-sub-result
				 ;; t1 <: t2 failed, try other way
				 (begin
				   ;; restore subst-list
				   (tc:set-current-subst-list! saved-subst-list)
				   (check-subtype-judgement t2 t1 subtype-var supertype-var)))))
		      )))))))))))

(define tc:check-subtype-judgement
  (lambda (hs md app bind attrs recurse)
    (lambda (subtype supertype subtype-var supertype-var)
      (if (tc:error-noted?)
	  ;; Type error already, so just pass it on
	  (recurse (cdr hs) attrs)			    
	  ;; Attempt subtype test, first apply current substitution to vars
	  (let* ((cur-app (app (tc:get-current-subst)))
		 (subtype-val (cur-app subtype))
		 (supertype-val (cur-app supertype)))
	    (if (> (type-tracing-level) 2)
		(begin
		  (displayln "tc:sequence: Checking Subtype Judgement")
		  (displayln "subtype-val: " subtype-val)
		  (displayln "supertype-val: " supertype-val)))

	    (let ((subtype-substl ((tc:subtype-mgu md) subtype-val supertype-val)))
	      (if (null? subtype-substl)
		  ;;  subtype relationship failure
		  (begin
		    ;; Update unification environment
		    (tc:note-error!)
		    (recurse (cdr hs) attrs))
		  ;;  subtype relation is valid, pass on subst
		  (begin 
		    ;; Update unification environment
		    (tc:set-current-subst-list!
		     (list
		      (tc:subst-compose
		       (tc:get-current-subst)
		       (tc:subst-compose
			(car subtype-substl)
			(tc:subst-compose
			 (bind subtype-var subtype-val)
			 (bind supertype-var supertype-val))))))		      
		    (recurse (cdr hs) attrs)))))))))

(define tc:annotation->type
  (lambda (x)
    (tc:root (cdr x))))


) ;; end module