module Agda.TypeChecking.Monad.Context where
import Control.Monad.Reader
import Data.List hiding (sort)
import qualified Data.Map as Map
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Internal
import Agda.Syntax.Scope.Monad (getLocalVars, setLocalVars)
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Monad.Open
import Agda.Utils.Functor
import Agda.Utils.List ((!!!), downFrom)
import Agda.Utils.Monad
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 cont = do
locals <- liftTCM $ getLocalVars
liftTCM $ setLocalVars []
a <- modifyContext (const []) cont
liftTCM $ setLocalVars locals
return a
escapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a
escapeContext n = modifyContext $ drop n
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 $ (x',) <$> a
modifyContext (ce :) ret
where
notTaken xs x = isNoName x || nameConcrete x `notElem` xs
class AddContext b where
addContext :: MonadTCM tcm => b -> tcm a -> tcm a
instance AddContext a => AddContext [a] where
addContext = flip (foldr addContext)
instance AddContext (Name, Dom Type) where
addContext = uncurry addCtx
instance AddContext (Dom (Name, Type)) where
addContext = addContext . distributeF
instance AddContext ([Name], Dom Type) where
addContext (xs, dom) = addContext (bindsToTel' id xs dom)
instance AddContext (String, Dom Type) where
addContext (s, dom) ret = do
x <- freshName_ s
addCtx x dom ret
instance AddContext (Dom (String, Type)) where
addContext = addContext . distributeF
instance AddContext Name where
addContext x = addContext (x, dummyDom)
instance AddContext String where
addContext s = addContext (s, dummyDom)
instance AddContext Telescope where
addContext tel ret = loop tel where
loop EmptyTel = ret
loop (ExtendTel t tel) = underAbstraction t tel loop
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
addCtxStrings_ :: MonadTCM tcm => [String] -> tcm a -> tcm a
addCtxStrings_ = flip (foldr addCtxString_)
dummyDom :: Dom Type
dummyDom = Common.Dom defaultArgInfo $ 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
x <- freshName_ $ realName $ absName a
addCtx x t $ k $ absBody a
where
realName s = if isNoName s then "x" else argNameToString 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 tel ret = loop tel where
loop EmptyTel = ret
loop (ExtendTel t tel) = underAbstraction t tel loop
addLetBinding :: MonadTCM tcm => ArgInfo -> Name -> Term -> Type -> tcm a -> tcm a
addLetBinding info x v t0 ret = do
let t = Common.Dom (setHiding NotHidden info) 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 = reverse . zipWith mkArg [0..] <$> getContext
where mkArg i (Common.Dom info _) = Common.Arg info $ var i
getContextTerms :: MonadTCM tcm => tcm [Term]
getContextTerms = map var . downFrom <$> getContextSize
getContextTelescope :: MonadTCM tcm => tcm Telescope
getContextTelescope = telFromList' nameToArgName . reverse <$> getContext
getContextId :: MonadTCM tcm => tcm [CtxId]
getContextId = asks $ map ctxId . envContext
lookupBV :: MonadTCM tcm => Nat -> tcm (Dom (Name, Type))
lookupBV n = do
ctx <- getContext
let failure = fail $ "deBruijn index out of scope: " ++ show n ++
" in context " ++ show (map (fst . unDom) ctx)
maybe failure (return . fmap (raise $ n + 1)) $ ctx !!! n
typeOfBV' :: MonadTCM tcm => Nat -> tcm (Dom Type)
typeOfBV' n = fmap snd <$> lookupBV n
typeOfBV :: MonadTCM tcm => Nat -> tcm Type
typeOfBV i = unDom <$> typeOfBV' i
nameOfBV :: MonadTCM tcm => Nat -> tcm Name
nameOfBV n = fst . unDom <$> lookupBV n
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 (nameConcrete x)