#if __GLASGOW_HASKELL__ <= 708
#endif
module Agda.TypeChecking.Monad.Context where
import Control.Applicative
import Control.Monad.Reader
import Control.Monad.State
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Monoid
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Scope.Monad (getLocalVars, setLocalVars)
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Monad.Open
import Agda.TypeChecking.Monad.Options
import Agda.Utils.Except ( MonadError(catchError) )
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List ((!!!), downFrom)
import Agda.Utils.Pretty
import Agda.Utils.Size
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
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
withModuleParameters :: ModuleParamDict -> TCM a -> TCM a
withModuleParameters mp ret = do
old <- use stModuleParameters
stModuleParameters .= mp
x <- ret
stModuleParameters .= old
return x
updateModuleParameters :: (MonadTCM tcm, MonadDebug tcm)
=> Substitution -> tcm a -> tcm a
updateModuleParameters sub ret = do
pm <- use stModuleParameters
let showMP pref mps = List.intercalate "\n" $
[ p ++ show m ++ " : " ++ show (mpSubstitution mp)
| (p, (m, mp)) <- zip (pref : repeat (map (const ' ') pref))
(Map.toList mps)
]
verboseS "tc.cxt.param" 105 $ do
cxt <- reverse <$> getContext
reportSLn "tc.cxt.param" 105 $ unlines $
[ "updatingModuleParameters"
, " sub = " ++ show sub
, " cxt (last added last in list) = " ++ unwords (map (show . fst . unDom) cxt)
, showMP " old = " pm
]
let pm' = applySubst sub pm
reportSLn "tc.cxt.param" 105 $ showMP " new = " pm'
stModuleParameters .= pm'
x <- ret
pm1 <- use stModuleParameters
let pm'' = Map.union pm (defaultModuleParameters <$ Map.difference pm1 pm)
stModuleParameters .= pm''
reportSLn "tc.cxt.param" 105 $ showMP " restored = " pm''
return x
weakenModuleParameters :: (MonadTCM tcm, MonadDebug tcm)
=> Nat -> tcm a -> tcm a
weakenModuleParameters n = updateModuleParameters (raiseS n)
getModuleParameterSub :: (Functor m, ReadTCState m) => ModuleName -> m Substitution
getModuleParameterSub m = do
r <- (^. stModuleParameters) <$> getTCState
case Map.lookup m r of
Nothing -> return IdS
Just mp -> return $ mpSubstitution mp
addCtx :: MonadTCM tcm => Name -> Dom Type -> tcm a -> tcm a
addCtx x a ret = do
ce <- mkContextEntry $ (x,) <$> a
modifyContext (ce :) ret
unshadowName :: MonadTCM tcm => Name -> tcm Name
unshadowName x = do
ctx <- map (nameConcrete . fst . unDom) <$> getContext
return $ head $ filter (notTaken ctx) $ iterate nextName x
where
notTaken xs x = isNoName x || nameConcrete x `notElem` xs
class AddContext b where
addContext :: MonadTCM tcm => b -> tcm a -> tcm a
contextSize :: b -> Nat
addContext' :: (MonadTCM tcm, MonadDebug tcm, AddContext b)
=> b -> tcm a -> tcm a
addContext' cxt = addContext cxt . weakenModuleParameters (contextSize cxt)
newtype KeepNames a = KeepNames a
#if __GLASGOW_HASKELL__ >= 710
instance AddContext a => AddContext [a] where
#else
instance AddContext a => AddContext [a] where
#endif
addContext = flip (foldr addContext)
contextSize = sum . map contextSize
instance AddContext (Name, Dom Type) where
addContext = uncurry addCtx
contextSize _ = 1
instance AddContext (Dom (Name, Type)) where
addContext = addContext . distributeF
contextSize _ = 1
instance AddContext (Dom (String, Type)) where
addContext = addContext . distributeF
contextSize _ = 1
instance AddContext ([Name], Dom Type) where
addContext (xs, dom) = addContext (bindsToTel' id xs dom)
contextSize (xs, _) = length xs
instance AddContext ([WithHiding Name], Dom Type) where
addContext ([] , dom) = id
addContext (WithHiding h x : xs, dom) =
addContext (x , mapHiding (mappend h) dom) .
addContext (xs, raise 1 dom)
contextSize (xs, _) = length xs
instance AddContext (String, Dom Type) where
addContext (s, dom) ret = do
x <- unshadowName =<< freshName_ s
addCtx x dom ret
contextSize _ = 1
instance AddContext (KeepNames String, Dom Type) where
addContext (KeepNames s, dom) ret = do
x <- freshName_ s
addCtx x dom ret
contextSize _ = 1
instance AddContext (Dom Type) where
addContext dom = addContext ("_", dom)
contextSize _ = 1
instance AddContext Name where
addContext x = addContext (x, dummyDom)
contextSize _ = 1
#if __GLASGOW_HASKELL__ >= 710
instance AddContext String where
#else
instance AddContext String where
#endif
addContext s = addContext (s, dummyDom)
contextSize _ = 1
instance AddContext (KeepNames Telescope) where
addContext (KeepNames tel) ret = loop tel where
loop EmptyTel = ret
loop (ExtendTel t tel) = underAbstraction' KeepNames t tel loop
contextSize (KeepNames tel) = size tel
instance AddContext Telescope where
addContext tel ret = loop tel where
loop EmptyTel = ret
loop (ExtendTel t tel) = underAbstraction t tel loop
contextSize = size
dummyDom :: Dom Type
dummyDom = defaultDom typeDontCare
underAbstraction :: (Subst t a, MonadTCM tcm) => Dom Type -> Abs a -> (a -> tcm b) -> tcm b
underAbstraction = underAbstraction' id
underAbstraction' :: (Subst t a, MonadTCM tcm, AddContext (name, Dom Type)) =>
(String -> name) -> Dom Type -> Abs a -> (a -> tcm b) -> tcm b
underAbstraction' _ _ (NoAbs _ v) k = k v
underAbstraction' wrap t a k = addContext (wrap $ realName $ absName a, t) $ k $ absBody a
where
realName s = if isNoName s then "x" else argNameToString s
underAbstraction_ :: (Subst t a, MonadTCM tcm) => Abs a -> (a -> tcm b) -> tcm b
underAbstraction_ = underAbstraction dummyDom
addLetBinding :: MonadTCM tcm => ArgInfo -> Name -> Term -> Type -> tcm a -> tcm a
addLetBinding info x v t0 ret = do
let t = Dom info t0
vt <- liftTCM $ makeOpen (v, t)
flip local ret $ \e -> e { envLetBindings = Map.insert x vt $ envLetBindings e }
getContext :: MonadReader TCEnv m => m [Dom (Name, Type)]
getContext = asks $ map ctxEntry . envContext
getContextSize :: (Applicative m, MonadReader TCEnv m) => m Nat
getContextSize = length <$> asks envContext
getContextArgs :: (Applicative m, MonadReader TCEnv m) => m Args
getContextArgs = reverse . zipWith mkArg [0..] <$> getContext
where mkArg i (Dom info _) = Arg info $ var i
getContextTerms :: (Applicative m, MonadReader TCEnv m) => m [Term]
getContextTerms = map var . downFrom <$> getContextSize
getContextTelescope :: (Applicative m, MonadReader TCEnv m) => m Telescope
getContextTelescope = telFromList' nameToArgName . reverse <$> getContext
getContextId :: MonadReader TCEnv m => m [CtxId]
getContextId = asks $ map ctxId . envContext
getContextNames :: (Applicative m, MonadReader TCEnv m) => m [Name]
getContextNames = map (fst . unDom) <$> getContext
lookupBV :: MonadReader TCEnv m => Nat -> m (Dom (Name, Type))
lookupBV n = do
ctx <- getContext
let failure = fail $ "de Bruijn index out of scope: " ++ show n ++
" in context " ++ prettyShow (map (fst . unDom) ctx)
maybe failure (return . fmap (raise $ n + 1)) $ ctx !!! n
typeOfBV' :: (Applicative m, MonadReader TCEnv m) => Nat -> m (Dom Type)
typeOfBV' n = fmap snd <$> lookupBV n
typeOfBV :: (Applicative m, MonadReader TCEnv m) => Nat -> m Type
typeOfBV i = unDom <$> typeOfBV' i
nameOfBV :: (Applicative m, MonadReader TCEnv m) => Nat -> m Name
nameOfBV n = fst . unDom <$> lookupBV n
getVarInfo
#if __GLASGOW_HASKELL__ <= 708
:: (Applicative m, MonadReader TCEnv m)
#else
:: MonadReader TCEnv m
#endif
=> Name -> m (Term, Dom Type)
getVarInfo x =
do ctx <- getContext
def <- asks envLetBindings
case List.findIndex ((==x) . fst . unDom) ctx of
Just n -> do
t <- typeOfBV' n
return (var n, t)
_ ->
case Map.lookup x def of
Just vt -> getOpen vt
_ -> fail $ "unbound variable " ++ prettyShow (nameConcrete x)