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

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 )

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

import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty
import Agda.Syntax.Concrete.Name (NameInScope(..), LensInScope(..), nameRoot, nameToRawName)
import Agda.Syntax.Concrete.Name qualified as C
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.TypeChecking.Warnings (warning, MonadWarning)

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


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

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 (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
$ Lens' TCEnv LocalRewriteRuleMap
-> (LocalRewriteRuleMap -> LocalRewriteRuleMap) -> tcm a -> tcm a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (LocalRewriteRuleMap -> f LocalRewriteRuleMap) -> TCEnv -> f TCEnv
Lens' TCEnv LocalRewriteRuleMap
eLocalRewriteRules (LocalRewriteRuleMap -> LocalRewriteRuleMap -> LocalRewriteRuleMap
forall a b. a -> b -> a
const LocalRewriteRuleMap
forall a. Null a => a
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!
--   Also updates head symbols of local rewrite rules with variable heads
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))
                . over eLocalRewriteRules (updateLocalRewriteHeads 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

-- | Update heads of local rewrite rules for the new context
updateLocalRewriteHeads ::
  Substitution -> LocalRewriteRuleMap -> LocalRewriteRuleMap
updateLocalRewriteHeads :: Substitution' Term -> LocalRewriteRuleMap -> LocalRewriteRuleMap
updateLocalRewriteHeads Substitution' Term
sub = ASetter
  LocalRewriteRuleMap
  LocalRewriteRuleMap
  (IntMap [Open RewriteRule])
  (IntMap [Open RewriteRule])
-> (IntMap [Open RewriteRule] -> IntMap [Open RewriteRule])
-> LocalRewriteRuleMap
-> LocalRewriteRuleMap
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  LocalRewriteRuleMap
  LocalRewriteRuleMap
  (IntMap [Open RewriteRule])
  (IntMap [Open RewriteRule])
Lens' LocalRewriteRuleMap (IntMap [Open RewriteRule])
lrewsVarHeaded ((Nat -> Nat)
-> IntMap [Open RewriteRule] -> IntMap [Open RewriteRule]
forall a. (Nat -> Nat) -> IntMap a -> IntMap a
IntMap.mapKeys Nat -> Nat
subHead)
  where
    subHead :: Nat -> Nat
subHead Nat
x = Nat -> Maybe Nat -> Nat
forall a. a -> Maybe a -> a
fromMaybe Nat
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Nat -> Nat) -> Maybe Nat -> Nat
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> Nat -> Maybe Nat
forall a. EndoSubst a => Substitution' a -> Nat -> Maybe Nat
lookupSVar Substitution' Term
sub Nat
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 =
  Lens' TCState ModuleCheckpoints
-> (ModuleCheckpoints -> ModuleCheckpoints) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens' (ModuleCheckpoints -> f ModuleCheckpoints) -> TCState -> f TCState
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 =
  Lens' TCState ModuleCheckpoints
-> (ModuleCheckpoints -> ModuleCheckpoints) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens' (ModuleCheckpoints -> f ModuleCheckpoints) -> TCState -> f TCState
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.
  Lens' TCState ModuleCheckpoints
-> (ModuleCheckpoints -> ModuleCheckpoints) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens' (ModuleCheckpoints -> f ModuleCheckpoints) -> TCState -> f TCState
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
<$> Lens' TCState ModuleCheckpoints -> m ModuleCheckpoints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (ModuleCheckpoints -> f ModuleCheckpoints) -> TCState -> f TCState
Lens' 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

  -- | Adds a local rewrite rule to the context
  addLocalRewrite :: RewriteRule -> 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 addLocalRewrite
    :: (MonadAddContext n, MonadTransControl t, t n ~ m)
    => RewriteRule -> m a -> m a
  addLocalRewrite RewriteRule
r = (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
$ RewriteRule -> n (StT t a) -> n (StT t a)
forall a. RewriteRule -> n a -> n a
forall (m :: * -> *) a.
MonadAddContext m =>
RewriteRule -> m a -> m a
addLocalRewrite RewriteRule
r

  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
    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
    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 = Maybe (RewDom' Term) -> (RewDom' Term -> m a -> m a) -> m a -> m a
forall b a. Maybe b -> (b -> a -> a) -> a -> a
applyWhenJust (Dom Type -> Maybe (RewDom' Term)
forall t e. Dom' t e -> Maybe (RewDom' t)
rewDom Dom Type
a) RewDom' Term -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
RewDom' Term -> m a -> m a
addRewDom (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$
  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

addRewDom :: MonadAddContext m => RewDom -> m a -> m a
addRewDom :: forall (m :: * -> *) a.
MonadAddContext m =>
RewDom' Term -> m a -> m a
addRewDom RewDom' Term
rew = case RewDom' Term -> Maybe RewriteRule
forall t. RewDom' t -> Maybe RewriteRule
rewDomRew RewDom' Term
rew of
  Just RewriteRule
r  -> RewriteRule -> m a -> m a
forall a. RewriteRule -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
RewriteRule -> m a -> m a
addLocalRewrite RewriteRule
r
  Maybe RewriteRule
Nothing -> m a -> m a
forall a. HasCallStack => a
__IMPOSSIBLE__

{-# INLINE withFreshName_ #-}
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)
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
  addLocalRewrite :: forall a. RewriteRule -> ListT m a -> ListT m a
addLocalRewrite RewriteRule
r      = (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
$ RewriteRule -> m a1 -> m a1
forall a. RewriteRule -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
RewriteRule -> m a -> m a
addLocalRewrite RewriteRule
r
  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 = TCM b
f
-- withShadowingNameTCM x = \f -> do
--   reportS "tc.cxt.shadowing" 80 $ "registered" <+> pretty x <+> "for shadowing"
--   when (isInScope x == InScope) $ tellUsedName x
--   (result , useds) <- listenUsedNames f
--   reportSLn "tc.cxt.shadowing" 90 $ "all used names: " ++ show useds
--   tellShadowing x useds
--   return result

--     where
--       listenUsedNames f = do
--         Lazy origUsedNames <- useTC stUsedNames
--         setTCLens stUsedNames (Lazy Map.empty)
--         result <- f
--         Lazy newUsedNames <- useTC stUsedNames
--         setTCLens stUsedNames $ Lazy (Map.unionWith (<>) origUsedNames newUsedNames)
--         return (result , newUsedNames)

--       tellUsedName x = do
--         let concreteX = nameConcrete x
--             rawX      = nameToRawName concreteX
--             rootX     = nameRoot concreteX
--         modifyTCLens stUsedNames \(Lazy ns) ->
--           Lazy (ns & key rootX %~ Just . Set1.insertSet rawX . Set1.toSet')

--       tellShadowing x useds = case Map.lookup (nameRoot $ nameConcrete x) useds of
--         Just shadows -> do
--           reportS "tc.cxt.shadowing" 80 $
--             "names shadowing" <+> pretty x <+> ": " <+>
--             prettyList_ (map' pretty $ toList shadows)
--           modifyTCLens stShadowingNames $ Lazy . Map.insertWith (<>) x shadows . unLazy
--         Nothing      -> return ()

-- {-# NOINLINE addCtxTEST #-}
-- addCtxTEST :: Name -> Dom Type -> TCM a -> TCM a
-- addCtxTEST x a ret = applyUnless (isNoName x) (withShadowingNameTCM x) $
--     defaultAddCtx x a ret

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

  {-# 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 = 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
$
    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 addLocalRewrite #-}
  addLocalRewrite :: forall a. RewriteRule -> TCM a -> TCM a
addLocalRewrite = RewriteRule -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
RewriteRule -> m a -> m a
defaultAddLocalRewrite

  {-# INLINE withFreshName #-}
  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

{-# INLINE defaultAddLocalRewrite #-}
-- | Adds a rewrite rule to the local typechecking environment
defaultAddLocalRewrite :: (MonadTCEnv m, ReadTCState m)
  => RewriteRule -> m a -> m a
defaultAddLocalRewrite :: forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
RewriteRule -> m a -> m a
defaultAddLocalRewrite RewriteRule
rew m a
ret = do
  rew' <- RewriteRule -> m (Open RewriteRule)
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
a -> m (Open a)
makeOpen RewriteRule
rew
  case rewHead rew of
    RewVarHead Nat
x -> Lens' TCEnv (IntMap [Open RewriteRule])
-> (IntMap [Open RewriteRule] -> IntMap [Open RewriteRule])
-> m a
-> m a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC ((LocalRewriteRuleMap -> f LocalRewriteRuleMap) -> TCEnv -> f TCEnv
Lens' TCEnv LocalRewriteRuleMap
eLocalRewriteRules ((LocalRewriteRuleMap -> f LocalRewriteRuleMap)
 -> TCEnv -> f TCEnv)
-> ((IntMap [Open RewriteRule] -> f (IntMap [Open RewriteRule]))
    -> LocalRewriteRuleMap -> f LocalRewriteRuleMap)
-> (IntMap [Open RewriteRule] -> f (IntMap [Open RewriteRule]))
-> TCEnv
-> f TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IntMap [Open RewriteRule] -> f (IntMap [Open RewriteRule]))
-> LocalRewriteRuleMap -> f LocalRewriteRuleMap
Lens' LocalRewriteRuleMap (IntMap [Open RewriteRule])
lrewsVarHeaded)
      (([Open RewriteRule] -> [Open RewriteRule] -> [Open RewriteRule])
-> Nat
-> [Open RewriteRule]
-> IntMap [Open RewriteRule]
-> IntMap [Open RewriteRule]
forall a. (a -> a -> a) -> Nat -> a -> IntMap a -> IntMap a
IntMap.insertWith [Open RewriteRule] -> [Open RewriteRule] -> [Open RewriteRule]
forall a. Monoid a => a -> a -> a
mappend Nat
x [Open RewriteRule
rew']) m a
ret
    RewDefHead QName
f -> Lens' TCEnv (HashMap QName [Open RewriteRule])
-> (HashMap QName [Open RewriteRule]
    -> HashMap QName [Open RewriteRule])
-> m a
-> m a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC ((LocalRewriteRuleMap -> f LocalRewriteRuleMap) -> TCEnv -> f TCEnv
Lens' TCEnv LocalRewriteRuleMap
eLocalRewriteRules ((LocalRewriteRuleMap -> f LocalRewriteRuleMap)
 -> TCEnv -> f TCEnv)
-> ((HashMap QName [Open RewriteRule]
     -> f (HashMap QName [Open RewriteRule]))
    -> LocalRewriteRuleMap -> f LocalRewriteRuleMap)
-> (HashMap QName [Open RewriteRule]
    -> f (HashMap QName [Open RewriteRule]))
-> TCEnv
-> f TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HashMap QName [Open RewriteRule]
 -> f (HashMap QName [Open RewriteRule]))
-> LocalRewriteRuleMap -> f LocalRewriteRuleMap
Lens' LocalRewriteRuleMap (HashMap QName [Open RewriteRule])
lrewsDefHeaded)
      (([Open RewriteRule] -> [Open RewriteRule] -> [Open RewriteRule])
-> QName
-> [Open RewriteRule]
-> HashMap QName [Open RewriteRule]
-> HashMap QName [Open RewriteRule]
forall k v.
Hashable k =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
HMap.insertWith [Open RewriteRule] -> [Open RewriteRule] -> [Open RewriteRule]
forall a. Monoid a => a -> a -> a
mappend QName
f [Open RewriteRule
rew']) m a
ret

{-# 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
  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 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 #-}
  contextSize :: Context -> Nat
contextSize = Context -> Nat
forall a. Sized a => a -> Nat
size

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 #-}
  contextSize :: ContextEntry -> Nat
contextSize ContextEntry
_ = Nat
1

instance AddContext (Name, Dom Type) where
  {-# INLINE addContext #-}
  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;
  contextSize :: (Name, Dom Type) -> Nat
contextSize (Name, Dom Type)
_ = Nat
1

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

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

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

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

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

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

instance AddContext (Dom Type) where
  {-# INLINE addContext #-}
  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
  {-# 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__)
  contextSize :: Name -> Nat
contextSize Name
_ = Nat
1

instance {-# OVERLAPPING #-} AddContext String where
  {-# INLINE addContext #-}
  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
  {-# INLINE addContext #-}
  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
  {-# INLINE addContext #-}
  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 #-}

{-# NOINLINE extendReduceEnv #-}
extendReduceEnv :: String -> Dom Type -> ReduceEnv -> ReduceEnv
extendReduceEnv :: String -> Dom Type -> ReduceEnv -> ReduceEnv
extendReduceEnv String
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' :: String
x' = case String
x of String
"" -> String
"x"; String
_ -> String
x
                          cn :: Name
cn = Range -> NameInScope -> NameParts -> Name
C.Name Range
forall a. Range' a
noRange NameInScope
InScope (String -> NameParts
C.stringNameParts String
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   String
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
$! String -> Dom Type -> ReduceEnv -> ReduceEnv
extendReduceEnv String
x Dom Type
a ReduceEnv
env
  NoAbs String
_ 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 = (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

{-# INLINE underAbstraction' #-}
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

{-# 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 = (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

{-# INLINE underAbstractionAbs' #-}
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.
{-# 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

unsafeRule :: (MonadWarning m) => RewriteSource -> IllegalRewriteRuleReason -> MaybeT m ()
unsafeRule :: forall (m :: * -> *).
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m ()
unsafeRule RewriteSource
s IllegalRewriteRuleReason
reason = m () -> MaybeT m ()
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> MaybeT m ()) -> m () -> MaybeT m ()
forall a b. (a -> b) -> a -> b
$ Warning -> m ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> m ()) -> Warning -> m ()
forall a b. (a -> b) -> a -> b
$ RewriteSource -> IllegalRewriteRuleReason -> Warning
IllegalRewriteRule RewriteSource
s IllegalRewriteRuleReason
reason

illegalRule :: (MonadWarning m) => RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule :: forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule RewriteSource
s IllegalRewriteRuleReason
reason = do
  RewriteSource -> IllegalRewriteRuleReason -> MaybeT m ()
forall (m :: * -> *).
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m ()
unsafeRule RewriteSource
s IllegalRewriteRuleReason
reason
  MaybeT m a
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

-- | 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. ArgInfo -> a -> Dom 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. ArgInfo -> a -> Dom 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 Name)]
getContextVars = Context -> [(Nat, Dom Name)]
contextVars (Context -> [(Nat, Dom Name)]) -> m Context -> m [(Nat, Dom 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 Name)]
getContextVars' = Context -> [(Nat, Dom Name)]
contextVars' (Context -> [(Nat, Dom Name)]) -> m Context -> m [(Nat, Dom 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 Name)]
contextVars = [(Nat, Dom Name)] -> [(Nat, Dom Name)]
forall a. [a] -> [a]
reverse ([(Nat, Dom Name)] -> [(Nat, Dom Name)])
-> (Context -> [(Nat, Dom Name)]) -> Context -> [(Nat, Dom Name)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> [(Nat, Dom Name)]
contextVars'

contextVars' :: Context -> [(Int, Dom Name)]
contextVars' :: Context -> [(Nat, Dom Name)]
contextVars' = (Nat -> ContextEntry -> (Nat, Dom Name))
-> Context -> [(Nat, Dom Name)]
forall a. (Nat -> ContextEntry -> a) -> Context -> [a]
cxWithIndex Nat -> ContextEntry -> (Nat, Dom Name)
forall {a}. a -> ContextEntry -> (a, Dom Name)
mkVar
  where
    mkVar :: a -> ContextEntry -> (a, Dom Name)
mkVar a
i (CtxVar Name
x Dom Type
a) = (a
i, Dom Type
a Dom Type -> Name -> Dom 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 Name) -> Arg Term) -> [(Nat, Dom Name)] -> Args
forall a b. (a -> b) -> [a] -> [b]
map' (\(Nat
i,Dom 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 Name -> Arg Name
forall t a. Dom' t a -> Arg a
argFromDom Dom Name
x) ([(Nat, Dom Name)] -> Args)
-> (Context -> [(Nat, Dom Name)]) -> Context -> Args
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> [(Nat, Dom 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' :: String
x' = Name -> String
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 (String -> Telescope -> Abs Telescope
forall a. String -> a -> Abs a
Abs String
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 Name) -> Name) -> [(Nat, Dom Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map' (Dom Name -> Name
forall t e. Dom' t e -> e
unDom (Dom Name -> Name)
-> ((Nat, Dom Name) -> Dom Name) -> (Nat, Dom Name) -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Nat, Dom Name) -> Dom Name
forall a b. (a, b) -> b
snd) ([(Nat, Dom Name)] -> [Name])
-> (Context -> [(Nat, Dom Name)]) -> Context -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> [(Nat, Dom Name)]
contextVars

contextNames' :: Context -> [Name]
contextNames' :: Context -> [Name]
contextNames' = ((Nat, Dom Name) -> Name) -> [(Nat, Dom Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map' (Dom Name -> Name
forall t e. Dom' t e -> e
unDom (Dom Name -> Name)
-> ((Nat, Dom Name) -> Dom Name) -> (Nat, Dom Name) -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Nat, Dom Name) -> Dom Name
forall a b. (a, b) -> b
snd) ([(Nat, Dom Name)] -> [Name])
-> (Context -> [(Nat, Dom Name)]) -> Context -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> [(Nat, Dom 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 Name)]
forall (m :: * -> *). MonadTCEnv m => m [(Nat, Dom 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.