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 :: (Arg (Name, Type) -> Arg (Name, Type)) -> ContextEntry -> ContextEntry
modifyContextEntry f ce = ce { ctxEntry = f (ctxEntry ce) }
modifyContextEntries :: (Arg (Name, Type) -> Arg (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 => Arg (Name, Type) -> tcm ContextEntry
mkContextEntry x = do
i <- fresh
return $ Ctx i x
addCtx :: MonadTCM tcm => Name -> Arg Type -> tcm a -> tcm a
addCtx x a ret = do
ctx <- map (nameConcrete . fst . unArg) <$> getContext
let x' = head $ filter (notTaken ctx) $ iterate nextName x
ce <- mkContextEntry $ fmap ((,) x') a
flip local ret $ \e -> e { envContext = ce : envContext e }
where
notTaken xs x = isNoName (nameConcrete x) || nameConcrete x `notElem` xs
addContext :: MonadTCM tcm => [Arg (Name, Type)] -> tcm a -> tcm a
addContext ctx m =
foldr (\arg -> addCtx (fst $ unArg arg) (fmap snd arg)) m ctx
addCtxString :: MonadTCM tcm => String -> Arg Type -> tcm a -> tcm a
addCtxString s a m = do
x <- freshName_ s
addCtx x a m
inContext :: MonadTCM tcm => [Arg (Name, Type)] -> tcm a -> tcm a
inContext xs ret = do
ctx <- mapM mkContextEntry xs
flip local ret $ \e -> e { envContext = ctx }
underAbstraction :: (Raise a, MonadTCM tcm) => Arg Type -> Abs a -> (a -> tcm b) -> tcm b
underAbstraction _ (NoAbs _ v) k = k v
underAbstraction t a k = do
xs <- map (nameConcrete . fst . unArg) <$> 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 "_" = "y"
realName s = s
underAbstraction_ :: (Raise a, MonadTCM tcm) => Abs a -> (a -> tcm b) -> tcm b
underAbstraction_ = underAbstraction (Arg NotHidden Relevant $ sort Prop)
addCtxTel :: MonadTCM tcm => Telescope -> tcm a -> tcm a
addCtxTel EmptyTel ret = ret
addCtxTel (ExtendTel t tel) ret = underAbstraction t tel $ \tel -> addCtxTel tel ret
getContext :: MonadTCM tcm => tcm [Arg (Name, Type)]
getContext = asks $ map ctxEntry . envContext
getContextArgs :: MonadTCM tcm => tcm Args
getContextArgs = do
ctx <- getContext
return $ reverse $ [ Arg h r $ Var i [] | (Arg 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 (Arg h r (x, t)) = ExtendTel (Arg h r t) . Abs (show x)
addCtxs :: MonadTCM tcm => [Name] -> Arg Type -> tcm a -> tcm a
addCtxs [] _ k = k
addCtxs (x:xs) t k = addCtx x t $ addCtxs xs (raise 1 t) k
getContextId :: MonadTCM tcm => tcm [CtxId]
getContextId = asks $ map ctxId . envContext
addLetBinding :: MonadTCM tcm => Relevance -> Name -> Term -> Type -> tcm a -> tcm a
addLetBinding rel x v t0 ret = do
let t = Arg NotHidden rel t0
vt <- liftTCM $ makeOpen (v, t)
flip local ret $ \e -> e { envLetBindings = Map.insert x vt $ envLetBindings e }
typeOfBV' :: MonadTCM tcm => Nat -> tcm (Arg Type)
typeOfBV' n =
do ctx <- getContext
Arg h r (_,t) <- ctx !!! n
return $ Arg h r $ raise (n + 1) t
typeOfBV :: MonadTCM tcm => Nat -> tcm Type
typeOfBV i = unArg <$> typeOfBV' i
nameOfBV :: MonadTCM tcm => Nat -> tcm Name
nameOfBV n =
do ctx <- getContext
Arg _ _ (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 . unArg) ctx)
(x:_) !!!! 0 = return x
(_:xs) !!!! n = xs !!!! (n 1)
getVarInfo :: MonadTCM tcm => Name -> tcm (Term, Arg Type)
getVarInfo x =
do ctx <- getContext
def <- asks envLetBindings
case findIndex ((==x) . fst . unArg) ctx of
Just n0 ->
do let n = fromIntegral n0
t <- typeOfBV' n
return (Var n [], t)
_ ->
case Map.lookup x def of
Just vt -> liftTCM $ getOpen vt
_ -> fail $ "unbound variable " ++ show x
escapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a
escapeContext n = local $ \e -> e { envContext = drop n $ envContext e }