{-| 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 Mikan.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 Data.Text.Short (ShortText)
import Data.Text.Short qualified as TS

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

import Mikan.TypeChecking.Monad hiding (getConstInfo, typeOfConst)
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Telescope
import Mikan.TypeChecking.Pretty ()  -- instances only

import Mikan.Utils.List1 ( List1, pattern (:|) )
import Mikan.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 CommandLineOptions
NamesT m PragmaOptions
(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 CommandLineOptions
forall (m :: * -> *). HasOptions m => NamesT m PragmaOptions
$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 Doc)
-> (forall a.
    VerboseKey -> VerboseLevel -> Doc -> 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 Doc
forall a.
VerboseKey
-> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a
forall a.
VerboseKey -> VerboseLevel -> Doc -> 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 Doc)
-> (forall a. VerboseKey -> VerboseLevel -> Doc -> 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 Doc
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey
-> VerboseLevel -> VerboseKey -> NamesT m a -> NamesT m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> Doc -> 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 Doc
formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m Doc
$ctraceDebugMessage :: forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> Doc -> NamesT m a -> NamesT m a
traceDebugMessage :: forall a.
VerboseKey -> VerboseLevel -> Doc -> 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)
Monad (NamesT m) =>
(HasCallStack => FileId -> NamesT m File)
-> (File -> NamesT m FileId) -> MonadFileId (NamesT m)
HasCallStack => FileId -> NamesT m File
File -> NamesT m FileId
forall (m :: * -> *).
Monad m =>
(HasCallStack => FileId -> m File)
-> (File -> m FileId) -> MonadFileId m
forall (m :: * -> *). MonadFileId m => Monad (NamesT m)
forall (m :: * -> *).
(MonadFileId m, HasCallStack) =>
FileId -> NamesT m File
forall (m :: * -> *). MonadFileId m => File -> NamesT m FileId
$cfileFromId :: forall (m :: * -> *).
(MonadFileId m, HasCallStack) =>
FileId -> NamesT m File
fileFromId :: HasCallStack => FileId -> NamesT m File
$cidFromFile :: forall (m :: * -> *). MonadFileId m => File -> NamesT m FileId
idFromFile :: File -> NamesT m FileId
MonadFileId
           , 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)
MonadTCEnv (NamesT m)
MonadTCState (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 => MonadTCEnv (NamesT m)
forall (m :: * -> *). MonadTCM m => MonadTCState (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 SessionState
NamesT m TCState
Monad (NamesT m) =>
NamesT m TCState
-> (forall a b.
    Lens' TCState a -> (a -> a) -> NamesT m b -> NamesT m b)
-> NamesT m SessionState
-> (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)
-> m SessionState
-> (forall a. (TCState -> TCState) -> m a -> m a)
-> ReadTCState m
forall (m :: * -> *). ReadTCState m => Monad (NamesT m)
forall (m :: * -> *). ReadTCState m => NamesT m SessionState
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
$cgetSessionState :: forall (m :: * -> *). ReadTCState m => NamesT m SessionState
getSessionState :: NamesT m SessionState
$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.
    IsAxiom
    -> 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 -> ArgName -> (Name -> NamesT m a) -> NamesT m a)
-> MonadAddContext (NamesT m)
forall a. Range -> ArgName -> (Name -> 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 a.
IsAxiom
-> Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
forall (m :: * -> *).
MonadTCEnv m =>
(forall a. Name -> Dom Type -> m a -> m a)
-> (forall a.
    IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a)
-> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
-> (forall a. Range -> ArgName -> (Name -> m a) -> m a)
-> MonadAddContext m
forall (m :: * -> *). MonadAddContext m => MonadTCEnv (NamesT m)
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> ArgName -> (Name -> 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
forall (m :: * -> *) a.
MonadAddContext m =>
IsAxiom
-> Origin -> Name -> Term -> Dom Type -> 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 =>
IsAxiom
-> Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
addLetBinding' :: forall a.
IsAxiom
-> 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 -> ArgName -> (Name -> NamesT m a) -> NamesT m a
withFreshName :: forall a. Range -> ArgName -> (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)
MonadDebug (NamesT m)
MonadTCEnv (NamesT m)
(Functor (NamesT m), Applicative (NamesT m), HasOptions (NamesT m),
 MonadDebug (NamesT m), MonadTCEnv (NamesT m)) =>
(HasCallStack => QName -> NamesT m Definition)
-> (HasCallStack => QName -> NamesT m (Either SigError Definition))
-> HasConstInfo (NamesT m)
HasCallStack => QName -> NamesT m (Either SigError Definition)
HasCallStack => QName -> NamesT m Definition
forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadDebug m,
 MonadTCEnv m) =>
(HasCallStack => QName -> m Definition)
-> (HasCallStack => QName -> m (Either SigError Definition))
-> 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 => MonadDebug (NamesT m)
forall (m :: * -> *). HasConstInfo m => MonadTCEnv (NamesT m)
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> NamesT m (Either SigError Definition)
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> NamesT m Definition
$cgetConstInfo :: forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> NamesT m Definition
getConstInfo :: HasCallStack => QName -> NamesT m Definition
$cgetConstInfo' :: forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> NamesT m (Either SigError Definition)
getConstInfo' :: HasCallStack => QName -> NamesT m (Either SigError Definition)
HasConstInfo
           , MonadFileId (NamesT m)
MonadDebug (NamesT m)
MonadReduce (NamesT m)
MonadTCEnv (NamesT m)
ReadTCState (NamesT m)
HasConstInfo (NamesT m)
MonadAddContext (NamesT m)
HasBuiltins (NamesT m)
(HasBuiltins (NamesT m), HasConstInfo (NamesT m),
 MonadAddContext (NamesT m), MonadDebug (NamesT m),
 MonadFileId (NamesT m), MonadReduce (NamesT m),
 MonadTCEnv (NamesT m), ReadTCState (NamesT m)) =>
PureTCM (NamesT m)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadFileId m,
 MonadReduce m) =>
MonadFileId (NamesT m)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadFileId m,
 MonadReduce m) =>
MonadDebug (NamesT m)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadFileId m,
 MonadReduce m) =>
MonadReduce (NamesT m)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadFileId m,
 MonadReduce m) =>
MonadTCEnv (NamesT m)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadFileId m,
 MonadReduce m) =>
ReadTCState (NamesT m)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadFileId m,
 MonadReduce m) =>
HasConstInfo (NamesT m)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadFileId m,
 MonadReduce m) =>
MonadAddContext (NamesT m)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadFileId m,
 MonadReduce m) =>
HasBuiltins (NamesT m)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadDebug m,
 MonadFileId m, MonadReduce m, MonadTCEnv m, ReadTCState m) =>
PureTCM m
PureTCM
           )


-- | A list of variable names from a context.
type Names = [ShortText]

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 =>
ArgName
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind ArgName
n (forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a
f = ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
Abs ArgName
n (a -> Abs a) -> NamesT m a -> NamesT m (Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m a
forall (m :: * -> *) a.
Monad m =>
ArgName
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m a
bind' ArgName
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 =>
ArgName
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m a
bind' ArgName
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
-> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam ArgInfo
info ArgName
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
<$> ArgName
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
    -> NamesT m Term)
-> NamesT m (Abs Term)
forall (m :: * -> *) a.
Monad m =>
ArgName
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind ArgName
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 =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
n NamesT m Term -> NamesT m Term
f = ArgInfo
-> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
Monad m =>
ArgInfo
-> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam ArgInfo
defaultArgInfo ArgName
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 ArgName
n AbsN a
x') = Names -> a -> AbsN a
forall a. Names -> a -> AbsN a
AbsN (ArgName
n ArgName -> 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 (ArgName
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
<$> ArgName
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
    -> NamesT m (AbsN a))
-> NamesT m (Abs (AbsN a))
forall (m :: * -> *) a.
Monad m =>
ArgName
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind ArgName
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 ArgName] -> (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 ArgName
x:[Arg ArgName]
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
<$> ArgName
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
    -> NamesT m (AbsN a))
-> NamesT m (Abs (AbsN a))
forall (m :: * -> *) a.
Monad m =>
ArgName
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind ArgName
x (\ forall b. (Subst b, DeBruijn b) => NamesT m b
x -> [Arg ArgName] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
forall (m :: * -> *) a.
Monad m =>
[Arg ArgName] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
bindNArg [Arg ArgName]
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 ArgName -> (Vars1 m -> NamesT m a) -> NamesT m (AbsN a)
bindN1 (ArgName
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
<$> ArgName
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
    -> NamesT m (AbsN a))
-> NamesT m (Abs (AbsN a))
forall (m :: * -> *) a.
Monad m =>
ArgName
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind ArgName
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 :: (Monad m) => [Arg ArgName] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
glamN :: forall (m :: * -> *).
Monad m =>
[Arg ArgName] -> (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 ArgName
n:[Arg ArgName]
ns) NamesT m Args -> NamesT m Term
f = ArgInfo
-> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
Monad m =>
ArgInfo
-> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam ArgInfo
i ArgName
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 ArgName] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
Monad m =>
[Arg ArgName] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
glamN [Arg ArgName]
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
             ) =>
             ShortText -> NamesT m Type -> (Var m -> NamesT m a) -> NamesT m a
abstractT :: forall (m :: * -> *) a.
(Monad m, Abstract a) =>
ArgName -> NamesT m Type -> (Var m -> NamesT m a) -> NamesT m a
abstractT ArgName
n NamesT m Type
ty Var m -> NamesT m a
f = do
  u <- ArgName -> (Var m -> NamesT m a) -> NamesT m (Abs a)
forall (m :: * -> *) a.
Monad m =>
ArgName
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind ArgName
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 t. a -> Dom' t a
defaultDom Type
ty) (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ ArgName -> Telescope -> Abs Telescope
forall a. ArgName -> a -> Abs a
Abs ArgName
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)