Check.hs

module PiSigma.Check where

import Control.Monad

import PiSigma.Syntax
import PiSigma.Evaluation
import PiSigma.Print
import PiSigma.Equality

--import Debug.Trace
--trace "check\n" $

-- closures are the other way around
-- should be fixed by changing closures.

{-
fog :: CTerm -> Closure
fog (g,t) = (con2scope g,t)
-}

failc :: Env e => Clos Term -> [Msg] -> Eval e a
failc t m = failp ([S "Checking:\t",C t,S "\n"]++m)

-- | Takes a term and an (unevaluated) type. We first
-- handle the cases that may potentially change the
-- environment. If none of those cases match, we can
-- safely evaluate the type and call check'.
check :: Env e => Clos Term -> Clos Type -> Eval e ()
--check (g,t) c | trace ("check\ng ="++(show g)++"\n t="++(show t)++"\nc="++(show c)++"\n") False = undefined

check (Let p t,g) c = 
    do g' <- checkProg (p,g)
       check (t,g') c

check (gt @  (Split t (x,(y,u)),g)) c = 
    do sigab <- infer' (t,g)
       case sigab of
         (VQ Sigma ((a,(z,b)),s)) -> 
             do t'      <- eval (t,g)
                (_,g')  <- tdecl x g (a,s)
                b       <- subst (z,(b,s)) (Var x, g')
                (_,g'') <- tdecl y g' b
                case t' of
                  (Ne (NVar i)) ->
                      letn' i (Pair (Var x,Var y), g'')
                                (check (u,g'') c)
                      -- this is a bit silly since we know the ids.
                  _ -> check (u,g'') c
                      -- instead of failing, we just omit the assignment.
         _ -> failc gt [S "split : Sigma type expected\nFound:\t",V sigab,S "\n(split)\n"]

check gt @ (t'@(Case t lus),g) c = 
    do enum <- infer' (t,g)
       case enum of
         VEnum ls -> 
             let ls' = map fst lus
             in if ls /= ls'
                then do -- pt' <- prt t'
                        failc gt [S ("case: labels don't match"
                                     ++ "\n expected : " ++ show ls
                                     ++ "\n inferred : " ++ show ls'
                                     ++ "\n(match)\n")]
                -- set equivalence would be sufficent
                else do t' <- eval (t,g)
                        case t' of
                          -- if the scrutinee is a variable, we add a constraint
                          -- while checking each of the branches
                          (Ne (NVar i)) ->
                               mapM_ (\ (l,u) -> 
                                      letn' i (label l)
                                            (check (u,g) c)) lus
                          -- if the scrutinee is not a variable, we do not add
                          -- a constraint, but continue
                          _ -> mapM_ (\ (l,u) -> check (u,g) c) lus
         _ -> failc gt [S "case : enum type expected\nFound:\t",V enum,S "\n(case)\n"]
         {- Problem: here and other places: we try to print the term t which isn't yet 
            typechecked and may contain undefined variables which may crash the printer...
            see undef-bug.pi
         -}
check (Force t,g) (a , s) =
    check (t,g) (Lift a , s)

check t a = do a' <- feval a
               check' t a'

check' :: Env e => Clos Term -> Val -> Eval e ()
check' gt (VBox (Boxed a)) = check gt a  -- do we still need this line?
check' (Lam (x,t),g) (VQ Pi ((a,(y,b)),s)) =
    do (i,g') <- tdecl x g (a,s)
       let s' = extendScope s y (i,Nothing)
       check (t,g') (b,s')
check' gt @ (Lam _,g) a = failc gt [S "Expected:\t",V a,S "\n(Lam)\n"]
check' (Pair (t,u),g) (VQ Sigma ((a,(y,b)),s)) =
    do check (t,g) (a,s)
       b <- subst (y,(b,s)) (t,g)
       check (u,g) b
check' gt @ (t @ (Pair _),g) a = failc gt [S "Expected\t",V a,S "\n(Pair)\n"]
-- Labels cannot be inferred because there is no way to know
-- what the other labels are.
check' gt @ (Label l,g) a @ (VEnum ls) | l `elem` ls = return ()
check' gt @ (Label l,g) a = failc gt [S "Expected\t",V a,S "\n(Label)\n"]
-- To check that [sigma] is a type, it's sufficient to know
-- that sigma is a type. The alternative would seem to be to
-- assume that ^Type == Type, but that does not work.
check' (Box a,g) VType =
    check (a,g) ty
check' (Box t,g) (VLift a) =
    check (t,g) a
check' gt @ (Box _,g) a = failc gt [S "Expected\t",V a,S "\n(Box)\n"]
check' t a =
    do b <- infer' t
       catchE (eq a b)
         (\ s -> failc t [S "Expected:\t",V a,
                          S "\nFound:\t",V b,S $ "\n(check)\n"])
-- ++s++"\n"++(show a)++"\n"++(show b)])
-- useful for debugging.

inferVar :: Env e => Clos Name -> Eval e (Clos Type)
inferVar (x,g) =
    case lookupCon g x of
      Just a  -> return a
      Nothing -> fail ("Undefined variable: "++x++"\n(inferVar)\n")

infer :: Env e => Clos Term -> Eval e (Clos Type)
--infer (g,t) | trace ("infer\ng ="++(show g)++"\n t="++(show t)++"\n") False = undefined

infer (Var x,g) = inferVar (x,g)

infer (Let tel t,g) = 
    do g' <- checkProg (tel,g)
       infer (t,g')  

infer (Type,g) = return ty

infer (Q _ (a,(x,b)),g) = 
    do check (a,g) ty
       (_,g') <- tdecl x g (a,g)
       check (b,g') ty
       return ty

infer gt@(t :. u,g) = 
    do piab <- infer' (t,g)
       case piab of 
         (VQ Pi ((a,(x,b)),s)) -> do check (u,g) (a,s)
                                     subst (x,(b,s)) (u,g)
         _ -> failc gt [S "Pi type expected, but found:\t",
                        V piab,
                        S "\n(app)\n"]

infer (Enum _,_) = return ty

infer (Box t,g) =
    liftM (\ (a,s) -> (Lift a,s)) (infer (t,g))

-- TODO: either use infer', or explain why forced eval
-- cannot be used here.
infer gt@(Force t,g) =
    do a  <- infer (t,g)
       a' <- eval a
       case a' of
         VLift b -> return b
         _       -> failc gt [S "Lifted type expected\n(Force)\n"]
infer (Lift a,g) =
    do check (a,g) ty
       return ty

infer gt = failc gt [S "Not inferable\n(infer)\n"]


-- | Infers a type and evaluates it.
infer' :: Env e => Clos Term -> Eval e Val
infer' gt =
    do a <- infer gt
       feval a

checkProg :: Env e => Clos Prog -> Eval e Scope
checkProg ([],g) = return g
checkProg ((Decl x a):tel,g) = 
    do check (a,g) ty 
       (_,g') <- decl x (PrtInfo {name=x, expand=False}) g (Just (a,g))
       checkProg (tel,g')
checkProg ((Defn x t):tel,g) =
    do a <- inferVar (x,g)
       check (t,g) a
       i <- getId x g
       defn' i (t,g)
       checkProg (tel,g)