    module Agda.TypeChecking.Monad.Open
            ( makeOpen
            , getOpen
            , tryGetOpen
            , isClosed
            ) where

    import Control.Applicative
    import Control.Monad.Trans
    import Control.Monad.Trans.Maybe
    import qualified Data.Map as Map
    import qualified Data.Set as Set

    import Agda.Syntax.Internal
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.State (currentModuleNameHash)

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

    import Agda.Utils.Lens
    import Agda.Utils.Maybe

    -- | Create an open term in the current context.
    makeOpen :: (ReadTCState m, MonadTCEnv m) => a -> m (Open a)
    makeOpen :: forall (m :: * -> *) a.
    (ReadTCState m, MonadTCEnv m) =>
    a -> m (Open a)
    makeOpen a
    x = do
        cp  <- Lens' TCEnv CheckpointId -> m CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
    Lens' TCEnv CheckpointId
    eCurrentCheckpoint
        env <- viewTC eCheckpoints
        m   <- currentModuleNameHash
        return $ OpenThing cp env m x

    -- | Extract the value from an open term. The checkpoint at which it was
    --   created must be in scope.
    getOpen :: (TermSubst a, MonadTCEnv m) => Open a -> m a
    getOpen :: forall a (m :: * -> *).
    (TermSubst a, MonadTCEnv m) =>
    Open a -> m a
    getOpen (OpenThing CheckpointId
    cp Map CheckpointId Substitution
    _ ModuleNameHash
    _ a
    x) = do
      sub <- CheckpointId -> m Substitution
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    CheckpointId -> tcm Substitution
    checkpointSubstitution CheckpointId
    cp
      return $ applySubst sub x

    -- | Extract the value from an open term. If the checkpoint is no longer in scope use the provided
    --   function to pull the object to the most recent common checkpoint. The function is given the
    --   substitution from the common ancestor to the checkpoint of the thing.
    tryGetOpen :: (TermSubst a, ReadTCState m, MonadTCEnv m) => (Substitution -> a -> Maybe a) -> Open a -> m (Maybe a)
    tryGetOpen :: forall a (m :: * -> *).
    (TermSubst a, ReadTCState m, MonadTCEnv m) =>
    (Substitution -> a -> Maybe a) -> Open a -> m (Maybe a)
    tryGetOpen Substitution -> a -> Maybe a
    extract Open a
    open = do
      OpenThing cp env _ x <- Open a -> m (Open a)
    forall {m :: * -> *} {a}. ReadTCState m => Open a -> m (Open a)
    restrict Open a
    open -- Strip the env if from another module
      runMaybeT $ do
          (`applySubst` x) <$> (liftMaybe =<< viewTC (eCheckpoints . key cp))
        <|> do  -- Checkpoint no longer in scope
          curEnv <- lift $ viewTC eCheckpoints
          parent <- findParent env curEnv
          let Just subToOld = Map.lookup parent env
              Just subToCur = Map.lookup parent curEnv
          (applySubst subToCur) <$> liftMaybe (extract subToOld x)
      where
        -- If this comes from a different file, the checkpoints refer to checkpoints in that file and
        -- not in the current file. To avoid confusing them we set the checkpoint to -1 and only keep
        -- checkpoint 0 (which is shared between files) in the environment.
        restrict :: Open a -> m (Open a)
    restrict o :: Open a
    o@(OpenThing CheckpointId
    cp Map CheckpointId Substitution
    env ModuleNameHash
    m a
    x) = do
          cur <- m ModuleNameHash
    forall (m :: * -> *). ReadTCState m => m ModuleNameHash
    currentModuleNameHash
          if m == cur then return o
                      else return $ OpenThing (-1) (Map.filterWithKey (\ CheckpointId
    k Substitution
    _ -> CheckpointId
    k CheckpointId -> CheckpointId -> Bool
    forall a. Eq a => a -> a -> Bool
    == CheckpointId
    0) env) m x

        findParent :: Map a a -> Map a b -> f a
    findParent Map a a
    m1 Map a b
    m2 = case Map a a -> Maybe (a, a)
    forall k a. Map k a -> Maybe (k, a)
    Map.lookupMax (Map a a -> Map a b -> Map a a
    forall k a b. Ord k => Map k a -> Map k b -> Map k a
    Map.intersection Map a a
    m1 Map a b
    m2) of
          Maybe (a, a)
    Nothing       -> f a
    forall a. f a
    forall (f :: * -> *) a. Alternative f => f a
    empty
          Just (a
    max, a
    _) -> a -> f a
    forall a. a -> f a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    max

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