{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances       #-}

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

e.g. if given t, u :: Term, Γ ⊢ t, u : A, we can build "λ f. f t u" like this:

runNames [] $ do
  -- @open@ binds @t@ and @u@ to computations that know how to weaken themselves in
  -- an extended context

  [t,u] <- mapM open [t,u]

  -- @lam@ gives the illusion of HOAS by providing f as a computation
  -- It also extends the internal context with the name "f", so that
  -- @t@ and @u@ will get weakened in the body.
  -- Then we finish the job using the (<@>) combinator from Agda.TypeChecking.Primitive

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

-}
module Agda.TypeChecking.Names where

import Control.Monad.Fail (MonadFail)

import Control.Monad.Reader
import Control.Monad.State

import Data.List

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

import Agda.TypeChecking.Monad hiding (getConstInfo, typeOfConst)
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free

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

instance HasBuiltins m => HasBuiltins (NamesT m) where
  getBuiltinThing :: String -> NamesT m (Maybe (Builtin PrimFun))
getBuiltinThing String
b = m (Maybe (Builtin PrimFun)) -> NamesT m (Maybe (Builtin PrimFun))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (Builtin PrimFun)) -> NamesT m (Maybe (Builtin PrimFun)))
-> m (Maybe (Builtin PrimFun))
-> NamesT m (Maybe (Builtin PrimFun))
forall a b. (a -> b) -> a -> b
$ String -> m (Maybe (Builtin PrimFun))
forall (m :: * -> *).
HasBuiltins m =>
String -> m (Maybe (Builtin PrimFun))
getBuiltinThing String
b

newtype NamesT m a = NamesT { NamesT m a -> ReaderT Names m a
unName :: ReaderT Names m a }
  deriving ( a -> NamesT m b -> NamesT m a
(a -> b) -> NamesT m a -> NamesT m b
(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
<$ :: a -> NamesT m b -> NamesT m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> NamesT m b -> NamesT m a
fmap :: (a -> b) -> NamesT m a -> NamesT m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> NamesT m a -> NamesT m b
Functor
           , Functor (NamesT m)
a -> NamesT m a
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)
NamesT m a -> NamesT m b -> NamesT m b
NamesT m a -> NamesT m b -> NamesT m a
NamesT m (a -> b) -> NamesT m a -> NamesT m b
(a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
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
<* :: NamesT m a -> NamesT m b -> NamesT m a
$c<* :: forall (m :: * -> *) a b.
Applicative m =>
NamesT m a -> NamesT m b -> NamesT m a
*> :: NamesT m a -> NamesT m b -> NamesT m b
$c*> :: forall (m :: * -> *) a b.
Applicative m =>
NamesT m a -> NamesT m b -> NamesT m b
liftA2 :: (a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
$cliftA2 :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
<*> :: NamesT m (a -> b) -> NamesT m a -> NamesT m b
$c<*> :: forall (m :: * -> *) a b.
Applicative m =>
NamesT m (a -> b) -> NamesT m a -> NamesT m b
pure :: a -> NamesT m a
$cpure :: forall (m :: * -> *) a. Applicative m => a -> NamesT m a
$cp1Applicative :: forall (m :: * -> *). Applicative m => Functor (NamesT m)
Applicative
           , Applicative (NamesT m)
a -> NamesT m a
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)
NamesT m a -> (a -> NamesT m b) -> NamesT m b
NamesT m a -> NamesT m b -> NamesT m b
forall a. a -> NamesT m a
forall a b. NamesT m a -> NamesT m b -> NamesT m b
forall a b. NamesT m a -> (a -> NamesT m b) -> NamesT m b
forall (m :: * -> *). Monad m => Applicative (NamesT m)
forall (m :: * -> *) a. Monad m => a -> NamesT m a
forall (m :: * -> *) a b.
Monad m =>
NamesT m a -> NamesT m b -> NamesT m b
forall (m :: * -> *) a b.
Monad m =>
NamesT m a -> (a -> NamesT m b) -> NamesT m b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> NamesT m a
$creturn :: forall (m :: * -> *) a. Monad m => a -> NamesT m a
>> :: NamesT m a -> NamesT m b -> NamesT m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
NamesT m a -> NamesT m b -> NamesT m b
>>= :: NamesT m a -> (a -> NamesT m b) -> NamesT m b
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
NamesT m a -> (a -> NamesT m b) -> NamesT m b
$cp1Monad :: forall (m :: * -> *). Monad m => Applicative (NamesT m)
Monad
           , Monad (NamesT m)
Monad (NamesT m)
-> (forall a. String -> NamesT m a) -> MonadFail (NamesT m)
String -> NamesT m a
forall a. String -> NamesT m a
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
forall (m :: * -> *). MonadFail m => Monad (NamesT m)
forall (m :: * -> *) a. MonadFail m => String -> NamesT m a
fail :: String -> NamesT m a
$cfail :: forall (m :: * -> *) a. MonadFail m => String -> NamesT m a
$cp1MonadFail :: forall (m :: * -> *). MonadFail m => Monad (NamesT m)
MonadFail
           , m a -> NamesT m a
(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
lift :: m a -> NamesT m a
$clift :: forall (m :: * -> *) a. Monad m => m a -> NamesT m a
MonadTrans
           , MonadState s
           , Monad (NamesT m)
Monad (NamesT m)
-> (forall a. IO a -> NamesT m a) -> MonadIO (NamesT m)
IO a -> NamesT m a
forall a. IO a -> NamesT m a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
forall (m :: * -> *). MonadIO m => Monad (NamesT m)
forall (m :: * -> *) a. MonadIO m => IO a -> NamesT m a
liftIO :: IO a -> NamesT m a
$cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> NamesT m a
$cp1MonadIO :: forall (m :: * -> *). MonadIO m => Monad (NamesT m)
MonadIO
           , Monad (NamesT m)
Functor (NamesT m)
Applicative (NamesT m)
NamesT m PragmaOptions
NamesT m CommandLineOptions
Functor (NamesT m)
-> Applicative (NamesT m)
-> Monad (NamesT m)
-> NamesT m PragmaOptions
-> NamesT m CommandLineOptions
-> HasOptions (NamesT m)
forall (m :: * -> *).
Functor m
-> Applicative m
-> Monad m
-> m PragmaOptions
-> m CommandLineOptions
-> HasOptions m
forall (m :: * -> *). HasOptions m => Monad (NamesT m)
forall (m :: * -> *). HasOptions m => Functor (NamesT m)
forall (m :: * -> *). HasOptions m => Applicative (NamesT m)
forall (m :: * -> *). HasOptions m => NamesT m PragmaOptions
forall (m :: * -> *). HasOptions m => NamesT m CommandLineOptions
commandLineOptions :: NamesT m CommandLineOptions
$ccommandLineOptions :: forall (m :: * -> *). HasOptions m => NamesT m CommandLineOptions
pragmaOptions :: NamesT m PragmaOptions
$cpragmaOptions :: forall (m :: * -> *). HasOptions m => NamesT m PragmaOptions
$cp3HasOptions :: forall (m :: * -> *). HasOptions m => Monad (NamesT m)
$cp2HasOptions :: forall (m :: * -> *). HasOptions m => Applicative (NamesT m)
$cp1HasOptions :: forall (m :: * -> *). HasOptions m => Functor (NamesT m)
HasOptions
           , Monad (NamesT m)
Functor (NamesT m)
Applicative (NamesT m)
NamesT m Bool
NamesT m Verbosity
Functor (NamesT m)
-> Applicative (NamesT m)
-> Monad (NamesT m)
-> (String -> VerboseLevel -> String -> NamesT m ())
-> (forall a.
    String -> VerboseLevel -> String -> NamesT m a -> NamesT m a)
-> (String -> VerboseLevel -> TCM Doc -> NamesT m String)
-> NamesT m Verbosity
-> NamesT m Bool
-> (forall a. NamesT m a -> NamesT m a)
-> (forall a.
    String -> VerboseLevel -> String -> NamesT m a -> NamesT m a)
-> MonadDebug (NamesT m)
String -> VerboseLevel -> String -> NamesT m ()
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
String -> VerboseLevel -> TCM Doc -> NamesT m String
NamesT m a -> NamesT m a
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 -> String -> m ())
-> (forall a. String -> VerboseLevel -> String -> m a -> m a)
-> (String -> VerboseLevel -> TCM Doc -> m String)
-> m Verbosity
-> m Bool
-> (forall a. m a -> m a)
-> (forall a. String -> VerboseLevel -> String -> m a -> m a)
-> MonadDebug m
forall (m :: * -> *). MonadDebug m => Monad (NamesT m)
forall (m :: * -> *). MonadDebug m => Functor (NamesT m)
forall (m :: * -> *). MonadDebug m => Applicative (NamesT m)
forall (m :: * -> *). MonadDebug m => NamesT m Bool
forall (m :: * -> *). MonadDebug m => NamesT m Verbosity
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> NamesT m ()
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
verboseBracket :: String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
$cverboseBracket :: forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
nowDebugPrinting :: NamesT m a -> NamesT m a
$cnowDebugPrinting :: forall (m :: * -> *) a. MonadDebug m => NamesT m a -> NamesT m a
isDebugPrinting :: NamesT m Bool
$cisDebugPrinting :: forall (m :: * -> *). MonadDebug m => NamesT m Bool
getVerbosity :: NamesT m Verbosity
$cgetVerbosity :: forall (m :: * -> *). MonadDebug m => NamesT m Verbosity
formatDebugMessage :: String -> VerboseLevel -> TCM Doc -> NamesT m String
$cformatDebugMessage :: forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> NamesT m String
traceDebugMessage :: String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
$ctraceDebugMessage :: forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
displayDebugMessage :: String -> VerboseLevel -> String -> NamesT m ()
$cdisplayDebugMessage :: forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> NamesT m ()
$cp3MonadDebug :: forall (m :: * -> *). MonadDebug m => Monad (NamesT m)
$cp2MonadDebug :: forall (m :: * -> *). MonadDebug m => Applicative (NamesT m)
$cp1MonadDebug :: forall (m :: * -> *). MonadDebug m => Functor (NamesT m)
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)
(TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
forall a. (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
forall (m :: * -> *).
Monad m
-> m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a)
-> MonadTCEnv m
forall (m :: * -> *). MonadTCEnv m => Monad (NamesT m)
forall (m :: * -> *). MonadTCEnv m => NamesT m TCEnv
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
localTC :: (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
$clocalTC :: forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
askTC :: NamesT m TCEnv
$caskTC :: forall (m :: * -> *). MonadTCEnv m => NamesT m TCEnv
$cp1MonadTCEnv :: forall (m :: * -> *). MonadTCEnv m => Monad (NamesT m)
MonadTCEnv
           , Monad (NamesT m)
NamesT m TCState
Monad (NamesT m)
-> NamesT m TCState
-> (TCState -> NamesT m ())
-> ((TCState -> TCState) -> NamesT m ())
-> MonadTCState (NamesT m)
TCState -> NamesT m ()
(TCState -> TCState) -> NamesT m ()
forall (m :: * -> *).
Monad m
-> m TCState
-> (TCState -> m ())
-> ((TCState -> TCState) -> m ())
-> MonadTCState m
forall (m :: * -> *). MonadTCState m => Monad (NamesT m)
forall (m :: * -> *). MonadTCState m => NamesT m TCState
forall (m :: * -> *). MonadTCState m => TCState -> NamesT m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> NamesT m ()
modifyTC :: (TCState -> TCState) -> NamesT m ()
$cmodifyTC :: forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> NamesT m ()
putTC :: TCState -> NamesT m ()
$cputTC :: forall (m :: * -> *). MonadTCState m => TCState -> NamesT m ()
getTC :: NamesT m TCState
$cgetTC :: forall (m :: * -> *). MonadTCState m => NamesT m TCState
$cp1MonadTCState :: forall (m :: * -> *). MonadTCState m => Monad (NamesT m)
MonadTCState
           , Applicative (NamesT m)
MonadIO (NamesT m)
MonadTCState (NamesT m)
MonadTCEnv (NamesT m)
HasOptions (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)
TCM a -> NamesT m a
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 => MonadTCState (NamesT m)
forall (m :: * -> *). MonadTCM m => MonadTCEnv (NamesT m)
forall (m :: * -> *). MonadTCM m => HasOptions (NamesT m)
forall (m :: * -> *) a. MonadTCM m => TCM a -> NamesT m a
liftTCM :: TCM a -> NamesT m a
$cliftTCM :: forall (m :: * -> *) a. MonadTCM m => TCM a -> NamesT m a
$cp5MonadTCM :: forall (m :: * -> *). MonadTCM m => HasOptions (NamesT m)
$cp4MonadTCM :: forall (m :: * -> *). MonadTCM m => MonadTCState (NamesT m)
$cp3MonadTCM :: forall (m :: * -> *). MonadTCM m => MonadTCEnv (NamesT m)
$cp2MonadTCM :: forall (m :: * -> *). MonadTCM m => MonadIO (NamesT m)
$cp1MonadTCM :: forall (m :: * -> *). MonadTCM m => Applicative (NamesT m)
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)
(TCState -> TCState) -> NamesT m a -> NamesT m a
Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
forall a. (TCState -> TCState) -> NamesT m a -> NamesT m a
forall a b. Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
forall (m :: * -> *).
Monad m
-> m TCState
-> (forall a b. Lens' a TCState -> (a -> a) -> m b -> m b)
-> (forall a. (TCState -> TCState) -> m a -> m a)
-> ReadTCState m
forall (m :: * -> *). ReadTCState m => Monad (NamesT m)
forall (m :: * -> *). ReadTCState m => NamesT m TCState
forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> NamesT m a -> NamesT m a
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
withTCState :: (TCState -> TCState) -> NamesT m a -> NamesT m a
$cwithTCState :: forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> NamesT m a -> NamesT m a
locallyTCState :: Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
$clocallyTCState :: forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b
getTCState :: NamesT m TCState
$cgetTCState :: forall (m :: * -> *). ReadTCState m => NamesT m TCState
$cp1ReadTCState :: forall (m :: * -> *). ReadTCState m => Monad (NamesT m)
ReadTCState
           , Applicative (NamesT m)
MonadTCEnv (NamesT m)
HasOptions (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)
ReduceM a -> NamesT m a
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 => MonadTCEnv (NamesT m)
forall (m :: * -> *). MonadReduce m => HasOptions (NamesT m)
forall (m :: * -> *). MonadReduce m => ReadTCState (NamesT m)
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> NamesT m a
liftReduce :: ReduceM a -> NamesT m a
$cliftReduce :: forall (m :: * -> *) a. MonadReduce m => ReduceM a -> NamesT m a
$cp4MonadReduce :: forall (m :: * -> *). MonadReduce m => HasOptions (NamesT m)
$cp3MonadReduce :: forall (m :: * -> *). MonadReduce m => ReadTCState (NamesT m)
$cp2MonadReduce :: forall (m :: * -> *). MonadReduce m => MonadTCEnv (NamesT m)
$cp1MonadReduce :: forall (m :: * -> *). MonadReduce m => Applicative (NamesT m)
MonadReduce
           , MonadError e
           , MonadTCEnv (NamesT m)
Range -> String -> (Name -> NamesT m a) -> NamesT m a
Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
Name -> Dom Type -> NamesT m a -> NamesT m a
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
MonadTCEnv (NamesT m)
-> (forall a. Name -> Dom Type -> NamesT m a -> NamesT m a)
-> (forall a. Name -> Term -> Dom Type -> NamesT m a -> NamesT m a)
-> (forall a.
    Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a)
-> (forall a.
    Range -> String -> (Name -> NamesT m a) -> NamesT m a)
-> MonadAddContext (NamesT m)
forall a. Range -> String -> (Name -> NamesT m a) -> NamesT m a
forall a. Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
forall a. Name -> Dom Type -> NamesT m a -> NamesT m a
forall a.
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
forall (m :: * -> *).
MonadTCEnv m
-> (forall a. Name -> Dom Type -> m a -> m a)
-> (forall a. Name -> Term -> Dom Type -> m a -> m a)
-> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
-> (forall a. Range -> String -> (Name -> m a) -> m a)
-> MonadAddContext m
forall (m :: * -> *). MonadAddContext m => MonadTCEnv (NamesT m)
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> String -> (Name -> NamesT m a) -> NamesT m a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> NamesT m a -> NamesT m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
withFreshName :: Range -> String -> (Name -> NamesT m a) -> NamesT m a
$cwithFreshName :: forall (m :: * -> *) a.
MonadAddContext m =>
Range -> String -> (Name -> NamesT m a) -> NamesT m a
updateContext :: Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
$cupdateContext :: forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
addLetBinding' :: Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
$caddLetBinding' :: forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
addCtx :: Name -> Dom Type -> NamesT m a -> NamesT m a
$caddCtx :: forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> NamesT m a -> NamesT m a
$cp1MonadAddContext :: forall (m :: * -> *). MonadAddContext m => MonadTCEnv (NamesT m)
MonadAddContext
           )

-- deriving instance MonadState s m => MonadState s (NamesT m)

type Names = [String]

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

-- We use @Fail@ instead of @Identity@ because the computation can fail.
runNames :: Names -> NamesT Fail a -> a
runNames :: 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 :: NamesT m Names
currentCxt = ReaderT Names m Names -> NamesT m Names
forall (m :: * -> *) a. ReaderT Names m a -> NamesT m a
NamesT ReaderT Names m Names
forall r (m :: * -> *). MonadReader r m => m r
ask

cxtSubst :: MonadFail m => Names -> NamesT m (Substitution' a)
cxtSubst :: Names -> NamesT m (Substitution' a)
cxtSubst Names
ctx = do
  Names
ctx' <- NamesT m Names
forall (m :: * -> *). Monad m => NamesT m Names
currentCxt
  if (Names
ctx Names -> Names -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` Names
ctx')
     then Substitution' a -> NamesT m (Substitution' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Substitution' a -> NamesT m (Substitution' a))
-> Substitution' a -> NamesT m (Substitution' a)
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Substitution' a
forall a. VerboseLevel -> Substitution' a
raiseS (Names -> VerboseLevel
forall i a. Num i => [a] -> i
genericLength Names
ctx' VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- Names -> VerboseLevel
forall i a. Num i => [a] -> i
genericLength Names
ctx)
     else String -> NamesT m (Substitution' a)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> NamesT m (Substitution' a))
-> String -> NamesT m (Substitution' a)
forall a b. (a -> b) -> a -> b
$ String
"thing out of context (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Names -> String
forall a. Show a => a -> String
show Names
ctx String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not a sub context of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Names -> String
forall a. Show a => a -> String
show Names
ctx' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

inCxt :: (MonadFail m, Subst t a) => Names -> a -> NamesT m a
inCxt :: Names -> a -> NamesT m a
inCxt Names
ctx a
a = do
  Substitution' t
sigma <- Names -> NamesT m (Substitution' t)
forall (m :: * -> *) a.
MonadFail m =>
Names -> NamesT m (Substitution' a)
cxtSubst Names
ctx
  a -> NamesT m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> NamesT m a) -> a -> NamesT m a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
sigma a
a

-- closed terms
cl' :: Applicative m => a -> NamesT m a
cl' :: a -> NamesT m a
cl' = a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

cl :: Monad m => m a -> NamesT m a
cl :: m a -> NamesT m a
cl = m a -> NamesT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

open :: (MonadFail m, Subst t a) => a -> NamesT m (NamesT m a)
open :: a -> NamesT m (NamesT m a)
open a
a = do
  Names
ctx <- ReaderT Names m Names -> NamesT m Names
forall (m :: * -> *) a. ReaderT Names m a -> NamesT m a
NamesT ReaderT Names m Names
forall r (m :: * -> *). MonadReader r m => m r
ask
  NamesT m a -> NamesT m (NamesT m a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NamesT m a -> NamesT m (NamesT m a))
-> NamesT m a -> NamesT m (NamesT m a)
forall a b. (a -> b) -> a -> b
$ Names -> a -> NamesT m a
forall (m :: * -> *) t a.
(MonadFail m, Subst t a) =>
Names -> a -> NamesT m a
inCxt Names
ctx a
a

bind' :: (MonadFail m, Subst t' b, DeBruijn b, Subst t a, Free a) => ArgName -> (NamesT m b -> NamesT m a) -> NamesT m a
bind' :: String -> (NamesT m b -> NamesT m a) -> NamesT m a
bind' String
n NamesT m b -> NamesT m a
f = do
  Names
cxt <- ReaderT Names m Names -> NamesT m Names
forall (m :: * -> *) a. ReaderT Names m a -> NamesT m a
NamesT ReaderT Names m Names
forall r (m :: * -> *). MonadReader r m => m r
ask
  (ReaderT Names m a -> NamesT m a
forall (m :: * -> *) a. ReaderT Names m a -> NamesT m a
NamesT (ReaderT Names m a -> NamesT m a)
-> (NamesT m a -> ReaderT Names m a) -> NamesT m a -> NamesT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Names -> Names) -> ReaderT Names m a -> ReaderT Names m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (String
nString -> Names -> Names
forall a. a -> [a] -> [a]
:) (ReaderT Names m a -> ReaderT Names m a)
-> (NamesT m a -> ReaderT Names m a)
-> NamesT m a
-> ReaderT Names m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamesT m a -> ReaderT Names m a
forall (m :: * -> *) a. NamesT m a -> ReaderT Names m a
unName (NamesT m a -> NamesT m a) -> NamesT m a -> NamesT m a
forall a b. (a -> b) -> a -> b
$ NamesT m b -> NamesT m a
f (Names -> b -> NamesT m b
forall (m :: * -> *) t a.
(MonadFail m, Subst t a) =>
Names -> a -> NamesT m a
inCxt (String
nString -> Names -> Names
forall a. a -> [a] -> [a]
:Names
cxt) (VerboseLevel -> b
forall a. DeBruijn a => VerboseLevel -> a
deBruijnVar VerboseLevel
0)))

bind :: ( MonadFail m
        , Subst t' b
        , DeBruijn b
        , Subst t a
        , Free a
        ) =>
        ArgName -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
bind :: String -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
bind String
n NamesT m b -> NamesT m a
f = String -> a -> Abs a
forall a. String -> a -> Abs a
Abs String
n (a -> Abs a) -> NamesT m a -> NamesT m (Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> (NamesT m b -> NamesT m a) -> NamesT m a
forall (m :: * -> *) t' b t a.
(MonadFail m, Subst t' b, DeBruijn b, Subst t a, Free a) =>
String -> (NamesT m b -> NamesT m a) -> NamesT m a
bind' String
n NamesT m b -> NamesT m a
f

glam :: MonadFail m
     => ArgInfo -> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam :: ArgInfo
-> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam ArgInfo
info String
n NamesT m Term -> NamesT m Term
f = ArgInfo -> Abs Term -> Term
Lam ArgInfo
info (Abs Term -> Term) -> NamesT m (Abs Term) -> NamesT m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> (NamesT m Term -> NamesT m Term) -> NamesT m (Abs Term)
forall (m :: * -> *) t' b t a.
(MonadFail m, Subst t' b, DeBruijn b, Subst t a, Free a) =>
String -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
bind String
n NamesT m Term -> NamesT m Term
f

glamN :: (Functor m, MonadFail m) =>
         [Arg ArgName] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
glamN :: [Arg String] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
glamN [] NamesT m Args -> NamesT m Term
f = NamesT m Args -> NamesT m Term
f (NamesT m Args -> NamesT m Term) -> NamesT m Args -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ Args -> NamesT m Args
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
glamN (Arg ArgInfo
i String
n:[Arg String]
ns) NamesT m Args -> NamesT m Term
f = ArgInfo
-> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
ArgInfo
-> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam ArgInfo
i String
n ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
x -> [Arg String] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
(Functor m, MonadFail m) =>
[Arg String] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
glamN [Arg String]
ns (\ NamesT m Args
xs -> NamesT m Args -> NamesT m Term
f ((:) (Arg Term -> Args -> Args)
-> NamesT m (Arg Term) -> NamesT m (Args -> Args)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Term -> Arg Term) -> NamesT m Term -> NamesT m (Arg Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT m Term
x) NamesT m (Args -> Args) -> NamesT m Args -> NamesT m Args
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT m Args
xs))

lam :: MonadFail m
    => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam :: 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 :: 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