    {-# LANGUAGE CPP #-}

    module Agda.TypeChecking.Monad.Open
    	( makeOpen
    	, makeClosed
    	, getOpen
    	, tryOpen
    	) where

    import Control.Applicative
    import Control.Monad
    import Control.Monad.Error
    import Data.List

    import Agda.Syntax.Common

    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Monad.Base

    import {-# SOURCE #-} Agda.TypeChecking.Monad.Context

    #include "../../undefined.h"
    import Agda.Utils.Impossible

    -- | Create an open term in the current context.
    makeOpen :: MonadTCM tcm => a -> tcm (Open a)
    makeOpen x = do
        ctx <- getContextId
        return $ OpenThing ctx x

    -- | Create an open term which is closed.
    makeClosed :: a -> Open a
    makeClosed = OpenThing []

    -- | Extract the value from an open term. Must be done in an extension of the
    --   context in which the term was created.
    getOpen :: (MonadTCM tcm, Raise a) => Open a -> tcm 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 :: (MonadTCM tcm, Raise a) => Open a -> tcm (Maybe a)
    tryOpen o = liftTCM $
      (Just <$> getOpen o)
      `catchError` \_ -> return Nothing