{-| 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

-- 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.Telescope
import Agda.TypeChecking.Pretty ()  -- instances only

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

instance HasBuiltins m => HasBuiltins (NamesT m) where
  getBuiltinThing :: SomeBuiltin -> NamesT m (Maybe (Builtin PrimFun))
getBuiltinThing SomeBuiltin
b = m (Maybe (Builtin PrimFun)) -> NamesT m (Maybe (Builtin PrimFun))
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
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
$ SomeBuiltin -> m (Maybe (Builtin PrimFun))
forall (m :: * -> *).
HasBuiltins m =>
SomeBuiltin -> m (Maybe (Builtin PrimFun))
getBuiltinThing SomeBuiltin
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
$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
           , 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
$cfail :: forall (m :: * -> *) a. MonadFail m => String -> NamesT m a
fail :: forall a. 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
$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)) =>
(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 ProfileOptions
-> 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 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 =>
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
$cformatDebugMessage :: forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> NamesT m String
formatDebugMessage :: String -> VerboseLevel -> TCM Doc -> NamesT m String
$ctraceDebugMessage :: 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
$cverboseBracket :: forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
verboseBracket :: forall a.
String -> VerboseLevel -> String -> 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 -> String -> (Name -> NamesT m a) -> NamesT m a)
-> MonadAddContext (NamesT m)
forall a. Range -> String -> (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 -> 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 =>
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 -> String -> (Name -> NamesT m a) -> NamesT m a
withFreshName :: forall a. Range -> String -> (Name -> NamesT m a) -> NamesT m a
MonadAddContext
           , Functor (NamesT m)
MonadFail (NamesT m)
Applicative (NamesT m)
HasOptions (NamesT m)
MonadDebug (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 => HasOptions (NamesT m)
forall (m :: * -> *). HasConstInfo m => MonadDebug (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
$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
           , 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
           )


-- | 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 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

{-# INLINABLE cxtSubst #-}
-- | @cxtSubst Γ@ returns the substitution needed to go
--   from Γ to the current context.
--
--   Fails if @Γ@ is not a subcontext of the current one.
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 a. a -> NamesT m 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 a. [a] -> 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 a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Names
ctx)
     else String -> NamesT m (Substitution' a)
forall a. String -> NamesT m 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
"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
")"

{-# 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 :: (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 a. 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 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 :: (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 a. a -> 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

-- | 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 :: MonadFail m => ArgName -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a) -> NamesT m (Abs a)
bind :: forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
n (forall b. (Subst b, DeBruijn b) => 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
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m a
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m a
bind' String
n (forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a
f

{-# INLINABLE bind' #-}
-- | Like @bind@ but returns a bare term.
bind' :: MonadFail m => ArgName -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a) -> NamesT m a
bind' :: forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m a
bind' String
n (forall b. (Subst b, DeBruijn b) => 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 a.
(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
$ (forall b. (Subst b, DeBruijn 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)))


-- * Helpers to build lambda abstractions.

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
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
    -> NamesT m Term)
-> NamesT m (Abs Term)
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
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 :: 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


-- * 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 String
n AbsN a
x') = Names -> a -> AbsN a
forall a. Names -> a -> AbsN a
AbsN (String
n String -> 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] -> Substitution' (SubstArg a))
-> [SubstArg a] -> Substitution' (SubstArg a)
forall a b. (a -> b) -> a -> b
$ [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 :: ( MonadFail m
        ) =>
        [ArgName] -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
bindN :: forall (m :: * -> *) a.
MonadFail 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 (String
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
<$> String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
    -> NamesT m (AbsN a))
-> NamesT m (Abs (AbsN a))
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
x (\ forall b. (Subst b, DeBruijn b) => NamesT m b
x -> Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
forall (m :: * -> *) a.
MonadFail 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 :: ( MonadFail m
        ) =>
        [Arg ArgName] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
bindNArg :: forall (m :: * -> *) a.
MonadFail m =>
[Arg String] -> (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 String
x:[Arg String]
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
<$> String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
    -> NamesT m (AbsN a))
-> NamesT m (Abs (AbsN a))
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
x (\ forall b. (Subst b, DeBruijn b) => NamesT m b
x -> [Arg String] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
forall (m :: * -> *) a.
MonadFail m =>
[Arg String] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
bindNArg [Arg String]
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 :: MonadFail m
  => List1 ArgName -> (Vars1 m -> NamesT m a) -> NamesT m (AbsN a)
bindN1 :: forall (m :: * -> *) a.
MonadFail m =>
List1 String -> (Vars1 m -> NamesT m a) -> NamesT m (AbsN a)
bindN1 (String
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
<$> String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
    -> NamesT m (AbsN a))
-> NamesT m (Abs (AbsN a))
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
x (\ forall b. (Subst b, DeBruijn b) => NamesT m b
x -> Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
forall (m :: * -> *) a.
MonadFail 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, 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 a. a -> NamesT m a
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 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
  AbsN a
f <- NamesT m (AbsN a)
f
  [SubstArg a]
xs <- [NamesT m (SubstArg a)] -> NamesT m [SubstArg a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [NamesT m (SubstArg a)]
xs
  Bool -> NamesT m () -> NamesT m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([SubstArg a] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [SubstArg a]
xs VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== Names -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length (AbsN a -> Names
forall a. AbsN a -> Names
absNName AbsN a
f)) (NamesT m () -> NamesT m ()) -> NamesT m () -> NamesT m ()
forall a b. (a -> b) -> a -> b
$ NamesT m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
  a -> NamesT m a
forall a. 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
$ AbsN a -> [SubstArg a] -> a
forall a. Subst a => AbsN a -> [SubstArg a] -> a
absAppN AbsN a
f [SubstArg a]
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
  AbsN a
f <- NamesT m (AbsN a)
f
  [SubstArg a]
xs <- NamesT m [SubstArg a]
xs
  Bool -> NamesT m () -> NamesT m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([SubstArg a] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [SubstArg a]
xs VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== Names -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length (AbsN a -> Names
forall a. AbsN a -> Names
absNName AbsN a
f)) (NamesT m () -> NamesT m ()) -> NamesT m () -> NamesT m ()
forall a b. (a -> b) -> a -> b
$ NamesT m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
  a -> NamesT m a
forall a. 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
$ AbsN a -> [SubstArg a] -> a
forall a. Subst a => AbsN a -> [SubstArg a] -> a
absAppN AbsN a
f [SubstArg a]
xs

{-# INLINABLE abstractN #-}
abstractN :: ( MonadFail m
             , Abstract a
             ) =>
             NamesT m Telescope -> (Vars m -> NamesT m a) -> NamesT m a
abstractN :: forall (m :: * -> *) a.
(MonadFail 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
  Telescope
tel <- NamesT m Telescope
tel
  AbsN a
u <- Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
forall (m :: * -> *) a.
MonadFail m =>
Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
bindN (Telescope -> Names
teleNames Telescope
tel) Vars m -> NamesT m a
f
  a -> NamesT m a
forall a. 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
$ Telescope -> a -> a
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ AbsN a -> a
forall a. AbsN a -> a
unAbsN AbsN a
u

{-# INLINABLE abstractT #-}
abstractT :: ( MonadFail m
             , Abstract a
             ) =>
             String -> NamesT m Type -> (Var m -> NamesT m a) -> NamesT m a
abstractT :: forall (m :: * -> *) a.
(MonadFail m, Abstract a) =>
String -> NamesT m Type -> (Var m -> NamesT m a) -> NamesT m a
abstractT String
n NamesT m Type
ty Var m -> NamesT m a
f = do
  Abs a
u <- String -> (Var m -> NamesT m a) -> NamesT m (Abs a)
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
n Var m -> NamesT m a
f
  Type
ty <- NamesT m Type
ty
  let tel :: Telescope
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
$ String -> Telescope -> Abs Telescope
forall a. String -> a -> Abs a
Abs String
n Telescope
forall a. Tele a
EmptyTel
  a -> NamesT m a
forall a. 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
$ Telescope -> a -> a
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ Abs a -> a
forall a. Abs a -> a
unAbs Abs a
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)