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.Free
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.Utils.Pretty
import Agda.Utils.Size

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' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' CheckpointId TCEnv
eCurrentCheckpoint (forall a b. a -> b -> a
const CheckpointId
0)
        forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' (Map CheckpointId Substitution) TCEnv
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' a TCState -> (a -> a) -> m b -> m b
locallyTCState Lens' (Map ModuleName CheckpointId) TCState
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' a ScopeInfo -> (a -> a) -> m b -> m b
locallyScope Lens' LocalVars ScopeInfo
scopeLocals (forall a b. a -> b -> a
const [])
        forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' LetBindings TCEnv
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' a ScopeInfo -> (a -> a) -> m b -> m b
locallyScope Lens' LocalVars ScopeInfo
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' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
  Map ModuleName CheckpointId
oldMods <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC  Lens' (Map ModuleName CheckpointId) TCState
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' a TCEnv -> m a
viewTC Lens' (Map CheckpointId Substitution) TCEnv
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
prCps Map a a
cps = forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [ forall a. Show a => a -> Doc
pshow a
c Doc -> Doc -> Doc
<+> Doc
": " Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
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 -> 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
$ Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ Doc
"old =" Doc -> Doc -> Doc
<+> forall a. Show a => a -> Doc
pshow CheckpointId
old
      , Doc
"new =" Doc -> Doc -> Doc
<+> forall a. Show a => a -> Doc
pshow CheckpointId
chkpt
      , Doc
"sub =" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Substitution
sub
      , Doc
"cxt =" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Telescope
cxt
      , Doc
"old substs =" Doc -> Doc -> Doc
<+> forall {a} {a}. (Show a, Pretty a) => Map a a -> Doc
prCps Map CheckpointId Substitution
cps
      , Doc
"new substs =" Doc -> Doc -> Doc
<?> forall {a} {a}. (Show a, Pretty a) => Map a a -> Doc
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' a TCState -> m a
useTC Lens' (Map ModuleName CheckpointId) TCState
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' (Map ModuleName CheckpointId) TCState
stModuleCheckpoints forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> 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' a TCEnv -> m a
viewTC (Lens' (Map CheckpointId Substitution) TCEnv
eCheckpoints forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Ord k => k -> Lens' (Maybe v) (Map k 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' i o -> i
^. Lens' (Map ModuleName CheckpointId) TCState
stModuleCheckpoints forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Ord k => k -> Lens' (Maybe v) (Map k 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' :: 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)
    => Name -> Term -> Dom Type -> m a -> m a
  addLetBinding' 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 =>
Name -> Term -> Dom (Type'' Term Term) -> m a -> m a
addLetBinding' 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 (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.
Name -> Term -> Dom (Type'' Term Term) -> ListT m a -> ListT m a
addLetBinding' 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 =>
Name -> Term -> Dom (Type'' Term Term) -> m a -> m a
addLetBinding' 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 -> 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
"registered" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> Doc
"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 -> 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
"all used names: " Doc -> Doc -> Doc
<+> String -> Doc
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' a TCState -> m a
useTC Lens' (Map String (DList String)) TCState
stUsedNames
        forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens Lens' (Map String (DList String)) TCState
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' a TCState -> m a
useTC Lens' (Map String (DList String)) TCState
stUsedNames
        forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens Lens' (Map String (DList String)) TCState
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' a TCState -> (a -> a) -> m ()
modifyTCLens (Lens' (Map String (DList String)) TCState
stUsedNames forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Ord k => k -> Lens' (Maybe v) (Map k 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 -> 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
"names shadowing" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> Doc
": " Doc -> Doc -> Doc
<+>
            forall a. Pretty a => [a] -> Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
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' a TCState -> (a -> a) -> m ()
modifyTCLens Lens' (Map Name (DList String)) TCState
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 a. Bool -> (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. Name -> Term -> Dom (Type'' Term Term) -> TCM a -> TCM a
addLetBinding' Name
x Term
u Dom (Type'' Term Term)
a TCM a
ret = forall a. Bool -> (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) =>
Name -> Term -> Dom (Type'' Term Term) -> m a -> m a
defaultAddLetBinding' 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

getLetBindings :: MonadTCM tcm => tcm [(Name,(Term,Dom Type))]
getLetBindings :: forall (tcm :: * -> *).
MonadTCM tcm =>
tcm [(Name, (Term, Dom (Type'' Term Term)))]
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 (Term, Dom (Type'' Term Term))
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 (Term, Dom (Type'' Term Term))
o

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

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


-- * 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 (Term, Dom (Type'' Term Term))
vt -> forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen Open (Term, Dom (Type'' Term Term))
vt
                    Maybe (Open (Term, Dom (Type'' Term Term)))
_       -> 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
")"