(* Type Checking *)
(* Author: Carsten Schuermann *)

functor TypeCheck (structure IntSyn' : INTSYN
		   structure Conv : CONV
		     sharing Conv.IntSyn = IntSyn'
		   structure Whnf : WHNF
		     sharing Whnf.IntSyn = IntSyn' 
		   structure Print : PRINT
		     sharing Print.IntSyn = IntSyn')
  : TYPECHECK =
struct
  structure IntSyn = IntSyn'
  exception Error of string

  local 
    structure I = IntSyn

    (* some well-formedness conditions are assumed for input expressions *)
    (* e.g. don't contain "Kind", Evar's are consistently instantiated, ... *)

    (* checkExp (G, (U, s1), (V2, s2)) = ()

       Invariant: 
       If   G |- s1 : G1   
       and  G |- s2 : G2    G2 |- V2 : L
       returns () if there is a V1 s.t.
	    G1 |- U : V1
       and  G  |- V1 [s1] = V2 [s2] : L
       otherwise exception Error is raised
    *)
    fun checkExp (G, Us, Vs) =
	let 
	  val Us' = inferExp (G, Us)
	in
	  if Conv.conv (Us', Vs) then ()
	  else raise Error ("Type mismatch")
	end

    and inferUni (I.Type) = I.Kind
        (* impossible: Kind *)

    (* inferExp (G, (U, s)) = (V', s')

       Invariant: 
       If   G  |- s : G1
       then if G1 |- U : V   (U doesn't contain EVAR's, FVAR's) 
	    then  G  |- s' : G'     G' |- V' : L
	    and   G  |- V [s] = V'[s'] : L
	    else exception Error is raised. 
     *)
    and inferExpW (G, (I.Uni (L), _)) = (I.Uni (inferUni L), I.id)
      | inferExpW (G, (I.Pi ((D, _) , V), s)) = 
	  (checkDec (G, (D, s));
	   inferExp (I.Decl (G, I.decSub (D, s)), (V, I.dot1 s)))
      | inferExpW (G, (I.Root (C, S), s)) = 
	  inferSpine (G, (S, s), Whnf.whnf (inferCon (G, C), I.id))
      | inferExpW (G, (I.Lam (D, U), s)) =
	  (checkDec (G, (D, s)); 
	   (I.Pi ((I.decSub (D, s), I.Maybe),
		  I.EClo (inferExp (I.Decl (G, I.decSub (D, s)), (U, I.dot1 s)))), I.id))
      (* no cases for Redex, EVars and EClo's *)

    (* inferExp (G, Us) = (V', s')

       Invariant: same as inferExp, argument is not in whnf 
    *)
    and inferExp (G, Us) = inferExpW (G, Whnf.whnf Us)

    (* inferSpine (G, (S, s1), (V, s2)) = (V', s')

       Invariant: 
       If   G |- s1 : G1  
       and  G |- s2 : G2  and  G2 |- V : L ,   (V, s2) in whnf  
       and  (S,V  don't contain EVAR's, FVAR's) 
       then if   there ex V1, V1'  G1 |- S : V1 > V1'
	    then G |- s' : G'    and  G' |- V' : L
	    and  G |- V1 [s1]   = V [s2] : L
            and  G |- V1'[s1]   = V' [s'] : L
    *)
    and inferSpine (G, (I.Nil, _), Vs) = Vs
      | inferSpine (G, (I.SClo (S, s'), s), Vs) = 
	  inferSpine (G, (S, I.comp (s', s)), Vs)
      | inferSpine (G, (I.App (U, S), s1), (I.Pi ((I.Dec (_, V1), _), V2), s2)) =
	  (checkExp(G, (U, s1), (V1, s2));
	   inferSpine (G, (S, s1), Whnf.whnf (V2, I.Dot (I.Exp (I.EClo (U, s1), V1), s2))))
	  (* G |- Pi (x:V1, V2) [s2] = Pi (x: V1 [s2], V2 [1.s2 o ^1] : L
	     G |- U [s1] : V1 [s2]
	     Hence
	     G |- S [s1] : V2 [1. s2 o ^1] [U [s1], id] > V' [s']
	     which is equal to
	     G |- S [s1] : V2 [U[s1], s2] > V' [s']

	     Note that G |- U[s1] : V1 [s2]
	     and hence V2 must be under the substitution    U[s1]: V1, s2
	  *)
      | inferSpine (G, (I.App (U , S), _), (V, s)) = (* V <> (Pi x:V1. V2, s) *)
	  raise  Error ("Expression is applied, but not a function")

    (* inferCon (G, C) = V'

       Invariant: 
       If    G |- C : V  
       and  (C  doesn't contain FVars)
       then  G' |- V' : L      (for some level L) 
       and   G |- V = V' : L
       else exception Error is raised. 
    *)
    and inferCon (G, I.BVar (k')) = 
        let 
	  val I.Dec (_,V) = I.ctxDec (G, k')
	in
	  V
	end
      | inferCon (G, I.Const(c)) = I.constType (c)
      | inferCon (G, I.Def(d))  = I.constType (d)
      (* no case for FVar *)

    (* checkDec (G, (x:V, s)) = B

       Invariant: 
       If G |- s : G1 
       then B iff G |- V[s] : type
    *)
    and checkDec (G, (I.Dec (_, V) ,s)) =
          checkExp (G, (V, s), (I.Uni (I.Type), I.id))

    fun check (U, V) = checkExp (I.Null, (U, I.id), (V, I.id))
    fun infer U = I.EClo (inferExp (I.Null, (U, I.id)))

    fun checkCtx (I.Null) =  ()
      | checkCtx (I.Decl (G, D)) = 
          (checkCtx G; checkDec (G, (D, I.id)))
    
  in
      val check = check
      val infer = infer
      val typeCheck = fn (G, (U, V)) => 
	                   (checkCtx G; checkExp (G, (U, I.id), (V, I.id)))
  end  (* local ... *)
end; (* functor TypeCheck *)