module Agda.TypeChecking.Monad.Context where

import Data.Text (Text)
import qualified Data.Text as T

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         ( WriterT )
-- Control.Monad.Fail import is redundant since GHC 8.8.1
import Control.Monad.Fail (MonadFail)

import qualified Data.DList as DL
import Data.Foldable
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.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.Syntax.Common.Pretty
import Agda.Utils.Size
import Agda.Utils.Update

import Agda.Utils.Impossible

-- * Modifying the context

-- | Modify a 'Context' in a computation.  Warning: does not update
--   the checkpoints. Use @updateContext@ instead.
{-# INLINE unsafeModifyContext #-}
unsafeModifyContext :: MonadTCEnv tcm => (Context -> Context) -> tcm a -> tcm a
unsafeModifyContext :: forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext Context -> Context
f = (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a. (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 = f $ envContext e }

{-# INLINE modifyContextInfo #-}
-- | Modify the 'Dom' part of context entries.
modifyContextInfo :: MonadTCEnv tcm => (forall e. Dom e -> Dom e) -> tcm a -> tcm a
modifyContextInfo :: forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(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
$ (ContextEntry -> ContextEntry) -> Context -> Context
forall a b. (a -> b) -> [a] -> [b]
map ContextEntry -> ContextEntry
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 :: forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
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' TCEnv CheckpointId
-> (CheckpointId -> CheckpointId) -> tcm a -> tcm a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
Lens' TCEnv CheckpointId
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' TCEnv (Map CheckpointId (Substitution' Term))
-> (Map CheckpointId (Substitution' Term)
    -> Map CheckpointId (Substitution' Term))
-> tcm a
-> tcm a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Map CheckpointId (Substitution' Term)
 -> f (Map CheckpointId (Substitution' Term)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map CheckpointId (Substitution' Term))
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' TCState (Map ModuleName CheckpointId)
-> (Map ModuleName CheckpointId -> Map ModuleName CheckpointId)
-> tcm a
-> tcm a
forall a b. Lens' TCState a -> (a -> a) -> tcm b -> tcm b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
-> TCState -> f TCState
Lens' TCState (Map ModuleName CheckpointId)
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' ScopeInfo [(Name, LocalVar)]
-> ([(Name, LocalVar)] -> [(Name, LocalVar)]) -> tcm a -> tcm a
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' ScopeInfo a -> (a -> a) -> m b -> m b
locallyScope ([(Name, LocalVar)] -> f [(Name, LocalVar)])
-> ScopeInfo -> f ScopeInfo
Lens' ScopeInfo [(Name, LocalVar)]
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' TCEnv (Map Name (Open LetBinding))
-> (Map Name (Open LetBinding) -> Map Name (Open LetBinding))
-> tcm a
-> tcm a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Map Name (Open LetBinding) -> f (Map Name (Open LetBinding)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map Name (Open LetBinding))
eLetBindings (Map Name (Open LetBinding)
-> Map Name (Open LetBinding) -> Map Name (Open LetBinding)
forall a b. a -> b -> a
const Map Name (Open LetBinding)
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 :: forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
unsafeInTopContext m a
cont =
  Lens' ScopeInfo [(Name, LocalVar)]
-> ([(Name, LocalVar)] -> [(Name, LocalVar)]) -> m a -> m a
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' ScopeInfo a -> (a -> a) -> m b -> m b
locallyScope ([(Name, LocalVar)] -> f [(Name, LocalVar)])
-> ScopeInfo -> f ScopeInfo
Lens' ScopeInfo [(Name, LocalVar)]
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 :: forall (tcm :: * -> *) a. MonadTCM tcm => Nat -> tcm a -> tcm a
unsafeEscapeContext Nat
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
$ Nat -> Context -> Context
forall a. Nat -> [a] -> [a]
drop Nat
n

{-# SPECIALIZE escapeContext :: Impossible -> Int -> TCM a -> TCM a #-}
-- | 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 :: forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext Impossible
err Nat
n = Substitution' Term -> (Context -> Context) -> m a -> m a
forall a. Substitution' Term -> (Context -> Context) -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution' Term -> (Context -> Context) -> m a -> m a
updateContext (Impossible -> Nat -> Substitution' Term
forall a. Impossible -> Nat -> Substitution' a
strengthenS Impossible
err Nat
n) ((Context -> Context) -> m a -> m a)
-> (Context -> Context) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Nat -> Context -> Context
forall a. Nat -> [a] -> [a]
drop Nat
n

-- * Manipulating checkpoints --

{-# SPECIALIZE checkpoint :: Substitution -> TCM a -> TCM a #-}
-- | Add a new checkpoint. Do not use directly!
checkpoint
  :: (MonadDebug tcm, MonadTCM tcm, MonadFresh CheckpointId tcm, ReadTCState tcm)
  => Substitution -> tcm a -> tcm a
checkpoint :: forall (tcm :: * -> *) a.
(MonadDebug tcm, MonadTCM tcm, MonadFresh CheckpointId tcm,
 ReadTCState tcm) =>
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
$ String -> Nat -> String -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"tc.cxt.checkpoint" Nat
105 (String -> tcm ()) -> String -> tcm ()
forall a b. (a -> b) -> a -> b
$ String
"New checkpoint {"
  CheckpointId
old     <- Lens' TCEnv CheckpointId -> tcm CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
Lens' TCEnv CheckpointId
eCurrentCheckpoint
  Map ModuleName CheckpointId
oldMods <- Lens' TCState (Map ModuleName CheckpointId)
-> tcm (Map ModuleName CheckpointId)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC  (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
-> TCState -> f TCState
Lens' TCState (Map ModuleName CheckpointId)
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
$ String -> Nat -> tcm () -> tcm ()
forall (m :: * -> *). MonadDebug m => String -> Nat -> m () -> m ()
verboseS String
"tc.cxt.checkpoint" Nat
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' TCEnv (Map CheckpointId (Substitution' Term))
-> tcm (Map CheckpointId (Substitution' Term))
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Map CheckpointId (Substitution' Term)
 -> f (Map CheckpointId (Substitution' Term)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map CheckpointId (Substitution' Term))
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 a b. (a -> b) -> Map CheckpointId a -> Map CheckpointId b
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 Aspects
prCps Map a a
cps = [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat [ a -> Doc Aspects
forall a. Show a => a -> Doc Aspects
pshow a
c Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
": " Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
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 ]
    String -> Nat -> TCM (Doc Aspects) -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCM (Doc Aspects) -> m ()
reportSDoc String
"tc.cxt.checkpoint" Nat
105 (TCM (Doc Aspects) -> tcm ()) -> TCM (Doc Aspects) -> tcm ()
forall a b. (a -> b) -> a -> b
$ Doc Aspects -> TCM (Doc Aspects)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc Aspects -> TCM (Doc Aspects))
-> Doc Aspects -> TCM (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ Nat -> Doc Aspects -> Doc Aspects
forall a. Nat -> Doc a -> Doc a
nest Nat
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat
      [ Doc Aspects
"old =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> CheckpointId -> Doc Aspects
forall a. Show a => a -> Doc Aspects
pshow CheckpointId
old
      , Doc Aspects
"new =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> CheckpointId -> Doc Aspects
forall a. Show a => a -> Doc Aspects
pshow CheckpointId
chkpt
      , Doc Aspects
"sub =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Substitution' Term -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty Substitution' Term
sub
      , Doc Aspects
"cxt =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Telescope -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty Telescope
cxt
      , Doc Aspects
"old substs =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Map CheckpointId (Substitution' Term) -> Doc Aspects
forall {a} {a}. (Show a, Pretty a) => Map a a -> Doc Aspects
prCps Map CheckpointId (Substitution' Term)
cps
      , Doc Aspects
"new substs =" Doc Aspects -> Doc Aspects -> Doc Aspects
<?> Map CheckpointId (Substitution' Term) -> Doc Aspects
forall {a} {a}. (Show a, Pretty a) => Map a a -> Doc Aspects
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 a. (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 = chkpt
    , envCheckpoints       = Map.insert chkpt IdS $
                              fmap (applySubst sub) (envCheckpoints env)
    }
  Map ModuleName CheckpointId
newMods <- Lens' TCState (Map ModuleName CheckpointId)
-> tcm (Map ModuleName CheckpointId)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
-> TCState -> f TCState
Lens' TCState (Map ModuleName CheckpointId)
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..
  (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
-> TCState -> f TCState
Lens' TCState (Map ModuleName CheckpointId)
stModuleCheckpoints Lens' TCState (Map ModuleName CheckpointId)
-> Map ModuleName CheckpointId -> tcm ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> 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 a b. a -> Map ModuleName b -> Map ModuleName a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Map ModuleName CheckpointId
newMods)
  tcm () -> tcm ()
forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Nat -> String -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"tc.cxt.checkpoint" Nat
105 String
"}"
  a -> tcm a
forall a. 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 :: forall (tcm :: * -> *).
MonadTCEnv tcm =>
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 a. a -> tcm a
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' :: forall (tcm :: * -> *).
MonadTCEnv tcm =>
CheckpointId -> tcm (Maybe (Substitution' Term))
checkpointSubstitution' CheckpointId
chkpt = Lens' TCEnv (Maybe (Substitution' Term))
-> tcm (Maybe (Substitution' Term))
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC ((Map CheckpointId (Substitution' Term)
 -> f (Map CheckpointId (Substitution' Term)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map CheckpointId (Substitution' Term))
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'
     (Map CheckpointId (Substitution' Term))
     (Maybe (Substitution' Term))
forall k v. Ord k => k -> Lens' (Map k v) (Maybe 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 :: forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ModuleName -> m (Maybe (Substitution' Term))
getModuleParameterSub ModuleName
m = do
  Maybe CheckpointId
mcp <- (TCState -> Lens' TCState (Maybe CheckpointId) -> Maybe CheckpointId
forall o i. o -> Lens' o i -> i
^. (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
-> TCState -> f TCState
Lens' TCState (Map ModuleName CheckpointId)
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' (Map ModuleName CheckpointId) (Maybe CheckpointId)
forall k v. Ord k => k -> Lens' (Map k v) (Maybe 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse CheckpointId -> m (Substitution' Term)
forall (tcm :: * -> *).
MonadTCEnv tcm =>
CheckpointId -> tcm (Substitution' Term)
checkpointSubstitution Maybe CheckpointId
mcp


-- * Adding to the context

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' :: Origin -> 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 a. Name -> Dom Type -> n a -> n 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)
    => Origin -> Name -> Term -> Dom Type -> m a -> m a
  addLetBinding' Origin
o 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
$ Origin -> Name -> Term -> Dom Type -> n (StT t a) -> n (StT t a)
forall a. Origin -> Name -> Term -> Dom Type -> n a -> n a
forall (m :: * -> *) a.
MonadAddContext m =>
Origin -> Name -> Term -> Dom Type -> m a -> m a
addLetBinding' Origin
o 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 a. Substitution' Term -> (Context -> Context) -> n a -> n 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 String
x Name -> m a
cont = do
    StT t a
st <- (Run t -> n (StT t a)) -> t n (StT t a)
forall (m :: * -> *) a. Monad m => (Run t -> m a) -> t m 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 -> String -> (Name -> n (StT t a)) -> n (StT t a)
forall a. Range -> String -> (Name -> n a) -> n a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> String -> (Name -> m a) -> m a
withFreshName Range
r String
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 (m :: * -> *) a. Monad m => m (StT t a) -> t m 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 a. a -> n a
forall (m :: * -> *) a. Monad m => a -> m a
return StT t a
st

{-# INLINE defaultAddCtx #-}
-- | Default implementation of addCtx in terms of updateContext
defaultAddCtx :: MonadAddContext m => Name -> Dom Type -> m a -> m a
defaultAddCtx :: forall (m :: * -> *) a.
MonadAddContext m =>
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 a. Substitution' Term -> (Context -> Context) -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution' Term -> (Context -> Context) -> m a -> m a
updateContext (Nat -> Substitution' Term
forall a. Nat -> Substitution' a
raiseS Nat
1) (((Name
x,) (Type -> (Name, Type)) -> Dom Type -> ContextEntry
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
a) ContextEntry -> Context -> Context
forall a. a -> [a] -> [a]
:) m a
ret

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

instance MonadAddContext m => MonadAddContext (ChangeT m)
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 :: forall a. 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 a. Name -> Dom Type -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> m a -> m a
addCtx Name
x Dom Type
a
  addLetBinding' :: forall a.
Origin -> Name -> Term -> Dom Type -> ListT m a -> ListT m a
addLetBinding' Origin
o 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
$ Origin -> Name -> Term -> Dom Type -> m a1 -> m a1
forall a. Origin -> Name -> Term -> Dom Type -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Origin -> Name -> Term -> Dom Type -> m a -> m a
addLetBinding' Origin
o Name
x Term
u Dom Type
a
  updateContext :: forall a.
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 a. Substitution' Term -> (Context -> Context) -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution' Term -> (Context -> Context) -> m a -> m a
updateContext Substitution' Term
sub Context -> Context
f
  withFreshName :: forall a. Range -> String -> (Name -> ListT m a) -> ListT m a
withFreshName Range
r String
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
-> String
-> (Name -> m (Maybe (a, ListT m a)))
-> m (Maybe (a, ListT m a))
forall a. Range -> String -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> String -> (Name -> m a) -> m a
withFreshName Range
r String
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 :: forall b. Name -> TCM b -> TCM b
withShadowingNameTCM Name
x TCM b
f = do
  String -> Nat -> TCM (Doc Aspects) -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCM (Doc Aspects) -> m ()
reportSDoc String
"tc.cxt.shadowing" Nat
80 (TCM (Doc Aspects) -> TCMT IO ())
-> TCM (Doc Aspects) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Doc Aspects -> TCM (Doc Aspects)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc Aspects -> TCM (Doc Aspects))
-> Doc Aspects -> TCM (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"registered" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty Name
x Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"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 String (DList String)
useds) <- TCM b -> TCMT IO (b, Map String (DList String))
forall {m :: * -> *} {a}.
(ReadTCState m, MonadTCState m) =>
m a -> m (a, Map String (DList String))
listenUsedNames TCM b
f
  String -> Nat -> TCM (Doc Aspects) -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCM (Doc Aspects) -> m ()
reportSDoc String
"tc.cxt.shadowing" Nat
90 (TCM (Doc Aspects) -> TCMT IO ())
-> TCM (Doc Aspects) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Doc Aspects -> TCM (Doc Aspects)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc Aspects -> TCM (Doc Aspects))
-> Doc Aspects -> TCM (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"all used names: " Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc Aspects
forall a. String -> Doc a
text (Map String (DList String) -> String
forall a. Show a => a -> String
show Map String (DList String)
useds)
  Name -> Map String (DList String) -> TCMT IO ()
forall {m :: * -> *}.
(MonadDebug m, MonadTCState m) =>
Name -> Map String (DList String) -> m ()
tellShadowing Name
x Map String (DList String)
useds
  b -> TCM b
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return b
result

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

      tellUsedName :: Name -> m ()
tellUsedName Name
x = do
        let concreteX :: Name
concreteX = Name -> Name
nameConcrete Name
x
            rawX :: String
rawX      = Name -> String
nameToRawName Name
concreteX
            rootX :: String
rootX     = Name -> String
nameRoot Name
concreteX
        Lens' TCState (Maybe (DList String))
-> (Maybe (DList String) -> Maybe (DList String)) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens ((Map String (DList String) -> f (Map String (DList String)))
-> TCState -> f TCState
Lens' TCState (Map String (DList String))
stUsedNames ((Map String (DList String) -> f (Map String (DList String)))
 -> TCState -> f TCState)
-> ((Maybe (DList String) -> f (Maybe (DList String)))
    -> Map String (DList String) -> f (Map String (DList String)))
-> (Maybe (DList String) -> f (Maybe (DList String)))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Lens' (Map String (DList String)) (Maybe (DList String))
forall k v. Ord k => k -> Lens' (Map k v) (Maybe v)
key String
rootX) ((Maybe (DList String) -> Maybe (DList String)) -> m ())
-> (Maybe (DList String) -> Maybe (DList String)) -> m ()
forall a b. (a -> b) -> a -> b
$
          DList String -> Maybe (DList String)
forall a. a -> Maybe a
Just (DList String -> Maybe (DList String))
-> (Maybe (DList String) -> DList String)
-> Maybe (DList String)
-> Maybe (DList String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
rawX String -> DList String -> DList String
forall a. a -> DList a -> DList a
`DL.cons`) (DList String -> DList String)
-> (Maybe (DList String) -> DList String)
-> Maybe (DList String)
-> DList String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (DList String) -> DList String
forall m. Monoid m => Maybe m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold

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

instance MonadAddContext TCM where
  addCtx :: forall a. 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 b a. IsBool b => b -> (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' :: forall a. Origin -> Name -> Term -> Dom Type -> TCM a -> TCM a
addLetBinding' Origin
o Name
x Term
u Dom Type
a TCM a
ret = Bool -> (TCM a -> TCM a) -> TCM a -> TCM a
forall b a. IsBool b => b -> (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
$
    Origin -> Name -> Term -> Dom Type -> TCM a -> TCM a
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
Origin -> Name -> Term -> Dom Type -> m a -> m a
defaultAddLetBinding' Origin
o Name
x Term
u Dom Type
a TCM a
ret

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

  withFreshName :: forall a. Range -> String -> (Name -> TCM a) -> TCM a
withFreshName Range
r String
x Name -> TCM a
m = Range -> String -> TCMT IO Name
forall (m :: * -> *).
MonadFresh NameId m =>
Range -> String -> m Name
freshName Range
r String
x TCMT IO Name -> (Name -> TCM a) -> TCM a
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
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 :: forall (m :: * -> *) b.
(MonadAddContext m, MonadFresh NameId m) =>
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 a. 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 b
ret

-- | Various specializations of @addCtx@.
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 :: forall (m :: * -> *) a. MonadAddContext m => [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 a b. (a -> b -> b) -> b -> [a] -> b
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
forall (m :: * -> *) a. MonadAddContext m => a -> m a -> m a
addContext); {-# INLINABLE addContext #-}
  contextSize :: [a] -> Nat
contextSize = [Nat] -> Nat
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Nat] -> Nat) -> ([a] -> [Nat]) -> [a] -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Nat) -> [a] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map a -> Nat
forall b. AddContext b => b -> Nat
contextSize

instance AddContext (Name, Dom Type) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
(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 a. Name -> Dom Type -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> m a -> m a
addCtx; {-# INLINE addContext #-}
  contextSize :: (Name, Dom Type) -> Nat
contextSize (Name, Dom Type)
_ = Nat
1
{-# SPECIALIZE addContext :: (Name, Dom Type) -> TCM a -> TCM a #-}

instance AddContext (Dom (Name, Type)) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
ContextEntry -> 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
forall (m :: * -> *) a.
MonadAddContext m =>
(Name, Dom Type) -> m a -> m a
addContext ((Name, Dom Type) -> m a -> m a)
-> (ContextEntry -> (Name, Dom Type)) -> ContextEntry -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> (Name, Dom Type)
forall (t :: * -> *) (m :: * -> *) a.
(Decoration t, Functor m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a.
Functor m =>
Dom' Term (m a) -> m (Dom' Term a)
distributeF
  contextSize :: ContextEntry -> Nat
contextSize ContextEntry
_ = Nat
1

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

instance AddContext ([Name], Dom Type) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
([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
forall (m :: * -> *) a. MonadAddContext m => Context -> 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) -> Nat
contextSize ([Name]
xs, Dom Type
_) = [Name] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Name]
xs

instance AddContext (List1 Name, Dom Type) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
(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
forall (m :: * -> *) a. MonadAddContext m => Context -> 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) -> Nat
contextSize (List1 Name
xs, Dom Type
_) = List1 Name -> Nat
forall a. NonEmpty a -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length List1 Name
xs

instance AddContext ([WithHiding Name], Dom Type) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
([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
forall (m :: * -> *) a.
MonadAddContext m =>
(NonEmpty (WithHiding Name), Dom Type) -> 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) -> Nat
contextSize ([WithHiding Name]
xs, Dom Type
_) = [WithHiding Name] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [WithHiding Name]
xs

instance AddContext (List1 (WithHiding Name), Dom Type) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
(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
forall (m :: * -> *) a.
MonadAddContext m =>
(Name, Dom Type) -> 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
forall (m :: * -> *) a.
MonadAddContext m =>
([WithHiding Name], Dom Type) -> m a -> m a
addContext ([WithHiding Name]
xs, Nat -> Dom Type -> Dom Type
forall a. Subst a => Nat -> a -> a
raise Nat
1 Dom Type
dom)
  contextSize :: (NonEmpty (WithHiding Name), Dom Type) -> Nat
contextSize (NonEmpty (WithHiding Name)
xs, Dom Type
_) = NonEmpty (WithHiding Name) -> Nat
forall a. NonEmpty a -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length NonEmpty (WithHiding Name)
xs

instance AddContext ([Arg Name], Type) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
([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
forall (m :: * -> *) a.
MonadAddContext m =>
([NamedArg Name], Type) -> 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_ Name) -> Arg Name -> NamedArg Name)
-> (Name -> Named_ Name)
-> [Arg Name]
-> [NamedArg Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Named_ Name) -> Arg Name -> NamedArg Name
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Name -> Named_ Name
forall a name. a -> Named name a
unnamed [Arg Name]
xs :: [NamedArg Name], Type
t)
  contextSize :: ([Arg Name], Type) -> Nat
contextSize ([Arg Name]
xs, Type
_) = [Arg Name] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Arg Name]
xs

instance AddContext (List1 (Arg Name), Type) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
(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
forall (m :: * -> *) a.
MonadAddContext m =>
(List1 (NamedArg Name), Type) -> m a -> m a
addContext (((Arg Name -> NamedArg Name)
-> List1 (Arg Name) -> List1 (NamedArg Name)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
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_ Name) -> Arg Name -> NamedArg Name)
-> (Name -> Named_ Name)
-> List1 (Arg Name)
-> List1 (NamedArg Name)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Named_ Name) -> Arg Name -> NamedArg Name
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Name -> Named_ Name
forall a name. a -> Named name a
unnamed List1 (Arg Name)
xs :: List1 (NamedArg Name), Type
t)
  contextSize :: (List1 (Arg Name), Type) -> Nat
contextSize (List1 (Arg Name)
xs, Type
_) = List1 (Arg Name) -> Nat
forall a. NonEmpty a -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length List1 (Arg Name)
xs

instance AddContext ([NamedArg Name], Type) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
([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
forall (m :: * -> *) a.
MonadAddContext m =>
(List1 (NamedArg Name), Type) -> 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) -> Nat
contextSize ([NamedArg Name]
xs, Type
_) = [NamedArg Name] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [NamedArg Name]
xs

instance AddContext (List1 (NamedArg Name), Type) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
(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
forall (m :: * -> *) a.
MonadAddContext m =>
(Name, Dom Type) -> 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 a b. a -> Dom' Term b -> Dom' Term a
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
forall (m :: * -> *) a.
MonadAddContext m =>
([NamedArg Name], Type) -> m a -> m a
addContext ([NamedArg Name]
xs, Nat -> Type -> Type
forall a. Subst a => Nat -> a -> a
raise Nat
1 Type
t)
  contextSize :: (List1 (NamedArg Name), Type) -> Nat
contextSize (List1 (NamedArg Name)
xs, Type
_) = List1 (NamedArg Name) -> Nat
forall a. NonEmpty a -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length List1 (NamedArg Name)
xs

instance AddContext (String, Dom Type) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
s, Dom Type
dom) m a
ret =
    Range -> String -> (Name -> m a) -> m a
forall a. Range -> String -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> String -> (Name -> m a) -> m a
withFreshName Range
forall a. Range' a
noRange String
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 a. 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 :: (String, Dom Type) -> Nat
contextSize (String, Dom Type)
_ = Nat
1
{-# SPECIALIZE addContext :: (String, Dom Type) -> TCM a -> TCM a #-}

instance AddContext (Text, Dom Type) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
(Text, Dom Type) -> m a -> m a
addContext (Text
s, Dom Type
dom) m a
ret = (String, Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (Text -> String
T.unpack Text
s, Dom Type
dom) m a
ret
  contextSize :: (Text, Dom Type) -> Nat
contextSize (Text, Dom Type)
_ = Nat
1
{-# SPECIALIZE addContext :: (Text, Dom Type) -> TCM a -> TCM a #-}

instance AddContext (KeepNames String, Dom Type) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
(KeepNames String, Dom Type) -> m a -> m a
addContext (KeepNames String
s, Dom Type
dom) m a
ret =
    Range -> String -> (Name -> m a) -> m a
forall a. Range -> String -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> String -> (Name -> m a) -> m a
withFreshName Range
forall a. Range' a
noRange String
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 a. 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 String, Dom Type) -> Nat
contextSize (KeepNames String, Dom Type)
_ = Nat
1
{-# SPECIALIZE addContext :: (KeepNames String, Dom Type) -> TCM a -> TCM a #-}

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

instance AddContext Name where
  addContext :: forall (m :: * -> *) a. MonadAddContext m => 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
forall (m :: * -> *) a.
MonadAddContext m =>
(Name, Dom Type) -> m a -> m a
addContext (Name
x, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__)
  contextSize :: Name -> Nat
contextSize Name
_ = Nat
1

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

instance AddContext (KeepNames Telescope) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
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) = (String -> KeepNames String)
-> Dom Type -> Abs Telescope -> (Telescope -> m a) -> m a
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
(String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' String -> KeepNames String
forall a. a -> KeepNames a
KeepNames Dom Type
t Abs Telescope
tel Telescope -> m a
loop
  contextSize :: KeepNames Telescope -> Nat
contextSize (KeepNames Telescope
tel) = Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
tel
{-# SPECIALIZE addContext :: KeepNames Telescope -> TCM a -> TCM a #-}

instance AddContext Telescope where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
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) = (String -> String)
-> Dom Type -> Abs Telescope -> (Telescope -> m a) -> m a
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
(String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' String -> String
forall a. a -> a
id Dom Type
t Abs Telescope
tel Telescope -> m a
loop
  contextSize :: Telescope -> Nat
contextSize = Telescope -> Nat
forall a. Sized a => a -> Nat
size
{-# SPECIALIZE addContext :: Telescope -> TCM a -> TCM a #-}

-- | 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 :: forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction = (String -> String) -> Dom Type -> Abs a -> (a -> m b) -> m b
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
(String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' String -> String
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' :: forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
(String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' String -> name
_ Dom Type
_ (NoAbs String
_ a
v) a -> m b
k = a -> m b
k a
v
underAbstraction' String -> name
wrap Dom Type
t Abs a
a a -> m b
k = (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
(String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs' String -> 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 :: forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs = (String -> String) -> Dom Type -> Abs a -> (a -> m b) -> m b
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
(String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs' String -> String
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' :: forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
(String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs' String -> 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
forall (m :: * -> *) a.
MonadAddContext m =>
(name, Dom Type) -> m a -> m a
addContext (String -> name
wrap (String -> name) -> String -> name
forall a b. (a -> b) -> a -> b
$ String -> String
realName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Abs a -> String
forall a. Abs a -> String
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 :: String -> String
realName String
s = if String -> Bool
forall a. IsNoName a => a -> Bool
isNoName String
s then String
"x" else String -> String
argNameToString String
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_ :: forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
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 :: forall a b (m :: * -> *).
(Subst a, Subst b, MonadAddContext m) =>
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

mapAbstraction_
  :: (Subst a, Subst b, MonadAddContext m)
  => (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction_ :: forall a b (m :: * -> *).
(Subst a, Subst b, MonadAddContext m) =>
(a -> m b) -> Abs a -> m (Abs b)
mapAbstraction_ = Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
forall a b (m :: * -> *).
(Subst a, Subst b, MonadAddContext m) =>
Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__

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

-- | Add a let bound variable
{-# SPECIALIZE addLetBinding' :: Origin -> Name -> Term -> Dom Type -> TCM a -> TCM a #-}
defaultAddLetBinding' :: (ReadTCState m, MonadTCEnv m) => Origin -> Name -> Term -> Dom Type -> m a -> m a
defaultAddLetBinding' :: forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
Origin -> Name -> Term -> Dom Type -> m a -> m a
defaultAddLetBinding' Origin
o Name
x Term
v Dom Type
t m a
ret = do
    Open LetBinding
vt <- LetBinding -> m (Open LetBinding)
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
a -> m (Open a)
makeOpen (LetBinding -> m (Open LetBinding))
-> LetBinding -> m (Open LetBinding)
forall a b. (a -> b) -> a -> b
$ Origin -> Term -> Dom Type -> LetBinding
LetBinding Origin
o 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 a. (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.insert x vt $ envLetBindings e }

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


{-# SPECIALIZE removeLetBinding :: Name -> TCM a -> TCM a #-}
-- | Remove a let bound variable.
removeLetBinding :: MonadTCEnv m => Name -> m a -> m a
removeLetBinding :: forall (m :: * -> *) a. MonadTCEnv m => Name -> m a -> m a
removeLetBinding Name
x = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \ TCEnv
e -> TCEnv
e { envLetBindings = Map.delete x (envLetBindings e) }

{-# SPECIALIZE removeLetBindingsFrom :: Name -> TCM a -> TCM a #-}
-- | Remove a let bound variable and all let bindings introduced after it. For instance before
--   printing its body to avoid folding the binding itself, or using bindings defined later.
--   Relies on the invariant that names introduced later are sorted after earlier names.
removeLetBindingsFrom :: MonadTCEnv m => Name -> m a -> m a
removeLetBindingsFrom :: forall (m :: * -> *) a. MonadTCEnv m => Name -> m a -> m a
removeLetBindingsFrom Name
x = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \ TCEnv
e -> TCEnv
e { envLetBindings = fst $ Map.split x (envLetBindings e) }

-- * Querying the context

-- | Get the current context.
{-# SPECIALIZE getContext :: TCM Context #-}
getContext :: MonadTCEnv m => m Context
getContext :: forall (m :: * -> *). MonadTCEnv m => 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 :: forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize = Context -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length (Context -> Nat) -> m Context -> m Nat
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 :: forall (m :: * -> *). (Applicative m, MonadTCEnv m) => 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
. (Nat -> ContextEntry -> Arg Term) -> [Nat] -> Context -> Args
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Nat -> ContextEntry -> Arg Term
forall {t} {b}. Nat -> Dom' t b -> Arg Term
mkArg [Nat
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 :: Nat -> Dom' t b -> Arg Term
mkArg Nat
i Dom' t b
dom = Nat -> Term
var Nat
i Term -> Arg b -> Arg Term
forall a b. a -> Arg b -> Arg a
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 :: forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Term]
getContextTerms = (Nat -> Term) -> [Nat] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Nat -> Term
var ([Nat] -> [Term]) -> (Nat -> [Nat]) -> Nat -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom (Nat -> [Term]) -> m Nat -> m [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Nat
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize

-- | Get the current context as a 'Telescope'.
{-# SPECIALIZE getContextTelescope :: TCM Telescope #-}
getContextTelescope :: (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope :: forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope = (Name -> String) -> Context -> Telescope
forall a. (a -> String) -> ListTel' a -> Telescope
telFromList' Name -> String
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 :: forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
getContextNames = (ContextEntry -> Name) -> Context -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (ContextEntry -> (Name, Type)) -> ContextEntry -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> (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)
--
lookupBV_ :: Nat -> Context -> Maybe ContextEntry
lookupBV_ :: Nat -> Context -> Maybe ContextEntry
lookupBV_ Nat
n Context
ctx = Nat -> ContextEntry -> ContextEntry
forall a. Subst a => Nat -> a -> a
raise (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) (ContextEntry -> ContextEntry)
-> Maybe ContextEntry -> Maybe ContextEntry
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context
ctx Context -> Nat -> Maybe ContextEntry
forall a. [a] -> Nat -> Maybe a
!!! Nat
n

{-# SPECIALIZE lookupBV' :: Nat -> TCM (Maybe ContextEntry) #-}
lookupBV' :: MonadTCEnv m => Nat -> m (Maybe ContextEntry)
lookupBV' :: forall (m :: * -> *). MonadTCEnv m => Nat -> m (Maybe ContextEntry)
lookupBV' Nat
n = Nat -> Context -> Maybe ContextEntry
lookupBV_ Nat
n (Context -> Maybe ContextEntry)
-> m Context -> m (Maybe ContextEntry)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext

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

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

{-# SPECIALIZE typeOfBV :: Nat -> TCM Type #-}
typeOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Type
typeOfBV :: forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m Type
typeOfBV Nat
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
<$> Nat -> m (Dom Type)
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m (Dom Type)
domOfBV Nat
i

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

{-# SPECIALIZE nameOfBV :: Nat -> TCM Name #-}
nameOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Name
nameOfBV :: forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m Name
nameOfBV Nat
n = (Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (ContextEntry -> (Name, Type)) -> ContextEntry -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> (Name, Type)
forall t e. Dom' t e -> e
unDom (ContextEntry -> Name) -> m ContextEntry -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat -> m ContextEntry
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Nat -> m ContextEntry
lookupBV Nat
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 :: forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Name -> m (Term, Dom Type)
getVarInfo Name
x =
    do  Context
ctx <- m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
        Map Name (Open LetBinding)
def <- (TCEnv -> Map Name (Open LetBinding))
-> m (Map Name (Open LetBinding))
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Map Name (Open LetBinding)
envLetBindings
        case (ContextEntry -> Bool) -> Context -> Maybe Nat
forall a. (a -> Bool) -> [a] -> Maybe Nat
List.findIndex ((Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x) (Name -> Bool) -> (ContextEntry -> Name) -> ContextEntry -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (ContextEntry -> (Name, Type)) -> ContextEntry -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> (Name, Type)
forall t e. Dom' t e -> e
unDom) Context
ctx of
            Just Nat
n -> do
                Dom Type
t <- Nat -> m (Dom Type)
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m (Dom Type)
domOfBV Nat
n
                (Term, Dom Type) -> m (Term, Dom Type)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Nat -> Term
var Nat
n, Dom Type
t)
            Maybe Nat
_       ->
                case Name -> Map Name (Open LetBinding) -> Maybe (Open LetBinding)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x Map Name (Open LetBinding)
def of
                    Just Open LetBinding
vt -> do
                      LetBinding Origin
_ Term
v Dom Type
t <- Open LetBinding -> m LetBinding
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen Open LetBinding
vt
                      (Term, Dom Type) -> m (Term, Dom Type)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Dom Type
t)
                    Maybe (Open LetBinding)
_       -> String -> m (Term, Dom Type)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m (Term, Dom Type)) -> String -> m (Term, Dom Type)
forall a b. (a -> b) -> a -> b
$ String
"unbound variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Pretty a => a -> String
prettyShow (Name -> Name
nameConcrete Name
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                String
" (id: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ NameId -> String
forall a. Pretty a => a -> String
prettyShow (Name -> NameId
nameId Name
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"