{-| 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.Errors
import Agda.TypeChecking.Level
import Agda.TypeChecking.Pretty ()  -- instances only
import Agda.TypeChecking.Free

import Agda.Utils.Fail (Fail, runFail_)
import Agda.Utils.Impossible

instance HasBuiltins m => HasBuiltins (NamesT m) where
  getBuiltinThing :: String -> NamesT m (Maybe (Builtin PrimFun))
getBuiltinThing String
b = m (Maybe (Builtin PrimFun)) -> NamesT m (Maybe (Builtin PrimFun))
forall (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
$ String -> m (Maybe (Builtin PrimFun))
forall (m :: * -> *).
HasBuiltins m =>
String -> m (Maybe (Builtin PrimFun))
getBuiltinThing String
b

newtype NamesT m a = NamesT { forall (m :: * -> *) a. NamesT m a -> ReaderT Names m a
unName :: ReaderT Names m a }
  deriving ( (forall a b. (a -> b) -> NamesT m a -> NamesT m b)
-> (forall a b. a -> NamesT m b -> NamesT m a)
-> Functor (NamesT m)
forall a b. a -> NamesT m b -> NamesT m a
forall a b. (a -> b) -> NamesT m a -> NamesT m b
forall (m :: * -> *) a b.
Functor m =>
a -> NamesT m b -> NamesT m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> NamesT m a -> NamesT m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$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 :: * -> *) a. Monad m => m a -> NamesT m a)
-> MonadTrans NamesT
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
$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' a TCState -> (a -> a) -> NamesT m b -> NamesT m b)
-> (forall a. (TCState -> TCState) -> NamesT m a -> NamesT m a)
-> ReadTCState (NamesT m)
forall a. (TCState -> TCState) -> NamesT m a -> NamesT m a
forall a b. Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
forall (m :: * -> *).
Monad m
-> m TCState
-> (forall a b. Lens' a TCState -> (a -> a) -> m b -> m b)
-> (forall a. (TCState -> TCState) -> m a -> m a)
-> ReadTCState m
forall {m :: * -> *}. ReadTCState m => Monad (NamesT m)
forall (m :: * -> *). ReadTCState m => NamesT m TCState
forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> NamesT m a -> NamesT m a
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
$cgetTCState :: forall (m :: * -> *). ReadTCState m => NamesT m TCState
getTCState :: NamesT m TCState
$clocallyTCState :: forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
locallyTCState :: forall a b. Lens' a TCState -> (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. Name -> Term -> Dom Type -> NamesT m a -> NamesT m a)
-> (forall a.
    Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a)
-> (forall a.
    Range -> String -> (Name -> NamesT m a) -> NamesT m a)
-> MonadAddContext (NamesT m)
forall a. Range -> String -> (Name -> NamesT m a) -> NamesT m a
forall a. Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
forall a. Name -> Dom Type -> NamesT m a -> NamesT m a
forall a.
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
forall (m :: * -> *).
MonadTCEnv m
-> (forall a. Name -> Dom Type -> m a -> m a)
-> (forall a. Name -> Term -> Dom Type -> m a -> m a)
-> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
-> (forall a. Range -> String -> (Name -> m a) -> m a)
-> MonadAddContext m
forall {m :: * -> *}. MonadAddContext m => MonadTCEnv (NamesT m)
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> String -> (Name -> NamesT m a) -> NamesT m a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> NamesT m a -> NamesT m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
$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 =>
Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
addLetBinding' :: forall a. 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)
MonadTCEnv (NamesT m)
MonadDebug (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 => MonadTCEnv (NamesT m)
forall {m :: * -> *}. HasConstInfo m => MonadDebug (NamesT m)
forall (m :: * -> *).
HasConstInfo m =>
QName -> NamesT m RewriteRules
forall (m :: * -> *).
HasConstInfo m =>
QName -> NamesT m (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> NamesT m Definition
$cgetConstInfo :: forall (m :: * -> *).
HasConstInfo m =>
QName -> NamesT m Definition
getConstInfo :: QName -> NamesT m Definition
$cgetConstInfo' :: forall (m :: * -> *).
HasConstInfo m =>
QName -> NamesT m (Either SigError Definition)
getConstInfo' :: QName -> NamesT m (Either SigError Definition)
$cgetRewriteRulesFor :: forall (m :: * -> *).
HasConstInfo m =>
QName -> NamesT m RewriteRules
getRewriteRulesFor :: QName -> NamesT m RewriteRules
HasConstInfo
           , MonadTCEnv (NamesT m)
MonadReduce (NamesT m)
ReadTCState (NamesT m)
HasBuiltins (NamesT m)
MonadAddContext (NamesT m)
MonadDebug (NamesT m)
HasConstInfo (NamesT m)
HasBuiltins (NamesT m)
-> HasConstInfo (NamesT m)
-> MonadAddContext (NamesT m)
-> MonadDebug (NamesT m)
-> MonadReduce (NamesT m)
-> MonadTCEnv (NamesT m)
-> ReadTCState (NamesT m)
-> PureTCM (NamesT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadTCEnv (NamesT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadReduce (NamesT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
ReadTCState (NamesT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
HasBuiltins (NamesT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadAddContext (NamesT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadDebug (NamesT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
HasConstInfo (NamesT m)
forall (m :: * -> *).
HasBuiltins m
-> HasConstInfo m
-> MonadAddContext m
-> MonadDebug m
-> MonadReduce m
-> MonadTCEnv m
-> ReadTCState m
-> PureTCM m
PureTCM
           )


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

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

runNames :: Names -> NamesT Fail a -> a
runNames :: forall a. Names -> NamesT Fail a -> a
runNames Names
n NamesT Fail a
m = Fail a -> a
forall a. Fail a -> a
runFail_ (Names -> NamesT Fail a -> Fail a
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT Names
n NamesT Fail a
m)

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

-- | @cxtSubst Γ@ 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
")"

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

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


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

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

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

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

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


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

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

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

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)