module Agda.TypeChecking.Monad.Open
( makeOpen
, makeClosed, isClosed
, getOpen
, tryOpen
) where
import Control.Applicative
import Control.Monad
import Control.Monad.Reader
import Data.List
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Context
import Agda.Utils.Except ( MonadError(catchError) )
makeOpen :: a -> TCM (Open a)
makeOpen x = do
ctx <- getContextId
return $ OpenThing ctx x
makeClosed :: a -> Open a
makeClosed = OpenThing []
isClosed :: Open a -> Bool
isClosed (OpenThing cxt _) = null cxt
getOpen :: (Subst t a, MonadReader TCEnv m) => Open a -> m a
getOpen (OpenThing [] x) = return x
getOpen (OpenThing ctx x) = do
ctx' <- getContextId
unless (ctx `isSuffixOf` ctx') $ fail $ "thing out of context (" ++ show ctx ++ " is not a sub context of " ++ show ctx' ++ ")"
return $ raise (genericLength ctx' genericLength ctx) x
tryOpen :: (Subst t a, MonadReader TCEnv m) => Open a -> m (Maybe a)
tryOpen (OpenThing [] x) = return $ Just x
tryOpen (OpenThing ctx x) = do
ctx' <- getContextId
if (ctx `isSuffixOf` ctx')
then return $ Just $ raise (genericLength ctx' genericLength ctx) x
else return Nothing