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

import Agda.Syntax.Internal
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Monad.Base

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

import Agda.Utils.Lens

-- | Create an open term in the current context.
makeOpen :: MonadTCEnv m => a -> m (Open a)
makeOpen :: 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
    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 -> a -> Open a
forall a. CheckpointId -> a -> Open a
OpenThing CheckpointId
cp a
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 :: Open a -> m a
getOpen (OpenThing CheckpointId
cp 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 -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub a
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 :: Open a -> m (Maybe a)
tryGetOpen (OpenThing CheckpointId
cp a
x) = (Substitution -> a) -> Maybe Substitution -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
`applySubst` a
x) (Maybe Substitution -> Maybe a)
-> m (Maybe Substitution) -> m (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Maybe Substitution) TCEnv -> 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)

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