    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
        CheckpointId
    cp  <- Lens' CheckpointId TCEnv -> m CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' CheckpointId TCEnv
    eCurrentCheckpoint
        Map CheckpointId Substitution
    env <- Lens' (Map CheckpointId Substitution) TCEnv
    -> m (Map CheckpointId Substitution)
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' (Map CheckpointId Substitution) TCEnv
    eCheckpoints
        ModuleNameHash
    m   <- m ModuleNameHash
    forall (m :: * -> *). ReadTCState m => m ModuleNameHash
    currentModuleNameHash
        Open a -> m (Open a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Open a -> m (Open a)) -> Open a -> m (Open a)
    forall a b. (a -> b) -> a -> b
    $ CheckpointId
    -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
    forall a.
    CheckpointId
    -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
    OpenThing CheckpointId
    cp Map CheckpointId Substitution
    env ModuleNameHash
    m a
    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
      Substitution
    sub <- CheckpointId -> m Substitution
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    CheckpointId -> tcm Substitution
    checkpointSubstitution CheckpointId
    cp
      a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> m a) -> a -> m a
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg a)
    sub a
    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 CheckpointId
    cp Map CheckpointId Substitution
    env ModuleNameHash
    _ a
    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
      MaybeT m a -> m (Maybe a)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT m a -> m (Maybe a)) -> MaybeT m a -> m (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ do
          (Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` a
    x) (Substitution -> a) -> MaybeT m Substitution -> MaybeT m a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Maybe Substitution -> MaybeT m Substitution
    forall (f :: * -> *) a. Alternative f => Maybe a -> f a
    liftMaybe (Maybe Substitution -> MaybeT m Substitution)
    -> MaybeT m (Maybe Substitution) -> MaybeT m Substitution
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Lens' (Maybe Substitution) TCEnv -> MaybeT m (Maybe Substitution)
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC ((Map CheckpointId Substitution
     -> f (Map CheckpointId Substitution))
    -> TCEnv -> f TCEnv
    Lens' (Map CheckpointId Substitution) TCEnv
    eCheckpoints ((Map CheckpointId Substitution
      -> f (Map CheckpointId Substitution))
     -> TCEnv -> f TCEnv)
    -> ((Maybe Substitution -> f (Maybe Substitution))
        -> Map CheckpointId Substitution
        -> f (Map CheckpointId Substitution))
    -> (Maybe Substitution -> f (Maybe Substitution))
    -> TCEnv
    -> f TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CheckpointId
    -> Lens' (Maybe Substitution) (Map CheckpointId Substitution)
    forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
    key CheckpointId
    cp))
        MaybeT m a -> MaybeT m a -> MaybeT m a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> do  -- Checkpoint no longer in scope
          Map CheckpointId Substitution
    curEnv <- m (Map CheckpointId Substitution)
    -> MaybeT m (Map CheckpointId Substitution)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m (Map CheckpointId Substitution)
     -> MaybeT m (Map CheckpointId Substitution))
    -> m (Map CheckpointId Substitution)
    -> MaybeT m (Map CheckpointId Substitution)
    forall a b. (a -> b) -> a -> b
    $ Lens' (Map CheckpointId Substitution) TCEnv
    -> m (Map CheckpointId Substitution)
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' (Map CheckpointId Substitution) TCEnv
    eCheckpoints
          CheckpointId
    parent <- Map CheckpointId Substitution
    -> Map CheckpointId Substitution -> MaybeT m CheckpointId
    forall {a} {f :: * -> *} {a} {a}.
    (Ord a, Alternative f, Monad f) =>
    Map a a -> Map a a -> f a
    findParent Map CheckpointId Substitution
    env Map CheckpointId Substitution
    curEnv
          let Just Substitution
    subToOld = CheckpointId -> Map CheckpointId Substitution -> Maybe Substitution
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup CheckpointId
    parent Map CheckpointId Substitution
    env
              Just Substitution
    subToCur = CheckpointId -> Map CheckpointId Substitution -> Maybe Substitution
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup CheckpointId
    parent Map CheckpointId Substitution
    curEnv
          (Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg a)
    subToCur) (a -> a) -> MaybeT m a -> MaybeT m a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe a -> MaybeT m a
    forall (f :: * -> *) a. Alternative f => Maybe a -> f a
    liftMaybe (Substitution -> a -> Maybe a
    extract Substitution
    subToOld a
    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
          ModuleNameHash
    cur <- m ModuleNameHash
    forall (m :: * -> *). ReadTCState m => m ModuleNameHash
    currentModuleNameHash
          if ModuleNameHash
    m ModuleNameHash -> ModuleNameHash -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleNameHash
    cur then Open a -> m (Open a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Open a
    o
                      else Open a -> m (Open a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Open a -> m (Open a)) -> Open a -> m (Open a)
    forall a b. (a -> b) -> a -> b
    $ CheckpointId
    -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
    forall a.
    CheckpointId
    -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
    OpenThing (-CheckpointId
    1) ((CheckpointId -> Substitution -> Bool)
    -> Map CheckpointId Substitution -> Map CheckpointId Substitution
    forall k a. (k -> a -> Bool) -> Map k a -> Map k a
    Map.filterWithKey (\ CheckpointId
    k Substitution
    _ -> CheckpointId
    k CheckpointId -> CheckpointId -> Bool
    forall a. Eq a => a -> a -> Bool
    == CheckpointId
    0) Map CheckpointId Substitution
    env) ModuleNameHash
    m a
    x

        findParent :: Map a a -> Map a a -> f a
    findParent Map a a
    m1 Map a a
    m2
          | Set a -> Bool
    forall a. Set a -> Bool
    Set.null Set a
    keys = f a
    forall (f :: * -> *) a. Alternative f => f a
    empty
          | Bool
    otherwise     = a -> f a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> f a) -> a -> f a
    forall a b. (a -> b) -> a -> b
    $ Set a -> a
    forall a. Set a -> a
    Set.findMax Set a
    keys
          where
            keys :: Set a
    keys = Set a -> Set a -> Set a
    forall a. Ord a => Set a -> Set a -> Set a
    Set.intersection (Map a a -> Set a
    forall k a. Map k a -> Set k
    Map.keysSet Map a a
    m1) (Map a a -> Set a
    forall k a. Map k a -> Set k
    Map.keysSet Map a a
    m2)

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