{-| EDSL to construct terms without touching De Bruijn indices.

e.g. if given t, u :: Term, Γ ⊢ t, u : A, we can build "λ f. f t u" like this:

runNames [] $ do
  -- @open@ binds @t@ and @u@ to computations that know how to weaken themselves in
  -- an extended context

  [t,u] <- mapM open [t,u]

  -- @lam@ gives the illusion of HOAS by providing f as a computation
  -- It also extends the internal context with the name "f", so that
  -- @t@ and @u@ will get weakened in the body.
  -- Then we finish the job using the (<@>) combinator from Agda.TypeChecking.Primitive

  lam "f" $ \ f -> f <@> t <@> u

-}
module Agda.TypeChecking.Names where

-- Control.Monad.Fail import is redundant since GHC 8.8.1
import Control.Monad.Fail (MonadFail)

import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State

import Data.List (isSuffixOf)

import Agda.Syntax.Common hiding (Nat)
import Agda.Syntax.Internal

import Agda.TypeChecking.Monad hiding (getConstInfo, typeOfConst)
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free

import Agda.Utils.Fail (Fail, runFail_)

instance HasBuiltins m => HasBuiltins (NamesT m) where
  getBuiltinThing :: String -> NamesT m (Maybe (Builtin PrimFun))
getBuiltinThing String
b = m (Maybe (Builtin PrimFun)) -> NamesT m (Maybe (Builtin PrimFun))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (Builtin PrimFun)) -> NamesT m (Maybe (Builtin PrimFun)))
-> m (Maybe (Builtin PrimFun))
-> NamesT m (Maybe (Builtin PrimFun))
forall a b. (a -> b) -> a -> b
$ String -> m (Maybe (Builtin PrimFun))
forall (m :: * -> *).
HasBuiltins m =>
String -> m (Maybe (Builtin PrimFun))
getBuiltinThing String
b

newtype NamesT m a = NamesT { forall (m :: * -> *) a. NamesT m a -> ReaderT Names m a
unName :: ReaderT Names m a }
  deriving ( (forall a b. (a -> b) -> NamesT m a -> NamesT m b)
-> (forall a b. a -> NamesT m b -> NamesT m a)
-> Functor (NamesT m)
forall a b. a -> NamesT m b -> NamesT m a
forall a b. (a -> b) -> NamesT m a -> NamesT m b
forall (m :: * -> *) a b.
Functor m =>
a -> NamesT m b -> NamesT m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> NamesT m a -> NamesT m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> NamesT m b -> NamesT m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> NamesT m b -> NamesT m a
fmap :: forall a b. (a -> b) -> NamesT m a -> NamesT m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> NamesT m a -> NamesT m b
Functor
           , Functor (NamesT m)
Functor (NamesT m)
-> (forall a. a -> NamesT m a)
-> (forall a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b)
-> (forall a b c.
    (a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c)
-> (forall a b. NamesT m a -> NamesT m b -> NamesT m b)
-> (forall a b. NamesT m a -> NamesT m b -> NamesT m a)
-> Applicative (NamesT m)
forall a. a -> NamesT m a
forall a b. NamesT m a -> NamesT m b -> NamesT m a
forall a b. NamesT m a -> NamesT m b -> NamesT m b
forall a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b
forall a b c.
(a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall {m :: * -> *}. Applicative m => Functor (NamesT m)
forall (m :: * -> *) a. Applicative m => a -> NamesT m a
forall (m :: * -> *) a b.
Applicative m =>
NamesT m a -> NamesT m b -> NamesT m a
forall (m :: * -> *) a b.
Applicative m =>
NamesT m a -> NamesT m b -> NamesT m b
forall (m :: * -> *) a b.
Applicative m =>
NamesT m (a -> b) -> NamesT m a -> NamesT m b
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
<* :: forall a b. NamesT m a -> NamesT m b -> NamesT m a
$c<* :: forall (m :: * -> *) a b.
Applicative m =>
NamesT m a -> NamesT m b -> NamesT m a
*> :: forall a b. NamesT m a -> NamesT m b -> NamesT m b
$c*> :: forall (m :: * -> *) a b.
Applicative m =>
NamesT m a -> NamesT m b -> NamesT m b
liftA2 :: forall a b c.
(a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
$cliftA2 :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
<*> :: forall a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b
$c<*> :: forall (m :: * -> *) a b.
Applicative m =>
NamesT m (a -> b) -> NamesT m a -> NamesT m b
pure :: forall a. a -> NamesT m a
$cpure :: forall (m :: * -> *) a. Applicative m => a -> NamesT m a
Applicative
           , Applicative (NamesT m)
Applicative (NamesT m)
-> (forall a b. NamesT m a -> (a -> NamesT m b) -> NamesT m b)
-> (forall a b. NamesT m a -> NamesT m b -> NamesT m b)
-> (forall a. a -> NamesT m a)
-> Monad (NamesT m)
forall a. a -> NamesT m a
forall a b. NamesT m a -> NamesT m b -> NamesT m b
forall a b. NamesT m a -> (a -> NamesT m b) -> NamesT m b
forall {m :: * -> *}. Monad m => Applicative (NamesT m)
forall (m :: * -> *) a. Monad m => a -> NamesT m a
forall (m :: * -> *) a b.
Monad m =>
NamesT m a -> NamesT m b -> NamesT m b
forall (m :: * -> *) a b.
Monad m =>
NamesT m a -> (a -> NamesT m b) -> NamesT m b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> NamesT m a
$creturn :: forall (m :: * -> *) a. Monad m => a -> NamesT m a
>> :: forall a b. NamesT m a -> NamesT m b -> NamesT m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
NamesT m a -> NamesT m b -> NamesT m b
>>= :: forall a b. NamesT m a -> (a -> NamesT m b) -> NamesT m b
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
NamesT m a -> (a -> NamesT m b) -> NamesT m b
Monad
           , Monad (NamesT m)
Monad (NamesT m)
-> (forall a. String -> NamesT m a) -> MonadFail (NamesT m)
forall a. String -> NamesT m a
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
forall {m :: * -> *}. MonadFail m => Monad (NamesT m)
forall (m :: * -> *) a. MonadFail m => String -> NamesT m a
fail :: forall a. String -> NamesT m a
$cfail :: forall (m :: * -> *) a. MonadFail m => String -> NamesT m a
MonadFail
           , (forall (m :: * -> *) a. Monad m => m a -> NamesT m a)
-> MonadTrans NamesT
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
lift :: forall (m :: * -> *) a. Monad m => m a -> NamesT m a
$clift :: forall (m :: * -> *) a. Monad m => m a -> NamesT m a
MonadTrans
           , MonadState s
           , Monad (NamesT m)
Monad (NamesT m)
-> (forall a. IO a -> NamesT m a) -> MonadIO (NamesT m)
forall a. IO a -> NamesT m a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
forall {m :: * -> *}. MonadIO m => Monad (NamesT m)
forall (m :: * -> *) a. MonadIO m => IO a -> NamesT m a
liftIO :: forall a. IO a -> NamesT m a
$cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> NamesT m a
MonadIO
           , Monad (NamesT m)
Functor (NamesT m)
Applicative (NamesT m)
NamesT m PragmaOptions
NamesT m CommandLineOptions
Functor (NamesT m)
-> Applicative (NamesT m)
-> Monad (NamesT m)
-> NamesT m PragmaOptions
-> NamesT m CommandLineOptions
-> HasOptions (NamesT m)
forall (m :: * -> *).
Functor m
-> Applicative m
-> Monad m
-> m PragmaOptions
-> m CommandLineOptions
-> HasOptions m
forall {m :: * -> *}. HasOptions m => Monad (NamesT m)
forall {m :: * -> *}. HasOptions m => Functor (NamesT m)
forall {m :: * -> *}. HasOptions m => Applicative (NamesT m)
forall (m :: * -> *). HasOptions m => NamesT m PragmaOptions
forall (m :: * -> *). HasOptions m => NamesT m CommandLineOptions
commandLineOptions :: NamesT m CommandLineOptions
$ccommandLineOptions :: forall (m :: * -> *). HasOptions m => NamesT m CommandLineOptions
pragmaOptions :: NamesT m PragmaOptions
$cpragmaOptions :: forall (m :: * -> *). HasOptions m => NamesT m PragmaOptions
HasOptions
           , Monad (NamesT m)
Functor (NamesT m)
Applicative (NamesT m)
NamesT m Bool
NamesT m Verbosity
Functor (NamesT m)
-> Applicative (NamesT m)
-> Monad (NamesT m)
-> (String -> VerboseLevel -> TCM Doc -> NamesT m String)
-> (forall a.
    String -> VerboseLevel -> String -> NamesT m a -> NamesT m a)
-> (forall a.
    String -> VerboseLevel -> String -> NamesT m a -> NamesT m a)
-> NamesT m Verbosity
-> NamesT m Bool
-> (forall a. NamesT m a -> NamesT m a)
-> MonadDebug (NamesT m)
String -> VerboseLevel -> TCM Doc -> NamesT m String
forall a.
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
forall a. NamesT m a -> NamesT m a
forall (m :: * -> *).
Functor m
-> Applicative m
-> Monad m
-> (String -> VerboseLevel -> TCM Doc -> m String)
-> (forall a. String -> VerboseLevel -> String -> m a -> m a)
-> (forall a. String -> VerboseLevel -> String -> m a -> m a)
-> m Verbosity
-> m Bool
-> (forall a. m a -> m a)
-> MonadDebug m
forall {m :: * -> *}. MonadDebug m => Monad (NamesT m)
forall {m :: * -> *}. MonadDebug m => Functor (NamesT m)
forall {m :: * -> *}. MonadDebug m => Applicative (NamesT m)
forall (m :: * -> *). MonadDebug m => NamesT m Bool
forall (m :: * -> *). MonadDebug m => NamesT m Verbosity
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> NamesT m String
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
forall (m :: * -> *) a. MonadDebug m => NamesT m a -> NamesT m a
nowDebugPrinting :: forall a. NamesT m a -> NamesT m a
$cnowDebugPrinting :: forall (m :: * -> *) a. MonadDebug m => NamesT m a -> NamesT m a
isDebugPrinting :: NamesT m Bool
$cisDebugPrinting :: forall (m :: * -> *). MonadDebug m => NamesT m Bool
getVerbosity :: NamesT m Verbosity
$cgetVerbosity :: forall (m :: * -> *). MonadDebug m => NamesT m Verbosity
verboseBracket :: forall a.
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
$cverboseBracket :: forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
traceDebugMessage :: forall a.
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
$ctraceDebugMessage :: forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
formatDebugMessage :: String -> VerboseLevel -> TCM Doc -> NamesT m String
$cformatDebugMessage :: forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> NamesT m String
MonadDebug
           , Monad (NamesT m)
NamesT m TCEnv
Monad (NamesT m)
-> NamesT m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a)
-> MonadTCEnv (NamesT m)
forall a. (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
forall (m :: * -> *).
Monad m
-> m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a)
-> MonadTCEnv m
forall {m :: * -> *}. MonadTCEnv m => Monad (NamesT m)
forall (m :: * -> *). MonadTCEnv m => NamesT m TCEnv
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
localTC :: forall a. (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
$clocalTC :: forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
askTC :: NamesT m TCEnv
$caskTC :: forall (m :: * -> *). MonadTCEnv m => NamesT m TCEnv
MonadTCEnv
           , Monad (NamesT m)
NamesT m TCState
Monad (NamesT m)
-> NamesT m TCState
-> (TCState -> NamesT m ())
-> ((TCState -> TCState) -> NamesT m ())
-> MonadTCState (NamesT m)
TCState -> NamesT m ()
(TCState -> TCState) -> NamesT m ()
forall (m :: * -> *).
Monad m
-> m TCState
-> (TCState -> m ())
-> ((TCState -> TCState) -> m ())
-> MonadTCState m
forall {m :: * -> *}. MonadTCState m => Monad (NamesT m)
forall (m :: * -> *). MonadTCState m => NamesT m TCState
forall (m :: * -> *). MonadTCState m => TCState -> NamesT m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> NamesT m ()
modifyTC :: (TCState -> TCState) -> NamesT m ()
$cmodifyTC :: forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> NamesT m ()
putTC :: TCState -> NamesT m ()
$cputTC :: forall (m :: * -> *). MonadTCState m => TCState -> NamesT m ()
getTC :: NamesT m TCState
$cgetTC :: forall (m :: * -> *). MonadTCState m => NamesT m TCState
MonadTCState
           , Applicative (NamesT m)
MonadIO (NamesT m)
HasOptions (NamesT m)
MonadTCState (NamesT m)
MonadTCEnv (NamesT m)
Applicative (NamesT m)
-> MonadIO (NamesT m)
-> MonadTCEnv (NamesT m)
-> MonadTCState (NamesT m)
-> HasOptions (NamesT m)
-> (forall a. TCM a -> NamesT m a)
-> MonadTCM (NamesT m)
forall a. TCM a -> NamesT m a
forall (tcm :: * -> *).
Applicative tcm
-> MonadIO tcm
-> MonadTCEnv tcm
-> MonadTCState tcm
-> HasOptions tcm
-> (forall a. TCM a -> tcm a)
-> MonadTCM tcm
forall {m :: * -> *}. MonadTCM m => Applicative (NamesT m)
forall {m :: * -> *}. MonadTCM m => MonadIO (NamesT m)
forall {m :: * -> *}. MonadTCM m => HasOptions (NamesT m)
forall {m :: * -> *}. MonadTCM m => MonadTCState (NamesT m)
forall {m :: * -> *}. MonadTCM m => MonadTCEnv (NamesT m)
forall (m :: * -> *) a. MonadTCM m => TCM a -> NamesT m a
liftTCM :: forall a. TCM a -> NamesT m a
$cliftTCM :: forall (m :: * -> *) a. MonadTCM m => TCM a -> NamesT m a
MonadTCM
           , Monad (NamesT m)
NamesT m TCState
Monad (NamesT m)
-> NamesT m TCState
-> (forall a b.
    Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b)
-> (forall a. (TCState -> TCState) -> NamesT m a -> NamesT m a)
-> ReadTCState (NamesT m)
forall a. (TCState -> TCState) -> NamesT m a -> NamesT m a
forall a b. Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
forall (m :: * -> *).
Monad m
-> m TCState
-> (forall a b. Lens' a TCState -> (a -> a) -> m b -> m b)
-> (forall a. (TCState -> TCState) -> m a -> m a)
-> ReadTCState m
forall {m :: * -> *}. ReadTCState m => Monad (NamesT m)
forall (m :: * -> *). ReadTCState m => NamesT m TCState
forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> NamesT m a -> NamesT m a
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
withTCState :: forall a. (TCState -> TCState) -> NamesT m a -> NamesT m a
$cwithTCState :: forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> NamesT m a -> NamesT m a
locallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
$clocallyTCState :: forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
getTCState :: NamesT m TCState
$cgetTCState :: forall (m :: * -> *). ReadTCState m => NamesT m TCState
ReadTCState
           , Applicative (NamesT m)
HasOptions (NamesT m)
MonadTCEnv (NamesT m)
ReadTCState (NamesT m)
Applicative (NamesT m)
-> MonadTCEnv (NamesT m)
-> ReadTCState (NamesT m)
-> HasOptions (NamesT m)
-> (forall a. ReduceM a -> NamesT m a)
-> MonadReduce (NamesT m)
forall a. ReduceM a -> NamesT m a
forall (m :: * -> *).
Applicative m
-> MonadTCEnv m
-> ReadTCState m
-> HasOptions m
-> (forall a. ReduceM a -> m a)
-> MonadReduce m
forall {m :: * -> *}. MonadReduce m => Applicative (NamesT m)
forall {m :: * -> *}. MonadReduce m => HasOptions (NamesT m)
forall {m :: * -> *}. MonadReduce m => MonadTCEnv (NamesT m)
forall {m :: * -> *}. MonadReduce m => ReadTCState (NamesT m)
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> NamesT m a
liftReduce :: forall a. ReduceM a -> NamesT m a
$cliftReduce :: forall (m :: * -> *) a. MonadReduce m => ReduceM a -> NamesT m a
MonadReduce
           , MonadError e
           , MonadTCEnv (NamesT m)
MonadTCEnv (NamesT m)
-> (forall a. Name -> Dom Type -> NamesT m a -> NamesT m a)
-> (forall a. Name -> Term -> Dom Type -> NamesT m a -> NamesT m a)
-> (forall a.
    Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a)
-> (forall a.
    Range -> String -> (Name -> NamesT m a) -> NamesT m a)
-> MonadAddContext (NamesT m)
forall a. Range -> String -> (Name -> NamesT m a) -> NamesT m a
forall a. Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
forall a. Name -> Dom Type -> NamesT m a -> NamesT m a
forall a.
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
forall (m :: * -> *).
MonadTCEnv m
-> (forall a. Name -> Dom Type -> m a -> m a)
-> (forall a. Name -> Term -> Dom Type -> m a -> m a)
-> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
-> (forall a. Range -> String -> (Name -> m a) -> m a)
-> MonadAddContext m
forall {m :: * -> *}. MonadAddContext m => MonadTCEnv (NamesT m)
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> String -> (Name -> NamesT m a) -> NamesT m a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> NamesT m a -> NamesT m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
withFreshName :: forall a. Range -> String -> (Name -> NamesT m a) -> NamesT m a
$cwithFreshName :: forall (m :: * -> *) a.
MonadAddContext m =>
Range -> String -> (Name -> NamesT m a) -> NamesT m a
updateContext :: forall a.
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
$cupdateContext :: forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
addLetBinding' :: forall a. Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
$caddLetBinding' :: forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
addCtx :: forall a. Name -> Dom Type -> NamesT m a -> NamesT m a
$caddCtx :: forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> NamesT m a -> NamesT m a
MonadAddContext
           , Functor (NamesT m)
MonadFail (NamesT m)
Applicative (NamesT m)
MonadDebug (NamesT m)
HasOptions (NamesT m)
MonadTCEnv (NamesT m)
Functor (NamesT m)
-> Applicative (NamesT m)
-> MonadFail (NamesT m)
-> HasOptions (NamesT m)
-> MonadDebug (NamesT m)
-> MonadTCEnv (NamesT m)
-> (QName -> NamesT m Definition)
-> (QName -> NamesT m (Either SigError Definition))
-> (QName -> NamesT m RewriteRules)
-> HasConstInfo (NamesT m)
QName -> NamesT m RewriteRules
QName -> NamesT m (Either SigError Definition)
QName -> NamesT m Definition
forall (m :: * -> *).
Functor m
-> Applicative m
-> MonadFail m
-> HasOptions m
-> MonadDebug m
-> MonadTCEnv m
-> (QName -> m Definition)
-> (QName -> m (Either SigError Definition))
-> (QName -> m RewriteRules)
-> HasConstInfo m
forall {m :: * -> *}. HasConstInfo m => Functor (NamesT m)
forall {m :: * -> *}. HasConstInfo m => MonadFail (NamesT m)
forall {m :: * -> *}. HasConstInfo m => Applicative (NamesT m)
forall {m :: * -> *}. HasConstInfo m => MonadDebug (NamesT m)
forall {m :: * -> *}. HasConstInfo m => HasOptions (NamesT m)
forall {m :: * -> *}. HasConstInfo m => MonadTCEnv (NamesT m)
forall (m :: * -> *).
HasConstInfo m =>
QName -> NamesT m RewriteRules
forall (m :: * -> *).
HasConstInfo m =>
QName -> NamesT m (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> NamesT m Definition
getRewriteRulesFor :: QName -> NamesT m RewriteRules
$cgetRewriteRulesFor :: forall (m :: * -> *).
HasConstInfo m =>
QName -> NamesT m RewriteRules
getConstInfo' :: QName -> NamesT m (Either SigError Definition)
$cgetConstInfo' :: forall (m :: * -> *).
HasConstInfo m =>
QName -> NamesT m (Either SigError Definition)
getConstInfo :: QName -> NamesT m Definition
$cgetConstInfo :: forall (m :: * -> *).
HasConstInfo m =>
QName -> NamesT m Definition
HasConstInfo
           , MonadDebug (NamesT m)
MonadTCEnv (NamesT m)
MonadReduce (NamesT m)
ReadTCState (NamesT m)
MonadAddContext (NamesT m)
HasBuiltins (NamesT m)
HasConstInfo (NamesT m)
HasBuiltins (NamesT m)
-> HasConstInfo (NamesT m)
-> MonadAddContext (NamesT m)
-> MonadDebug (NamesT m)
-> MonadReduce (NamesT m)
-> MonadTCEnv (NamesT m)
-> ReadTCState (NamesT m)
-> PureTCM (NamesT m)
forall (m :: * -> *).
HasBuiltins m
-> HasConstInfo m
-> MonadAddContext m
-> MonadDebug m
-> MonadReduce m
-> MonadTCEnv m
-> ReadTCState m
-> PureTCM m
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadDebug (NamesT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadTCEnv (NamesT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadReduce (NamesT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
ReadTCState (NamesT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadAddContext (NamesT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
HasBuiltins (NamesT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
HasConstInfo (NamesT m)
PureTCM
           )

-- deriving instance MonadState s m => MonadState s (NamesT m)

type Names = [String]

runNamesT :: Names -> NamesT m a -> m a
runNamesT :: forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT Names
n NamesT m a
m = ReaderT Names m a -> Names -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (NamesT m a -> ReaderT Names m a
forall (m :: * -> *) a. NamesT m a -> ReaderT Names m a
unName NamesT m a
m) Names
n

-- We use @Fail@ instead of @Identity@ because the computation can fail.
runNames :: Names -> NamesT Fail a -> a
runNames :: forall a. Names -> NamesT Fail a -> a
runNames Names
n NamesT Fail a
m = Fail a -> a
forall a. Fail a -> a
runFail_ (Names -> NamesT Fail a -> Fail a
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT Names
n NamesT Fail a
m)

currentCxt :: Monad m => NamesT m Names
currentCxt :: forall (m :: * -> *). Monad m => NamesT m Names
currentCxt = ReaderT Names m Names -> NamesT m Names
forall (m :: * -> *) a. ReaderT Names m a -> NamesT m a
NamesT ReaderT Names m Names
forall r (m :: * -> *). MonadReader r m => m r
ask

cxtSubst :: MonadFail m => Names -> NamesT m (Substitution' a)
cxtSubst :: forall (m :: * -> *) a.
MonadFail m =>
Names -> NamesT m (Substitution' a)
cxtSubst Names
ctx = do
  Names
ctx' <- NamesT m Names
forall (m :: * -> *). Monad m => NamesT m Names
currentCxt
  if (Names
ctx Names -> Names -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` Names
ctx')
     then Substitution' a -> NamesT m (Substitution' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Substitution' a -> NamesT m (Substitution' a))
-> Substitution' a -> NamesT m (Substitution' a)
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Substitution' a
forall a. VerboseLevel -> Substitution' a
raiseS (Names -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Names
ctx' VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- Names -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Names
ctx)
     else String -> NamesT m (Substitution' a)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> NamesT m (Substitution' a))
-> String -> NamesT m (Substitution' a)
forall a b. (a -> b) -> a -> b
$ String
"thing out of context (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Names -> String
forall a. Show a => a -> String
show Names
ctx String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not a sub context of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Names -> String
forall a. Show a => a -> String
show Names
ctx' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

inCxt :: (MonadFail m, Subst a) => Names -> a -> NamesT m a
inCxt :: forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
Names -> a -> NamesT m a
inCxt Names
ctx a
a = do
  Substitution' (SubstArg a)
sigma <- Names -> NamesT m (Substitution' (SubstArg a))
forall (m :: * -> *) a.
MonadFail m =>
Names -> NamesT m (Substitution' a)
cxtSubst Names
ctx
  a -> NamesT m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> NamesT m a) -> a -> NamesT m a
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
sigma a
a

-- closed terms
cl' :: Applicative m => a -> NamesT m a
cl' :: forall (m :: * -> *) a. Applicative m => a -> NamesT m a
cl' = a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

cl :: Monad m => m a -> NamesT m a
cl :: forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl = m a -> NamesT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

open :: (MonadFail m, Subst a) => a -> NamesT m (NamesT m a)
open :: forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open a
a = do
  Names
ctx <- ReaderT Names m Names -> NamesT m Names
forall (m :: * -> *) a. ReaderT Names m a -> NamesT m a
NamesT ReaderT Names m Names
forall r (m :: * -> *). MonadReader r m => m r
ask
  NamesT m a -> NamesT m (NamesT m a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NamesT m a -> NamesT m (NamesT m a))
-> NamesT m a -> NamesT m (NamesT m a)
forall a b. (a -> b) -> a -> b
$ Names -> a -> NamesT m a
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
Names -> a -> NamesT m a
inCxt Names
ctx a
a

bind' :: (MonadFail m, Subst b, DeBruijn b, Subst a, Free a) => ArgName -> (NamesT m b -> NamesT m a) -> NamesT m a
bind' :: forall (m :: * -> *) b a.
(MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
String -> (NamesT m b -> NamesT m a) -> NamesT m a
bind' String
n NamesT m b -> NamesT m a
f = do
  Names
cxt <- ReaderT Names m Names -> NamesT m Names
forall (m :: * -> *) a. ReaderT Names m a -> NamesT m a
NamesT ReaderT Names m Names
forall r (m :: * -> *). MonadReader r m => m r
ask
  (ReaderT Names m a -> NamesT m a
forall (m :: * -> *) a. ReaderT Names m a -> NamesT m a
NamesT (ReaderT Names m a -> NamesT m a)
-> (NamesT m a -> ReaderT Names m a) -> NamesT m a -> NamesT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Names -> Names) -> ReaderT Names m a -> ReaderT Names m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (String
nString -> Names -> Names
forall a. a -> [a] -> [a]
:) (ReaderT Names m a -> ReaderT Names m a)
-> (NamesT m a -> ReaderT Names m a)
-> NamesT m a
-> ReaderT Names m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamesT m a -> ReaderT Names m a
forall (m :: * -> *) a. NamesT m a -> ReaderT Names m a
unName (NamesT m a -> NamesT m a) -> NamesT m a -> NamesT m a
forall a b. (a -> b) -> a -> b
$ NamesT m b -> NamesT m a
f (Names -> b -> NamesT m b
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
Names -> a -> NamesT m a
inCxt (String
nString -> Names -> Names
forall a. a -> [a] -> [a]
:Names
cxt) (VerboseLevel -> b
forall a. DeBruijn a => VerboseLevel -> a
deBruijnVar VerboseLevel
0)))

bind :: ( MonadFail m
        , Subst b
        , DeBruijn b
        , Subst a
        , Free a
        ) =>
        ArgName -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
bind :: forall (m :: * -> *) b a.
(MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
String -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
bind String
n NamesT m b -> NamesT m a
f = String -> a -> Abs a
forall a. String -> a -> Abs a
Abs String
n (a -> Abs a) -> NamesT m a -> NamesT m (Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> (NamesT m b -> NamesT m a) -> NamesT m a
forall (m :: * -> *) b a.
(MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
String -> (NamesT m b -> NamesT m a) -> NamesT m a
bind' String
n NamesT m b -> NamesT m a
f

glam :: MonadFail m
     => ArgInfo -> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam :: forall (m :: * -> *).
MonadFail m =>
ArgInfo
-> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam ArgInfo
info String
n NamesT m Term -> NamesT m Term
f = ArgInfo -> Abs Term -> Term
Lam ArgInfo
info (Abs Term -> Term) -> NamesT m (Abs Term) -> NamesT m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> (NamesT m Term -> NamesT m Term) -> NamesT m (Abs Term)
forall (m :: * -> *) b a.
(MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
String -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
bind String
n NamesT m Term -> NamesT m Term
f

glamN :: (Functor m, MonadFail m) =>
         [Arg ArgName] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
glamN :: forall (m :: * -> *).
(Functor m, MonadFail m) =>
[Arg String] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
glamN [] NamesT m Args -> NamesT m Term
f = NamesT m Args -> NamesT m Term
f (NamesT m Args -> NamesT m Term) -> NamesT m Args -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ Args -> NamesT m Args
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
glamN (Arg ArgInfo
i String
n:[Arg String]
ns) NamesT m Args -> NamesT m Term
f = ArgInfo
-> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
ArgInfo
-> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam ArgInfo
i String
n ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
x -> [Arg String] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
(Functor m, MonadFail m) =>
[Arg String] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
glamN [Arg String]
ns (\ NamesT m Args
xs -> NamesT m Args -> NamesT m Term
f ((:) (Arg Term -> Args -> Args)
-> NamesT m (Arg Term) -> NamesT m (Args -> Args)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Term -> Arg Term) -> NamesT m Term -> NamesT m (Arg Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT m Term
x) NamesT m (Args -> Args) -> NamesT m Args -> NamesT m Args
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT m Args
xs))

lam :: MonadFail m
    => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam :: forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
n NamesT m Term -> NamesT m Term
f = ArgInfo
-> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
ArgInfo
-> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam ArgInfo
defaultArgInfo String
n NamesT m Term -> NamesT m Term
f

ilam :: MonadFail m
    => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam :: forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
n NamesT m Term -> NamesT m Term
f = ArgInfo
-> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
ArgInfo
-> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam (Relevance -> ArgInfo -> ArgInfo
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant ArgInfo
defaultArgInfo) String
n NamesT m Term -> NamesT m Term
f