module Check where

import Val
import Conv
import Core.Abs
import Exp1
import Cont

-- checking the correctness of a type, and of an expression

check :: Cont -> Val -> Exp -> G ()
checkT :: Cont -> Exp -> G ()

checkT con ESet = return ()
checkT con (EFun x a b) =
 do
  checkT con a
  v <- return (evalCon con a)
  u <- genCon con x v
  checkT (upCon x u v con) b
checkT con e = check con Set e

-- check a body of a definition

check con (Fun v f) (ELam x e) =
 do
  u <- genCon con x v
  check (upCon x u v con) (f u) e
check con v (EIdent n) =
 do
  v' <- return (snd (getVT n con))
  eqT (length con) v v'
check con v (EApp n es) =
 do
  v' <- checkI con (snd (getVT n con)) es
  eqT (length con) v v'
check con v (Efun nes) =
 mapM_ (checkP con v) nes
check _ _ e = fail ("check " ++ show e)

checkP con (Fun (App h ps) f) (Bcon i e) =
 do
  (v,w) <- return (getVT i con)
  check con (itCurry (apps v ps) (inst w ps) f) e
checkP _ _ _ = fail "checkP"

-- check a vector of exps against an iterated function type

checkI con (Fun a f) (e:es) =
 do
  check con a e
  checkI con (f (evalCon con e)) es
checkI _ v []  = return v
checkI _ _ _   = fail "checkI"