    -- {-# LANGUAGE CPP #-}

    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) )

    -- | Create an open term in the current context.
    makeOpen :: a -> TCM (Open a)
    makeOpen x = do
        cp <- viewTC eCurrentCheckpoint
        return $ OpenThing cp x

    -- | Extract the value from an open term. The checkpoint at which it was
    --   created must be in scope.
    getOpen :: (Subst Term a, MonadTCEnv m) => Open a -> m a
    getOpen (OpenThing cp x) = do
      sub <- checkpointSubstitution cp
      return $ applySubst sub x

    -- | Extract the value from an open term. Returns `Nothing` if the checkpoint
    --   at which it was created is not in scope.
    tryGetOpen :: (Subst Term a, MonadTCEnv m) => Open a -> m (Maybe a)
    tryGetOpen (OpenThing cp x) = fmap (`applySubst` x) <$> viewTC (eCheckpoints . key cp)

    -- | An 'Open' is closed if it has checkpoint 0.
    isClosed :: Open a -> Bool
    isClosed (OpenThing cp _) = cp == 0