{-| 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          ( liftM2, unless )
import Control.Monad.Except   ( MonadError )
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.Reader   ( MonadReader(..), ReaderT, runReaderT )
import Control.Monad.State    ( MonadState )
import Control.Monad.Trans    ( MonadTrans, lift )

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 :: * -> *). Monad m => Monad (NamesT m))
-> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a)
-> MonadTrans NamesT
forall (m :: * -> *). Monad m => Monad (NamesT m)
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *). Monad m => Monad (t m))
-> (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