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

e.g. 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.
  -- We apply f with the (<@>) combinator from Agda.TypeChecking.Primitive.

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

-}
module Agda.TypeChecking.Names where

import Control.Monad          ( liftM2, unless )
import Control.Monad.Except   ( MonadError )
import Control.Monad.Identity ( Identity, runIdentity )
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.Telescope
import Agda.TypeChecking.Pretty ()  -- instances only

import Agda.Utils.Fail (Fail, runFail_)
import Agda.Utils.List1 ( List1, pattern (:|) )
import Agda.Utils.Impossible

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
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> NamesT m a -> NamesT m b
fmap :: forall a b. (a -> b) -> NamesT m a -> NamesT m b
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> NamesT m b -> NamesT m a
<$ :: forall a b. a -> NamesT m b -> NamesT m a
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
$cpure :: forall (m :: * -> *) a. Applicative m => a -> NamesT m a
pure :: forall a. a -> NamesT m a
$c<*> :: forall (m :: * -> *) a b.
Applicative m =>
NamesT m (a -> b) -> NamesT m a -> NamesT m b
<*> :: forall a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b
$cliftA2 :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
liftA2 :: forall a b c.
(a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
$c*> :: forall (m :: * -> *) a b.
Applicative m =>
NamesT m a -> NamesT m b -> NamesT m b
*> :: 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 a
<* :: forall a b. NamesT m a -> NamesT m b -> 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
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
NamesT m a -> (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 -> NamesT m b -> NamesT m b
>> :: forall a b. NamesT m a -> NamesT m b -> NamesT m b
$creturn :: forall (m :: * -> *) a. Monad m => a -> NamesT m a
return :: forall a. a -> NamesT m a
Monad
           , (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
$clift :: forall (m :: * -> *) a. Monad m => m a -> NamesT m a
lift :: 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
$cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> NamesT m a
liftIO :: forall a. 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
$cpragmaOptions :: forall (m :: * -> *). HasOptions m => NamesT m PragmaOptions
pragmaOptions :: NamesT m PragmaOptions
$ccommandLineOptions :: forall (m :: * -> *). HasOptions m => NamesT m CommandLineOptions
commandLineOptions :: NamesT m CommandLineOptions
HasOptions
           , Monad (NamesT m)
Functor (NamesT m)
Applicative (NamesT m)
NamesT m Bool
NamesT m Verbosity
NamesT m ProfileOptions
(Functor (NamesT m), Applicative (NamesT m), Monad (NamesT m)) =>
(VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m VerboseKey)
-> (forall a.
    VerboseKey
    -> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a)
-> (forall a.
    VerboseKey
    -> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a)
-> NamesT m Verbosity
-> NamesT m ProfileOptions
-> NamesT m Bool
-> (forall a. NamesT m a -> NamesT m a)
-> MonadDebug (NamesT m)
VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m VerboseKey
forall a.
VerboseKey
-> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a
forall a. NamesT m a -> NamesT m a
forall (m :: * -> *).
(Functor m, Applicative m, Monad m) =>
(VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey)
-> (forall a.
    VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a)
-> (forall a.
    VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a)
-> m Verbosity
-> m ProfileOptions
-> 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 => NamesT m ProfileOptions
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m VerboseKey
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey
-> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a
forall (m :: * -> *) a. MonadDebug m => NamesT m a -> NamesT m a
$cformatDebugMessage :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m VerboseKey
formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m VerboseKey
$ctraceDebugMessage :: forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey
-> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a
traceDebugMessage :: forall a.
VerboseKey
-> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a
$cverboseBracket :: forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey
-> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a
verboseBracket :: forall a.
VerboseKey
-> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a
$cgetVerbosity :: forall (m :: * -> *). MonadDebug m => NamesT m Verbosity
getVerbosity :: NamesT m Verbosity
$cgetProfileOptions :: forall (m :: * -> *). MonadDebug m => NamesT m ProfileOptions
getProfileOptions :: NamesT m ProfileOptions
$cisDebugPrinting :: forall (m :: * -> *). MonadDebug m => NamesT m Bool
isDebugPrinting :: NamesT m Bool
$cnowDebugPrinting :: forall (m :: * -> *) a. MonadDebug m => NamesT m a -> NamesT m a
nowDebugPrinting :: forall a. NamesT m a -> NamesT m a
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
$caskTC :: forall (m :: * -> *). MonadTCEnv m => NamesT m TCEnv
askTC :: NamesT m TCEnv
$clocalTC :: forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
localTC :: forall a. (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
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 ()
$cgetTC :: forall (m :: * -> *). MonadTCState m => NamesT m TCState
getTC :: NamesT m TCState
$cputTC :: forall (m :: * -> *). MonadTCState m => TCState -> NamesT m ()
putTC :: TCState -> NamesT m ()
$cmodifyTC :: forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> NamesT m ()
modifyTC :: (TCState -> TCState) -> NamesT m ()
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
$cliftTCM :: forall (m :: * -> *) a. MonadTCM m => TCM a -> NamesT m a
liftTCM :: forall a. TCM a -> NamesT m a
MonadTCM
           , Monad (NamesT m)
NamesT m TCState
Monad (NamesT m) =>
NamesT m TCState
-> (forall a b.
    Lens' TCState a -> (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' TCState a -> (a -> a) -> NamesT m b -> NamesT m b
forall (m :: * -> *).
Monad m =>
m TCState
-> (forall a b. Lens' TCState a -> (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' TCState a -> (a -> a) -> NamesT m b -> NamesT m b
$cgetTCState :: forall (m :: * -> *). ReadTCState m => NamesT m TCState
getTCState :: NamesT m TCState
$clocallyTCState :: forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> NamesT m b -> NamesT m b
locallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> NamesT m b -> NamesT m b
$cwithTCState :: forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> NamesT m a -> NamesT m a
withTCState :: forall a. (TCState -> TCState) -> NamesT m a -> NamesT m a
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
$cliftReduce :: forall (m :: * -> *) a. MonadReduce m => ReduceM a -> NamesT m a
liftReduce :: forall a. 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.
    Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a)
-> (forall a.
    Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a)
-> (forall a.
    Range -> VerboseKey -> (Name -> NamesT m a) -> NamesT m a)
-> MonadAddContext (NamesT m)
forall a. Range -> VerboseKey -> (Name -> NamesT m a) -> NamesT m a
forall a.
Origin -> 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. Origin -> Name -> Term -> Dom Type -> m a -> m a)
-> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
-> (forall a. Range -> VerboseKey -> (Name -> m a) -> m a)
-> MonadAddContext m
forall (m :: * -> *). MonadAddContext m => MonadTCEnv (NamesT m)
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> VerboseKey -> (Name -> NamesT m a) -> NamesT m a
forall (m :: * -> *) a.
MonadAddContext m =>
Origin -> 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
$caddCtx :: forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> NamesT m a -> NamesT m a
addCtx :: forall a. Name -> Dom Type -> NamesT m a -> NamesT m a
$caddLetBinding' :: forall (m :: * -> *) a.
MonadAddContext m =>
Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
addLetBinding' :: forall a.
Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
$cupdateContext :: forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
updateContext :: forall a.
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
$cwithFreshName :: forall (m :: * -> *) a.
MonadAddContext m =>
Range -> VerboseKey -> (Name -> NamesT m a) -> NamesT m a
withFreshName :: forall a. Range -> VerboseKey -> (Name -> NamesT m a) -> NamesT m a
MonadAddContext
           , Monad (NamesT m)
Functor (NamesT m)
Applicative (NamesT m)
(Functor (NamesT m), Applicative (NamesT m), Monad (NamesT m)) =>
(SomeBuiltin -> NamesT m (Maybe (Builtin PrimFun)))
-> HasBuiltins (NamesT m)
SomeBuiltin -> NamesT m (Maybe (Builtin PrimFun))
forall (m :: * -> *).
(Functor m, Applicative m, Monad m) =>
(SomeBuiltin -> m (Maybe (Builtin PrimFun))) -> HasBuiltins m
forall (m :: * -> *). HasBuiltins m => Monad (NamesT m)
forall (m :: * -> *). HasBuiltins m => Functor (NamesT m)
forall (m :: * -> *). HasBuiltins m => Applicative (NamesT m)
forall (m :: * -> *).
HasBuiltins m =>
SomeBuiltin -> NamesT m (Maybe (Builtin PrimFun))
$cgetBuiltinThing :: forall (m :: * -> *).
HasBuiltins m =>
SomeBuiltin -> NamesT m (Maybe (Builtin PrimFun))
getBuiltinThing :: SomeBuiltin -> NamesT m (Maybe (Builtin PrimFun))
HasBuiltins
           , Functor (NamesT m)
Applicative (NamesT m)
HasOptions (NamesT m)
MonadTCEnv (NamesT m)
MonadDebug (NamesT m)
(Functor (NamesT m), Applicative (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, 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 => Applicative (NamesT m)
forall (m :: * -> *). HasConstInfo m => HasOptions (NamesT m)
forall (m :: * -> *). HasConstInfo m => MonadTCEnv (NamesT m)
forall (m :: * -> *). HasConstInfo m => MonadDebug (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
$cgetConstInfo :: forall (m :: * -> *).
HasConstInfo m =>
QName -> NamesT m Definition
getConstInfo :: QName -> NamesT m Definition
$cgetConstInfo' :: forall (m :: * -> *).
HasConstInfo m =>
QName -> NamesT m (Either SigError Definition)
getConstInfo' :: QName -> NamesT m (Either SigError Definition)
$cgetRewriteRulesFor :: forall (m :: * -> *).
HasConstInfo m =>
QName -> NamesT m RewriteRules
getRewriteRulesFor :: QName -> NamesT m RewriteRules
HasConstInfo
           , MonadTCEnv (NamesT m)
MonadReduce (NamesT m)
ReadTCState (NamesT m)
HasBuiltins (NamesT m)
MonadAddContext (NamesT m)
MonadDebug (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,
 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) =>
HasBuiltins (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) =>
MonadDebug (NamesT m)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
HasConstInfo (NamesT m)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadDebug m,
 MonadReduce m, MonadTCEnv m, ReadTCState m) =>
PureTCM m
PureTCM
           )


-- | A list of variable names from a context.
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

runNames :: Names -> NamesT Identity a -> a
runNames :: forall a. Names -> NamesT Identity a -> a
runNames Names
n NamesT Identity a
m = Identity a -> a
forall a. Identity a -> a
runIdentity (Names -> NamesT Identity a -> Identity a
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT Names
n NamesT Identity 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

{-# INLINABLE cxtSubst #-}
-- | @cxtSubst Γ@ returns the substitution needed to go
--   from Γ to the current context.
--
--   Precondition @Γ@ is not a subcontext of the current one.
cxtSubst :: Monad m => Names -> NamesT m (Substitution' a)
cxtSubst :: forall (m :: * -> *) a.
Monad m =>
Names -> NamesT m (Substitution' a)
cxtSubst Names
ctx = do
  ctx' <- NamesT m Names
forall (m :: * -> *). Monad m => NamesT m Names
currentCxt
  if (ctx `isSuffixOf` ctx')
     then return $ raiseS (length ctx' - length ctx)
     else
      -- trace ("out of context (" ++ show ctx ++ " is not a sub context of " ++ show ctx' ++ ")")
       __IMPOSSIBLE__


{-# INLINABLE inCxt #-}
-- | @inCxt Γ t@ takes a @t@ in context @Γ@ and produce an action that
--   will return @t@ weakened to the current context.
--
--   Fails whenever @cxtSubst Γ@ would.
inCxt :: (Monad m, Subst a) => Names -> a -> NamesT m a
inCxt :: forall (m :: * -> *) a.
(Monad m, Subst a) =>
Names -> a -> NamesT m a
inCxt Names
ctx a
a = do
  sigma <- Names -> NamesT m (Substitution' (SubstArg a))
forall (m :: * -> *) a.
Monad m =>
Names -> NamesT m (Substitution' a)
cxtSubst Names
ctx
  return $ applySubst sigma 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 a. 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 (m :: * -> *) a. Monad m => m a -> NamesT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

{-# INLINABLE open #-}
-- | Open terms in the current context.
open :: (Monad m, Subst a) => a -> NamesT m (NamesT m a)
open :: forall (m :: * -> *) a.
(Monad m, Subst a) =>
a -> NamesT m (NamesT m a)
open a
a = do
  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
  pure $ inCxt ctx a

-- | Monadic actions standing for variables.
--
--   @b@ is quantified over so the same variable can be used e.g. both
--   as a pattern and as an expression.
type Var m = forall b. (Subst b, DeBruijn b) => NamesT m b


{-# INLINE bind #-}
-- | @bind n f@ provides @f@ with a fresh variable, which can be used in any extended context.
--
--   Returns an @Abs@ which binds the extra variable.
bind :: Monad m => ArgName -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a) -> NamesT m (Abs a)
bind :: forall (m :: * -> *) a.
Monad m =>
VerboseKey
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind VerboseKey
n (forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a
f = VerboseKey -> a -> Abs a
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
n (a -> Abs a) -> NamesT m a -> NamesT m (Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseKey
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m a
forall (m :: * -> *) a.
Monad m =>
VerboseKey
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m a
bind' VerboseKey
n (forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a
f

{-# INLINABLE bind' #-}
-- | Like @bind@ but returns a bare term.
bind' :: Monad m => ArgName -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a) -> NamesT m a
bind' :: forall (m :: * -> *) a.
Monad m =>
VerboseKey
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m a
bind' VerboseKey
n (forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a
f = do
  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
  (NamesT . local (n:) . unName $ f (inCxt (n:cxt) (deBruijnVar 0)))


-- * Helpers to build lambda abstractions.

glam :: Monad m
     => ArgInfo -> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam :: forall (m :: * -> *).
Monad m =>
ArgInfo
-> VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam ArgInfo
info VerboseKey
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
<$> VerboseKey
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
    -> NamesT m Term)
-> NamesT m (Abs Term)
forall (m :: * -> *) a.
Monad m =>
VerboseKey
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind VerboseKey
n (\ forall b. (Subst b, DeBruijn b) => NamesT m b
x -> NamesT m Term -> NamesT m Term
f NamesT m Term
forall b. (Subst b, DeBruijn b) => NamesT m b
x)

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

ilam :: Monad m
    => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam :: forall (m :: * -> *).
Monad m =>
VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam VerboseKey
n NamesT m Term -> NamesT m Term
f = ArgInfo
-> VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
Monad m =>
ArgInfo
-> VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam ArgInfo
defaultIrrelevantArgInfo VerboseKey
n NamesT m Term -> NamesT m Term
f


-- * Combinators for n-ary binders.

data AbsN a = AbsN { forall a. AbsN a -> Names
absNName :: [ArgName], forall a. AbsN a -> a
unAbsN :: a } deriving ((forall a b. (a -> b) -> AbsN a -> AbsN b)
-> (forall a b. a -> AbsN b -> AbsN a) -> Functor AbsN
forall a b. a -> AbsN b -> AbsN a
forall a b. (a -> b) -> AbsN a -> AbsN b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> AbsN a -> AbsN b
fmap :: forall a b. (a -> b) -> AbsN a -> AbsN b
$c<$ :: forall a b. a -> AbsN b -> AbsN a
<$ :: forall a b. a -> AbsN b -> AbsN a
Functor,(forall m. Monoid m => AbsN m -> m)
-> (forall m a. Monoid m => (a -> m) -> AbsN a -> m)
-> (forall m a. Monoid m => (a -> m) -> AbsN a -> m)
-> (forall a b. (a -> b -> b) -> b -> AbsN a -> b)
-> (forall a b. (a -> b -> b) -> b -> AbsN a -> b)
-> (forall b a. (b -> a -> b) -> b -> AbsN a -> b)
-> (forall b a. (b -> a -> b) -> b -> AbsN a -> b)
-> (forall a. (a -> a -> a) -> AbsN a -> a)
-> (forall a. (a -> a -> a) -> AbsN a -> a)
-> (forall a. AbsN a -> [a])
-> (forall a. AbsN a -> Bool)
-> (forall a. AbsN a -> VerboseLevel)
-> (forall a. Eq a => a -> AbsN a -> Bool)
-> (forall a. Ord a => AbsN a -> a)
-> (forall a. Ord a => AbsN a -> a)
-> (forall a. Num a => AbsN a -> a)
-> (forall a. Num a => AbsN a -> a)
-> Foldable AbsN
forall a. Eq a => a -> AbsN a -> Bool
forall a. Num a => AbsN a -> a
forall a. Ord a => AbsN a -> a
forall m. Monoid m => AbsN m -> m
forall a. AbsN a -> Bool
forall a. AbsN a -> VerboseLevel
forall a. AbsN a -> [a]
forall a. (a -> a -> a) -> AbsN a -> a
forall m a. Monoid m => (a -> m) -> AbsN a -> m
forall b a. (b -> a -> b) -> b -> AbsN a -> b
forall a b. (a -> b -> b) -> b -> AbsN a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> VerboseLevel)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => AbsN m -> m
fold :: forall m. Monoid m => AbsN m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> AbsN a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> AbsN a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> AbsN a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> AbsN a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> AbsN a -> b
foldr :: forall a b. (a -> b -> b) -> b -> AbsN a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> AbsN a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> AbsN a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> AbsN a -> b
foldl :: forall b a. (b -> a -> b) -> b -> AbsN a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> AbsN a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> AbsN a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> AbsN a -> a
foldr1 :: forall a. (a -> a -> a) -> AbsN a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> AbsN a -> a
foldl1 :: forall a. (a -> a -> a) -> AbsN a -> a
$ctoList :: forall a. AbsN a -> [a]
toList :: forall a. AbsN a -> [a]
$cnull :: forall a. AbsN a -> Bool
null :: forall a. AbsN a -> Bool
$clength :: forall a. AbsN a -> VerboseLevel
length :: forall a. AbsN a -> VerboseLevel
$celem :: forall a. Eq a => a -> AbsN a -> Bool
elem :: forall a. Eq a => a -> AbsN a -> Bool
$cmaximum :: forall a. Ord a => AbsN a -> a
maximum :: forall a. Ord a => AbsN a -> a
$cminimum :: forall a. Ord a => AbsN a -> a
minimum :: forall a. Ord a => AbsN a -> a
$csum :: forall a. Num a => AbsN a -> a
sum :: forall a. Num a => AbsN a -> a
$cproduct :: forall a. Num a => AbsN a -> a
product :: forall a. Num a => AbsN a -> a
Foldable,Functor AbsN
Foldable AbsN
(Functor AbsN, Foldable AbsN) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> AbsN a -> f (AbsN b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    AbsN (f a) -> f (AbsN a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> AbsN a -> m (AbsN b))
-> (forall (m :: * -> *) a. Monad m => AbsN (m a) -> m (AbsN a))
-> Traversable AbsN
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => AbsN (m a) -> m (AbsN a)
forall (f :: * -> *) a. Applicative f => AbsN (f a) -> f (AbsN a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> AbsN a -> m (AbsN b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> AbsN a -> f (AbsN b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> AbsN a -> f (AbsN b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> AbsN a -> f (AbsN b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => AbsN (f a) -> f (AbsN a)
sequenceA :: forall (f :: * -> *) a. Applicative f => AbsN (f a) -> f (AbsN a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> AbsN a -> m (AbsN b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> AbsN a -> m (AbsN b)
$csequence :: forall (m :: * -> *) a. Monad m => AbsN (m a) -> m (AbsN a)
sequence :: forall (m :: * -> *) a. Monad m => AbsN (m a) -> m (AbsN a)
Traversable)

instance Subst a => Subst (AbsN a) where
  type SubstArg (AbsN a) = SubstArg a
  applySubst :: Substitution' (SubstArg (AbsN a)) -> AbsN a -> AbsN a
applySubst Substitution' (SubstArg (AbsN a))
rho (AbsN Names
xs a
a) = Names -> a -> AbsN a
forall a. Names -> a -> AbsN a
AbsN Names
xs (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (VerboseLevel
-> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
forall a. VerboseLevel -> Substitution' a -> Substitution' a
liftS (Names -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Names
xs) Substitution' (SubstArg a)
Substitution' (SubstArg (AbsN a))
rho) a
a)

-- | Will crash on @NoAbs@
toAbsN :: Abs (AbsN a) -> AbsN a
toAbsN :: forall a. Abs (AbsN a) -> AbsN a
toAbsN (Abs VerboseKey
n AbsN a
x') = Names -> a -> AbsN a
forall a. Names -> a -> AbsN a
AbsN (VerboseKey
n VerboseKey -> Names -> Names
forall a. a -> [a] -> [a]
: AbsN a -> Names
forall a. AbsN a -> Names
absNName AbsN a
x') (AbsN a -> a
forall a. AbsN a -> a
unAbsN AbsN a
x')
toAbsN NoAbs{}    = AbsN a
forall a. HasCallStack => a
__IMPOSSIBLE__

{-# INLINABLE absAppN #-}
absAppN :: Subst a => AbsN a -> [SubstArg a] -> a
absAppN :: forall a. Subst a => AbsN a -> [SubstArg a] -> a
absAppN AbsN a
f [SubstArg a]
xs = [SubstArg a] -> Substitution' (SubstArg a)
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([SubstArg a] -> [SubstArg a]
forall a. [a] -> [a]
reverse [SubstArg a]
xs) Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` AbsN a -> a
forall a. AbsN a -> a
unAbsN AbsN a
f

type ArgVars m = (forall b. (Subst b, DeBruijn b) => [NamesT m (Arg b)])

type Vars m = (forall b. (Subst b, DeBruijn b) => [NamesT m b])

{-# INLINABLE bindN #-}
bindN :: ( Monad m
        ) =>
        [ArgName] -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
bindN :: forall (m :: * -> *) a.
Monad m =>
Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
bindN [] Vars m -> NamesT m a
f = Names -> a -> AbsN a
forall a. Names -> a -> AbsN a
AbsN [] (a -> AbsN a) -> NamesT m a -> NamesT m (AbsN a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Vars m -> NamesT m a
f []
bindN (VerboseKey
x:Names
xs) Vars m -> NamesT m a
f = Abs (AbsN a) -> AbsN a
forall a. Abs (AbsN a) -> AbsN a
toAbsN (Abs (AbsN a) -> AbsN a)
-> NamesT m (Abs (AbsN a)) -> NamesT m (AbsN a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseKey
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
    -> NamesT m (AbsN a))
-> NamesT m (Abs (AbsN a))
forall (m :: * -> *) a.
Monad m =>
VerboseKey
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind VerboseKey
x (\ forall b. (Subst b, DeBruijn b) => NamesT m b
x -> Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
forall (m :: * -> *) a.
Monad m =>
Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
bindN Names
xs (\ Vars m
xs -> Vars m -> NamesT m a
f (NamesT m b
forall b. (Subst b, DeBruijn b) => NamesT m b
xNamesT m b -> [NamesT m b] -> [NamesT m b]
forall a. a -> [a] -> [a]
:[NamesT m b]
Vars m
xs)))

{-# INLINABLE bindNArg #-}
bindNArg :: ( Monad m
        ) =>
        [Arg ArgName] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
bindNArg :: forall (m :: * -> *) a.
Monad m =>
[Arg VerboseKey] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
bindNArg [] ArgVars m -> NamesT m a
f = Names -> a -> AbsN a
forall a. Names -> a -> AbsN a
AbsN [] (a -> AbsN a) -> NamesT m a -> NamesT m (AbsN a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgVars m -> NamesT m a
f []
bindNArg (Arg ArgInfo
i VerboseKey
x:[Arg VerboseKey]
xs) ArgVars m -> NamesT m a
f = Abs (AbsN a) -> AbsN a
forall a. Abs (AbsN a) -> AbsN a
toAbsN (Abs (AbsN a) -> AbsN a)
-> NamesT m (Abs (AbsN a)) -> NamesT m (AbsN a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseKey
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
    -> NamesT m (AbsN a))
-> NamesT m (Abs (AbsN a))
forall (m :: * -> *) a.
Monad m =>
VerboseKey
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind VerboseKey
x (\ forall b. (Subst b, DeBruijn b) => NamesT m b
x -> [Arg VerboseKey] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
forall (m :: * -> *) a.
Monad m =>
[Arg VerboseKey] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
bindNArg [Arg VerboseKey]
xs (\ ArgVars m
xs -> ArgVars m -> NamesT m a
f ((ArgInfo -> b -> Arg b
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (b -> Arg b) -> NamesT m b -> NamesT m (Arg b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT m b
forall b. (Subst b, DeBruijn b) => NamesT m b
x)NamesT m (Arg b) -> [NamesT m (Arg b)] -> [NamesT m (Arg b)]
forall a. a -> [a] -> [a]
:[NamesT m (Arg b)]
ArgVars m
xs)))


type Vars1 m = (forall b. (Subst b, DeBruijn b) => List1 (NamesT m b))

bindN1 :: Monad m
  => List1 ArgName -> (Vars1 m -> NamesT m a) -> NamesT m (AbsN a)
bindN1 :: forall (m :: * -> *) a.
Monad m =>
List1 VerboseKey -> (Vars1 m -> NamesT m a) -> NamesT m (AbsN a)
bindN1 (VerboseKey
x :| Names
xs) Vars1 m -> NamesT m a
f = Abs (AbsN a) -> AbsN a
forall a. Abs (AbsN a) -> AbsN a
toAbsN (Abs (AbsN a) -> AbsN a)
-> NamesT m (Abs (AbsN a)) -> NamesT m (AbsN a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseKey
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
    -> NamesT m (AbsN a))
-> NamesT m (Abs (AbsN a))
forall (m :: * -> *) a.
Monad m =>
VerboseKey
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind VerboseKey
x (\ forall b. (Subst b, DeBruijn b) => NamesT m b
x -> Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
forall (m :: * -> *) a.
Monad m =>
Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
bindN Names
xs (\ Vars m
xs -> Vars1 m -> NamesT m a
f (NamesT m b
forall b. (Subst b, DeBruijn b) => NamesT m b
x NamesT m b -> [NamesT m b] -> NonEmpty (NamesT m b)
forall a. a -> [a] -> NonEmpty a
:| [NamesT m b]
Vars m
xs)))

glamN :: (Functor m, Monad m) =>
         [Arg ArgName] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
glamN :: forall (m :: * -> *).
(Functor m, Monad m) =>
[Arg VerboseKey]
-> (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 a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
glamN (Arg ArgInfo
i VerboseKey
n:[Arg VerboseKey]
ns) NamesT m Args -> NamesT m Term
f = ArgInfo
-> VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
Monad m =>
ArgInfo
-> VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam ArgInfo
i VerboseKey
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 VerboseKey]
-> (NamesT m Args -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
(Functor m, Monad m) =>
[Arg VerboseKey]
-> (NamesT m Args -> NamesT m Term) -> NamesT m Term
glamN [Arg VerboseKey]
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 a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT m Args
xs))


applyN :: ( Monad m
        , Subst a
        ) =>
        NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a
applyN :: forall (m :: * -> *) a.
(Monad m, Subst a) =>
NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a
applyN NamesT m (AbsN a)
f [NamesT m (SubstArg a)]
xs = do
  f <- NamesT m (AbsN a)
f
  xs <- sequence xs
  unless (length xs == length (absNName f)) $ __IMPOSSIBLE__
  return $ absAppN f xs

{-# INLINABLE applyN' #-}
applyN' :: ( Monad m
        , Subst a
        ) =>
        NamesT m (AbsN a) -> NamesT m [SubstArg a] -> NamesT m a
applyN' :: forall (m :: * -> *) a.
(Monad m, Subst a) =>
NamesT m (AbsN a) -> NamesT m [SubstArg a] -> NamesT m a
applyN' NamesT m (AbsN a)
f NamesT m [SubstArg a]
xs = do
  f <- NamesT m (AbsN a)
f
  xs <- xs
  unless (length xs == length (absNName f)) $ __IMPOSSIBLE__
  return $ absAppN f xs

{-# INLINABLE abstractN #-}
abstractN :: ( Monad m
             , Abstract a
             ) =>
             NamesT m Telescope -> (Vars m -> NamesT m a) -> NamesT m a
abstractN :: forall (m :: * -> *) a.
(Monad m, Abstract a) =>
NamesT m Telescope -> (Vars m -> NamesT m a) -> NamesT m a
abstractN NamesT m Telescope
tel Vars m -> NamesT m a
f = do
  tel <- NamesT m Telescope
tel
  u <- bindN (teleNames tel) f
  return $ abstract tel $ unAbsN u

{-# INLINABLE abstractT #-}
abstractT :: ( Monad m
             , Abstract a
             ) =>
             String -> NamesT m Type -> (Var m -> NamesT m a) -> NamesT m a
abstractT :: forall (m :: * -> *) a.
(Monad m, Abstract a) =>
VerboseKey -> NamesT m Type -> (Var m -> NamesT m a) -> NamesT m a
abstractT VerboseKey
n NamesT m Type
ty Var m -> NamesT m a
f = do
  u <- VerboseKey -> (Var m -> NamesT m a) -> NamesT m (Abs a)
forall (m :: * -> *) a.
Monad m =>
VerboseKey
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind VerboseKey
n Var m -> NamesT m a
f
  ty <- ty
  let tel = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
ty) (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Telescope -> Abs Telescope
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
n Telescope
forall a. Tele a
EmptyTel
  return $ abstract tel $ unAbs u


lamTel :: Monad m => NamesT m (Abs [Term]) -> NamesT m ([Term])
lamTel :: forall (m :: * -> *).
Monad m =>
NamesT m (Abs [Term]) -> NamesT m [Term]
lamTel NamesT m (Abs [Term])
t = (Abs Term -> Term) -> [Abs Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo) ([Abs Term] -> [Term])
-> (Abs [Term] -> [Abs Term]) -> Abs [Term] -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Abs [Term] -> [Abs Term]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => Abs (f a) -> f (Abs a)
sequenceA (Abs [Term] -> [Term]) -> NamesT m (Abs [Term]) -> NamesT m [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT m (Abs [Term])
t

appTel :: Monad m => NamesT m [Term] -> NamesT m Term -> NamesT m [Term]
appTel :: forall (m :: * -> *).
Monad m =>
NamesT m [Term] -> NamesT m Term -> NamesT m [Term]
appTel = ([Term] -> Term -> [Term])
-> NamesT m [Term] -> NamesT m Term -> NamesT m [Term]
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\ [Term]
fs Term
x -> (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo Term
x]) [Term]
fs)