module Agda.TypeChecking.Monad.Context where

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

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

import qualified Data.DList as DL
import Data.Foldable
import qualified Data.List as List
import qualified Data.Map as Map

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

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

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

import Agda.Utils.Impossible

-- * Modifying the context

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

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

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

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

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

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

-- * Manipulating checkpoints --

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

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

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

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


-- * Adding to the context

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

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

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

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

  default addCtx
    :: (MonadAddContext n, MonadTransControl t, t n ~ m)
    => Name -> Dom Type -> m a -> m a
  addCtx Name
x Dom (Type'' Term Term)
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 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom (Type'' Term Term) -> m a -> m a
addCtx Name
x Dom (Type'' Term Term)
a

  default addLetBinding'
    :: (MonadAddContext n, MonadTransControl t, t n ~ m)
    => Origin -> Name -> Term -> Dom Type -> m a -> m a
  addLetBinding' Origin
o Name
x Term
u Dom (Type'' Term Term)
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 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadAddContext m =>
Origin -> Name -> Term -> Dom (Type'' Term Term) -> m a -> m a
addLetBinding' Origin
o Name
x Term
u Dom (Type'' Term Term)
a

  default updateContext
    :: (MonadAddContext n, MonadTransControl t, t n ~ m)
    => Substitution -> (Context -> Context) -> m a -> m a
  updateContext Substitution
sub Context -> Context
f = 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 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> m a -> m a
updateContext Substitution
sub Context -> Context
f

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance AddContext (Text, Dom Type) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
(Text, Dom (Type'' Term Term)) -> m a -> m a
addContext (Text
s, Dom (Type'' Term Term)
dom) m a
ret = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Text -> String
T.unpack Text
s, Dom (Type'' Term Term)
dom) m a
ret
  contextSize :: (Text, Dom (Type'' Term Term)) -> Int
contextSize (Text, Dom (Type'' Term Term))
_ = Int
1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


-- | 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 = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC forall a b. (a -> b) -> a -> b
$ \ TCEnv
e -> TCEnv
e { envLetBindings :: LetBindings
envLetBindings = forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Name
x (TCEnv -> LetBindings
envLetBindings TCEnv
e) }

-- | 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 = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC forall a b. (a -> b) -> a -> b
$ \ TCEnv
e -> TCEnv
e { envLetBindings :: LetBindings
envLetBindings = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> (Map k a, Map k a)
Map.split Name
x (TCEnv -> LetBindings
envLetBindings TCEnv
e) }

-- * Querying the context

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

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

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

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

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

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

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

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

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

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

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

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

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