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 = (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envContext = f $ envContext e }

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

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

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

-- | Delete the last @n@ bindings from the context.
--
--   Doesn't update checkpoints! Use `escapeContext` or `updateContext
--   rho (drop n)` instead, for an appropriate substitution `rho`.
{-# SPECIALIZE unsafeEscapeContext :: Int -> TCM a -> TCM a #-}
unsafeEscapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a
unsafeEscapeContext :: forall (tcm :: * -> *) a. MonadTCM tcm => Int -> tcm a -> tcm a
unsafeEscapeContext Int
n = (Context -> Context) -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext ((Context -> Context) -> tcm a -> tcm a)
-> (Context -> Context) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Int -> Context -> Context
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 = Substitution' Term -> (Context -> Context) -> m a -> m a
forall a. Substitution' Term -> (Context -> Context) -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution' Term -> (Context -> Context) -> m a -> m a
updateContext (Impossible -> Int -> Substitution' Term
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
err Int
n) ((Context -> Context) -> m a -> m a)
-> (Context -> Context) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Int -> Context -> Context
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' Term -> tcm a -> tcm a
checkpoint Substitution' Term
sub tcm a
k = do
  tcm () -> tcm ()
forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.cxt.checkpoint" Int
105 (String -> tcm ()) -> String -> tcm ()
forall a b. (a -> b) -> a -> b
$ String
"New checkpoint {"
  CheckpointId
old     <- Lens' TCEnv CheckpointId -> tcm CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
Lens' TCEnv CheckpointId
eCurrentCheckpoint
  Map ModuleName CheckpointId
oldMods <- Lens' TCState (Map ModuleName CheckpointId)
-> tcm (Map ModuleName CheckpointId)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC  (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
-> TCState -> f TCState
Lens' TCState (Map ModuleName CheckpointId)
stModuleCheckpoints
  CheckpointId
chkpt <- tcm CheckpointId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
  tcm () -> tcm ()
forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> tcm () -> tcm ()
forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS String
"tc.cxt.checkpoint" Int
105 (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ do
    Telescope
cxt <- tcm Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
    Map CheckpointId (Substitution' Term)
cps <- Lens' TCEnv (Map CheckpointId (Substitution' Term))
-> tcm (Map CheckpointId (Substitution' Term))
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Map CheckpointId (Substitution' Term)
 -> f (Map CheckpointId (Substitution' Term)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map CheckpointId (Substitution' Term))
eCheckpoints
    let cps' :: Map CheckpointId (Substitution' Term)
cps' = CheckpointId
-> Substitution' Term
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert CheckpointId
chkpt Substitution' Term
forall a. Substitution' a
IdS (Map CheckpointId (Substitution' Term)
 -> Map CheckpointId (Substitution' Term))
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall a b. (a -> b) -> a -> b
$ (Substitution' Term -> Substitution' Term)
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall a b. (a -> b) -> Map CheckpointId a -> Map CheckpointId b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' (SubstArg (Substitution' Term))
-> Substitution' Term -> Substitution' Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Substitution' Term))
sub) Map CheckpointId (Substitution' Term)
cps
        prCps :: Map a a -> Doc Aspects
prCps Map a a
cps = [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat [ a -> Doc Aspects
forall a. Show a => a -> Doc Aspects
pshow a
c Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
": " Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
s | (a
c, a
s) <- Map a a -> [(a, a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map a a
cps ]
    String -> Int -> TCM (Doc Aspects) -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM (Doc Aspects) -> m ()
reportSDoc String
"tc.cxt.checkpoint" Int
105 (TCM (Doc Aspects) -> tcm ()) -> TCM (Doc Aspects) -> tcm ()
forall a b. (a -> b) -> a -> b
$ Doc Aspects -> TCM (Doc Aspects)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc Aspects -> TCM (Doc Aspects))
-> Doc Aspects -> TCM (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ Int -> Doc Aspects -> Doc Aspects
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat
      [ Doc Aspects
"old =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> CheckpointId -> Doc Aspects
forall a. Show a => a -> Doc Aspects
pshow CheckpointId
old
      , Doc Aspects
"new =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> CheckpointId -> Doc Aspects
forall a. Show a => a -> Doc Aspects
pshow CheckpointId
chkpt
      , Doc Aspects
"sub =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Substitution' Term -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty Substitution' Term
sub
      , Doc Aspects
"cxt =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Telescope -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty Telescope
cxt
      , Doc Aspects
"old substs =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Map CheckpointId (Substitution' Term) -> Doc Aspects
forall {a} {a}. (Show a, Pretty a) => Map a a -> Doc Aspects
prCps Map CheckpointId (Substitution' Term)
cps
      , Doc Aspects
"new substs =" Doc Aspects -> Doc Aspects -> Doc Aspects
<?> Map CheckpointId (Substitution' Term) -> Doc Aspects
forall {a} {a}. (Show a, Pretty a) => Map a a -> Doc Aspects
prCps Map CheckpointId (Substitution' Term)
cps'
      ]
  a
x <- ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> tcm a -> (TCEnv -> TCEnv) -> tcm a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC tcm a
k ((TCEnv -> TCEnv) -> tcm a) -> (TCEnv -> TCEnv) -> tcm a
forall a b. (a -> b) -> a -> b
$ \ TCEnv
env -> TCEnv
env
    { envCurrentCheckpoint = chkpt
    , envCheckpoints       = Map.insert chkpt IdS $
                              fmap (applySubst sub) (envCheckpoints env)
    }
  Map ModuleName CheckpointId
newMods <- Lens' TCState (Map ModuleName CheckpointId)
-> tcm (Map ModuleName CheckpointId)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
-> TCState -> f TCState
Lens' TCState (Map ModuleName CheckpointId)
stModuleCheckpoints
  -- Set the checkpoint for introduced modules to the old checkpoint when the
  -- new one goes out of scope. #2897: This isn't actually sound for modules
  -- created under refined parent parameters, but as long as those modules
  -- aren't named we shouldn't look at the checkpoint. The right thing to do
  -- would be to not store these modules in the checkpoint map, but todo..
  (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
-> TCState -> f TCState
Lens' TCState (Map ModuleName CheckpointId)
stModuleCheckpoints Lens' TCState (Map ModuleName CheckpointId)
-> Map ModuleName CheckpointId -> tcm ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` Map ModuleName CheckpointId
-> Map ModuleName CheckpointId -> Map ModuleName CheckpointId
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map ModuleName CheckpointId
oldMods (CheckpointId
old CheckpointId
-> Map ModuleName CheckpointId -> Map ModuleName CheckpointId
forall a b. a -> Map ModuleName b -> Map ModuleName a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Map ModuleName CheckpointId
newMods)
  tcm () -> tcm ()
forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting (tcm () -> tcm ()) -> tcm () -> tcm ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.cxt.checkpoint" Int
105 String
"}"
  a -> tcm a
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x

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

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

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


-- * Adding to the context

{-# 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 = (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'' Term Term) -> n (StT t a) -> n (StT t a)
forall a. Name -> Dom (Type'' Term Term) -> n a -> n a
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 = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
(MonadTransControl t, Monad (t m), Monad m) =>
(m (StT t a) -> m (StT t b)) -> t m a -> t m b
liftThrough ((n (StT t a) -> n (StT t a)) -> t n a -> t n a)
-> (n (StT t a) -> n (StT t a)) -> t n a -> t n a
forall a b. (a -> b) -> a -> b
$ Origin
-> Name
-> Term
-> Dom (Type'' Term Term)
-> n (StT t a)
-> n (StT t a)
forall a.
Origin -> Name -> Term -> Dom (Type'' Term Term) -> n a -> n a
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' Term
sub Context -> Context
f = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
(MonadTransControl t, Monad (t m), Monad m) =>
(m (StT t a) -> m (StT t b)) -> t m a -> t m b
liftThrough ((n (StT t a) -> n (StT t a)) -> t n a -> t n a)
-> (n (StT t a) -> n (StT t a)) -> t n a -> t n a
forall a b. (a -> b) -> a -> b
$ Substitution' Term
-> (Context -> Context) -> n (StT t a) -> n (StT t a)
forall a. Substitution' Term -> (Context -> Context) -> n a -> n a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution' Term -> (Context -> Context) -> m a -> m a
updateContext Substitution' Term
sub Context -> Context
f

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

-- | 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 =
  Substitution' Term -> (Context -> Context) -> m a -> m a
forall a. Substitution' Term -> (Context -> Context) -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution' Term -> (Context -> Context) -> m a -> m a
updateContext (Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS Int
1) (((Name
x,) (Type'' Term Term -> (Name, Type'' Term Term))
-> Dom (Type'' Term Term) -> ContextEntry
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom (Type'' Term Term)
a) ContextEntry -> Context -> Context
forall a. a -> [a] -> [a]
:) m a
ret

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

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

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

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

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

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

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

instance MonadAddContext TCM where
  addCtx :: forall a. Name -> Dom (Type'' Term Term) -> TCM a -> TCM a
addCtx Name
x Dom (Type'' Term Term)
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'' Term Term) -> TCM a -> TCM a
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 = Bool -> (TCM a -> TCM a) -> TCM a -> TCM a
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless (Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x) (Name -> TCM a -> TCM a
forall b. Name -> TCM b -> TCM b
withShadowingNameTCM Name
x) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$
    Origin -> Name -> Term -> Dom (Type'' Term Term) -> TCM a -> TCM a
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' Term -> (Context -> Context) -> TCM a -> TCM a
updateContext Substitution' Term
sub Context -> Context
f = (Context -> Context) -> TCMT IO a -> TCMT IO a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext Context -> Context
f (TCMT IO a -> TCMT IO a)
-> (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution' Term -> TCMT IO a -> TCMT IO a
forall (tcm :: * -> *) a.
(MonadDebug tcm, MonadTCM tcm, MonadFresh CheckpointId tcm,
 ReadTCState tcm) =>
Substitution' Term -> tcm a -> tcm a
checkpoint Substitution' Term
sub

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

addRecordNameContext
  :: (MonadAddContext m, MonadFresh NameId m)
  => Dom Type -> m b -> m b
addRecordNameContext :: forall (m :: * -> *) b.
(MonadAddContext m, MonadFresh NameId m) =>
Dom (Type'' Term Term) -> m b -> m b
addRecordNameContext Dom (Type'' Term Term)
dom m b
ret = do
  Name
x <- Name -> Name
forall a. LensInScope a => a -> a
setNotInScope (Name -> Name) -> m Name -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Name
forall (m :: * -> *). MonadFresh NameId m => m Name
freshRecordName
  Name -> Dom (Type'' Term Term) -> m b -> m b
forall a. Name -> Dom (Type'' Term Term) -> m a -> m a
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 = (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)
  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 (Name, Dom Type) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
(Name, Dom (Type'' Term Term)) -> m a -> m a
addContext = (Name -> Dom (Type'' Term Term) -> m a -> m a)
-> (Name, Dom (Type'' Term Term)) -> m a -> m a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Dom (Type'' Term Term) -> m a -> m a
forall a. Name -> Dom (Type'' Term Term) -> m a -> m a
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 =>
ContextEntry -> m a -> m a
addContext = (Name, Dom (Type'' Term Term)) -> 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'' Term Term)) -> m a -> m a
addContext ((Name, Dom (Type'' Term Term)) -> m a -> m a)
-> (ContextEntry -> (Name, Dom (Type'' Term Term)))
-> ContextEntry
-> m a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> (Name, Dom (Type'' Term Term))
forall (t :: * -> *) (m :: * -> *) a.
(Decoration t, Functor m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a.
Functor m =>
Dom' Term (m a) -> m (Dom' Term a)
distributeF
  contextSize :: ContextEntry -> Int
contextSize ContextEntry
_ = Int
1

instance AddContext (Dom (String, Type)) where
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
Dom (String, Type'' Term Term) -> m a -> m a
addContext = (String, Dom (Type'' Term Term)) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom (Type'' Term Term)) -> m a -> m a
addContext ((String, Dom (Type'' Term Term)) -> m a -> m a)
-> (Dom (String, Type'' Term Term)
    -> (String, Dom (Type'' Term Term)))
-> Dom (String, Type'' Term Term)
-> m a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (String, Type'' Term Term) -> (String, Dom (Type'' Term Term))
forall (t :: * -> *) (m :: * -> *) a.
(Decoration t, Functor m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a.
Functor m =>
Dom' Term (m a) -> m (Dom' Term a)
distributeF
  contextSize :: Dom (String, Type'' 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) = Context -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext ((Name -> Name) -> [Name] -> Dom (Type'' Term Term) -> Context
forall a.
(Name -> a) -> [Name] -> Dom (Type'' Term Term) -> ListTel' a
bindsToTel' Name -> Name
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)
_) = [Name] -> Int
forall a. [a] -> Int
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) = Context -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext ((Name -> Name) -> List1 Name -> Dom (Type'' Term Term) -> Context
forall a.
(Name -> a) -> List1 Name -> Dom (Type'' Term Term) -> ListTel' a
bindsToTel'1 Name -> Name
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)
_) = 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
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
([WithHiding Name], Dom (Type'' Term Term)) -> m a -> m a
addContext ([]    , Dom (Type'' Term Term)
dom) = m a -> m a
forall a. a -> a
id
  addContext (WithHiding Name
x : [WithHiding Name]
xs, Dom (Type'' Term Term)
dom) = (NonEmpty (WithHiding Name), Dom (Type'' Term Term)) -> 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'' Term Term)) -> 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'' Term Term)
dom)
  contextSize :: ([WithHiding Name], Dom (Type'' Term Term)) -> Int
contextSize ([WithHiding Name]
xs, Dom (Type'' Term Term)
_) = [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
  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) =
    (Name, Dom (Type'' Term Term)) -> 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'' Term Term)) -> m a -> m a
addContext (Name
x , (Hiding -> Hiding)
-> Dom (Type'' Term Term) -> Dom (Type'' Term Term)
forall a. LensHiding a => (Hiding -> Hiding) -> a -> a
mapHiding (Hiding -> Hiding -> Hiding
forall a. Monoid a => a -> a -> a
mappend Hiding
h) Dom (Type'' Term Term)
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'' Term Term)) -> 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'' Term Term)) -> m a -> m a
addContext ([WithHiding Name]
xs, Int -> Dom (Type'' Term Term) -> Dom (Type'' Term Term)
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)
_) = 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
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
([Arg Name], Type'' Term Term) -> m a -> m a
addContext ([Arg Name]
xs, Type'' Term Term
t) = ([NamedArg Name], Type'' Term Term) -> 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'' Term Term) -> 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'' Term Term
t)
  contextSize :: ([Arg Name], Type'' Term Term) -> Int
contextSize ([Arg Name]
xs, Type'' Term Term
_) = [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
  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) = (List1 (NamedArg Name), Type'' Term Term) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(List1 (NamedArg Name), Type'' Term Term) -> m a -> m a
addContext (((Arg Name -> NamedArg Name)
-> List1 (Arg Name) -> List1 (NamedArg Name)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Arg Name -> NamedArg Name)
 -> List1 (Arg Name) -> List1 (NamedArg Name))
-> ((Name -> Named_ Name) -> Arg Name -> NamedArg Name)
-> (Name -> Named_ Name)
-> List1 (Arg Name)
-> List1 (NamedArg Name)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Named_ Name) -> Arg Name -> NamedArg Name
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Name -> Named_ Name
forall a name. a -> Named name a
unnamed List1 (Arg Name)
xs :: List1 (NamedArg Name), Type'' Term Term
t)
  contextSize :: (List1 (Arg Name), Type'' Term Term) -> Int
contextSize (List1 (Arg Name)
xs, Type'' Term Term
_) = 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
  addContext :: forall (m :: * -> *) a.
MonadAddContext m =>
([NamedArg Name], Type'' Term Term) -> m a -> m a
addContext ([], Type'' Term Term
_)     = m a -> m a
forall a. a -> a
id
  addContext (NamedArg Name
x : [NamedArg Name]
xs, Type'' Term Term
t) = (List1 (NamedArg Name), Type'' Term Term) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(List1 (NamedArg Name), Type'' Term Term) -> m a -> m a
addContext (NamedArg Name
x NamedArg Name -> [NamedArg Name] -> List1 (NamedArg Name)
forall a. a -> [a] -> NonEmpty a
:| [NamedArg Name]
xs, Type'' Term Term
t)
  contextSize :: ([NamedArg Name], Type'' Term Term) -> Int
contextSize ([NamedArg Name]
xs, Type'' Term Term
_) = [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
  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) =
    (Name, Dom (Type'' Term Term)) -> 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'' Term Term)) -> m a -> m a
addContext (NamedArg Name -> Name
forall a. NamedArg a -> a
namedArg NamedArg Name
x, Type'' Term Term
t Type'' Term Term -> Dom' Term () -> Dom (Type'' Term Term)
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'' Term Term) -> 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'' Term Term) -> m a -> m a
addContext ([NamedArg Name]
xs, Int -> Type'' Term Term -> Type'' Term Term
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
_) = List1 (NamedArg Name) -> Int
forall a. NonEmpty a -> Int
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 =
    Range -> String -> (Name -> m a) -> m a
forall a. Range -> String -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> String -> (Name -> m a) -> m a
withFreshName Range
forall a. Range' a
noRange String
s ((Name -> m a) -> m a) -> (Name -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \Name
x -> Name -> Dom (Type'' Term Term) -> m a -> m a
forall a. Name -> Dom (Type'' Term Term) -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom (Type'' Term Term) -> m a -> m a
addCtx (Name -> Name
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 = (String, Dom (Type'' Term Term)) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom (Type'' Term Term)) -> 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 =
    Range -> String -> (Name -> m a) -> m a
forall a. Range -> String -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> String -> (Name -> m a) -> m a
withFreshName Range
forall a. Range' a
noRange String
s ((Name -> m a) -> m a) -> (Name -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \ Name
x -> Name -> Dom (Type'' Term Term) -> m a -> m a
forall a. Name -> Dom (Type'' Term Term) -> m a -> m a
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 = (String, Dom (Type'' Term Term)) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom (Type'' Term Term)) -> 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 = (Name, Dom (Type'' Term Term)) -> 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'' Term Term)) -> m a -> m a
addContext (Name
x, Dom (Type'' Term Term)
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 = (String, Dom (Type'' Term Term)) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom (Type'' Term Term)) -> m a -> m a
addContext (String
s, Dom (Type'' Term Term)
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) = (String -> KeepNames String)
-> Dom (Type'' Term Term)
-> Abs Telescope
-> (Telescope -> m a)
-> m a
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 -> KeepNames String
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) = Telescope -> Int
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) = (String -> String)
-> Dom (Type'' Term Term)
-> Abs Telescope
-> (Telescope -> m a)
-> m a
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 -> String
forall a. a -> a
id Dom (Type'' Term Term)
t Abs Telescope
tel Telescope -> m a
loop
  contextSize :: Telescope -> Int
contextSize = Telescope -> Int
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 = (String -> String)
-> Dom (Type'' Term Term) -> Abs a -> (a -> m b) -> m b
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 -> String
forall a. a -> a
id

underAbstraction' :: (Subst a, MonadAddContext m, AddContext (name, Dom Type)) =>
                     (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' :: forall a (m :: * -> *) name b.
(Subst a, MonadAddContext m,
 AddContext (name, Dom (Type'' 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 = (String -> name)
-> Dom (Type'' Term Term) -> Abs a -> (a -> m b) -> m b
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 = (String -> String)
-> Dom (Type'' Term Term) -> Abs a -> (a -> m b) -> m b
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 -> String
forall a. a -> a
id

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

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

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

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

-- | Add a let bound variable
{-# SPECIALIZE addLetBinding :: ArgInfo -> Origin -> Name -> Term -> Type -> TCM a -> TCM a #-}
addLetBinding :: MonadAddContext m => ArgInfo -> Origin -> Name -> Term -> Type -> m a -> m a
addLetBinding :: forall (m :: * -> *) a.
MonadAddContext m =>
ArgInfo -> Origin -> Name -> Term -> Type'' Term Term -> m a -> m a
addLetBinding ArgInfo
info Origin
o Name
x Term
v Type'' Term Term
t0 m a
ret = Origin -> Name -> Term -> Dom (Type'' Term Term) -> m a -> m a
forall a.
Origin -> Name -> Term -> Dom (Type'' Term Term) -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Origin -> Name -> Term -> Dom (Type'' Term Term) -> m a -> m a
addLetBinding' Origin
o Name
x Term
v (ArgInfo -> Type'' Term Term -> Dom (Type'' Term Term)
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 = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \ TCEnv
e -> TCEnv
e { envLetBindings = Map.delete x (envLetBindings e) }

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

-- * Querying the context

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

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

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

-- | Generate @[var (n - 1), ..., var 0]@ for all declarations in the context.
{-# SPECIALIZE getContextTerms :: TCM [Term] #-}
getContextTerms :: (Applicative m, MonadTCEnv m) => m [Term]
getContextTerms :: forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Term]
getContextTerms = (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
var ([Int] -> [Term]) -> (Int -> [Int]) -> Int -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Term]) -> m Int -> m [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Int
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 = (Name -> String) -> Context -> Telescope
forall a. (a -> String) -> ListTel' a -> Telescope
telFromList' Name -> String
nameToArgName (Context -> Telescope)
-> (Context -> Context) -> Context -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context
forall a. [a] -> [a]
reverse (Context -> Telescope) -> m Context -> m Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext

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

-- | get type of bound variable (i.e. deBruijn index)
--
{-# 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 = do
  Context
ctx <- m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
  Maybe ContextEntry -> m (Maybe ContextEntry)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ContextEntry -> m (Maybe ContextEntry))
-> Maybe ContextEntry -> m (Maybe ContextEntry)
forall a b. (a -> b) -> a -> b
$ 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
<$> Context
ctx Context -> Int -> Maybe ContextEntry
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 ContextEntry
lookupBV Int
n = do
  let failure :: m ContextEntry
failure = do
        Context
ctx <- m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
        String -> m ContextEntry
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m ContextEntry) -> String -> m ContextEntry
forall a b. (a -> b) -> a -> b
$ String
"de Bruijn index out of scope: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++
               String
" in context " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Pretty a => a -> String
prettyShow ((ContextEntry -> Name) -> Context -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type'' Term Term) -> Name
forall a b. (a, b) -> a
fst ((Name, Type'' Term Term) -> Name)
-> (ContextEntry -> (Name, Type'' Term Term))
-> ContextEntry
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> (Name, Type'' Term Term)
forall t e. Dom' t e -> e
unDom) Context
ctx)
  m ContextEntry
-> (ContextEntry -> m ContextEntry)
-> m (Maybe ContextEntry)
-> m ContextEntry
forall (m :: * -> *) b a.
Monad m =>
m b -> (a -> m b) -> m (Maybe a) -> m b
maybeM m ContextEntry
failure ContextEntry -> m ContextEntry
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (m (Maybe ContextEntry) -> m ContextEntry)
-> m (Maybe ContextEntry) -> m ContextEntry
forall a b. (a -> b) -> a -> b
$ Int -> m (Maybe ContextEntry)
forall (m :: * -> *). MonadTCEnv m => Int -> m (Maybe ContextEntry)
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 = ((Name, Type'' Term Term) -> Type'' Term Term)
-> ContextEntry -> Dom (Type'' Term Term)
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, Type'' Term Term) -> Type'' Term Term
forall a b. (a, b) -> b
snd (ContextEntry -> Dom (Type'' Term Term))
-> m ContextEntry -> m (Dom (Type'' Term Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m ContextEntry
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Int -> m ContextEntry
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 = Dom (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom (Dom (Type'' Term Term) -> Type'' Term Term)
-> m (Dom (Type'' Term Term)) -> m (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m (Dom (Type'' Term Term))
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 = (ContextEntry -> Name) -> Maybe ContextEntry -> Maybe Name
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name, Type'' Term Term) -> Name
forall a b. (a, b) -> a
fst ((Name, Type'' Term Term) -> Name)
-> (ContextEntry -> (Name, Type'' Term Term))
-> ContextEntry
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> (Name, Type'' Term Term)
forall t e. Dom' t e -> e
unDom) (Maybe ContextEntry -> Maybe Name)
-> m (Maybe ContextEntry) -> m (Maybe Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m (Maybe ContextEntry)
forall (m :: * -> *). MonadTCEnv m => Int -> m (Maybe ContextEntry)
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 = (Name, Type'' Term Term) -> Name
forall a b. (a, b) -> a
fst ((Name, Type'' Term Term) -> Name)
-> (ContextEntry -> (Name, Type'' Term Term))
-> ContextEntry
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> (Name, Type'' Term Term)
forall t e. Dom' t e -> e
unDom (ContextEntry -> Name) -> m ContextEntry -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m ContextEntry
forall (m :: * -> *).
(MonadFail 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 :: (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 <- m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
        Map Name (Open LetBinding)
def <- (TCEnv -> Map Name (Open LetBinding))
-> m (Map Name (Open LetBinding))
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Map Name (Open LetBinding)
envLetBindings
        case (ContextEntry -> Bool) -> Context -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
List.findIndex ((Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==Name
x) (Name -> Bool) -> (ContextEntry -> Name) -> ContextEntry -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Type'' Term Term) -> Name
forall a b. (a, b) -> a
fst ((Name, Type'' Term Term) -> Name)
-> (ContextEntry -> (Name, Type'' Term Term))
-> ContextEntry
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> (Name, Type'' Term Term)
forall t e. Dom' t e -> e
unDom) Context
ctx of
            Just Int
n -> do
                Dom (Type'' Term Term)
t <- Int -> m (Dom (Type'' Term Term))
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m (Dom (Type'' Term Term))
domOfBV Int
n
                (Term, Dom (Type'' Term Term)) -> m (Term, Dom (Type'' Term Term))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Term
var Int
n, Dom (Type'' Term Term)
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 Origin
_ Term
v Dom (Type'' Term Term)
t <- Open LetBinding -> m LetBinding
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen Open LetBinding
vt
                      (Term, Dom (Type'' Term Term)) -> m (Term, Dom (Type'' Term Term))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Dom (Type'' Term Term)
t)
                    Maybe (Open LetBinding)
_       -> String -> m (Term, Dom (Type'' Term Term))
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m (Term, Dom (Type'' Term Term)))
-> String -> m (Term, Dom (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ String
"unbound variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Pretty a => a -> String
prettyShow (Name -> Name
nameConcrete Name
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                String
" (id: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ NameId -> String
forall a. Pretty a => a -> String
prettyShow (Name -> NameId
nameId Name
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"