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 x = do
    cp  <- viewTC 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 (OpenThing cp _ _ x) = do
  sub <- checkpointSubstitution 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 extract open = do
  OpenThing cp env _ x <- restrict 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 o@(OpenThing cp env m x) = do
      cur <- currentModuleNameHash
      if m == cur then return o
                  else return $ OpenThing (-1) (Map.filterWithKey (\ k _ -> k == 0) env) m x

    findParent m1 m2
      | Set.null keys = empty
      | otherwise     = return $ Set.findMax keys
      where
        keys = Set.intersection (Map.keysSet m1) (Map.keysSet m2)

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