module Agda.TypeChecking.Monad.Context where
import Control.Monad.Reader
import Data.List hiding (sort)
import qualified Data.Map as Map
import Agda.Syntax.Concrete.Name (isNoName)
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Monad.Open
import Agda.Utils.Monad
import Agda.Utils.Fresh
#include "../../undefined.h"
import Agda.Utils.Impossible
modifyContextEntry :: (Dom (Name, Type) -> Dom (Name, Type)) -> ContextEntry -> ContextEntry
modifyContextEntry f ce = ce { ctxEntry = f (ctxEntry ce) }
modifyContextEntries :: (Dom (Name, Type) -> Dom (Name, Type)) -> Context -> Context
modifyContextEntries f = map (modifyContextEntry f)
modifyContext :: MonadTCM tcm => (Context -> Context) -> tcm a -> tcm a
modifyContext f = local $ \ e -> e { envContext = f (envContext e) }
mkContextEntry :: MonadTCM tcm => Dom (Name, Type) -> tcm ContextEntry
mkContextEntry x = do
i <- fresh
return $ Ctx i x
inContext :: MonadTCM tcm => [Dom (Name, Type)] -> tcm a -> tcm a
inContext xs ret = do
ctx <- mapM mkContextEntry xs
modifyContext (const ctx) ret
inTopContext :: MonadTCM tcm => tcm a -> tcm a
inTopContext = modifyContext $ const []
escapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a
escapeContext n = modifyContext $ drop n
escapeContextToTopLevel :: MonadTCM tcm => tcm a -> tcm a
escapeContextToTopLevel = modifyContext $ const []
addCtx :: MonadTCM tcm => Name -> Dom Type -> tcm a -> tcm a
addCtx x a ret = do
ctx <- map (nameConcrete . fst . unDom) <$> getContext
let x' = head $ filter (notTaken ctx) $ iterate nextName x
ce <- mkContextEntry $ fmap ((,) x') a
modifyContext (ce :) ret
where
notTaken xs x = isNoName (nameConcrete x) || nameConcrete x `notElem` xs
addContext :: MonadTCM tcm => [Dom (Name, Type)] -> tcm a -> tcm a
addContext ctx m =
foldr (\arg -> addCtx (fst $ unDom arg) (fmap snd arg)) m ctx
addCtxs :: MonadTCM tcm => [Name] -> Dom Type -> tcm a -> tcm a
addCtxs [] _ k = k
addCtxs (x:xs) t k = addCtx x t $ addCtxs xs (raise 1 t) k
addCtxString :: MonadTCM tcm => String -> Dom Type -> tcm a -> tcm a
addCtxString s a m = do
x <- freshName_ s
addCtx x a m
addCtxString_ :: MonadTCM tcm => String -> tcm a -> tcm a
addCtxString_ s = addCtxString s dummyDom
dummyDom :: Dom Type
dummyDom = Dom NotHidden Relevant $ El Prop $ Sort Prop
underAbstraction :: (Subst a, MonadTCM tcm) => Dom Type -> Abs a -> (a -> tcm b) -> tcm b
underAbstraction _ (NoAbs _ v) k = k v
underAbstraction t a k = do
xs <- map (nameConcrete . fst . unDom) <$> getContext
x <- freshName_ $ realName $ absName a
let y = head $ filter (notTaken xs) $ iterate nextName x
addCtx y t $ k $ absBody a
where
notTaken xs x = isNoName (nameConcrete x) || notElem (nameConcrete x) xs
realName "_" = "x"
realName s = s
underAbstraction_ :: (Subst a, MonadTCM tcm) => Abs a -> (a -> tcm b) -> tcm b
underAbstraction_ = underAbstraction dummyDom
addCtxTel :: MonadTCM tcm => Telescope -> tcm a -> tcm a
addCtxTel EmptyTel ret = ret
addCtxTel (ExtendTel t tel) ret = underAbstraction t tel $ \tel -> addCtxTel tel ret
addLetBinding :: MonadTCM tcm => Relevance -> Name -> Term -> Type -> tcm a -> tcm a
addLetBinding rel x v t0 ret = do
let t = Dom NotHidden rel t0
vt <- liftTCM $ makeOpen (v, t)
flip local ret $ \e -> e { envLetBindings = Map.insert x vt $ envLetBindings e }
getContext :: MonadTCM tcm => tcm [Dom (Name, Type)]
getContext = asks $ map ctxEntry . envContext
getContextSize :: MonadTCM tcm => tcm Nat
getContextSize = genericLength <$> asks envContext
getContextArgs :: MonadTCM tcm => tcm Args
getContextArgs = do
ctx <- getContext
return $ reverse $ [ Arg h r $ var i | (Dom h r _, i) <- zip ctx [0..] ]
getContextTerms :: MonadTCM tcm => tcm [Term]
getContextTerms = map unArg <$> getContextArgs
getContextTelescope :: MonadTCM tcm => tcm Telescope
getContextTelescope = foldr extTel EmptyTel . reverse <$> getContext
where
extTel (Dom h r (x, t)) = ExtendTel (Dom h r t) . Abs (show x)
getContextId :: MonadTCM tcm => tcm [CtxId]
getContextId = asks $ map ctxId . envContext
typeOfBV' :: MonadTCM tcm => Nat -> tcm (Dom Type)
typeOfBV' n =
do ctx <- getContext
Dom h r (_,t) <- ctx !!! n
return $ Dom h r $ raise (n + 1) t
typeOfBV :: MonadTCM tcm => Nat -> tcm Type
typeOfBV i = unDom <$> typeOfBV' i
nameOfBV :: MonadTCM tcm => Nat -> tcm Name
nameOfBV n =
do ctx <- getContext
Dom _ _ (x,_) <- ctx !!! n
return x
xs !!! n = xs !!!! n
where
[] !!!! _ = do
ctx <- getContext
fail $ "deBruijn index out of scope: " ++ show n ++ " in context " ++ show (map (fst . unDom) ctx)
(x:_) !!!! 0 = return x
(_:xs) !!!! n = xs !!!! (n 1)
getVarInfo :: MonadTCM tcm => Name -> tcm (Term, Dom Type)
getVarInfo x =
do ctx <- getContext
def <- asks envLetBindings
case findIndex ((==x) . fst . unDom) ctx of
Just n -> do
t <- typeOfBV' n
return (Var n [], t)
_ ->
case Map.lookup x def of
Just vt -> liftTCM $ getOpen vt
_ -> fail $ "unbound variable " ++ show x