module Agda.TypeChecking.CheckInternal
( checkType
, checkInternal
, checkInternal'
, defaultAction, Action(..)
, infer
) where
import Control.Arrow ((&&&), (***), first, second)
import Control.Applicative
import Control.Monad
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Datatypes (getConType)
import Agda.TypeChecking.Level
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.ProjectionLike (elimView)
import Agda.TypeChecking.Records (getDefType)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Utils.Functor (($>))
import Agda.Utils.Monad
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
checkType :: Type -> TCM ()
checkType t = void $ checkType' t
checkType' :: Type -> TCM Sort
checkType' t = do
reportSDoc "tc.check.internal" 20 $ sep
[ text "checking internal type "
, prettyTCM t
]
v <- elimView True $ unEl t
case ignoreSharing v of
Pi a b -> do
s1 <- checkType' $ unDom a
s2 <- (b $>) <$> do
addContext (absName b, a) $ do
checkType' $ absBody b
return $ dLub s1 s2
Sort s -> do
_ <- checkSort defaultAction s
return $ sSuc s
Var i es -> do
a <- typeOfBV i
checkTypeSpine a (Var i []) es
Def f es -> do
a <- defType <$> getConstInfo f
checkTypeSpine a (Def f []) es
MetaV x es -> do
a <- metaType x
checkTypeSpine a (MetaV x []) es
v@Lam{} -> typeError $ InvalidType v
v@Con{} -> typeError $ InvalidType v
v@Lit{} -> typeError $ InvalidType v
v@Level{} -> typeError $ InvalidType v
DontCare v -> checkType' $ t $> v
Shared{} -> __IMPOSSIBLE__
checkTypeSpine :: Type -> Term -> Elims -> TCM Sort
checkTypeSpine a self es = shouldBeSort =<< do snd <$> inferSpine a self es
data Action = Action { preAction :: Type -> Term -> TCM Term
, postAction :: Type -> Term -> TCM Term }
defaultAction :: Action
defaultAction = Action (\ _ v -> return v) (\ _ v -> return v)
checkInternal :: Term -> Type -> TCM ()
checkInternal v t = void $ checkInternal' defaultAction v t
checkInternal' :: Action -> Term -> Type -> TCM Term
checkInternal' action v t = do
reportSDoc "tc.check.internal" 20 $ sep
[ text "checking internal "
, nest 2 $ sep [ prettyTCM v <+> text ":"
, nest 2 $ prettyTCM t ] ]
v <- elimView True =<< preAction action t v
postAction action t =<< case ignoreSharing v of
Var i es -> do
a <- typeOfBV i
checkSpine action a (Var i []) es t
Def f es -> do
a <- defType <$> getConstInfo f
checkSpine action a (Def f []) es t
MetaV x es -> do
a <- metaType x
checkSpine action a (MetaV x []) es t
Con c vs -> do
TelV tel t <- telView t
addCtxTel tel $ do
let failure = typeError $ DoesNotConstructAnElementOf (conName c) t
vs' = raise (size tel) vs ++ teleArgs tel
a <- maybe failure return =<< getConType c t
Con c vs2 <- checkArgs action a (Con c []) vs' t
return $ applySubst (strengthenS __IMPOSSIBLE__ (size tel))
$ Con c (take (length vs) vs2)
Lit l -> Lit l <$ ((`subtype` t) =<< litType l)
Lam ai vb -> do
(a, b) <- shouldBePi t
checkArgInfo ai $ domInfo a
addContext (suggest vb b, a) $ do
Lam ai . Abs (absName vb) <$> checkInternal' action (absBody vb) (absBody b)
Pi a b -> do
s <- shouldBeSort t
when (s == SizeUniv) $ typeError $ FunctionTypeInSizeUniv v
let st = sort s
sa = getSort a
sb = getSort (unAbs b)
mkDom v = El sa v <$ a
mkRng v = fmap (v <$) b
goInside = case b of Abs{} -> addContext (absName b, a)
NoAbs{} -> id
a <- mkDom <$> checkInternal' action (unEl $ unDom a) (sort sa)
goInside $ Pi a . mkRng <$> checkInternal' action (unEl $ unAbs b) (sort sb)
Sort s -> do
s <- checkSort action s
Sort s <$ ((sSuc s `leqSort`) =<< shouldBeSort t)
Level l -> do
l <- checkLevel action l
Level l <$ ((`subtype` t) =<< levelType)
DontCare v -> DontCare <$> checkInternal' action v t
Shared{} -> __IMPOSSIBLE__
checkSpine :: Action -> Type -> Term -> Elims -> Type -> TCM Term
checkSpine action a self es t = do
reportSDoc "tc.check.internal" 20 $ sep
[ text "checking spine "
, nest 2 $ sep [ parens (sep [ prettyTCM self <+> text ":"
, nest 2 $ prettyTCM a ])
, nest 4 $ prettyTCM es <+> text ":"
, nest 2 $ prettyTCM t ] ]
((v, v'), t') <- inferSpine' action a self self es
v' <$ coerceSize subtype v t' t
checkArgs :: Action -> Type -> Term -> Args -> Type -> TCM Term
checkArgs action a self vs t = checkSpine action a self (map Apply vs) t
checkArgInfo :: ArgInfo -> ArgInfo -> TCM ()
checkArgInfo ai ai' = do
checkHiding (getHiding ai) (getHiding ai')
checkRelevance (getRelevance ai) (getRelevance ai')
checkHiding :: Hiding -> Hiding -> TCM ()
checkHiding h h' = unless (h == h') $ typeError $ HidingMismatch h h'
checkRelevance :: Relevance -> Relevance -> TCM ()
checkRelevance r0 r0' = unless (r == r') $ typeError $ RelevanceMismatch r r'
where
r = canon r0
r' = canon r0'
canon Forced{} = Relevant
canon UnusedArg = Relevant
canon r = r
infer :: Term -> TCM Type
infer v = do
case ignoreSharing v of
Var i es -> do
a <- typeOfBV i
snd <$> inferSpine a (Var i []) es
Def f (Apply a : es) -> inferDef' f a es
Def f es -> inferDef f es
MetaV x es -> do
a <- metaType x
snd <$> inferSpine a (MetaV x []) es
Shared{} -> __IMPOSSIBLE__
_ -> __IMPOSSIBLE__
inferDef :: QName -> Elims -> TCM Type
inferDef f es = do
a <- defType <$> getConstInfo f
snd <$> inferSpine a (Def f []) es
inferDef' :: QName -> Arg Term -> Elims -> TCM Type
inferDef' f a es = do
isProj <- isProjection f
case isProj of
Just Projection{ projIndex = n } | n > 0 -> do
let self = unArg a
b <- infer self
snd <$> inferSpine b self (Proj f : es)
_ -> inferDef f (Apply a : es)
inferSpine :: Type -> Term -> Elims -> TCM (Term, Type)
inferSpine a v es = first fst <$> inferSpine' defaultAction a v v es
inferSpine' :: Action -> Type -> Term -> Term -> Elims -> TCM ((Term, Term), Type)
inferSpine' action t self self' [] = return ((self, self'), t)
inferSpine' action t self self' (e : es) = do
reportSDoc "tc.infer.internal" 30 $ sep
[ text "inferSpine': "
, text "type t = " <+> prettyTCM t
, text "self = " <+> prettyTCM self
, text "self' = " <+> prettyTCM self'
, text "eliminated by e = " <+> prettyTCM e
]
case e of
Apply (Arg ai v) -> do
(a, b) <- shouldBePi t
checkArgInfo ai $ domInfo a
v' <- checkInternal' action v $ unDom a
inferSpine' action (b `absApp` v) (self `applyE` [e]) (self' `applyE` [Apply (Arg ai v')]) es
Proj f -> do
(a, b) <- shouldBePi =<< shouldBeProjectible t f
u <- f `applyDef` (argFromDom a $> self)
u' <- f `applyDef` (argFromDom a $> self')
inferSpine' action (b `absApp` self) u u' es
shouldBeProjectible :: Type -> QName -> TCM Type
shouldBeProjectible t f = maybe failure return =<< getDefType f =<< reduce t
where failure = typeError $ ShouldBeRecordType t
shouldBePi :: Type -> TCM (Dom Type, Abs Type)
shouldBePi t = ifPiType t (\ a b -> return (a, b)) $ const $ typeError $ ShouldBePi t
shouldBeSort :: Type -> TCM Sort
shouldBeSort t = ifIsSort t return (typeError $ ShouldBeASort t)
ifIsSort :: Type -> (Sort -> TCM a) -> TCM a -> TCM a
ifIsSort t yes no = do
t <- reduce t
case ignoreSharing $ unEl t of
Sort s -> yes s
_ -> no
checkSort :: Action -> Sort -> TCM Sort
checkSort action s =
case s of
Type l -> Type <$> checkLevel action l
Prop -> __IMPOSSIBLE__
Inf -> typeError $ SetOmegaNotValidType
SizeUniv -> typeError $ InvalidTypeSort s
DLub a b -> do
a <- checkSort action a
addContext (absName b, defaultDom (sort a) :: Dom Type) $ do
DLub a . Abs (absName b) <$> checkSort action (absBody b)
checkLevel :: Action -> Level -> TCM Level
checkLevel action (Max ls) = Max <$> mapM checkPlusLevel ls
where
checkPlusLevel l@ClosedLevel{} = return l
checkPlusLevel (Plus k l) = Plus k <$> checkLevelAtom l
checkLevelAtom l = do
lvl <- levelType
UnreducedLevel <$> case l of
MetaLevel x es -> checkInternal' action (MetaV x es) lvl
BlockedLevel _ v -> checkInternal' action v lvl
NeutralLevel _ v -> checkInternal' action v lvl
UnreducedLevel v -> checkInternal' action v lvl
metaType :: MetaId -> TCM Type
metaType x = jMetaType . mvJudgement <$> lookupMeta x
subtype :: Type -> Type -> TCM ()
subtype t1 t2 = do
ifIsSort t1 (\ s1 -> (s1 `leqSort`) =<< shouldBeSort t2) $
leqType t1 t2