-- {-# OPTIONS_GHC -ddump-simpl -dsuppress-all -dno-suppress-type-signatures -ddump-to-file -dno-typeable-binds #-}

module Mikan.TypeChecking.Monad.Context where

import Data.Text (Text)
import Data.Text qualified 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 )

import Data.Foldable
import Data.HashMap.Strict qualified as HMap
import Data.IntMap qualified as IntMap
import Data.List qualified as List
import Data.Map qualified as Map
import Data.Set qualified as Set
import Data.Set (Set)
import Data.Text.Short (ShortText)

import Mikan.Syntax.Abstract.Name
import Mikan.Syntax.Common
import Mikan.Syntax.Common.Pretty
import Mikan.Syntax.Concrete.Name (NameInScope(..), LensInScope(..), nameRoot, nameToRawName)
import Mikan.Syntax.Concrete.Name qualified as C
import Mikan.Syntax.Internal
import Mikan.Syntax.Position
import Mikan.Syntax.Scope.Base

import Mikan.TypeChecking.Monad.Base
import Mikan.TypeChecking.Monad.Debug
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Monad.Open
import Mikan.TypeChecking.Monad.State
import Mikan.TypeChecking.Warnings (warning, MonadWarning)

import Mikan.Utils.Function
import Mikan.Utils.Functor
import Mikan.Utils.Impossible
import Mikan.Utils.Lens
import Mikan.Utils.List
import Mikan.Utils.ListT
import Mikan.Utils.List1 (List1, pattern (:|))
import Mikan.Utils.List1 qualified as List1
import Mikan.Utils.Set1 qualified as Set1
import Mikan.Utils.Maybe
import Mikan.Utils.Monad (mzero, void)
import Mikan.Utils.Null (empty)
import Mikan.Utils.Size
import Mikan.Utils.Tuple
import Mikan.Utils.Update


import Mikan.Utils.StrictReader qualified as Strict
import Mikan.Utils.StrictWriter qualified as Strict
import Mikan.Utils.StrictState  qualified as Strict

import Mikan.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 (ASetter TCEnv TCEnv Context Context
-> (Context -> Context) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv Context Context
Lens' TCEnv Context
eContext Context -> Context
f)

{-# 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) -> Context' a -> Context' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ContextEntry -> ContextEntry) -> Context -> Context)
-> (ContextEntry -> ContextEntry) -> Context -> Context
forall a b. (a -> b) -> a -> b
$ \case
    (CtxVar Name
x Dom Type
a)   -> Name -> Dom Type -> ContextEntry
CtxVar Name
x (Dom Type -> Dom Type
forall e. Dom e -> Dom e
f Dom Type
a)

-- | Change to top (=empty) context. Resets the checkpoints.
{-# INLINE inTopContext #-}
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 Context
CxEmpty)
        (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' 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 -> tcm a
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withoutModuleCheckpoints
        (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!
{-# INLINE unsafeInTopContext #-}
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 Context
CxEmpty) 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`.
{-# INLINE unsafeEscapeContext #-}
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
cxDrop Nat
n

{-# INLINE escapeContext #-}
-- | 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
cxDrop Nat
n

-- * Manipulating checkpoints --

-- {-# NOINLINE checkpoint' #-}
-- checkpoint' :: Substitution -> TCM a -> TCM a
-- checkpoint' = checkpoint

{-# INLINE checkpoint #-}
-- | Add a new checkpoint. Do not use directly!
checkpoint :: Substitution -> TCM a -> TCM a
checkpoint :: forall a. Substitution' Term -> TCM a -> TCM a
checkpoint Substitution' Term
sub TCM a
k = do
  TCMT IO () -> TCMT IO ()
forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String -> Nat -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"tc.cxt.checkpoint" Nat
105 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String
"New checkpoint {"
  old <- Lens' TCEnv CheckpointId -> TCMT IO CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
Lens' TCEnv CheckpointId
eCurrentCheckpoint
  tc <- getTC
  let oldChkpts = TCState
tc TCState
-> Getting ModuleCheckpoints TCState ModuleCheckpoints
-> ModuleCheckpoints
forall s a. s -> Getting a s a -> a
^. Getting ModuleCheckpoints TCState ModuleCheckpoints
Lens' TCState ModuleCheckpoints
stModuleCheckpoints
  let chkpt     = TCState
tc TCState
-> Getting CheckpointId TCState CheckpointId -> CheckpointId
forall s a. s -> Getting a s a -> a
^. Getting CheckpointId TCState CheckpointId
forall i. HasFresh i => Lens' TCState i
Lens' TCState CheckpointId
freshLens
  putTC $! tc & freshLens .~ (nextFresh' chkpt)

  unlessDebugPrinting $ verboseS "tc.cxt.checkpoint" 105 $ do
    cxt <- getContextTelescope
    cps <- viewTC eCheckpoints
    let 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
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 ]
    reportS "tc.cxt.checkpoint" 105 $ nest 2 $ vcat
      [ "old =" <+> pshow old
      , "new =" <+> pshow chkpt
      , "sub =" <+> pretty sub
      , "cxt =" <+> pretty cxt
      , "mods =" <+> pretty oldChkpts
      , "old substs =" <+> prCps cps
      , "new substs =" <?> prCps cps'
      ]

  x <- localTC (  set eCurrentCheckpoint chkpt
                . over eCheckpoints (Map.insert chkpt IdS . fmap (applySubst sub))
               )
               k

  unlessDebugPrinting $ verboseS "tc.cxt.checkpoint" 105 $ do
    newChkpts <- useTC stModuleCheckpoints
    reportS "tc.cxt.checkpoint" 105 $ nest 2 $
      "mods before unwind =" <+> pretty newChkpts

  -- 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..

  -- [HACK: Repairing module checkpoints after state resets]
  -- Ideally, we could just walk up the current module checkpoint stack
  -- until we hit the the @old@ checkpoint. This works in most cases, but breaks if
  -- @k@ resets the typechecking state to a state defined *before* the call to
  -- @checkpoint@: this can result in us discarding module checkpoints.
  --
  -- To prevent this, we walk up the current module checkpoint stack until
  -- we hit our previous checkpoint, and add any module checkpoints onto
  -- the checkpoint stack we had before we ran @k@.
  unwindModuleCheckpointsOnto old oldChkpts

  unlessDebugPrinting $ verboseS "tc.cxt.checkpoint" 105 $ do
    unwoundChkpts <- useTC stModuleCheckpoints
    reportS "tc.cxt.checkpoint" 105 $ nest 2 $
      "unwound mods =" <+> pretty unwoundChkpts

  unlessDebugPrinting $ reportSLn "tc.cxt.checkpoint" 105 "}"
  return x

-- | Add a module checkpoint for the provided @ModuleName@.
{-# SPECIALIZE setModuleCheckpoint :: ModuleName -> CheckpointId -> TCM () #-}
setModuleCheckpoint :: (MonadTCState m) => ModuleName -> CheckpointId -> m ()
setModuleCheckpoint :: forall (m :: * -> *).
MonadTCState m =>
ModuleName -> CheckpointId -> m ()
setModuleCheckpoint !ModuleName
mname !CheckpointId
newChkpt =
  ASetter' TCState ModuleCheckpoints
-> (ModuleCheckpoints -> ModuleCheckpoints) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ASetter' TCState ModuleCheckpoints
Lens' TCState ModuleCheckpoints
stModuleCheckpoints \case
      (ModuleCheckpointsSection ModuleCheckpoints
chkpts Set ModuleName
mnames CheckpointId
chkpt) | CheckpointId
chkpt CheckpointId -> CheckpointId -> Bool
forall a. Eq a => a -> a -> Bool
== CheckpointId
newChkpt ->
        ModuleCheckpoints
-> Set ModuleName -> CheckpointId -> ModuleCheckpoints
ModuleCheckpointsSection ModuleCheckpoints
chkpts (ModuleName -> Set ModuleName -> Set ModuleName
forall a. Ord a => a -> Set a -> Set a
Set.insert ModuleName
mname Set ModuleName
mnames) CheckpointId
chkpt
      ModuleCheckpoints
chkpts -> ModuleCheckpoints
-> Set ModuleName -> CheckpointId -> ModuleCheckpoints
ModuleCheckpointsSection ModuleCheckpoints
chkpts (ModuleName -> Set ModuleName
forall a. a -> Set a
Set.singleton ModuleName
mname) CheckpointId
newChkpt

-- | Set every module checkpoint in the checkpoint stack to the provided @CheckpointId@.
{-# SPECIALIZE setAllModuleCheckpoints :: CheckpointId -> TCM () #-}
setAllModuleCheckpoints :: (MonadTCState m) => CheckpointId -> m ()
setAllModuleCheckpoints :: forall (m :: * -> *). MonadTCState m => CheckpointId -> m ()
setAllModuleCheckpoints !CheckpointId
chkpt =
  ASetter' TCState ModuleCheckpoints
-> (ModuleCheckpoints -> ModuleCheckpoints) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ASetter' TCState ModuleCheckpoints
Lens' TCState ModuleCheckpoints
stModuleCheckpoints \case
    ModuleCheckpoints
ModuleCheckpointsTop -> ModuleCheckpoints
ModuleCheckpointsTop
    ModuleCheckpointsSection ModuleCheckpoints
chkpts Set ModuleName
siblings CheckpointId
_ -> Set ModuleName -> ModuleCheckpoints -> ModuleCheckpoints
setAll Set ModuleName
siblings ModuleCheckpoints
chkpts
  where
    setAll :: Set ModuleName -> ModuleCheckpoints -> ModuleCheckpoints
    setAll :: Set ModuleName -> ModuleCheckpoints -> ModuleCheckpoints
setAll Set ModuleName
acc ModuleCheckpoints
ModuleCheckpointsTop = ModuleCheckpoints
-> Set ModuleName -> CheckpointId -> ModuleCheckpoints
ModuleCheckpointsSection ModuleCheckpoints
ModuleCheckpointsTop Set ModuleName
acc CheckpointId
chkpt
    setAll Set ModuleName
acc (ModuleCheckpointsSection ModuleCheckpoints
chkpts Set ModuleName
siblings CheckpointId
_) = Set ModuleName -> ModuleCheckpoints -> ModuleCheckpoints
setAll (Set ModuleName -> Set ModuleName -> Set ModuleName
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set ModuleName
siblings Set ModuleName
acc) ModuleCheckpoints
chkpts

-- | Unwind the current module checkpoint stack until we reach a target @CheckpointId@,
--   and place the checkpoints onto the provided @ModuleCheckpoints@ stack.
{-# SPECIALIZE NOINLINE unwindModuleCheckpointsOnto :: CheckpointId -> ModuleCheckpoints -> TCM () #-} -- TODO
unwindModuleCheckpointsOnto :: (MonadTCState m) => CheckpointId -> ModuleCheckpoints -> m ()
unwindModuleCheckpointsOnto :: forall (m :: * -> *).
MonadTCState m =>
CheckpointId -> ModuleCheckpoints -> m ()
unwindModuleCheckpointsOnto !CheckpointId
unwindTo !ModuleCheckpoints
oldChkpts =
  -- We know that the checkpoints in the stack are sorted,
  -- so we can do a preliminary check to see if there's
  -- any work to be done.
  ASetter' TCState ModuleCheckpoints
-> (ModuleCheckpoints -> ModuleCheckpoints) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ASetter' TCState ModuleCheckpoints
Lens' TCState ModuleCheckpoints
stModuleCheckpoints \case
    ModuleCheckpointsSection ModuleCheckpoints
chkpts Set ModuleName
siblings CheckpointId
chkpt | CheckpointId
unwindTo CheckpointId -> CheckpointId -> Bool
forall a. Ord a => a -> a -> Bool
< CheckpointId
chkpt -> Set ModuleName -> ModuleCheckpoints -> ModuleCheckpoints
unwind Set ModuleName
siblings ModuleCheckpoints
chkpts
    ModuleCheckpoints
_ -> ModuleCheckpoints
oldChkpts
  where
    unwind :: Set ModuleName -> ModuleCheckpoints -> ModuleCheckpoints
    unwind :: Set ModuleName -> ModuleCheckpoints -> ModuleCheckpoints
unwind Set ModuleName
acc ModuleCheckpoints
ModuleCheckpointsTop =
      ModuleCheckpoints
-> Set ModuleName -> CheckpointId -> ModuleCheckpoints
ModuleCheckpointsSection ModuleCheckpoints
ModuleCheckpointsTop Set ModuleName
acc CheckpointId
unwindTo
    unwind Set ModuleName
acc (ModuleCheckpointsSection ModuleCheckpoints
chkpts Set ModuleName
siblings CheckpointId
chkpt)
      | CheckpointId
chkpt CheckpointId -> CheckpointId -> Bool
forall a. Ord a => a -> a -> Bool
< CheckpointId
unwindTo =
        -- If the unwind target isnt present in the stack, we add it
        -- ourselves.
        ModuleCheckpoints
-> Set ModuleName -> CheckpointId -> ModuleCheckpoints
ModuleCheckpointsSection ModuleCheckpoints
oldChkpts Set ModuleName
acc CheckpointId
unwindTo
      | CheckpointId
chkpt CheckpointId -> CheckpointId -> Bool
forall a. Eq a => a -> a -> Bool
== CheckpointId
unwindTo =
        -- Make sure to avoid adding duplicate entries into the unwind
        -- stack: this would break later unwinds!
        ModuleCheckpoints
-> Set ModuleName -> CheckpointId -> ModuleCheckpoints
ModuleCheckpointsSection ModuleCheckpoints
oldChkpts (Set ModuleName -> Set ModuleName -> Set ModuleName
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set ModuleName
siblings Set ModuleName
acc) CheckpointId
chkpt
      | Bool
otherwise = Set ModuleName -> ModuleCheckpoints -> ModuleCheckpoints
unwind (Set ModuleName -> Set ModuleName -> Set ModuleName
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set ModuleName
siblings Set ModuleName
acc) ModuleCheckpoints
chkpts

{-# INLINE withoutModuleCheckpoints #-}
-- | Run a computation with no module checkpoints set.
withoutModuleCheckpoints :: (ReadTCState m) => m a -> m a
withoutModuleCheckpoints :: forall (m :: * -> *) a. ReadTCState m => m a -> m a
withoutModuleCheckpoints = Lens' TCState ModuleCheckpoints
-> (ModuleCheckpoints -> ModuleCheckpoints) -> m a -> m a
forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (ModuleCheckpoints -> f ModuleCheckpoints) -> TCState -> f TCState
Lens' TCState ModuleCheckpoints
stModuleCheckpoints (ModuleCheckpoints -> ModuleCheckpoints -> ModuleCheckpoints
forall a b. a -> b -> a
const ModuleCheckpoints
ModuleCheckpointsTop)

{-# SPECIALIZE checkpointSubstitution :: CheckpointId -> TCM Substitution #-}
-- | 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'

{-# SPECIALIZE checkpointSubstitution' :: CheckpointId -> TCM (Maybe Substitution) #-}
-- | 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 the @CheckpointId@ of a module name.
getModuleCheckpoint :: ModuleName -> ModuleCheckpoints -> Maybe CheckpointId
getModuleCheckpoint :: ModuleName -> ModuleCheckpoints -> Maybe CheckpointId
getModuleCheckpoint ModuleName
mname ModuleCheckpoints
ModuleCheckpointsTop = Maybe CheckpointId
forall a. Maybe a
Nothing
getModuleCheckpoint ModuleName
mname (ModuleCheckpointsSection ModuleCheckpoints
chkpts Set ModuleName
siblings CheckpointId
chkid)
  | ModuleName -> Set ModuleName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ModuleName
mname Set ModuleName
siblings = CheckpointId -> Maybe CheckpointId
forall a. a -> Maybe a
Just CheckpointId
chkid
  | Bool
otherwise = ModuleName -> ModuleCheckpoints -> Maybe CheckpointId
getModuleCheckpoint ModuleName
mname ModuleCheckpoints
chkpts

{-# SPECIALIZE getModuleParameterSub :: ModuleName -> TCM (Maybe Substitution) #-}
-- | 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
  chkpt <- ModuleName -> ModuleCheckpoints -> Maybe CheckpointId
getModuleCheckpoint ModuleName
m (ModuleCheckpoints -> Maybe CheckpointId)
-> m ModuleCheckpoints -> m (Maybe CheckpointId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getter TCState ModuleCheckpoints -> m ModuleCheckpoints
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (ModuleCheckpoints -> f ModuleCheckpoints) -> TCState -> f TCState
Lens' TCState ModuleCheckpoints
Getter TCState ModuleCheckpoints
stModuleCheckpoints
  traverse checkpointSubstitution chkpt

-- * 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' ::
       IsAxiom   -- ^ Does this let binding come from a 'LetAxiom'?
    -> 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)
    => IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a
  addLetBinding' IsAxiom
isAxiom 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
$ IsAxiom
-> Origin -> Name -> Term -> Dom Type -> n (StT t a) -> n (StT t a)
forall a.
IsAxiom -> Origin -> Name -> Term -> Dom Type -> n a -> n a
forall (m :: * -> *) a.
MonadAddContext m =>
IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a
addLetBinding' IsAxiom
isAxiom 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 ShortText
x Name -> m a
cont = do
    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 -> ShortText -> (Name -> n (StT t a)) -> n (StT t a)
forall a. Range -> ShortText -> (Name -> n a) -> n a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> ShortText -> (Name -> m a) -> m a
withFreshName Range
r ShortText
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
    restoreT $ return 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 -> Dom Type -> Context -> Context
CxExtendVar Name
x Dom Type
a) m a
ret

{-# INLINE withFreshName_ #-}
withFreshName_ :: (MonadAddContext m) => ArgName -> (Name -> m a) -> m a
withFreshName_ :: forall (m :: * -> *) a.
MonadAddContext m =>
ShortText -> (Name -> m a) -> m a
withFreshName_ = Range -> ShortText -> (Name -> m a) -> m a
forall a. Range -> ShortText -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> ShortText -> (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)
instance MonadAddContext m => MonadAddContext (Strict.ReaderT r m)
instance MonadAddContext m => MonadAddContext (Strict.StateT r m)
instance (Monoid w, MonadAddContext m) => MonadAddContext (Strict.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.
IsAxiom
-> Origin -> Name -> Term -> Dom Type -> ListT m a -> ListT m a
addLetBinding' IsAxiom
isAxiom 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
$ IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a1 -> m a1
forall a.
IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a
addLetBinding' IsAxiom
isAxiom 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 -> ShortText -> (Name -> ListT m a) -> ListT m a
withFreshName Range
r ShortText
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
-> ShortText
-> (Name -> m (Maybe (a, ListT m a)))
-> m (Maybe (a, ListT m a))
forall a. Range -> ShortText -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> ShortText -> (Name -> m a) -> m a
withFreshName Range
r ShortText
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

instance MonadAddContext TCM where
  {-# INLINE addCtx #-}
  addCtx :: forall a. Name -> Dom Type -> TCM a -> TCM a
addCtx !Name
x !Dom Type
a !TCM a
ret = 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

  {-# INLINE addLetBinding' #-}
  addLetBinding' :: forall a.
IsAxiom -> Origin -> Name -> Term -> Dom Type -> TCM a -> TCM a
addLetBinding' IsAxiom
isAxiom Origin
o Name
x Term
u Dom Type
a TCM a
ret = IsAxiom -> Origin -> Name -> Term -> Dom Type -> TCM a -> TCM a
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a
defaultAddLetBinding' IsAxiom
isAxiom Origin
o Name
x Term
u Dom Type
a TCM a
ret

  {-# INLINE updateContext #-}
  updateContext :: forall a.
Substitution' Term -> (Context -> Context) -> TCM a -> TCM a
updateContext !Substitution' Term
sub !Context -> Context
f !TCM a
act = (Context -> Context) -> TCM a -> TCM a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext Context -> Context
f (Substitution' Term -> TCM a -> TCM a
forall a. Substitution' Term -> TCM a -> TCM a
checkpoint Substitution' Term
sub TCM a
act)

  {-# INLINE withFreshName #-}
  withFreshName :: forall a. Range -> ShortText -> (Name -> TCM a) -> TCM a
withFreshName Range
r ShortText
x Name -> TCM a
m = Range -> ShortText -> TCMT IO Name
forall (m :: * -> *).
MonadFresh NameId m =>
Range -> ShortText -> m Name
freshName Range
r ShortText
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

{-# INLINE addRecordNameContext #-}
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
  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
  addCtx x dom ret

-- | Various specializations of @addCtx@.
class AddContext b where
  addContext :: (MonadAddContext m) => b -> m a -> m a

-- | 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 #-}

instance AddContext Context where
  addContext :: forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext = (m a -> Context -> m a) -> Context -> m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((m a -> ContextEntry -> m a) -> m a -> Context -> m a
forall b a. (b -> a -> b) -> b -> Context' a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((m a -> ContextEntry -> m a) -> m a -> Context -> m a)
-> (m a -> ContextEntry -> m a) -> m a -> Context -> m a
forall a b. (a -> b) -> a -> b
$ (ContextEntry -> m a -> m a) -> m a -> ContextEntry -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ContextEntry -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
ContextEntry -> m a -> m a
addContext); {-# INLINABLE addContext #-}

instance AddContext ContextEntry where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
ContextEntry -> m a -> m a
addContext (CtxVar Name
x Dom Type
a) = 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
a
  {-# INLINE addContext #-}

instance t ~ Term => AddContext (Name, Dom' t Type) where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
(Name, Dom' t Type) -> m a -> m a
addContext = (Name -> Dom' t Type -> m a -> m a)
-> (Name, Dom' t Type) -> m a -> m a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Dom' t Type -> m a -> m a
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;

instance t ~ Term => AddContext (Dom' t (Name, Type)) where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
Dom' t (Name, Type) -> m a -> m a
addContext = (Name, Dom' t 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' t Type) -> m a -> m a
addContext ((Name, Dom' t Type) -> m a -> m a)
-> (Dom' t (Name, Type) -> (Name, Dom' t Type))
-> Dom' t (Name, Type)
-> m a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' t (Name, Type) -> (Name, Dom' t Type)
forall (t :: * -> *) (m :: * -> *) a.
(Decoration t, Functor m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Functor m => Dom' t (m a) -> m (Dom' t a)
distributeF

instance t ~ Term => AddContext (Dom' t (ShortText, Type)) where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
Dom' t (ShortText, Type) -> m a -> m a
addContext = (ShortText, Dom' t Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(ShortText, Dom' t Type) -> m a -> m a
addContext ((ShortText, Dom' t Type) -> m a -> m a)
-> (Dom' t (ShortText, Type) -> (ShortText, Dom' t Type))
-> Dom' t (ShortText, Type)
-> m a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' t (ShortText, Type) -> (ShortText, Dom' t Type)
forall (t :: * -> *) (m :: * -> *) a.
(Decoration t, Functor m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Functor m => Dom' t (m a) -> m (Dom' t a)
distributeF

instance t ~ Term => AddContext ([Name], Dom' t Type) where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
([Name], Dom' t Type) -> m a -> m a
addContext ([Name]
xs, Dom' t Type
dom) = ListTel' Name -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
ListTel' Name -> m a -> m a
addContext ((Name -> Name) -> [Name] -> Dom Type -> ListTel' Name
forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' Name -> Name
forall a. a -> a
id [Name]
xs Dom' t Type
Dom Type
dom)

instance t ~ Term => AddContext (List1 Name, Dom' t Type) where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
(List1 Name, Dom' t Type) -> m a -> m a
addContext (List1 Name
xs, Dom' t Type
dom) = ListTel' Name -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
ListTel' Name -> m a -> m a
addContext ((Name -> Name) -> List1 Name -> Dom Type -> ListTel' Name
forall a. (Name -> a) -> List1 Name -> Dom Type -> ListTel' a
bindsToTel'1 Name -> Name
forall a. a -> a
id List1 Name
xs Dom' t Type
Dom Type
dom)

instance AddContext ([WithHiding Name], Dom Type) where
  {-# INLINE addContext #-}
  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)

instance AddContext (List1 (WithHiding Name), Dom Type) where
  {-# INLINE addContext #-}
  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)

instance AddContext ([Arg Name], Type) where
  {-# INLINE addContext #-}
  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)

instance AddContext (List1 (Arg Name), Type) where
  {-# INLINE addContext #-}
  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)

instance AddContext ([NamedArg Name], Type) where
  {-# INLINE addContext #-}
  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)

instance AddContext (List1 (NamedArg Name), Type) where
  {-# INLINE addContext #-}
  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)

instance t ~ Term => AddContext ([Dom' t Name], Type) where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
([Dom' t Name], Type) -> m a -> m a
addContext ([], Type
_)     = m a -> m a
forall a. a -> a
id
  addContext (Dom' t Name
x : [Dom' t Name]
xs, Type
t) = (NonEmpty (Dom' t Name), Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(NonEmpty (Dom' t Name), Type) -> m a -> m a
addContext (Dom' t Name
x Dom' t Name -> [Dom' t Name] -> NonEmpty (Dom' t Name)
forall a. a -> [a] -> NonEmpty a
:| [Dom' t Name]
xs, Type
t)

instance t ~ Term => AddContext (List1 (Dom' t Name), Type) where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
(List1 (Dom' t Name), Type) -> m a -> m a
addContext (Dom' t Name
x :| [Dom' t Name]
xs, Type
t) =
    (Name, Dom' t 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' t Type) -> m a -> m a
addContext (Dom' t Name -> Name
forall t e. Dom' t e -> e
unDom Dom' t Name
x, Dom' t Name
x Dom' t Name -> Type -> Dom' t Type
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Type
t) (m a -> m a) -> (m a -> m a) -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ([Dom' t Name], Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
([Dom' t Name], Type) -> m a -> m a
addContext ([Dom' t Name]
xs, Nat -> Type -> Type
forall a. Subst a => Nat -> a -> a
raise Nat
1 Type
t)

instance t ~ Term => AddContext (ShortText, Dom' t Type) where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
(ShortText, Dom' t Type) -> m a -> m a
addContext (ShortText
s, Dom' t Type
dom) m a
ret =
    Range -> ShortText -> (Name -> m a) -> m a
forall a. Range -> ShortText -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> ShortText -> (Name -> m a) -> m a
withFreshName Range
forall a. Range' a
noRange ShortText
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' t Type
Dom Type
dom m a
ret

instance t ~ Term => AddContext (KeepNames ShortText, Dom' t Type) where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
(KeepNames ShortText, Dom' t Type) -> m a -> m a
addContext (KeepNames ShortText
s, Dom' t Type
dom) m a
ret =
    Range -> ShortText -> (Name -> m a) -> m a
forall a. Range -> ShortText -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> ShortText -> (Name -> m a) -> m a
withFreshName Range
forall a. Range' a
noRange ShortText
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' t Type
Dom Type
dom m a
ret

instance t ~ Term => AddContext (Dom' t Type) where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
Dom' t Type -> m a -> m a
addContext Dom' t Type
dom = (ShortText, Dom' t Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(ShortText, Dom' t Type) -> m a -> m a
addContext (ShortText
"_" :: ShortText, Dom' t Type
dom)

instance AddContext Name where
  {-# INLINE addContext #-}
  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__)

instance AddContext ShortText where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
ShortText -> m a -> m a
addContext ShortText
s = (ShortText, Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(ShortText, Dom Type) -> m a -> m a
addContext (ShortText
s, Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__)

-- | Compute a weakening substitution and a context extension
-- (represented as a function between contexts) from the given
-- 'Telescope', as required by 'updateContext'.
--
-- This function should be accessed through the @'AddContext'@ instances
-- for @'Telescope'@ and @'KeepNames' 'Telescope'@.
addContextTele
  :: MonadAddContext m
  => (Name -> Name)
  -- ^ A modification on the names generated for the new context
  -- entries. Can be used to e.g. mark the new names as out of scope.
  -> Telescope
  -> m (Substitution, Context -> Context)
addContextTele :: forall (m :: * -> *).
MonadAddContext m =>
(Name -> Name)
-> Telescope -> m (Substitution' Term, Context -> Context)
addContextTele Name -> Name
wrap Telescope
tele = do
  let
    realName :: ShortText -> ShortText
realName ShortText
s = if ShortText -> Bool
forall a. IsNoName a => a -> Bool
isNoName ShortText
s then ShortText
"x" else ShortText -> ShortText
argNameToString ShortText
s

    loop :: Telescope -> m (Nat, Context -> Context)
loop Telescope
EmptyTel = (Nat, Context -> Context) -> m (Nat, Context -> Context)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Nat
0, Context -> Context
forall a. a -> a
id)
    loop (ExtendTel Dom Type
dom Abs Telescope
tel) = ShortText
-> (Name -> m (Nat, Context -> Context))
-> m (Nat, Context -> Context)
forall (m :: * -> *) a.
MonadAddContext m =>
ShortText -> (Name -> m a) -> m a
withFreshName_ (ShortText -> ShortText
realName (ShortText -> ShortText) -> ShortText -> ShortText
forall a b. (a -> b) -> a -> b
$ Abs Telescope -> ShortText
forall a. Abs a -> ShortText
absName Abs Telescope
tel) \Name
nms -> do
      (!n, !ext) <- Telescope -> m (Nat, Context -> Context)
loop (Abs Telescope -> Telescope
forall a. Abs a -> a
unAbs Abs Telescope
tel)
      let !nm = Name -> Name
wrap Name
nms
      pure $ (n + 1, ext . CxExtendVar nm dom)

  (!n, !tel) <- Telescope -> m (Nat, Context -> Context)
loop Telescope
tele
  pure $! (, tel) $! raiseS n
{-# SPECIALIZE addContextTele :: (Name -> Name) -> Telescope -> TCM (Substitution, Context -> Context) #-}

instance AddContext (KeepNames Telescope) where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
KeepNames Telescope -> m a -> m a
addContext (KeepNames Telescope
tel) m a
ret = do
    (sub, tel) <- (Name -> Name)
-> Telescope -> m (Substitution' Term, Context -> Context)
forall (m :: * -> *).
MonadAddContext m =>
(Name -> Name)
-> Telescope -> m (Substitution' Term, Context -> Context)
addContextTele Name -> Name
forall a. a -> a
id Telescope
tel
    updateContext sub tel ret

instance AddContext Telescope where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel m a
ret = do
    (sub, tel) <- (Name -> Name)
-> Telescope -> m (Substitution' Term, Context -> Context)
forall (m :: * -> *).
MonadAddContext m =>
(Name -> Name)
-> Telescope -> m (Substitution' Term, Context -> Context)
addContextTele Name -> Name
forall a. LensInScope a => a -> a
setNotInScope Telescope
tel
    updateContext sub tel ret

{-# NOINLINE extendReduceEnv #-}
extendReduceEnv :: ShortText -> Dom Type -> ReduceEnv -> ReduceEnv
extendReduceEnv :: ShortText -> Dom Type -> ReduceEnv -> ReduceEnv
extendReduceEnv ShortText
x !Dom Type
a !ReduceEnv
env =
  let !tcs :: TCState
tcs          = ReduceEnv -> TCState
redSt ReduceEnv
env
      (!NameId
nid, !TCState
tcs') = TCState -> (NameId, TCState)
forall i. HasFresh i => TCState -> (i, TCState)
nextFresh TCState
tcs
      ~Name
n            = let x' :: ShortText
x' = case ShortText
x of ShortText
"" -> ShortText
"x"; ShortText
_ -> ShortText
x
                          cn :: Name
cn = Range -> NameInScope -> NameParts -> Name
C.Name Range
forall a. Range' a
noRange NameInScope
InScope (ShortText -> NameParts
C.stringNameParts ShortText
x')
                      in NameId -> Name -> Name -> Range -> Fixity' -> Bool -> Name
Name NameId
nid Name
cn Name
cn Range
forall a. Range' a
noRange Fixity'
noFixity' Bool
False
      !re :: TCEnv
re           = ReduceEnv -> TCEnv
redEnv ReduceEnv
env
      !ec :: Context
ec           = TCEnv
re TCEnv -> Getting Context TCEnv Context -> Context
forall s a. s -> Getting a s a -> a
^. Getting Context TCEnv Context
Lens' TCEnv Context
eContext
      !ec' :: Context
ec'          = Name -> Dom Type -> Context -> Context
CxExtendVar Name
n Dom Type
a Context
ec
      !re' :: TCEnv
re'          = TCEnv
re TCEnv -> (TCEnv -> TCEnv) -> TCEnv
forall a b. a -> (a -> b) -> b
& ASetter TCEnv TCEnv Context Context
Lens' TCEnv Context
eContext ASetter TCEnv TCEnv Context Context -> Context -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Context
ec'
  in ReduceEnv
env {redEnv = re', redSt = tcs'}

{-# INLINE underAbsReduceM #-}
-- | Go under an abstraction in 'ReduceM'. This performs the minimal adjustment to make 'reduce'
--   work, which is to extend the local 'Context' with a name and a type.
underAbsReduceM :: Dom Type -> Abs a -> (a -> ReduceM b) -> ReduceM b
underAbsReduceM :: forall a b. Dom Type -> Abs a -> (a -> ReduceM b) -> ReduceM b
underAbsReduceM Dom Type
a Abs a
t a -> ReduceM b
k = (ReduceEnv -> b) -> ReduceM b
forall a. (ReduceEnv -> a) -> ReduceM a
ReduceM \ReduceEnv
env -> case Abs a
t of
  Abs   ShortText
x a
t -> ReduceM b -> ReduceEnv -> b
forall a. ReduceM a -> ReduceEnv -> a
unReduceM (a -> ReduceM b
k a
t) (ReduceEnv -> b) -> ReduceEnv -> b
forall a b. (a -> b) -> a -> b
$! ShortText -> Dom Type -> ReduceEnv -> ReduceEnv
extendReduceEnv ShortText
x Dom Type
a ReduceEnv
env
  NoAbs ShortText
_ a
t -> ReduceM b -> ReduceEnv -> b
forall a. ReduceM a -> ReduceEnv -> a
unReduceM (a -> ReduceM b
k a
t) ReduceEnv
env

{-# INLINE underAbsReduceM_ #-}
-- | Go under an abstraction in 'ReduceM' while adding a dummy type to the context.
underAbsReduceM_ :: Abs a -> (a -> ReduceM b) -> ReduceM b
underAbsReduceM_ :: forall a b. Abs a -> (a -> ReduceM b) -> ReduceM b
underAbsReduceM_ = Dom Type -> Abs a -> (a -> ReduceM b) -> ReduceM b
forall a b. Dom Type -> Abs a -> (a -> ReduceM b) -> ReduceM b
underAbsReduceM Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__

-- | Go under an abstraction.  Do not extend context in case of 'NoAbs'.
{-# INLINE underAbstraction  #-}
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 = (ShortText -> ShortText) -> Dom Type -> Abs a -> (a -> m b) -> m b
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
(ShortText -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' ShortText -> ShortText
forall a. a -> a
id

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

{-# INLINE underAbstractionAbs #-}
-- | 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 = (ShortText -> ShortText) -> Dom Type -> Abs a -> (a -> m b) -> m b
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
(ShortText -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs' ShortText -> ShortText
forall a. a -> a
id

{-# INLINE underAbstractionAbs' #-}
underAbstractionAbs'
  :: (Subst a, MonadAddContext m, AddContext (name, Dom Type))
  => (ShortText -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs' :: forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
(ShortText -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs' ShortText -> 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 (ShortText -> name
wrap (ShortText -> name) -> ShortText -> name
forall a b. (a -> b) -> a -> b
$ ShortText -> ShortText
realName (ShortText -> ShortText) -> ShortText -> ShortText
forall a b. (a -> b) -> a -> b
$ Abs a -> ShortText
forall a. Abs a -> ShortText
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 :: ShortText -> ShortText
realName ShortText
s = if ShortText -> Bool
forall a. IsNoName a => a -> Bool
isNoName ShortText
s then ShortText
"x" else ShortText -> ShortText
argNameToString ShortText
s

-- | Go under an abstract without worrying about the type to add to the context.
{-# INLINE underAbstraction_  #-}
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__

{-# INLINE mapAbstraction #-}
-- | Map a monadic function on the thing under the abstraction, adding
--   the abstracted variable to the context.
mapAbstraction
  :: (Subst a, MonadAddContext m)
  => Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction :: forall a (m :: * -> *) b.
(Subst a, 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, MonadAddContext m)
  => (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction_ :: forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
(a -> m b) -> Abs a -> m (Abs b)
mapAbstraction_ = Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
forall a (m :: * -> *) b.
(Subst a, 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
  bs <- Lens' TCEnv (Map Name (Open LetBinding))
-> tcm (Map Name (Open LetBinding))
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Map Name (Open LetBinding) -> f (Map Name (Open LetBinding)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map Name (Open LetBinding))
eLetBindings
  forM (Map.toList bs) $ \ (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.
{-# INLINE defaultAddLetBinding' #-}
defaultAddLetBinding' :: (ReadTCState m, MonadTCEnv m)
  => IsAxiom   -- ^ Does this let binding come from a 'LetAxiom'?
  -> Origin -> Name -> Term -> Dom Type -> m a -> m a
defaultAddLetBinding' :: forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a
defaultAddLetBinding' IsAxiom
isAxiom Origin
o Name
x Term
v Dom Type
t m a
ret = do
    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
$ IsAxiom -> Origin -> Term -> Dom Type -> LetBinding
LetBinding IsAxiom
isAxiom Origin
o Term
v Dom Type
t
    localTC (over eLetBindings (Map.insert x vt)) ret

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

-- | Add a let bound variable without a definition.
{-# INLINE addLetAxiom #-}
addLetAxiom :: (MonadWarning m) => ArgInfo -> Origin -> Name -> Term -> Type -> m a -> m a
addLetAxiom :: forall (m :: * -> *) a.
MonadWarning m =>
ArgInfo -> Origin -> Name -> Term -> Type -> m a -> m a
addLetAxiom ArgInfo
info Origin
o Name
x Term
v Type
t0 m a
ret =
  IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a
forall a.
IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a
addLetBinding' IsAxiom
YesAxiom Origin
o Name
x Term
v (ArgInfo -> Type -> Dom Type
forall a t. ArgInfo -> a -> Dom' t a
defaultArgDom ArgInfo
info Type
t0) m a
ret

{-# INLINE removeLetBinding #-}
-- | 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 (ASetter
  TCEnv
  TCEnv
  (Map Name (Open LetBinding))
  (Map Name (Open LetBinding))
-> (Map Name (Open LetBinding) -> Map Name (Open LetBinding))
-> TCEnv
-> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  TCEnv
  TCEnv
  (Map Name (Open LetBinding))
  (Map Name (Open LetBinding))
Lens' TCEnv (Map Name (Open LetBinding))
eLetBindings (Name -> Map Name (Open LetBinding) -> Map Name (Open LetBinding)
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Name
x))

{-# INLINE removeLetBindingsFrom #-}
-- | 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 (ASetter
  TCEnv
  TCEnv
  (Map Name (Open LetBinding))
  (Map Name (Open LetBinding))
-> (Map Name (Open LetBinding) -> Map Name (Open LetBinding))
-> TCEnv
-> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  TCEnv
  TCEnv
  (Map Name (Open LetBinding))
  (Map Name (Open LetBinding))
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
fst ((Map Name (Open LetBinding), Map Name (Open LetBinding))
 -> Map Name (Open LetBinding))
-> (Map Name (Open LetBinding)
    -> (Map Name (Open LetBinding), Map Name (Open LetBinding)))
-> Map Name (Open LetBinding)
-> Map Name (Open LetBinding)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name
-> Map Name (Open LetBinding)
-> (Map Name (Open LetBinding), Map Name (Open LetBinding))
forall k a. Ord k => k -> Map k a -> (Map k a, Map k a)
Map.split Name
x))

-- * Querying the context

-- | Get the current context.
{-# SPECIALIZE getContext :: TCM Context #-}
getContext :: MonadTCEnv m => m Context
getContext :: forall (m :: * -> *). MonadTCEnv m => m Context
getContext = Lens' TCEnv Context -> m Context
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Context -> f Context) -> TCEnv -> f TCEnv
Lens' TCEnv Context
eContext

-- | Get the size of the current context.
{-# SPECIALIZE getContextSize :: TCM Nat #-}
getContextSize :: (MonadTCEnv m) => m Nat
getContextSize :: forall (m :: * -> *). MonadTCEnv m => m Nat
getContextSize = Context -> Nat
forall a. Sized a => a -> Nat
size (Context -> Nat) -> m Context -> m Nat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext

{-# SPECIALIZE getContextVars :: TCM [(Int, Dom Name)] #-}
getContextVars :: (MonadTCEnv m) => m [(Int, Dom Name)]
getContextVars :: forall (m :: * -> *). MonadTCEnv m => m [(Nat, Dom' Term Name)]
getContextVars = Context -> [(Nat, Dom' Term Name)]
contextVars (Context -> [(Nat, Dom' Term Name)])
-> m Context -> m [(Nat, Dom' Term Name)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext

{-# SPECIALIZE getContextVars' :: TCM [(Int, Dom Name)] #-}
getContextVars' :: (MonadTCEnv m) => m [(Int, Dom Name)]
getContextVars' :: forall (m :: * -> *). MonadTCEnv m => m [(Nat, Dom' Term Name)]
getContextVars' = Context -> [(Nat, Dom' Term Name)]
contextVars' (Context -> [(Nat, Dom' Term Name)])
-> m Context -> m [(Nat, Dom' Term Name)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext

contextVars :: Context -> [(Int, Dom Name)]
contextVars :: Context -> [(Nat, Dom' Term Name)]
contextVars = [(Nat, Dom' Term Name)] -> [(Nat, Dom' Term Name)]
forall a. [a] -> [a]
reverse ([(Nat, Dom' Term Name)] -> [(Nat, Dom' Term Name)])
-> (Context -> [(Nat, Dom' Term Name)])
-> Context
-> [(Nat, Dom' Term Name)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> [(Nat, Dom' Term Name)]
contextVars'

contextVars' :: Context -> [(Int, Dom Name)]
contextVars' :: Context -> [(Nat, Dom' Term Name)]
contextVars' = (Nat -> ContextEntry -> (Nat, Dom' Term Name))
-> Context -> [(Nat, Dom' Term Name)]
forall a. (Nat -> ContextEntry -> a) -> Context -> [a]
cxWithIndex Nat -> ContextEntry -> (Nat, Dom' Term Name)
forall {a}. a -> ContextEntry -> (a, Dom' Term Name)
mkVar
  where
    mkVar :: a -> ContextEntry -> (a, Dom' Term Name)
mkVar a
i (CtxVar Name
x Dom Type
a) = (a
i, Dom Type
a Dom Type -> Name -> Dom' Term Name
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Name
x)

-- | Generate @[var (n - 1), ..., var 0]@ for all bound variables in the context.
{-# SPECIALIZE getContextArgs :: TCM Args #-}
getContextArgs :: (MonadTCEnv m) => m Args
getContextArgs :: forall (m :: * -> *). MonadTCEnv m => m Args
getContextArgs = Context -> Args
contextArgs (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

contextArgs :: Context -> Args
contextArgs :: Context -> Args
contextArgs = ((Nat, Dom' Term Name) -> Arg Term)
-> [(Nat, Dom' Term Name)] -> Args
forall a b. (a -> b) -> [a] -> [b]
map' (\(Nat
i,Dom' Term Name
x) -> Nat -> Term
var Nat
i Term -> Arg Name -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom' Term Name -> Arg Name
forall t a. Dom' t a -> Arg a
argFromDom Dom' Term Name
x) ([(Nat, Dom' Term Name)] -> Args)
-> (Context -> [(Nat, Dom' Term Name)]) -> Context -> Args
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> [(Nat, Dom' Term Name)]
contextVars

-- | Generate @[var (n - 1), ..., var 0]@ for all declarations in the context.
{-# SPECIALIZE getContextTerms :: TCM [Term] #-}
getContextTerms :: (MonadTCEnv m) => m [Term]
getContextTerms :: forall (m :: * -> *). MonadTCEnv m => m [Term]
getContextTerms = (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Term
forall e. Arg e -> e
unArg (Args -> [Term]) -> m Args -> m [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Args
forall (m :: * -> *). MonadTCEnv m => m Args
getContextArgs

contextTerms :: Context -> [Term]
contextTerms :: Context -> [Term]
contextTerms = (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Term
forall e. Arg e -> e
unArg (Args -> [Term]) -> (Context -> Args) -> Context -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Args
contextArgs

-- | Get the current context as a 'Telescope'.
{-# SPECIALIZE getContextTelescope :: TCM Telescope #-}
getContextTelescope :: (MonadTCEnv m) => m Telescope
getContextTelescope :: forall (m :: * -> *). MonadTCEnv m => m Telescope
getContextTelescope = Context -> Telescope
contextToTel (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

contextToTel :: Context -> Telescope
contextToTel :: Context -> Telescope
contextToTel = Telescope -> Context -> Telescope
go Telescope
forall a. Tele a
EmptyTel
  where
    go :: Telescope -> Context -> Telescope
go !Telescope
tel Context
CxEmpty              = Telescope
tel
    go Telescope
tel (CxExtendVar Name
x Dom Type
a Context
ctx) = let !x' :: ShortText
x' = Name -> ShortText
nameToArgName Name
x
                                   in Telescope -> Context -> Telescope
go (Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (ShortText -> Telescope -> Abs Telescope
forall a. ShortText -> a -> Abs a
Abs ShortText
x' Telescope
tel)) Context
ctx

-- | Get the names of all declarations in the context.
{-# SPECIALIZE getContextNames :: TCM [Name] #-}
getContextNames :: (MonadTCEnv m) => m [Name]
getContextNames :: forall (m :: * -> *). MonadTCEnv m => m [Name]
getContextNames = Context -> [Name]
contextNames (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

{-# SPECIALIZE getContextNames' :: TCM [Name] #-}
getContextNames' :: (MonadTCEnv m) => m [Name]
getContextNames' :: forall (m :: * -> *). MonadTCEnv m => m [Name]
getContextNames' = Context -> [Name]
contextNames' (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

contextNames :: Context -> [Name]
contextNames :: Context -> [Name]
contextNames = ((Nat, Dom' Term Name) -> Name)
-> [(Nat, Dom' Term Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map' (Dom' Term Name -> Name
forall t e. Dom' t e -> e
unDom (Dom' Term Name -> Name)
-> ((Nat, Dom' Term Name) -> Dom' Term Name)
-> (Nat, Dom' Term Name)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Nat, Dom' Term Name) -> Dom' Term Name
forall a b. (a, b) -> b
snd) ([(Nat, Dom' Term Name)] -> [Name])
-> (Context -> [(Nat, Dom' Term Name)]) -> Context -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> [(Nat, Dom' Term Name)]
contextVars

contextNames' :: Context -> [Name]
contextNames' :: Context -> [Name]
contextNames' = ((Nat, Dom' Term Name) -> Name)
-> [(Nat, Dom' Term Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map' (Dom' Term Name -> Name
forall t e. Dom' t e -> e
unDom (Dom' Term Name -> Name)
-> ((Nat, Dom' Term Name) -> Dom' Term Name)
-> (Nat, Dom' Term Name)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Nat, Dom' Term Name) -> Dom' Term Name
forall a b. (a, b) -> b
snd) ([(Nat, Dom' Term Name)] -> [Name])
-> (Context -> [(Nat, Dom' Term Name)]) -> Context -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> [(Nat, Dom' Term Name)]
contextVars'

-- | 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
<$> Nat -> Context -> Maybe ContextEntry
cxLookup Nat
n Context
ctx

{-# 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 ContextEntry #-}
lookupBV :: (MonadDebug m, MonadTCEnv m) => Nat -> m ContextEntry
lookupBV :: forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Nat -> m ContextEntry
lookupBV Nat
n = do
  let failure :: m ContextEntry
failure = do
        ctx <- m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
        __IMPOSSIBLE_VERBOSE__ $ unwords
          [ "de Bruijn index out of scope:", show n
          , "in context", prettyShow $ map' ctxEntryName $ cxEntries ctx
          ]
  m (Maybe ContextEntry)
-> m ContextEntry
-> (ContextEntry -> m ContextEntry)
-> m ContextEntry
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Nat -> m (Maybe ContextEntry)
forall (m :: * -> *). MonadTCEnv m => Nat -> m (Maybe ContextEntry)
lookupBV' Nat
n) m ContextEntry
failure ContextEntry -> m ContextEntry
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

ctxEntryName :: ContextEntry -> Name
ctxEntryName :: ContextEntry -> Name
ctxEntryName (CtxVar Name
x Dom Type
_) = Name
x

ctxEntryDom :: ContextEntry -> Dom Type
ctxEntryDom :: ContextEntry -> Dom Type
ctxEntryDom (CtxVar Name
_ Dom Type
a) = Dom Type
a

ctxEntryType :: ContextEntry -> Type
ctxEntryType :: ContextEntry -> Type
ctxEntryType = Dom Type -> Type
forall t e. Dom' t e -> e
unDom (Dom Type -> Type)
-> (ContextEntry -> Dom Type) -> ContextEntry -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> Dom Type
ctxEntryDom

{-# SPECIALIZE domOfBV :: Nat -> TCM (Dom Type) #-}
domOfBV :: (MonadDebug m, MonadTCEnv m) => Nat -> m (Dom Type)
domOfBV :: forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Nat -> m (Dom Type)
domOfBV Nat
n = ContextEntry -> Dom Type
ctxEntryDom (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 :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Nat -> m ContextEntry
lookupBV Nat
n

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

{-# SPECIALIZE nameOfBV' :: Nat -> TCM (Maybe Name) #-}
nameOfBV' :: (MonadTCEnv m) => Nat -> m (Maybe Name)
nameOfBV' :: forall (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 ContextEntry -> Name
ctxEntryName (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 :: (MonadDebug m, MonadTCEnv m) => Nat -> m Name
nameOfBV :: forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Nat -> m Name
nameOfBV Nat
n = ContextEntry -> Name
ctxEntryName (ContextEntry -> Name) -> m ContextEntry -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat -> m ContextEntry
forall (m :: * -> *).
(MonadDebug 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 :: (MonadDebug m, MonadFail m, MonadTCEnv m) => Name -> m (Term, Dom Type)
getVarInfo :: forall (m :: * -> *).
(MonadDebug m, MonadFail m, MonadTCEnv m) =>
Name -> m (Term, Dom Type)
getVarInfo Name
x =
    do  ctx <- m [(Nat, Dom' Term Name)]
forall (m :: * -> *). MonadTCEnv m => m [(Nat, Dom' Term Name)]
getContextVars'
        def <- viewTC eLetBindings
        case List.findIndex ((== x) . unDom . snd) ctx of
            Just Nat
n -> do
                t <- Nat -> m (Dom Type)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Nat -> m (Dom Type)
domOfBV Nat
n
                return (var n, 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 _isAxiom _origin v t <- Open LetBinding -> m LetBinding
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen Open LetBinding
vt
                      return (v, 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] -> String
unwords
                      [ String
"unbound variable"
                      , Name -> String
forall a. Pretty a => a -> String
prettyShow (Name -> String) -> Name -> String
forall a b. (a -> b) -> a -> b
$ Name -> Name
nameConcrete Name
x
                      , String
"(id: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ NameId -> String
forall a. Pretty a => a -> String
prettyShow (Name -> NameId
forall a. HasNameId a => a -> NameId
nameId Name
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                      ]
                      -- Andreas, 2026-01-20, issue #8325
                      -- This 'fail' is apparently not impossible;
                      -- it is apparently caught during a "refine".
                      -- TODO: It would be worthwhile investigating who wants to access
                      -- an out-of-scope variable.