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 (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
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 (Map CheckpointId Substitution
 -> f (Map CheckpointId Substitution))
-> TCEnv -> f TCEnv
Lens' (Map CheckpointId Substitution) TCEnv
eCheckpoints
    ModuleNameHash
m   <- m ModuleNameHash
forall (m :: * -> *). ReadTCState m => m ModuleNameHash
currentModuleNameHash
    Open a -> m (Open a)
forall a. a -> m 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 a. 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 a. 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 (m :: * -> *) a. Monad m => m a -> MaybeT m a
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 (Map CheckpointId Substitution
 -> f (Map CheckpointId Substitution))
-> TCEnv -> f TCEnv
Lens' (Map CheckpointId Substitution) TCEnv
eCheckpoints
      CheckpointId
parent <- Map CheckpointId Substitution
-> Map CheckpointId Substitution -> MaybeT m CheckpointId
forall {a} {f :: * -> *} {a} {b}.
(Ord a, Alternative f, Monad f) =>
Map a a -> Map a b -> 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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Open a
o
                  else Open a -> m (Open a)
forall a. a -> m 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 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