-- {-# 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' ContextEntry -> Context' ContextEntry) -> tcm a -> tcm a
unsafeModifyContext Context' ContextEntry -> Context' ContextEntry
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' ContextEntry) (Context' ContextEntry)
-> (Context' ContextEntry -> Context' ContextEntry)
-> TCEnv
-> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv (Context' ContextEntry) (Context' ContextEntry)
Lens' TCEnv (Context' ContextEntry)
eContext Context' ContextEntry -> Context' ContextEntry
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' ContextEntry -> Context' ContextEntry) -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context' ContextEntry -> Context' ContextEntry) -> tcm a -> tcm a
unsafeModifyContext ((Context' ContextEntry -> Context' ContextEntry)
 -> tcm a -> tcm a)
-> (Context' ContextEntry -> Context' ContextEntry)
-> tcm a
-> tcm a
forall a b. (a -> b) -> a -> b
$ (ContextEntry -> ContextEntry)
-> Context' ContextEntry -> Context' ContextEntry
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' ContextEntry -> Context' ContextEntry)
-> (ContextEntry -> ContextEntry)
-> Context' ContextEntry
-> Context' ContextEntry
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' ContextEntry -> Context' ContextEntry) -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context' ContextEntry -> Context' ContextEntry) -> tcm a -> tcm a
unsafeModifyContext (Context' ContextEntry
-> Context' ContextEntry -> Context' ContextEntry
forall a b. a -> b -> a
const Context' ContextEntry
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' ContextEntry -> Context' ContextEntry) -> m a -> m a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context' ContextEntry -> Context' ContextEntry) -> tcm a -> tcm a
unsafeModifyContext (Context' ContextEntry
-> Context' ContextEntry -> Context' ContextEntry
forall a b. a -> b -> a
const Context' ContextEntry
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 => Int -> tcm a -> tcm a
unsafeEscapeContext Int
n = (Context' ContextEntry -> Context' ContextEntry) -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context' ContextEntry -> Context' ContextEntry) -> tcm a -> tcm a
unsafeModifyContext ((Context' ContextEntry -> Context' ContextEntry)
 -> tcm a -> tcm a)
-> (Context' ContextEntry -> Context' ContextEntry)
-> tcm a
-> tcm a
forall a b. (a -> b) -> a -> b
$ Int -> Context' ContextEntry -> Context' ContextEntry
cxDrop Int
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 -> Int -> m a -> m a
escapeContext Impossible
err Int
n = Substitution' Term
-> (Context' ContextEntry -> Context' ContextEntry) -> m a -> m a
forall a.
Substitution' Term
-> (Context' ContextEntry -> Context' ContextEntry) -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution' Term
-> (Context' ContextEntry -> Context' ContextEntry) -> m a -> m a
updateContext (Impossible -> Int -> Substitution' Term
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
err Int
n) ((Context' ContextEntry -> Context' ContextEntry) -> m a -> m a)
-> (Context' ContextEntry -> Context' ContextEntry) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Int -> Context' ContextEntry -> Context' ContextEntry
cxDrop Int
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
$ [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cxt.checkpoint" Int
105 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"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 ((Int -> Int)
-> IntMap [Open RewriteRule] -> IntMap [Open RewriteRule]
forall a. (Int -> Int) -> IntMap a -> IntMap a
IntMap.mapKeys Int -> Int
subHead)
  where
    subHead :: Int -> Int
subHead Int
x = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> Int -> Maybe Int
forall a. EndoSubst a => Substitution' a -> Int -> Maybe Int
lookupSVar Substitution' Term
sub Int
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' ContextEntry -> Context' ContextEntry
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' ContextEntry -> Context' ContextEntry)
-> n (StT t a)
-> n (StT t a)
forall a.
Substitution' Term
-> (Context' ContextEntry -> Context' ContextEntry) -> n a -> n a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution' Term
-> (Context' ContextEntry -> Context' ContextEntry) -> m a -> m a
updateContext Substitution' Term
sub Context' ContextEntry -> Context' ContextEntry
f

  default withFreshName
    :: (MonadAddContext n, MonadTransControl t, t n ~ m)
    => Range -> ArgName -> (Name -> m a) -> m a
  withFreshName Range
r [Char]
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 -> [Char] -> (Name -> n (StT t a)) -> n (StT t a)
forall a. Range -> [Char] -> (Name -> n a) -> n a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> [Char] -> (Name -> m a) -> m a
withFreshName Range
r [Char]
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' ContextEntry -> Context' ContextEntry) -> m a -> m a
forall a.
Substitution' Term
-> (Context' ContextEntry -> Context' ContextEntry) -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution' Term
-> (Context' ContextEntry -> Context' ContextEntry) -> m a -> m a
updateContext (Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS Int
1) (Name -> Dom Type -> Context' ContextEntry -> Context' ContextEntry
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 =>
[Char] -> (Name -> m a) -> m a
withFreshName_ = Range -> [Char] -> (Name -> m a) -> m a
forall a. Range -> [Char] -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> [Char] -> (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' ContextEntry -> Context' ContextEntry)
-> ListT m a
-> ListT m a
updateContext Substitution' Term
sub Context' ContextEntry -> Context' ContextEntry
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' ContextEntry -> Context' ContextEntry) -> m a1 -> m a1
forall a.
Substitution' Term
-> (Context' ContextEntry -> Context' ContextEntry) -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution' Term
-> (Context' ContextEntry -> Context' ContextEntry) -> m a -> m a
updateContext Substitution' Term
sub Context' ContextEntry -> Context' ContextEntry
f
  withFreshName :: forall a. Range -> [Char] -> (Name -> ListT m a) -> ListT m a
withFreshName Range
r [Char]
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
-> [Char]
-> (Name -> m (Maybe (a, ListT m a)))
-> m (Maybe (a, ListT m a))
forall a. Range -> [Char] -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> [Char] -> (Name -> m a) -> m a
withFreshName Range
r [Char]
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' ContextEntry -> Context' ContextEntry)
-> TCM a
-> TCM a
updateContext !Substitution' Term
sub !Context' ContextEntry -> Context' ContextEntry
f !TCM a
act = (Context' ContextEntry -> Context' ContextEntry) -> TCM a -> TCM a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context' ContextEntry -> Context' ContextEntry) -> tcm a -> tcm a
unsafeModifyContext Context' ContextEntry -> Context' ContextEntry
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 -> [Char] -> (Name -> TCM a) -> TCM a
withFreshName Range
r [Char]
x Name -> TCM a
m = Range -> [Char] -> TCMT IO Name
forall (m :: * -> *).
MonadFresh NameId m =>
Range -> [Char] -> m Name
freshName Range
r [Char]
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 Int
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])
-> Int
-> [Open RewriteRule]
-> IntMap [Open RewriteRule]
-> IntMap [Open RewriteRule]
forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
IntMap.insertWith [Open RewriteRule] -> [Open RewriteRule] -> [Open RewriteRule]
forall a. Monoid a => a -> a -> a
mappend Int
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] -> Int
contextSize = [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> ([a] -> [Int]) -> [a] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Int) -> [a] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map a -> Int
forall b. AddContext b => b -> Int
contextSize

instance AddContext Context where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext = (m a -> Context' ContextEntry -> m a)
-> Context' ContextEntry -> m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((m a -> ContextEntry -> m a) -> m a -> Context' ContextEntry -> 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' ContextEntry -> m a)
-> (m a -> ContextEntry -> m a)
-> m a
-> Context' ContextEntry
-> 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' ContextEntry -> Int
contextSize = Context' ContextEntry -> Int
forall a. Sized a => a -> Int
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 -> Int
contextSize ContextEntry
_ = Int
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) -> Int
contextSize (Name, Dom Type)
_ = Int
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) -> Int
contextSize Dom (Name, Type)
_ = Int
1

instance AddContext (Dom (String, Type)) where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
Dom ([Char], Type) -> m a -> m a
addContext = ([Char], Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
([Char], Dom Type) -> m a -> m a
addContext (([Char], Dom Type) -> m a -> m a)
-> (Dom ([Char], Type) -> ([Char], Dom Type))
-> Dom ([Char], Type)
-> m a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom ([Char], Type) -> ([Char], 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 ([Char], Type) -> Int
contextSize Dom ([Char], Type)
_ = Int
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) = [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 ((Name -> Name) -> [Name] -> Dom Type -> [Dom (Name, Type)]
forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' Name -> Name
forall a. a -> a
id [Name]
xs Dom Type
dom)
  contextSize :: ([Name], Dom Type) -> Int
contextSize ([Name]
xs, Dom Type
_) = [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
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) = [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 ((Name -> Name) -> List1 Name -> Dom Type -> [Dom (Name, Type)]
forall a. (Name -> a) -> List1 Name -> Dom Type -> ListTel' a
bindsToTel'1 Name -> Name
forall a. a -> a
id List1 Name
xs Dom Type
dom)
  contextSize :: (List1 Name, Dom Type) -> Int
contextSize (List1 Name
xs, Dom Type
_) = List1 Name -> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
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) -> Int
contextSize ([WithHiding Name]
xs, Dom Type
_) = [WithHiding Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
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, Int -> Dom Type -> Dom Type
forall a. Subst a => Int -> a -> a
raise Int
1 Dom Type
dom)
  contextSize :: (NonEmpty (WithHiding Name), Dom Type) -> Int
contextSize (NonEmpty (WithHiding Name)
xs, Dom Type
_) = NonEmpty (WithHiding Name) -> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
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) -> Int
contextSize ([Arg Name]
xs, Type
_) = [Arg Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
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) = (NonEmpty (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 =>
(NonEmpty (NamedArg Name), Type) -> m a -> m a
addContext (((Arg Name -> NamedArg Name)
-> List1 (Arg Name) -> NonEmpty (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) -> NonEmpty (NamedArg Name))
-> ((Name -> Named_ Name) -> Arg Name -> NamedArg Name)
-> (Name -> Named_ Name)
-> List1 (Arg Name)
-> NonEmpty (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) -> Int
contextSize (List1 (Arg Name)
xs, Type
_) = List1 (Arg Name) -> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
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) = (NonEmpty (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 =>
(NonEmpty (NamedArg Name), Type) -> m a -> m a
addContext (NamedArg Name
x NamedArg Name -> [NamedArg Name] -> NonEmpty (NamedArg Name)
forall a. a -> [a] -> NonEmpty a
:| [NamedArg Name]
xs, Type
t)
  contextSize :: ([NamedArg Name], Type) -> Int
contextSize ([NamedArg Name]
xs, Type
_) = [NamedArg Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg Name]
xs

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

instance AddContext (String, Dom Type) where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
([Char], Dom Type) -> m a -> m a
addContext ([Char]
s, Dom Type
dom) m a
ret =
    Range -> [Char] -> (Name -> m a) -> m a
forall a. Range -> [Char] -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> [Char] -> (Name -> m a) -> m a
withFreshName Range
forall a. Range' a
noRange [Char]
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 :: ([Char], Dom Type) -> Int
contextSize ([Char], Dom Type)
_ = Int
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 = ([Char], Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
([Char], Dom Type) -> m a -> m a
addContext (Text -> [Char]
T.unpack Text
s, Dom Type
dom) m a
ret
  contextSize :: (Text, Dom Type) -> Int
contextSize (Text, Dom Type)
_ = Int
1

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

instance AddContext (Dom Type) where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a. MonadAddContext m => Dom Type -> m a -> m a
addContext Dom Type
dom = ([Char], Dom Type) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
([Char], Dom Type) -> m a -> m a
addContext ([Char]
"_" :: String, Dom Type
dom)
  contextSize :: Dom Type -> Int
contextSize Dom Type
_ = Int
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 -> Int
contextSize Name
_ = Int
1

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

instance AddContext (KeepNames Telescope) where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
KeepNames (Tele (Dom Type)) -> m a -> m a
addContext (KeepNames Tele (Dom Type)
tel) m a
ret = Tele (Dom Type) -> m a
loop Tele (Dom Type)
tel where
    loop :: Tele (Dom Type) -> m a
loop Tele (Dom Type)
EmptyTel          = m a
ret
    loop (ExtendTel Dom Type
t Abs (Tele (Dom Type))
tel) = ([Char] -> KeepNames [Char])
-> Dom Type
-> Abs (Tele (Dom Type))
-> (Tele (Dom Type) -> m a)
-> m a
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
([Char] -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' [Char] -> KeepNames [Char]
forall a. a -> KeepNames a
KeepNames Dom Type
t Abs (Tele (Dom Type))
tel Tele (Dom Type) -> m a
loop
  contextSize :: KeepNames (Tele (Dom Type)) -> Int
contextSize (KeepNames Tele (Dom Type)
tel) = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
{-# SPECIALIZE addContext :: KeepNames Telescope -> TCM a -> TCM a #-}

instance AddContext Telescope where
  {-# INLINE addContext #-}
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
tel m a
ret = Tele (Dom Type) -> m a
loop Tele (Dom Type)
tel where
    loop :: Tele (Dom Type) -> m a
loop Tele (Dom Type)
EmptyTel          = m a
ret
    loop (ExtendTel Dom Type
t Abs (Tele (Dom Type))
tel) = ([Char] -> [Char])
-> Dom Type
-> Abs (Tele (Dom Type))
-> (Tele (Dom Type) -> m a)
-> m a
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
([Char] -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' [Char] -> [Char]
forall a. a -> a
id Dom Type
t Abs (Tele (Dom Type))
tel Tele (Dom Type) -> m a
loop
  contextSize :: Tele (Dom Type) -> Int
contextSize = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size
{-# SPECIALIZE addContext :: Telescope -> TCM a -> TCM a #-}

{-# NOINLINE extendReduceEnv #-}
extendReduceEnv :: String -> Dom Type -> ReduceEnv -> ReduceEnv
extendReduceEnv :: [Char] -> Dom Type -> ReduceEnv -> ReduceEnv
extendReduceEnv [Char]
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' :: [Char]
x' = case [Char]
x of [Char]
"" -> [Char]
"x"; [Char]
_ -> [Char]
x
                          cn :: Name
cn = Range -> NameInScope -> NameParts -> Name
C.Name Range
forall a. Range' a
noRange NameInScope
InScope ([Char] -> NameParts
C.stringNameParts [Char]
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' ContextEntry
ec           = TCEnv
re TCEnv
-> Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
-> Context' ContextEntry
forall s a. s -> Getting a s a -> a
^. Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
Lens' TCEnv (Context' ContextEntry)
eContext
      !ec' :: Context' ContextEntry
ec'          = Name -> Dom Type -> Context' ContextEntry -> Context' ContextEntry
CxExtendVar Name
n Dom Type
a Context' ContextEntry
ec
      !re' :: TCEnv
re'          = TCEnv
re TCEnv -> (TCEnv -> TCEnv) -> TCEnv
forall a b. a -> (a -> b) -> b
& ASetter TCEnv TCEnv (Context' ContextEntry) (Context' ContextEntry)
Lens' TCEnv (Context' ContextEntry)
eContext ASetter TCEnv TCEnv (Context' ContextEntry) (Context' ContextEntry)
-> Context' ContextEntry -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Context' ContextEntry
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   [Char]
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
$! [Char] -> Dom Type -> ReduceEnv -> ReduceEnv
extendReduceEnv [Char]
x Dom Type
a ReduceEnv
env
  NoAbs [Char]
_ 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 = ([Char] -> [Char]) -> Dom Type -> Abs a -> (a -> m b) -> m b
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
([Char] -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' [Char] -> [Char]
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)) =>
([Char] -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' [Char] -> name
_ Dom Type
_ (NoAbs [Char]
_ a
v) a -> m b
k = a -> m b
k a
v
underAbstraction' [Char] -> name
wrap Dom Type
t Abs a
a a -> m b
k = ([Char] -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
([Char] -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs' [Char] -> 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 = ([Char] -> [Char]) -> Dom Type -> Abs a -> (a -> m b) -> m b
forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
([Char] -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs' [Char] -> [Char]
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)) =>
([Char] -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs' [Char] -> 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 ([Char] -> name
wrap ([Char] -> name) -> [Char] -> name
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
realName ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Abs a -> [Char]
forall a. Abs a -> [Char]
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 :: [Char] -> [Char]
realName [Char]
s = if [Char] -> Bool
forall a. IsNoName a => a -> Bool
isNoName [Char]
s then [Char]
"x" else [Char] -> [Char]
argNameToString [Char]
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' ContextEntry)
getContext = Lens' TCEnv (Context' ContextEntry) -> m (Context' ContextEntry)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Context' ContextEntry -> f (Context' ContextEntry))
-> TCEnv -> f TCEnv
Lens' TCEnv (Context' ContextEntry)
eContext

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

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

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

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

contextVars' :: Context -> [(Int, Dom Name)]
contextVars' :: Context' ContextEntry -> [(Int, Dom Name)]
contextVars' = (Int -> ContextEntry -> (Int, Dom Name))
-> Context' ContextEntry -> [(Int, Dom Name)]
forall a.
(Int -> ContextEntry -> a) -> Context' ContextEntry -> [a]
cxWithIndex Int -> ContextEntry -> (Int, 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' ContextEntry -> Args
contextArgs (Context' ContextEntry -> Args)
-> m (Context' ContextEntry) -> m Args
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Context' ContextEntry)
forall (m :: * -> *). MonadTCEnv m => m (Context' ContextEntry)
getContext

contextArgs :: Context -> Args
contextArgs :: Context' ContextEntry -> Args
contextArgs = ((Int, Dom Name) -> Arg Term) -> [(Int, Dom Name)] -> Args
forall a b. (a -> b) -> [a] -> [b]
map' (\(Int
i,Dom Name
x) -> Int -> Term
var Int
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) ([(Int, Dom Name)] -> Args)
-> (Context' ContextEntry -> [(Int, Dom Name)])
-> Context' ContextEntry
-> Args
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context' ContextEntry -> [(Int, 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' ContextEntry -> [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' ContextEntry -> Args)
-> Context' ContextEntry
-> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context' ContextEntry -> Args
contextArgs

-- | Get the current context as a 'Telescope'.
{-# SPECIALIZE getContextTelescope :: TCM Telescope #-}
getContextTelescope :: (MonadTCEnv m) => m Telescope
getContextTelescope :: forall (m :: * -> *). MonadTCEnv m => m (Tele (Dom Type))
getContextTelescope = Context' ContextEntry -> Tele (Dom Type)
contextToTel (Context' ContextEntry -> Tele (Dom Type))
-> m (Context' ContextEntry) -> m (Tele (Dom Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Context' ContextEntry)
forall (m :: * -> *). MonadTCEnv m => m (Context' ContextEntry)
getContext

contextToTel :: Context -> Telescope
contextToTel :: Context' ContextEntry -> Tele (Dom Type)
contextToTel = Tele (Dom Type) -> Context' ContextEntry -> Tele (Dom Type)
go Tele (Dom Type)
forall a. Tele a
EmptyTel
  where
    go :: Tele (Dom Type) -> Context' ContextEntry -> Tele (Dom Type)
go !Tele (Dom Type)
tel Context' ContextEntry
CxEmpty              = Tele (Dom Type)
tel
    go Tele (Dom Type)
tel (CxExtendVar Name
x Dom Type
a Context' ContextEntry
ctx) = let !x' :: [Char]
x' = Name -> [Char]
nameToArgName Name
x
                                   in Tele (Dom Type) -> Context' ContextEntry -> Tele (Dom Type)
go (Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a ([Char] -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. [Char] -> a -> Abs a
Abs [Char]
x' Tele (Dom Type)
tel)) Context' ContextEntry
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' ContextEntry -> [Name]
contextNames (Context' ContextEntry -> [Name])
-> m (Context' ContextEntry) -> m [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Context' ContextEntry)
forall (m :: * -> *). MonadTCEnv m => m (Context' ContextEntry)
getContext

{-# SPECIALIZE getContextNames' :: TCM [Name] #-}
getContextNames' :: (MonadTCEnv m) => m [Name]
getContextNames' :: forall (m :: * -> *). MonadTCEnv m => m [Name]
getContextNames' = Context' ContextEntry -> [Name]
contextNames' (Context' ContextEntry -> [Name])
-> m (Context' ContextEntry) -> m [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Context' ContextEntry)
forall (m :: * -> *). MonadTCEnv m => m (Context' ContextEntry)
getContext

contextNames :: Context -> [Name]
contextNames :: Context' ContextEntry -> [Name]
contextNames = ((Int, Dom Name) -> Name) -> [(Int, 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)
-> ((Int, Dom Name) -> Dom Name) -> (Int, Dom Name) -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Dom Name) -> Dom Name
forall a b. (a, b) -> b
snd) ([(Int, Dom Name)] -> [Name])
-> (Context' ContextEntry -> [(Int, Dom Name)])
-> Context' ContextEntry
-> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context' ContextEntry -> [(Int, Dom Name)]
contextVars

contextNames' :: Context -> [Name]
contextNames' :: Context' ContextEntry -> [Name]
contextNames' = ((Int, Dom Name) -> Name) -> [(Int, 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)
-> ((Int, Dom Name) -> Dom Name) -> (Int, Dom Name) -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Dom Name) -> Dom Name
forall a b. (a, b) -> b
snd) ([(Int, Dom Name)] -> [Name])
-> (Context' ContextEntry -> [(Int, Dom Name)])
-> Context' ContextEntry
-> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context' ContextEntry -> [(Int, Dom Name)]
contextVars'

-- | get type of bound variable (i.e. deBruijn index)
--
lookupBV_ :: Nat -> Context -> Maybe ContextEntry
lookupBV_ :: Int -> Context' ContextEntry -> Maybe ContextEntry
lookupBV_ Int
n Context' ContextEntry
ctx = Int -> ContextEntry -> ContextEntry
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (ContextEntry -> ContextEntry)
-> Maybe ContextEntry -> Maybe ContextEntry
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Context' ContextEntry -> Maybe ContextEntry
cxLookup Int
n Context' ContextEntry
ctx

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

{-# SPECIALIZE lookupBV :: Nat -> TCM ContextEntry #-}
lookupBV :: (MonadDebug m, MonadTCEnv m) => Nat -> m ContextEntry
lookupBV :: forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m ContextEntry
lookupBV Int
n = do
  let failure :: m ContextEntry
failure = do
        ctx <- m (Context' ContextEntry)
forall (m :: * -> *). MonadTCEnv m => m (Context' ContextEntry)
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 (Int -> m (Maybe ContextEntry)
forall (m :: * -> *). MonadTCEnv m => Int -> m (Maybe ContextEntry)
lookupBV' Int
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) =>
Int -> m (Dom Type)
domOfBV Int
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
<$> Int -> m ContextEntry
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m ContextEntry
lookupBV Int
n

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

{-# SPECIALIZE nameOfBV' :: Nat -> TCM (Maybe Name) #-}
nameOfBV' :: (MonadTCEnv m) => Nat -> m (Maybe Name)
nameOfBV' :: forall (m :: * -> *). MonadTCEnv m => Int -> m (Maybe Name)
nameOfBV' Int
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
<$> Int -> m (Maybe ContextEntry)
forall (m :: * -> *). MonadTCEnv m => Int -> m (Maybe ContextEntry)
lookupBV' Int
n

{-# SPECIALIZE nameOfBV :: Nat -> TCM Name #-}
nameOfBV :: (MonadDebug m, MonadTCEnv m) => Nat -> m Name
nameOfBV :: forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Name
nameOfBV Int
n = ContextEntry -> Name
ctxEntryName (ContextEntry -> Name) -> m ContextEntry -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m ContextEntry
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m ContextEntry
lookupBV Int
n

-- | Get the term corresponding to a named variable. If it is a lambda bound
--   variable the deBruijn index is returned and if it is a let bound variable
--   its definition is returned.
{-# SPECIALIZE getVarInfo :: Name -> TCM (Term, Dom Type) #-}
getVarInfo :: (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 [(Int, Dom Name)]
forall (m :: * -> *). MonadTCEnv m => m [(Int, Dom Name)]
getContextVars'
        def <- viewTC eLetBindings
        case List.findIndex ((== x) . unDom . snd) ctx of
            Just Int
n -> do
                t <- Int -> m (Dom Type)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m (Dom Type)
domOfBV Int
n
                return (var n, t)
            Maybe Int
_       ->
                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)
_ -> [Char] -> m (Term, Dom Type)
forall a. HasCallStack => [Char] -> m a
forall (m :: * -> *) a.
(MonadFail m, HasCallStack) =>
[Char] -> m a
fail ([Char] -> m (Term, Dom Type)) -> [Char] -> m (Term, Dom Type)
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords
                      [ [Char]
"unbound variable"
                      , Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Name -> [Char]) -> Name -> [Char]
forall a b. (a -> b) -> a -> b
$ Name -> Name
nameConcrete Name
x
                      , [Char]
"(id: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ NameId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Name -> NameId
forall a. HasNameId a => a -> NameId
nameId Name
x) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
                      ]
                      -- 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.