module Agda.TypeChecking.Monad.Open
( makeOpen
, getOpen
, tryGetOpen
, isClosed
) where
import Control.Monad
import Control.Monad.Reader
import qualified Data.List as List
import Agda.Syntax.Internal
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Monad.Base
import {-# SOURCE #-} Agda.TypeChecking.Monad.Context
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Except ( MonadError(catchError) )
makeOpen :: a -> TCM (Open a)
makeOpen x = do
cp <- viewTC eCurrentCheckpoint
return $ OpenThing cp x
getOpen :: (Subst Term a, MonadTCEnv m) => Open a -> m a
getOpen (OpenThing cp x) = do
sub <- checkpointSubstitution cp
return $ applySubst sub x
tryGetOpen :: (Subst Term a, MonadTCEnv m) => Open a -> m (Maybe a)
tryGetOpen (OpenThing cp x) = fmap (`applySubst` x) <$> viewTC (eCheckpoints . key cp)
isClosed :: Open a -> Bool
isClosed (OpenThing cp _) = cp == 0