module Agda.TypeChecking.Monad.Context where

import Control.Monad                ( (<=<), forM, when )
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Control  ( MonadTransControl(..), liftThrough )
import Control.Monad.Trans.Identity ( IdentityT )
import Control.Monad.Trans.Maybe
import Control.Monad.Writer
-- Control.Monad.Fail import is redundant since GHC 8.8.1
import Control.Monad.Fail (MonadFail)

import qualified Data.List as List
import qualified Data.Map as Map

import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name (NameInScope(..), LensInScope(..), nameRoot, nameToRawName)
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base

import Agda.TypeChecking.Free
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Monad.Open
import Agda.TypeChecking.Monad.State

import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List ((!!!), downFrom)
import Agda.Utils.ListT
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Pretty
import Agda.Utils.Size

import Agda.Utils.Impossible

-- * Modifying the context

-- | Modify a 'Context' in a computation.  Warning: does not update
--   the checkpoints. Use @updateContext@ instead.
{-# SPECIALIZE unsafeModifyContext :: (Context -> Context) -> TCM a -> TCM a #-}
unsafeModifyContext :: MonadTCEnv tcm => (Context -> Context) -> tcm a -> tcm a
unsafeModifyContext :: (Context -> Context) -> tcm a -> tcm a
unsafeModifyContext Context -> Context
f = (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envContext :: Context
envContext = Context -> Context
f (Context -> Context) -> Context -> Context
forall a b. (a -> b) -> a -> b
$ TCEnv -> Context
envContext TCEnv
e }

-- | Modify the 'Dom' part of context entries.
modifyContextInfo :: MonadTCEnv tcm => (forall e. Dom e -> Dom e) -> tcm a -> tcm a
modifyContextInfo :: (forall e. Dom e -> Dom e) -> tcm a -> tcm a
modifyContextInfo forall e. Dom e -> Dom e
f = (Context -> Context) -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext ((Context -> Context) -> tcm a -> tcm a)
-> (Context -> Context) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ (Dom (Name, Type) -> Dom (Name, Type)) -> Context -> Context
forall a b. (a -> b) -> [a] -> [b]
map Dom (Name, Type) -> Dom (Name, Type)
forall e. Dom e -> Dom e
f

-- | Change to top (=empty) context. Resets the checkpoints.
{-# SPECIALIZE inTopContext :: TCM a -> TCM a #-}
inTopContext :: (MonadTCEnv tcm, ReadTCState tcm) => tcm a -> tcm a
inTopContext :: tcm a -> tcm a
inTopContext tcm a
cont =
  (Context -> Context) -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext (Context -> Context -> Context
forall a b. a -> b -> a
const [])
        (tcm a -> tcm a) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Lens' CheckpointId TCEnv
-> (CheckpointId -> CheckpointId) -> tcm a -> tcm a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' CheckpointId TCEnv
eCurrentCheckpoint (CheckpointId -> CheckpointId -> CheckpointId
forall a b. a -> b -> a
const CheckpointId
0)
        (tcm a -> tcm a) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Lens' (Map CheckpointId (Substitution' Term)) TCEnv
-> (Map CheckpointId (Substitution' Term)
    -> Map CheckpointId (Substitution' Term))
-> tcm a
-> tcm a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' (Map CheckpointId (Substitution' Term)) TCEnv
eCheckpoints (Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall a b. a -> b -> a
const (Map CheckpointId (Substitution' Term)
 -> Map CheckpointId (Substitution' Term)
 -> Map CheckpointId (Substitution' Term))
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall a b. (a -> b) -> a -> b
$ CheckpointId
-> Substitution' Term -> Map CheckpointId (Substitution' Term)
forall k a. k -> a -> Map k a
Map.singleton CheckpointId
0 Substitution' Term
forall a. Substitution' a
IdS)
        (tcm a -> tcm a) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Lens' (Map ModuleName CheckpointId) TCState
-> (Map ModuleName CheckpointId -> Map ModuleName CheckpointId)
-> tcm a
-> tcm a
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> m b -> m b
locallyTCState Lens' (Map ModuleName CheckpointId) TCState
stModuleCheckpoints (Map ModuleName CheckpointId
-> Map ModuleName CheckpointId -> Map ModuleName CheckpointId
forall a b. a -> b -> a
const Map ModuleName CheckpointId
forall k a. Map k a
Map.empty)
        (tcm a -> tcm a) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Lens' [(Name, LocalVar)] ScopeInfo
-> ([(Name, LocalVar)] -> [(Name, LocalVar)]) -> tcm a -> tcm a
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a ScopeInfo -> (a -> a) -> m b -> m b
locallyScope Lens' [(Name, LocalVar)] ScopeInfo
scopeLocals ([(Name, LocalVar)] -> [(Name, LocalVar)] -> [(Name, LocalVar)]
forall a b. a -> b -> a
const [])
        (tcm a -> tcm a) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Lens' (Map Name (Open (Term, Dom Type))) TCEnv
-> (Map Name (Open (Term, Dom Type))
    -> Map Name (Open (Term, Dom Type)))
-> tcm a
-> tcm a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' (Map Name (Open (Term, Dom Type))) TCEnv
eLetBindings (Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall a b. a -> b -> a
const Map Name (Open (Term, Dom Type))
forall k a. Map k a
Map.empty)
        (tcm a -> tcm a) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ tcm a
cont

-- | Change to top (=empty) context, but don't update the checkpoints. Totally
--   not safe!
{-# SPECIALIZE unsafeInTopContext :: TCM a -> TCM a #-}
unsafeInTopContext :: (MonadTCEnv m, ReadTCState m) => m a -> m a
unsafeInTopContext :: m a -> m a
unsafeInTopContext m a
cont =
  Lens' [(Name, LocalVar)] ScopeInfo
-> ([(Name, LocalVar)] -> [(Name, LocalVar)]) -> m a -> m a
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a ScopeInfo -> (a -> a) -> m b -> m b
locallyScope Lens' [(Name, LocalVar)] ScopeInfo
scopeLocals ([(Name, LocalVar)] -> [(Name, LocalVar)] -> [(Name, LocalVar)]
forall a b. a -> b -> a
const []) (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$
    (Context -> Context) -> m a -> m a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext (Context -> Context -> Context
forall a b. a -> b -> a
const []) m a
cont

-- | Delete the last @n@ bindings from the context.
--
--   Doesn't update checkpoints! Use `escapeContext` or `updateContext
--   rho (drop n)` instead, for an appropriate substitution `rho`.
{-# SPECIALIZE unsafeEscapeContext :: Int -> TCM a -> TCM a #-}
unsafeEscapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a
unsafeEscapeContext :: Int -> tcm a -> tcm a
unsafeEscapeContext Int
n = (Context -> Context) -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext ((Context -> Context) -> tcm a -> tcm a)
-> (Context -> Context) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Int -> Context -> Context
forall a. Int -> [a] -> [a]
drop Int
n

-- | Delete the last @n@ bindings from the context. Any occurrences of
-- these variables are replaced with the given @err@.
escapeContext :: MonadAddContext m => Impossible -> Int -> m a -> m a
escapeContext :: Impossible -> Int -> m a -> m a
escapeContext Impossible
err Int
n = Substitution' Term -> (Context -> Context) -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution' Term -> (Context -> Context) -> m a -> m a
updateContext (Impossible -> Int -> Substitution' Term
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
err Int
n) ((Context -> Context) -> m a -> m a)
-> (Context -> Context) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Int -> Context -> Context
forall a. Int -> [a] -> [a]
drop Int
n

-- * Manipulating checkpoints --

-- | Add a new checkpoint. Do not use directly!
checkpoint
  :: (MonadDebug tcm, MonadTCM tcm, MonadFresh CheckpointId tcm, ReadTCState tcm)
  => Substitution -> tcm a -> tcm a
checkpoint :: Substitution' Term -> tcm a -> tcm a
checkpoint Substitution' Term
sub tcm a
k = do
  tcm () -> tcm ()
forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Int -> VerboseKey -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.cxt.checkpoint" Int
105 (VerboseKey -> tcm ()) -> VerboseKey -> tcm ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"New checkpoint {"
  CheckpointId
old     <- Lens' CheckpointId TCEnv -> tcm CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
  Map ModuleName CheckpointId
oldMods <- Lens' (Map ModuleName CheckpointId) TCState
-> tcm (Map ModuleName CheckpointId)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC  Lens' (Map ModuleName CheckpointId) TCState
stModuleCheckpoints
  CheckpointId
chkpt <- tcm CheckpointId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
  tcm () -> tcm ()
forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Int -> tcm () -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> m () -> m ()
verboseS VerboseKey
"tc.cxt.checkpoint" Int
105 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ do
    Telescope
cxt <- tcm Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
    Map CheckpointId (Substitution' Term)
cps <- Lens' (Map CheckpointId (Substitution' Term)) TCEnv
-> tcm (Map CheckpointId (Substitution' Term))
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' (Map CheckpointId (Substitution' Term)) TCEnv
eCheckpoints
    let cps' :: Map CheckpointId (Substitution' Term)
cps' = CheckpointId
-> Substitution' Term
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert CheckpointId
chkpt Substitution' Term
forall a. Substitution' a
IdS (Map CheckpointId (Substitution' Term)
 -> Map CheckpointId (Substitution' Term))
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall a b. (a -> b) -> a -> b
$ (Substitution' Term -> Substitution' Term)
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' (SubstArg (Substitution' Term))
-> Substitution' Term -> Substitution' Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Substitution' Term))
sub) Map CheckpointId (Substitution' Term)
cps
        prCps :: Map a a -> Doc
prCps Map a a
cps = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [ a -> Doc
forall a. Show a => a -> Doc
pshow a
c Doc -> Doc -> Doc
<+> Doc
": " Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
s | (a
c, a
s) <- Map a a -> [(a, a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map a a
cps ]
    VerboseKey -> Int -> TCM Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cxt.checkpoint" Int
105 (TCM Doc -> tcm ()) -> TCM Doc -> tcm ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ Doc
"old =" Doc -> Doc -> Doc
<+> CheckpointId -> Doc
forall a. Show a => a -> Doc
pshow CheckpointId
old
      , Doc
"new =" Doc -> Doc -> Doc
<+> CheckpointId -> Doc
forall a. Show a => a -> Doc
pshow CheckpointId
chkpt
      , Doc
"sub =" Doc -> Doc -> Doc
<+> Substitution' Term -> Doc
forall a. Pretty a => a -> Doc
pretty Substitution' Term
sub
      , Doc
"cxt =" Doc -> Doc -> Doc
<+> Telescope -> Doc
forall a. Pretty a => a -> Doc
pretty Telescope
cxt
      , Doc
"old substs =" Doc -> Doc -> Doc
<+> Map CheckpointId (Substitution' Term) -> Doc
forall a a. (Show a, Pretty a) => Map a a -> Doc
prCps Map CheckpointId (Substitution' Term)
cps
      , Doc
"new substs =" Doc -> Doc -> Doc
<?> Map CheckpointId (Substitution' Term) -> Doc
forall a a. (Show a, Pretty a) => Map a a -> Doc
prCps Map CheckpointId (Substitution' Term)
cps'
      ]
  a
x <- ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> tcm a -> (TCEnv -> TCEnv) -> tcm a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC tcm a
k ((TCEnv -> TCEnv) -> tcm a) -> (TCEnv -> TCEnv) -> tcm a
forall a b. (a -> b) -> a -> b
$ \ TCEnv
env -> TCEnv
env
    { envCurrentCheckpoint :: CheckpointId
envCurrentCheckpoint = CheckpointId
chkpt
    , envCheckpoints :: Map CheckpointId (Substitution' Term)
envCheckpoints       = CheckpointId
-> Substitution' Term
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert CheckpointId
chkpt Substitution' Term
forall a. Substitution' a
IdS (Map CheckpointId (Substitution' Term)
 -> Map CheckpointId (Substitution' Term))
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall a b. (a -> b) -> a -> b
$
                              (Substitution' Term -> Substitution' Term)
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' (SubstArg (Substitution' Term))
-> Substitution' Term -> Substitution' Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Substitution' Term))
sub) (TCEnv -> Map CheckpointId (Substitution' Term)
envCheckpoints TCEnv
env)
    }
  Map ModuleName CheckpointId
newMods <- Lens' (Map ModuleName CheckpointId) TCState
-> tcm (Map ModuleName CheckpointId)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map ModuleName CheckpointId) TCState
stModuleCheckpoints
  -- Set the checkpoint for introduced modules to the old checkpoint when the
  -- new one goes out of scope. #2897: This isn't actually sound for modules
  -- created under refined parent parameters, but as long as those modules
  -- aren't named we shouldn't look at the checkpoint. The right thing to do
  -- would be to not store these modules in the checkpoint map, but todo..
  Lens' (Map ModuleName CheckpointId) TCState
stModuleCheckpoints Lens' (Map ModuleName CheckpointId) TCState
-> Map ModuleName CheckpointId -> tcm ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` Map ModuleName CheckpointId
-> Map ModuleName CheckpointId -> Map ModuleName CheckpointId
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map ModuleName CheckpointId
oldMods (CheckpointId
old CheckpointId
-> Map ModuleName CheckpointId -> Map ModuleName CheckpointId
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Map ModuleName CheckpointId
-> Map ModuleName CheckpointId -> Map ModuleName CheckpointId
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference Map ModuleName CheckpointId
newMods Map ModuleName CheckpointId
oldMods)
  tcm () -> tcm ()
forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Int -> VerboseKey -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.cxt.checkpoint" Int
105 VerboseKey
"}"
  a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x

-- | Get the substitution from the context at a given checkpoint to the current context.
checkpointSubstitution :: MonadTCEnv tcm => CheckpointId -> tcm Substitution
checkpointSubstitution :: CheckpointId -> tcm (Substitution' Term)
checkpointSubstitution = tcm (Substitution' Term)
-> (Substitution' Term -> tcm (Substitution' Term))
-> Maybe (Substitution' Term)
-> tcm (Substitution' Term)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe tcm (Substitution' Term)
forall a. HasCallStack => a
__IMPOSSIBLE__ Substitution' Term -> tcm (Substitution' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Substitution' Term) -> tcm (Substitution' Term))
-> (CheckpointId -> tcm (Maybe (Substitution' Term)))
-> CheckpointId
-> tcm (Substitution' Term)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< CheckpointId -> tcm (Maybe (Substitution' Term))
forall (tcm :: * -> *).
MonadTCEnv tcm =>
CheckpointId -> tcm (Maybe (Substitution' Term))
checkpointSubstitution'

-- | Get the substitution from the context at a given checkpoint to the current context.
checkpointSubstitution' :: MonadTCEnv tcm => CheckpointId -> tcm (Maybe Substitution)
checkpointSubstitution' :: CheckpointId -> tcm (Maybe (Substitution' Term))
checkpointSubstitution' CheckpointId
chkpt = Lens' (Maybe (Substitution' Term)) TCEnv
-> tcm (Maybe (Substitution' Term))
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC ((Map CheckpointId (Substitution' Term)
 -> f (Map CheckpointId (Substitution' Term)))
-> TCEnv -> f TCEnv
Lens' (Map CheckpointId (Substitution' Term)) TCEnv
eCheckpoints ((Map CheckpointId (Substitution' Term)
  -> f (Map CheckpointId (Substitution' Term)))
 -> TCEnv -> f TCEnv)
-> ((Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
    -> Map CheckpointId (Substitution' Term)
    -> f (Map CheckpointId (Substitution' Term)))
-> (Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
-> TCEnv
-> f TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckpointId
-> Lens'
     (Maybe (Substitution' Term))
     (Map CheckpointId (Substitution' Term))
forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
key CheckpointId
chkpt)

-- | Get substitution @Γ ⊢ ρ : Γm@ where @Γ@ is the current context
--   and @Γm@ is the module parameter telescope of module @m@.
--
--   Returns @Nothing@ in case the we don't have a checkpoint for @m@.
getModuleParameterSub :: (MonadTCEnv m, ReadTCState m) => ModuleName -> m (Maybe Substitution)
getModuleParameterSub :: ModuleName -> m (Maybe (Substitution' Term))
getModuleParameterSub ModuleName
m = do
  Maybe CheckpointId
mcp <- (TCState -> Lens' (Maybe CheckpointId) TCState -> Maybe CheckpointId
forall o i. o -> Lens' i o -> i
^. (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
-> TCState -> f TCState
Lens' (Map ModuleName CheckpointId) TCState
stModuleCheckpoints ((Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
 -> TCState -> f TCState)
-> ((Maybe CheckpointId -> f (Maybe CheckpointId))
    -> Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
-> (Maybe CheckpointId -> f (Maybe CheckpointId))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName
-> Lens' (Maybe CheckpointId) (Map ModuleName CheckpointId)
forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
key ModuleName
m) (TCState -> Maybe CheckpointId)
-> m TCState -> m (Maybe CheckpointId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  (CheckpointId -> m (Substitution' Term))
-> Maybe CheckpointId -> m (Maybe (Substitution' Term))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CheckpointId -> m (Substitution' Term)
forall (tcm :: * -> *).
MonadTCEnv tcm =>
CheckpointId -> tcm (Substitution' Term)
checkpointSubstitution Maybe CheckpointId
mcp


-- * Adding to the context

{-# SPECIALIZE addCtx :: Name -> Dom Type -> TCM a -> TCM a #-}
class MonadTCEnv m => MonadAddContext m where
  -- | @addCtx x arg cont@ add a variable to the context.
  --
  --   Chooses an unused 'Name'.
  --
  --   Warning: Does not update module parameter substitution!
  addCtx :: Name -> Dom Type -> m a -> m a

  -- | Add a let bound variable to the context
  addLetBinding' :: Name -> Term -> Dom Type -> m a -> m a

  -- | Update the context.
  --   Requires a substitution that transports things living in the old context
  --   to the new.
  updateContext :: Substitution -> (Context -> Context) -> m a -> m a

  withFreshName :: Range -> ArgName -> (Name -> m a) -> m a

  default addCtx
    :: (MonadAddContext n, MonadTransControl t, t n ~ m)
    => Name -> Dom Type -> m a -> m a
  addCtx Name
x Dom Type
a = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
(MonadTransControl t, Monad (t m), Monad m) =>
(m (StT t a) -> m (StT t b)) -> t m a -> t m b
liftThrough ((n (StT t a) -> n (StT t a)) -> t n a -> t n a)
-> (n (StT t a) -> n (StT t a)) -> t n a -> t n a
forall a b. (a -> b) -> a -> b
$ Name -> Dom Type -> n (StT t a) -> n (StT t a)
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> m a -> m a
addCtx Name
x Dom Type
a

  default addLetBinding'
    :: (MonadAddContext n, MonadTransControl t, t n ~ m)
    => Name -> Term -> Dom Type -> m a -> m a
  addLetBinding' Name
x Term
u Dom Type
a = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
(MonadTransControl t, Monad (t m), Monad m) =>
(m (StT t a) -> m (StT t b)) -> t m a -> t m b
liftThrough ((n (StT t a) -> n (StT t a)) -> t n a -> t n a)
-> (n (StT t a) -> n (StT t a)) -> t n a -> t n a
forall a b. (a -> b) -> a -> b
$ Name -> Term -> Dom Type -> n (StT t a) -> n (StT t a)
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Term -> Dom Type -> m a -> m a
addLetBinding' Name
x Term
u Dom Type
a

  default updateContext
    :: (MonadAddContext n, MonadTransControl t, t n ~ m)
    => Substitution -> (Context -> Context) -> m a -> m a
  updateContext Substitution' Term
sub Context -> Context
f = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
(MonadTransControl t, Monad (t m), Monad m) =>
(m (StT t a) -> m (StT t b)) -> t m a -> t m b
liftThrough ((n (StT t a) -> n (StT t a)) -> t n a -> t n a)
-> (n (StT t a) -> n (StT t a)) -> t n a -> t n a
forall a b. (a -> b) -> a -> b
$ Substitution' Term
-> (Context -> Context) -> n (StT t a) -> n (StT t a)
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution' Term -> (Context -> Context) -> m a -> m a
updateContext Substitution' Term
sub Context -> Context
f

  default withFreshName
    :: (MonadAddContext n, MonadTransControl t, t n ~ m)
    => Range -> ArgName -> (Name -> m a) -> m a
  withFreshName Range
r VerboseKey
x Name -> m a
cont = do
    StT t a
st <- (Run t -> n (StT t a)) -> t n (StT t a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTransControl t, Monad m) =>
(Run t -> m a) -> t m a
liftWith ((Run t -> n (StT t a)) -> t n (StT t a))
-> (Run t -> n (StT t a)) -> t n (StT t a)
forall a b. (a -> b) -> a -> b
$ \ Run t
run -> do
      Range -> VerboseKey -> (Name -> n (StT t a)) -> n (StT t a)
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> VerboseKey -> (Name -> m a) -> m a
withFreshName Range
r VerboseKey
x ((Name -> n (StT t a)) -> n (StT t a))
-> (Name -> n (StT t a)) -> n (StT t a)
forall a b. (a -> b) -> a -> b
$ t n a -> n (StT t a)
Run t
run (t n a -> n (StT t a)) -> (Name -> t n a) -> Name -> n (StT t a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> m a
Name -> t n a
cont
    n (StT t a) -> t n a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTransControl t, Monad m) =>
m (StT t a) -> t m a
restoreT (n (StT t a) -> t n a) -> n (StT t a) -> t n a
forall a b. (a -> b) -> a -> b
$ StT t a -> n (StT t a)
forall (m :: * -> *) a. Monad m => a -> m a
return StT t a
st

-- | Default implementation of addCtx in terms of updateContext
defaultAddCtx :: MonadAddContext m => Name -> Dom Type -> m a -> m a
defaultAddCtx :: Name -> Dom Type -> m a -> m a
defaultAddCtx Name
x Dom Type
a m a
ret =
  Substitution' Term -> (Context -> Context) -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution' Term -> (Context -> Context) -> m a -> m a
updateContext (Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS Int
1) (((Name
x,) (Type -> (Name, Type)) -> Dom Type -> Dom (Name, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
a) Dom (Name, Type) -> Context -> Context
forall a. a -> [a] -> [a]
:) m a
ret

withFreshName_ :: (MonadAddContext m) => ArgName -> (Name -> m a) -> m a
withFreshName_ :: VerboseKey -> (Name -> m a) -> m a
withFreshName_ = Range -> VerboseKey -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> VerboseKey -> (Name -> m a) -> m a
withFreshName Range
forall a. Range' a
noRange

instance MonadAddContext m => MonadAddContext (ExceptT e m)
instance MonadAddContext m => MonadAddContext (IdentityT m)
instance MonadAddContext m => MonadAddContext (MaybeT m)
instance MonadAddContext m => MonadAddContext (ReaderT r m)
instance MonadAddContext m => MonadAddContext (StateT r m)
instance (Monoid w, MonadAddContext m) => MonadAddContext (WriterT w m)
deriving instance MonadAddContext m => MonadAddContext (BlockT m)

instance MonadAddContext m => MonadAddContext (ListT m) where
  addCtx :: Name -> Dom Type -> ListT m a -> ListT m a
addCtx Name
x Dom Type
a             = (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT ((forall a1. m a1 -> m a1) -> ListT m a -> ListT m a)
-> (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall a b. (a -> b) -> a -> b
$ Name -> Dom Type -> m a1 -> m a1
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> m a -> m a
addCtx Name
x Dom Type
a
  addLetBinding' :: Name -> Term -> Dom Type -> ListT m a -> ListT m a
addLetBinding' Name
x Term
u Dom Type
a   = (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT ((forall a1. m a1 -> m a1) -> ListT m a -> ListT m a)
-> (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall a b. (a -> b) -> a -> b
$ Name -> Term -> Dom Type -> m a1 -> m a1
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Term -> Dom Type -> m a -> m a
addLetBinding' Name
x Term
u Dom Type
a
  updateContext :: Substitution' Term
-> (Context -> Context) -> ListT m a -> ListT m a
updateContext Substitution' Term
sub Context -> Context
f    = (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT ((forall a1. m a1 -> m a1) -> ListT m a -> ListT m a)
-> (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> (Context -> Context) -> m a1 -> m a1
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution' Term -> (Context -> Context) -> m a -> m a
updateContext Substitution' Term
sub Context -> Context
f
  withFreshName :: Range -> VerboseKey -> (Name -> ListT m a) -> ListT m a
withFreshName Range
r VerboseKey
x Name -> ListT m a
cont = m (Maybe (a, ListT m a)) -> ListT m a
forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
ListT (m (Maybe (a, ListT m a)) -> ListT m a)
-> m (Maybe (a, ListT m a)) -> ListT m a
forall a b. (a -> b) -> a -> b
$ Range
-> VerboseKey
-> (Name -> m (Maybe (a, ListT m a)))
-> m (Maybe (a, ListT m a))
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> VerboseKey -> (Name -> m a) -> m a
withFreshName Range
r VerboseKey
x ((Name -> m (Maybe (a, ListT m a))) -> m (Maybe (a, ListT m a)))
-> (Name -> m (Maybe (a, ListT m a))) -> m (Maybe (a, ListT m a))
forall a b. (a -> b) -> a -> b
$ ListT m a -> m (Maybe (a, ListT m a))
forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
runListT (ListT m a -> m (Maybe (a, ListT m a)))
-> (Name -> ListT m a) -> Name -> m (Maybe (a, ListT m a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> ListT m a
cont

-- | Run the given TCM action, and register the given variable as
--   being shadowed by all the names with the same root that are added
--   to the context during this TCM action.
withShadowingNameTCM :: Name -> TCM b -> TCM b
withShadowingNameTCM :: Name -> TCM b -> TCM b
withShadowingNameTCM Name
x TCM b
f = do
  VerboseKey -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cxt.shadowing" Int
80 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Doc
"registered" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> Doc
"for shadowing"
  Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name -> NameInScope
forall a. LensInScope a => a -> NameInScope
isInScope Name
x NameInScope -> NameInScope -> Bool
forall a. Eq a => a -> a -> Bool
== NameInScope
InScope) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Name -> TCMT IO ()
forall (m :: * -> *). MonadTCState m => Name -> m ()
tellUsedName Name
x
  (b
result , Map VerboseKey [VerboseKey]
useds) <- TCM b -> TCMT IO (b, Map VerboseKey [VerboseKey])
forall (m :: * -> *) a.
(ReadTCState m, MonadTCState m) =>
m a -> m (a, Map VerboseKey [VerboseKey])
listenUsedNames TCM b
f
  VerboseKey -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cxt.shadowing" Int
90 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Doc
"all used names: " Doc -> Doc -> Doc
<+> VerboseKey -> Doc
text (Map VerboseKey [VerboseKey] -> VerboseKey
forall a. Show a => a -> VerboseKey
show Map VerboseKey [VerboseKey]
useds)
  Name -> Map VerboseKey [VerboseKey] -> TCMT IO ()
forall (m :: * -> *).
(MonadDebug m, MonadTCState m) =>
Name -> Map VerboseKey [VerboseKey] -> m ()
tellShadowing Name
x Map VerboseKey [VerboseKey]
useds
  b -> TCM b
forall (m :: * -> *) a. Monad m => a -> m a
return b
result

    where
      listenUsedNames :: m a -> m (a, Map VerboseKey [VerboseKey])
listenUsedNames m a
f = do
        Map VerboseKey [VerboseKey]
origUsedNames <- Lens' (Map VerboseKey [VerboseKey]) TCState
-> m (Map VerboseKey [VerboseKey])
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map VerboseKey [VerboseKey]) TCState
stUsedNames
        Lens' (Map VerboseKey [VerboseKey]) TCState
-> Map VerboseKey [VerboseKey] -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens Lens' (Map VerboseKey [VerboseKey]) TCState
stUsedNames Map VerboseKey [VerboseKey]
forall k a. Map k a
Map.empty
        a
result <- m a
f
        Map VerboseKey [VerboseKey]
newUsedNames <- Lens' (Map VerboseKey [VerboseKey]) TCState
-> m (Map VerboseKey [VerboseKey])
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map VerboseKey [VerboseKey]) TCState
stUsedNames
        Lens' (Map VerboseKey [VerboseKey]) TCState
-> Map VerboseKey [VerboseKey] -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens Lens' (Map VerboseKey [VerboseKey]) TCState
stUsedNames (Map VerboseKey [VerboseKey] -> m ())
-> Map VerboseKey [VerboseKey] -> m ()
forall a b. (a -> b) -> a -> b
$ ([VerboseKey] -> [VerboseKey] -> [VerboseKey])
-> Map VerboseKey [VerboseKey]
-> Map VerboseKey [VerboseKey]
-> Map VerboseKey [VerboseKey]
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith [VerboseKey] -> [VerboseKey] -> [VerboseKey]
forall a. [a] -> [a] -> [a]
(++) Map VerboseKey [VerboseKey]
origUsedNames Map VerboseKey [VerboseKey]
newUsedNames
        (a, Map VerboseKey [VerboseKey])
-> m (a, Map VerboseKey [VerboseKey])
forall (m :: * -> *) a. Monad m => a -> m a
return (a
result , Map VerboseKey [VerboseKey]
newUsedNames)

      tellUsedName :: Name -> m ()
tellUsedName Name
x = do
        let concreteX :: Name
concreteX = Name -> Name
nameConcrete Name
x
            rawX :: VerboseKey
rawX      = Name -> VerboseKey
nameToRawName Name
concreteX
            rootX :: VerboseKey
rootX     = Name -> VerboseKey
nameRoot Name
concreteX
        Lens' (Maybe [VerboseKey]) TCState
-> (Maybe [VerboseKey] -> Maybe [VerboseKey]) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
modifyTCLens ((Map VerboseKey [VerboseKey] -> f (Map VerboseKey [VerboseKey]))
-> TCState -> f TCState
Lens' (Map VerboseKey [VerboseKey]) TCState
stUsedNames ((Map VerboseKey [VerboseKey] -> f (Map VerboseKey [VerboseKey]))
 -> TCState -> f TCState)
-> ((Maybe [VerboseKey] -> f (Maybe [VerboseKey]))
    -> Map VerboseKey [VerboseKey] -> f (Map VerboseKey [VerboseKey]))
-> (Maybe [VerboseKey] -> f (Maybe [VerboseKey]))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey
-> Lens' (Maybe [VerboseKey]) (Map VerboseKey [VerboseKey])
forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
key VerboseKey
rootX) ((Maybe [VerboseKey] -> Maybe [VerboseKey]) -> m ())
-> (Maybe [VerboseKey] -> Maybe [VerboseKey]) -> m ()
forall a b. (a -> b) -> a -> b
$ [VerboseKey] -> Maybe [VerboseKey]
forall a. a -> Maybe a
Just ([VerboseKey] -> Maybe [VerboseKey])
-> (Maybe [VerboseKey] -> [VerboseKey])
-> Maybe [VerboseKey]
-> Maybe [VerboseKey]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VerboseKey
rawXVerboseKey -> [VerboseKey] -> [VerboseKey]
forall a. a -> [a] -> [a]
:) ([VerboseKey] -> [VerboseKey])
-> (Maybe [VerboseKey] -> [VerboseKey])
-> Maybe [VerboseKey]
-> [VerboseKey]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe [VerboseKey] -> [VerboseKey]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat

      tellShadowing :: Name -> Map VerboseKey [VerboseKey] -> m ()
tellShadowing Name
x Map VerboseKey [VerboseKey]
useds = case VerboseKey -> Map VerboseKey [VerboseKey] -> Maybe [VerboseKey]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Name -> VerboseKey
nameRoot (Name -> VerboseKey) -> Name -> VerboseKey
forall a b. (a -> b) -> a -> b
$ Name -> Name
nameConcrete Name
x) Map VerboseKey [VerboseKey]
useds of
        Just [VerboseKey]
shadows -> do
          VerboseKey -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cxt.shadowing" Int
80 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Doc
"names shadowing" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> Doc
": " Doc -> Doc -> Doc
<+> [Doc] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList_ ((VerboseKey -> Doc) -> [VerboseKey] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map VerboseKey -> Doc
forall a. Pretty a => a -> Doc
pretty [VerboseKey]
shadows)
          Lens' (Map Name [VerboseKey]) TCState
-> (Map Name [VerboseKey] -> Map Name [VerboseKey]) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
modifyTCLens Lens' (Map Name [VerboseKey]) TCState
stShadowingNames ((Map Name [VerboseKey] -> Map Name [VerboseKey]) -> m ())
-> (Map Name [VerboseKey] -> Map Name [VerboseKey]) -> m ()
forall a b. (a -> b) -> a -> b
$ ([VerboseKey] -> [VerboseKey] -> [VerboseKey])
-> Name
-> [VerboseKey]
-> Map Name [VerboseKey]
-> Map Name [VerboseKey]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [VerboseKey] -> [VerboseKey] -> [VerboseKey]
forall a. [a] -> [a] -> [a]
(++) Name
x [VerboseKey]
shadows
        Maybe [VerboseKey]
Nothing      -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

instance MonadAddContext TCM where
  addCtx :: Name -> Dom Type -> TCM a -> TCM a
addCtx Name
x Dom Type
a TCM a
ret = Bool -> (TCM a -> TCM a) -> TCM a -> TCM a
forall a. Bool -> (a -> a) -> a -> a
applyUnless (Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x) (Name -> TCM a -> TCM a
forall b. Name -> TCM b -> TCM b
withShadowingNameTCM Name
x) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$
    Name -> Dom Type -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> m a -> m a
defaultAddCtx Name
x Dom Type
a TCM a
ret

  addLetBinding' :: Name -> Term -> Dom Type -> TCM a -> TCM a
addLetBinding' Name
x Term
u Dom Type
a TCM a
ret = Bool -> (TCM a -> TCM a) -> TCM a -> TCM a
forall a. Bool -> (a -> a) -> a -> a
applyUnless (Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x) (Name -> TCM a -> TCM a
forall b. Name -> TCM b -> TCM b
withShadowingNameTCM Name
x) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$
    Name -> Term -> Dom Type -> TCM a -> TCM a
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
Name -> Term -> Dom Type -> m a -> m a
defaultAddLetBinding' Name
x Term
u Dom Type
a TCM a
ret

  updateContext :: Substitution' Term -> (Context -> Context) -> TCM a -> TCM a
updateContext Substitution' Term
sub Context -> Context
f = (Context -> Context) -> TCM a -> TCM a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext Context -> Context
f (TCM a -> TCM a) -> (TCM a -> TCM a) -> TCM a -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution' Term -> TCM a -> TCM a
forall (tcm :: * -> *) a.
(MonadDebug tcm, MonadTCM tcm, MonadFresh CheckpointId tcm,
 ReadTCState tcm) =>
Substitution' Term -> tcm a -> tcm a
checkpoint Substitution' Term
sub

  withFreshName :: Range -> VerboseKey -> (Name -> TCM a) -> TCM a
withFreshName Range
r VerboseKey
x Name -> TCM a
m = Range -> VerboseKey -> TCMT IO Name
forall (m :: * -> *).
MonadFresh NameId m =>
Range -> VerboseKey -> m Name
freshName Range
r VerboseKey
x TCMT IO Name -> (Name -> TCM a) -> TCM a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> TCM a
m

addRecordNameContext
  :: (MonadAddContext m, MonadFresh NameId m)
  => Dom Type -> m b -> m b
addRecordNameContext :: Dom Type -> m b -> m b
addRecordNameContext Dom Type
dom m b
ret = do
  Name
x <- Name -> Name
forall a. LensInScope a => a -> a
setNotInScope (Name -> Name) -> m Name -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Name
forall (m :: * -> *). MonadFresh NameId m => m Name
freshRecordName
  Name -> Dom Type -> m b -> m b
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> m a -> m a
addCtx Name
x Dom Type
dom m b
ret

-- | Various specializations of @addCtx@.
{-# SPECIALIZE addContext :: b -> TCM a -> TCM a #-}
class AddContext b where
  addContext :: (MonadAddContext m) => b -> m a -> m a
  contextSize :: b -> Nat

-- | Wrapper to tell 'addContext' not to mark names as
--   'NotInScope'. Used when adding a user-provided, but already type
--   checked, telescope to the context.
newtype KeepNames a = KeepNames a

instance {-# OVERLAPPABLE #-} AddContext a => AddContext [a] where
  addContext :: [a] -> m a -> m a
addContext = (m a -> [a] -> m a) -> [a] -> m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> m a -> m a) -> m a -> [a] -> m a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext)
  contextSize :: [a] -> Int
contextSize = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> ([a] -> [Int]) -> [a] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Int) -> [a] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map a -> Int
forall b. AddContext b => b -> Int
contextSize

instance AddContext (Name, Dom Type) where
  addContext :: (Name, Dom Type) -> m a -> m a
addContext = (Name -> Dom Type -> m a -> m a) -> (Name, Dom Type) -> m a -> m a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Dom Type -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> m a -> m a
addCtx
  contextSize :: (Name, Dom Type) -> Int
contextSize (Name, Dom Type)
_ = Int
1

instance AddContext (Dom (Name, Type)) where
  addContext :: Dom (Name, Type) -> m a -> m a
addContext = (Name, Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ((Name, Dom Type) -> m a -> m a)
-> (Dom (Name, Type) -> (Name, Dom Type))
-> Dom (Name, Type)
-> m a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Name, Type) -> (Name, Dom Type)
forall (t :: * -> *) (m :: * -> *) a.
(Decoration t, Functor m) =>
t (m a) -> m (t a)
distributeF
  contextSize :: Dom (Name, Type) -> Int
contextSize Dom (Name, Type)
_ = Int
1

instance AddContext (Dom (String, Type)) where
  addContext :: Dom (VerboseKey, Type) -> m a -> m a
addContext = (VerboseKey, Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ((VerboseKey, Dom Type) -> m a -> m a)
-> (Dom (VerboseKey, Type) -> (VerboseKey, Dom Type))
-> Dom (VerboseKey, Type)
-> m a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (VerboseKey, Type) -> (VerboseKey, Dom Type)
forall (t :: * -> *) (m :: * -> *) a.
(Decoration t, Functor m) =>
t (m a) -> m (t a)
distributeF
  contextSize :: Dom (VerboseKey, Type) -> Int
contextSize Dom (VerboseKey, Type)
_ = Int
1

instance AddContext ([Name], Dom Type) where
  addContext :: ([Name], Dom Type) -> m a -> m a
addContext ([Name]
xs, Dom Type
dom) = Context -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ((Name -> Name) -> [Name] -> Dom Type -> Context
forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' Name -> Name
forall a. a -> a
id [Name]
xs Dom Type
dom)
  contextSize :: ([Name], Dom Type) -> Int
contextSize ([Name]
xs, Dom Type
_) = [Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
xs

instance AddContext (List1 Name, Dom Type) where
  addContext :: (List1 Name, Dom Type) -> m a -> m a
addContext (List1 Name
xs, Dom Type
dom) = Context -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ((Name -> Name) -> List1 Name -> Dom Type -> Context
forall a. (Name -> a) -> List1 Name -> Dom Type -> ListTel' a
bindsToTel'1 Name -> Name
forall a. a -> a
id List1 Name
xs Dom Type
dom)
  contextSize :: (List1 Name, Dom Type) -> Int
contextSize (List1 Name
xs, Dom Type
_) = List1 Name -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length List1 Name
xs

instance AddContext ([WithHiding Name], Dom Type) where
  addContext :: ([WithHiding Name], Dom Type) -> m a -> m a
addContext ([]    , Dom Type
dom) = m a -> m a
forall a. a -> a
id
  addContext (WithHiding Name
x : [WithHiding Name]
xs, Dom Type
dom) = (NonEmpty (WithHiding Name), Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (WithHiding Name
x WithHiding Name -> [WithHiding Name] -> NonEmpty (WithHiding Name)
forall a. a -> [a] -> NonEmpty a
:| [WithHiding Name]
xs, Dom Type
dom)
  contextSize :: ([WithHiding Name], Dom Type) -> Int
contextSize ([WithHiding Name]
xs, Dom Type
_) = [WithHiding Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [WithHiding Name]
xs

instance AddContext (List1 (WithHiding Name), Dom Type) where
  addContext :: (NonEmpty (WithHiding Name), Dom Type) -> m a -> m a
addContext (WithHiding Hiding
h Name
x :| [WithHiding Name]
xs, Dom Type
dom) =
    (Name, Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Name
x , (Hiding -> Hiding) -> Dom Type -> Dom Type
forall a. LensHiding a => (Hiding -> Hiding) -> a -> a
mapHiding (Hiding -> Hiding -> Hiding
forall a. Monoid a => a -> a -> a
mappend Hiding
h) Dom Type
dom) (m a -> m a) -> (m a -> m a) -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ([WithHiding Name], Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([WithHiding Name]
xs, Int -> Dom Type -> Dom Type
forall a. Subst a => Int -> a -> a
raise Int
1 Dom Type
dom)
  contextSize :: (NonEmpty (WithHiding Name), Dom Type) -> Int
contextSize (NonEmpty (WithHiding Name)
xs, Dom Type
_) = NonEmpty (WithHiding Name) -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty (WithHiding Name)
xs

instance AddContext ([Arg Name], Type) where
  addContext :: ([Arg Name], Type) -> m a -> m a
addContext ([Arg Name]
xs, Type
t) = ([NamedArg Name], Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (((Arg Name -> NamedArg Name) -> [Arg Name] -> [NamedArg Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Arg Name -> NamedArg Name) -> [Arg Name] -> [NamedArg Name])
-> ((Name -> Named NamedName Name) -> Arg Name -> NamedArg Name)
-> (Name -> Named NamedName Name)
-> [Arg Name]
-> [NamedArg Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Named NamedName Name) -> Arg Name -> NamedArg Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Name -> Named NamedName Name
forall a name. a -> Named name a
unnamed [Arg Name]
xs :: [NamedArg Name], Type
t)
  contextSize :: ([Arg Name], Type) -> Int
contextSize ([Arg Name]
xs, Type
_) = [Arg Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Name]
xs

instance AddContext (List1 (Arg Name), Type) where
  addContext :: (List1 (Arg Name), Type) -> m a -> m a
addContext (List1 (Arg Name)
xs, Type
t) = (List1 (NamedArg Name), Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (((Arg Name -> NamedArg Name)
-> List1 (Arg Name) -> List1 (NamedArg Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Arg Name -> NamedArg Name)
 -> List1 (Arg Name) -> List1 (NamedArg Name))
-> ((Name -> Named NamedName Name) -> Arg Name -> NamedArg Name)
-> (Name -> Named NamedName Name)
-> List1 (Arg Name)
-> List1 (NamedArg Name)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Named NamedName Name) -> Arg Name -> NamedArg Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Name -> Named NamedName Name
forall a name. a -> Named name a
unnamed List1 (Arg Name)
xs :: List1 (NamedArg Name), Type
t)
  contextSize :: (List1 (Arg Name), Type) -> Int
contextSize (List1 (Arg Name)
xs, Type
_) = List1 (Arg Name) -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length List1 (Arg Name)
xs

instance AddContext ([NamedArg Name], Type) where
  addContext :: ([NamedArg Name], Type) -> m a -> m a
addContext ([], Type
_)     = m a -> m a
forall a. a -> a
id
  addContext (NamedArg Name
x : [NamedArg Name]
xs, Type
t) = (List1 (NamedArg Name), Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (NamedArg Name
x NamedArg Name -> [NamedArg Name] -> List1 (NamedArg Name)
forall a. a -> [a] -> NonEmpty a
:| [NamedArg Name]
xs, Type
t)
  contextSize :: ([NamedArg Name], Type) -> Int
contextSize ([NamedArg Name]
xs, Type
_) = [NamedArg Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg Name]
xs

instance AddContext (List1 (NamedArg Name), Type) where
  addContext :: (List1 (NamedArg Name), Type) -> m a -> m a
addContext (NamedArg Name
x :| [NamedArg Name]
xs, Type
t) =
    (Name, Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (NamedArg Name -> Name
forall a. NamedArg a -> a
namedArg NamedArg Name
x, Type
t Type -> Dom' Term () -> Dom Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NamedArg Name -> Dom' Term ()
domFromNamedArgName NamedArg Name
x) (m a -> m a) -> (m a -> m a) -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ([NamedArg Name], Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([NamedArg Name]
xs, Int -> Type -> Type
forall a. Subst a => Int -> a -> a
raise Int
1 Type
t)
  contextSize :: (List1 (NamedArg Name), Type) -> Int
contextSize (List1 (NamedArg Name)
xs, Type
_) = List1 (NamedArg Name) -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length List1 (NamedArg Name)
xs

instance AddContext (String, Dom Type) where
  addContext :: (VerboseKey, Dom Type) -> m a -> m a
addContext (VerboseKey
s, Dom Type
dom) m a
ret =
    Range -> VerboseKey -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> VerboseKey -> (Name -> m a) -> m a
withFreshName Range
forall a. Range' a
noRange VerboseKey
s ((Name -> m a) -> m a) -> (Name -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \Name
x -> Name -> Dom Type -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> m a -> m a
addCtx (Name -> Name
forall a. LensInScope a => a -> a
setNotInScope Name
x) Dom Type
dom m a
ret
  contextSize :: (VerboseKey, Dom Type) -> Int
contextSize (VerboseKey, Dom Type)
_ = Int
1

instance AddContext (KeepNames String, Dom Type) where
  addContext :: (KeepNames VerboseKey, Dom Type) -> m a -> m a
addContext (KeepNames VerboseKey
s, Dom Type
dom) m a
ret =
    Range -> VerboseKey -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> VerboseKey -> (Name -> m a) -> m a
withFreshName Range
forall a. Range' a
noRange VerboseKey
s ((Name -> m a) -> m a) -> (Name -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \ Name
x -> Name -> Dom Type -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> m a -> m a
addCtx Name
x Dom Type
dom m a
ret
  contextSize :: (KeepNames VerboseKey, Dom Type) -> Int
contextSize (KeepNames VerboseKey, Dom Type)
_ = Int
1

instance AddContext (Dom Type) where
  addContext :: Dom Type -> m a -> m a
addContext Dom Type
dom = (VerboseKey, Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (VerboseKey
"_" :: String, Dom Type
dom)
  contextSize :: Dom Type -> Int
contextSize Dom Type
_ = Int
1

instance AddContext Name where
  addContext :: Name -> m a -> m a
addContext Name
x = (Name, Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Name
x, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__)
  contextSize :: Name -> Int
contextSize Name
_ = Int
1

instance {-# OVERLAPPING #-} AddContext String where
  addContext :: VerboseKey -> m a -> m a
addContext VerboseKey
s = (VerboseKey, Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (VerboseKey
s, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__)
  contextSize :: VerboseKey -> Int
contextSize VerboseKey
_ = Int
1

instance AddContext (KeepNames Telescope) where
  addContext :: KeepNames Telescope -> m a -> m a
addContext (KeepNames Telescope
tel) m a
ret = Telescope -> m a
loop Telescope
tel where
    loop :: Telescope -> m a
loop Telescope
EmptyTel          = m a
ret
    loop (ExtendTel Dom Type
t Abs Telescope
tel) = (VerboseKey -> KeepNames VerboseKey)
-> Dom Type -> Abs Telescope -> (Telescope -> m a) -> m a
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
(VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' VerboseKey -> KeepNames VerboseKey
forall a. a -> KeepNames a
KeepNames Dom Type
t Abs Telescope
tel Telescope -> m a
loop
  contextSize :: KeepNames Telescope -> Int
contextSize (KeepNames Telescope
tel) = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel

instance AddContext Telescope where
  addContext :: Telescope -> m a -> m a
addContext Telescope
tel m a
ret = Telescope -> m a
loop Telescope
tel where
    loop :: Telescope -> m a
loop Telescope
EmptyTel          = m a
ret
    loop (ExtendTel Dom Type
t Abs Telescope
tel) = (VerboseKey -> VerboseKey)
-> Dom Type -> Abs Telescope -> (Telescope -> m a) -> m a
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
(VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' VerboseKey -> VerboseKey
forall a. a -> a
id Dom Type
t Abs Telescope
tel Telescope -> m a
loop
  contextSize :: Telescope -> Int
contextSize = Telescope -> Int
forall a. Sized a => a -> Int
size

-- | Go under an abstraction.  Do not extend context in case of 'NoAbs'.
{-# SPECIALIZE underAbstraction :: Subst a => Dom Type -> Abs a -> (a -> TCM b) -> TCM b #-}
underAbstraction :: (Subst a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction :: Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction = (VerboseKey -> VerboseKey)
-> Dom Type -> Abs a -> (a -> m b) -> m b
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
(VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' VerboseKey -> VerboseKey
forall a. a -> a
id

underAbstraction' :: (Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
                     (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' :: (VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' VerboseKey -> name
_ Dom Type
_ (NoAbs VerboseKey
_ a
v) a -> m b
k = a -> m b
k a
v
underAbstraction' VerboseKey -> name
wrap Dom Type
t Abs a
a a -> m b
k = (VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
(VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs' VerboseKey -> name
wrap Dom Type
t Abs a
a a -> m b
k

-- | Go under an abstraction, treating 'NoAbs' as 'Abs'.
underAbstractionAbs :: (Subst a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs :: Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs = (VerboseKey -> VerboseKey)
-> Dom Type -> Abs a -> (a -> m b) -> m b
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
(VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs' VerboseKey -> VerboseKey
forall a. a -> a
id

underAbstractionAbs'
  :: (Subst a, MonadAddContext m, AddContext (name, Dom Type))
  => (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs' :: (VerboseKey -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs' VerboseKey -> name
wrap Dom Type
t Abs a
a a -> m b
k = (name, Dom Type) -> m b -> m b
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (VerboseKey -> name
wrap (VerboseKey -> name) -> VerboseKey -> name
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseKey
realName (VerboseKey -> VerboseKey) -> VerboseKey -> VerboseKey
forall a b. (a -> b) -> a -> b
$ Abs a -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs a
a, Dom Type
t) (m b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$ a -> m b
k (a -> m b) -> a -> m b
forall a b. (a -> b) -> a -> b
$ Abs a -> a
forall a. Subst a => Abs a -> a
absBody Abs a
a
  where
    realName :: VerboseKey -> VerboseKey
realName VerboseKey
s = if VerboseKey -> Bool
forall a. IsNoName a => a -> Bool
isNoName VerboseKey
s then VerboseKey
"x" else VerboseKey -> VerboseKey
argNameToString VerboseKey
s

-- | Go under an abstract without worrying about the type to add to the context.
{-# SPECIALIZE underAbstraction_ :: Subst a => Abs a -> (a -> TCM b) -> TCM b #-}
underAbstraction_ :: (Subst a, MonadAddContext m) => Abs a -> (a -> m b) -> m b
underAbstraction_ :: Abs a -> (a -> m b) -> m b
underAbstraction_ = Dom Type -> Abs a -> (a -> m b) -> m b
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__

-- | Map a monadic function on the thing under the abstraction, adding
--   the abstracted variable to the context.
mapAbstraction
  :: (Subst a, Subst b, MonadAddContext m)
  => Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction :: Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction Dom Type
dom a -> m b
f Abs a
x = (Abs a
x Abs a -> b -> Abs b
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>) (b -> Abs b) -> m b -> m (Abs b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> Abs a -> (a -> m b) -> m b
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
dom Abs a
x a -> m b
f

getLetBindings :: MonadTCM tcm => tcm [(Name,(Term,Dom Type))]
getLetBindings :: tcm [(Name, (Term, Dom Type))]
getLetBindings = do
  Map Name (Open (Term, Dom Type))
bs <- (TCEnv -> Map Name (Open (Term, Dom Type)))
-> tcm (Map Name (Open (Term, Dom Type)))
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Map Name (Open (Term, Dom Type))
envLetBindings
  [(Name, Open (Term, Dom Type))]
-> ((Name, Open (Term, Dom Type)) -> tcm (Name, (Term, Dom Type)))
-> tcm [(Name, (Term, Dom Type))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map Name (Open (Term, Dom Type)) -> [(Name, Open (Term, Dom Type))]
forall k a. Map k a -> [(k, a)]
Map.toList Map Name (Open (Term, Dom Type))
bs) (((Name, Open (Term, Dom Type)) -> tcm (Name, (Term, Dom Type)))
 -> tcm [(Name, (Term, Dom Type))])
-> ((Name, Open (Term, Dom Type)) -> tcm (Name, (Term, Dom Type)))
-> tcm [(Name, (Term, Dom Type))]
forall a b. (a -> b) -> a -> b
$ \ (Name
n,Open (Term, Dom Type)
o) -> (,) Name
n ((Term, Dom Type) -> (Name, (Term, Dom Type)))
-> tcm (Term, Dom Type) -> tcm (Name, (Term, Dom Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Open (Term, Dom Type) -> tcm (Term, Dom Type)
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen Open (Term, Dom Type)
o

-- | Add a let bound variable
{-# SPECIALIZE addLetBinding' :: Name -> Term -> Dom Type -> TCM a -> TCM a #-}
defaultAddLetBinding' :: (ReadTCState m, MonadTCEnv m) => Name -> Term -> Dom Type -> m a -> m a
defaultAddLetBinding' :: Name -> Term -> Dom Type -> m a -> m a
defaultAddLetBinding' Name
x Term
v Dom Type
t m a
ret = do
    Open (Term, Dom Type)
vt <- (Term, Dom Type) -> m (Open (Term, Dom Type))
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
a -> m (Open a)
makeOpen (Term
v, Dom Type
t)
    ((TCEnv -> TCEnv) -> m a -> m a) -> m a -> (TCEnv -> TCEnv) -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC m a
ret ((TCEnv -> TCEnv) -> m a) -> (TCEnv -> TCEnv) -> m a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envLetBindings :: Map Name (Open (Term, Dom Type))
envLetBindings = Name
-> Open (Term, Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Open (Term, Dom Type)
vt (Map Name (Open (Term, Dom Type))
 -> Map Name (Open (Term, Dom Type)))
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall a b. (a -> b) -> a -> b
$ TCEnv -> Map Name (Open (Term, Dom Type))
envLetBindings TCEnv
e }

-- | Add a let bound variable
{-# SPECIALIZE addLetBinding :: ArgInfo -> Name -> Term -> Type -> TCM a -> TCM a #-}
addLetBinding :: MonadAddContext m => ArgInfo -> Name -> Term -> Type -> m a -> m a
addLetBinding :: ArgInfo -> Name -> Term -> Type -> m a -> m a
addLetBinding ArgInfo
info Name
x Term
v Type
t0 m a
ret = Name -> Term -> Dom Type -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Term -> Dom Type -> m a -> m a
addLetBinding' Name
x Term
v (ArgInfo -> Type -> Dom Type
forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
info Type
t0) m a
ret


-- * Querying the context

-- | Get the current context.
{-# SPECIALIZE getContext :: TCM [Dom (Name, Type)] #-}
getContext :: MonadTCEnv m => m [Dom (Name, Type)]
getContext :: m Context
getContext = (TCEnv -> Context) -> m Context
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Context
envContext

-- | Get the size of the current context.
{-# SPECIALIZE getContextSize :: TCM Nat #-}
getContextSize :: (Applicative m, MonadTCEnv m) => m Nat
getContextSize :: m Int
getContextSize = Context -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Context -> Int) -> m Context -> m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Context) -> m Context
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Context
envContext

-- | Generate @[var (n - 1), ..., var 0]@ for all declarations in the context.
{-# SPECIALIZE getContextArgs :: TCM Args #-}
getContextArgs :: (Applicative m, MonadTCEnv m) => m Args
getContextArgs :: m Args
getContextArgs = Args -> Args
forall a. [a] -> [a]
reverse (Args -> Args) -> (Context -> Args) -> Context -> Args
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Dom (Name, Type) -> Arg Term) -> [Int] -> Context -> Args
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Dom (Name, Type) -> Arg Term
forall t b. Int -> Dom' t b -> Arg Term
mkArg [Int
0..] (Context -> Args) -> m Context -> m Args
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
  where mkArg :: Int -> Dom' t b -> Arg Term
mkArg Int
i Dom' t b
dom = Int -> Term
var Int
i Term -> Arg b -> Arg Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom' t b -> Arg b
forall t a. Dom' t a -> Arg a
argFromDom Dom' t b
dom

-- | Generate @[var (n - 1), ..., var 0]@ for all declarations in the context.
{-# SPECIALIZE getContextTerms :: TCM [Term] #-}
getContextTerms :: (Applicative m, MonadTCEnv m) => m [Term]
getContextTerms :: m [Term]
getContextTerms = (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
var ([Int] -> [Term]) -> (Int -> [Int]) -> Int -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Term]) -> m Int -> m [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Int
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize

-- | Get the current context as a 'Telescope'.
{-# SPECIALIZE getContextTelescope :: TCM Telescope #-}
getContextTelescope :: (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope :: m Telescope
getContextTelescope = (Name -> VerboseKey) -> Context -> Telescope
forall a. (a -> VerboseKey) -> ListTel' a -> Telescope
telFromList' Name -> VerboseKey
nameToArgName (Context -> Telescope)
-> (Context -> Context) -> Context -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context
forall a. [a] -> [a]
reverse (Context -> Telescope) -> m Context -> m Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext

-- | Get the names of all declarations in the context.
{-# SPECIALIZE getContextNames :: TCM [Name] #-}
getContextNames :: (Applicative m, MonadTCEnv m) => m [Name]
getContextNames :: m [Name]
getContextNames = (Dom (Name, Type) -> Name) -> Context -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) (Context -> [Name]) -> m Context -> m [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext

-- | get type of bound variable (i.e. deBruijn index)
--
{-# SPECIALIZE lookupBV' :: Nat -> TCM (Maybe (Dom (Name, Type))) #-}
lookupBV' :: MonadTCEnv m => Nat -> m (Maybe (Dom (Name, Type)))
lookupBV' :: Int -> m (Maybe (Dom (Name, Type)))
lookupBV' Int
n = do
  Context
ctx <- m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
  Maybe (Dom (Name, Type)) -> m (Maybe (Dom (Name, Type)))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Dom (Name, Type)) -> m (Maybe (Dom (Name, Type))))
-> Maybe (Dom (Name, Type)) -> m (Maybe (Dom (Name, Type)))
forall a b. (a -> b) -> a -> b
$ Int -> Dom (Name, Type) -> Dom (Name, Type)
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Dom (Name, Type) -> Dom (Name, Type))
-> Maybe (Dom (Name, Type)) -> Maybe (Dom (Name, Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context
ctx Context -> Int -> Maybe (Dom (Name, Type))
forall a. [a] -> Int -> Maybe a
!!! Int
n

{-# SPECIALIZE lookupBV :: Nat -> TCM (Dom (Name, Type)) #-}
lookupBV :: (MonadFail m, MonadTCEnv m) => Nat -> m (Dom (Name, Type))
lookupBV :: Int -> m (Dom (Name, Type))
lookupBV Int
n = do
  let failure :: m (Dom (Name, Type))
failure = do
        Context
ctx <- m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
        VerboseKey -> m (Dom (Name, Type))
forall (m :: * -> *) a. MonadFail m => VerboseKey -> m a
fail (VerboseKey -> m (Dom (Name, Type)))
-> VerboseKey -> m (Dom (Name, Type))
forall a b. (a -> b) -> a -> b
$ VerboseKey
"de Bruijn index out of scope: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Int -> VerboseKey
forall a. Show a => a -> VerboseKey
show Int
n VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
               VerboseKey
" in context " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [Name] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow ((Dom (Name, Type) -> Name) -> Context -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) Context
ctx)
  m (Dom (Name, Type))
-> (Dom (Name, Type) -> m (Dom (Name, Type)))
-> m (Maybe (Dom (Name, Type)))
-> m (Dom (Name, Type))
forall (m :: * -> *) b a.
Monad m =>
m b -> (a -> m b) -> m (Maybe a) -> m b
maybeM m (Dom (Name, Type))
failure Dom (Name, Type) -> m (Dom (Name, Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (m (Maybe (Dom (Name, Type))) -> m (Dom (Name, Type)))
-> m (Maybe (Dom (Name, Type))) -> m (Dom (Name, Type))
forall a b. (a -> b) -> a -> b
$ Int -> m (Maybe (Dom (Name, Type)))
forall (m :: * -> *).
MonadTCEnv m =>
Int -> m (Maybe (Dom (Name, Type)))
lookupBV' Int
n

{-# SPECIALIZE domOfBV :: Nat -> TCM (Dom Type) #-}
domOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m (Dom Type)
domOfBV :: Int -> m (Dom Type)
domOfBV Int
n = ((Name, Type) -> Type) -> Dom (Name, Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, Type) -> Type
forall a b. (a, b) -> b
snd (Dom (Name, Type) -> Dom Type)
-> m (Dom (Name, Type)) -> m (Dom Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m (Dom (Name, Type))
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Int -> m (Dom (Name, Type))
lookupBV Int
n

{-# SPECIALIZE typeOfBV :: Nat -> TCM Type #-}
typeOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Type
typeOfBV :: Int -> m Type
typeOfBV Int
i = Dom Type -> Type
forall t e. Dom' t e -> e
unDom (Dom Type -> Type) -> m (Dom Type) -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m (Dom Type)
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m (Dom Type)
domOfBV Int
i

{-# SPECIALIZE nameOfBV' :: Nat -> TCM (Maybe Name) #-}
nameOfBV' :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m (Maybe Name)
nameOfBV' :: Int -> m (Maybe Name)
nameOfBV' Int
n = (Dom (Name, Type) -> Name)
-> Maybe (Dom (Name, Type)) -> Maybe Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) (Maybe (Dom (Name, Type)) -> Maybe Name)
-> m (Maybe (Dom (Name, Type))) -> m (Maybe Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m (Maybe (Dom (Name, Type)))
forall (m :: * -> *).
MonadTCEnv m =>
Int -> m (Maybe (Dom (Name, Type)))
lookupBV' Int
n

{-# SPECIALIZE nameOfBV :: Nat -> TCM Name #-}
nameOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Name
nameOfBV :: Int -> m Name
nameOfBV Int
n = (Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom (Dom (Name, Type) -> Name) -> m (Dom (Name, Type)) -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m (Dom (Name, Type))
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Int -> m (Dom (Name, Type))
lookupBV Int
n

-- | Get the term corresponding to a named variable. If it is a lambda bound
--   variable the deBruijn index is returned and if it is a let bound variable
--   its definition is returned.
{-# SPECIALIZE getVarInfo :: Name -> TCM (Term, Dom Type) #-}
getVarInfo :: (MonadFail m, MonadTCEnv m) => Name -> m (Term, Dom Type)
getVarInfo :: Name -> m (Term, Dom Type)
getVarInfo Name
x =
    do  Context
ctx <- m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
        Map Name (Open (Term, Dom Type))
def <- (TCEnv -> Map Name (Open (Term, Dom Type)))
-> m (Map Name (Open (Term, Dom Type)))
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Map Name (Open (Term, Dom Type))
envLetBindings
        case (Dom (Name, Type) -> Bool) -> Context -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
List.findIndex ((Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==Name
x) (Name -> Bool)
-> (Dom (Name, Type) -> Name) -> Dom (Name, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) Context
ctx of
            Just Int
n -> do
                Dom Type
t <- Int -> m (Dom Type)
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m (Dom Type)
domOfBV Int
n
                (Term, Dom Type) -> m (Term, Dom Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Term
var Int
n, Dom Type
t)
            Maybe Int
_       ->
                case Name
-> Map Name (Open (Term, Dom Type))
-> Maybe (Open (Term, Dom Type))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x Map Name (Open (Term, Dom Type))
def of
                    Just Open (Term, Dom Type)
vt -> Open (Term, Dom Type) -> m (Term, Dom Type)
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen Open (Term, Dom Type)
vt
                    Maybe (Open (Term, Dom Type))
_       -> VerboseKey -> m (Term, Dom Type)
forall (m :: * -> *) a. MonadFail m => VerboseKey -> m a
fail (VerboseKey -> m (Term, Dom Type))
-> VerboseKey -> m (Term, Dom Type)
forall a b. (a -> b) -> a -> b
$ VerboseKey
"unbound variable " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Name -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (Name -> Name
nameConcrete Name
x) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
                                VerboseKey
" (id: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ NameId -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (Name -> NameId
nameId Name
x) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
")"