module Agda.TypeChecking.Names where
import Control.Monad.Fail (MonadFail)
import Control.Monad ( liftM2, unless )
import Control.Monad.Except ( MonadError )
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.Reader ( MonadReader(..), ReaderT, runReaderT )
import Control.Monad.State ( MonadState )
import Control.Monad.Trans ( MonadTrans, lift )
import Data.List ( isSuffixOf )
import Agda.Syntax.Common hiding (Nat)
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad hiding (getConstInfo, typeOfConst)
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Pretty ()
import Agda.Utils.Fail (Fail, runFail_)
import Agda.Utils.List1 ( List1, pattern (:|) )
import Agda.Utils.Impossible
instance HasBuiltins m => HasBuiltins (NamesT m) where
getBuiltinThing :: SomeBuiltin -> NamesT m (Maybe (Builtin PrimFun))
getBuiltinThing SomeBuiltin
b = m (Maybe (Builtin PrimFun)) -> NamesT m (Maybe (Builtin PrimFun))
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (Builtin PrimFun)) -> NamesT m (Maybe (Builtin PrimFun)))
-> m (Maybe (Builtin PrimFun))
-> NamesT m (Maybe (Builtin PrimFun))
forall a b. (a -> b) -> a -> b
$ SomeBuiltin -> m (Maybe (Builtin PrimFun))
forall (m :: * -> *).
HasBuiltins m =>
SomeBuiltin -> m (Maybe (Builtin PrimFun))
getBuiltinThing SomeBuiltin
b
newtype NamesT m a = NamesT { forall (m :: * -> *) a. NamesT m a -> ReaderT Names m a
unName :: ReaderT Names m a }
deriving ( (forall a b. (a -> b) -> NamesT m a -> NamesT m b)
-> (forall a b. a -> NamesT m b -> NamesT m a)
-> Functor (NamesT m)
forall a b. a -> NamesT m b -> NamesT m a
forall a b. (a -> b) -> NamesT m a -> NamesT m b
forall (m :: * -> *) a b.
Functor m =>
a -> NamesT m b -> NamesT m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> NamesT m a -> NamesT m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> NamesT m a -> NamesT m b
fmap :: forall a b. (a -> b) -> NamesT m a -> NamesT m b
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> NamesT m b -> NamesT m a
<$ :: forall a b. a -> NamesT m b -> NamesT m a
Functor
, Functor (NamesT m)
Functor (NamesT m) =>
(forall a. a -> NamesT m a)
-> (forall a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b)
-> (forall a b c.
(a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c)
-> (forall a b. NamesT m a -> NamesT m b -> NamesT m b)
-> (forall a b. NamesT m a -> NamesT m b -> NamesT m a)
-> Applicative (NamesT m)
forall a. a -> NamesT m a
forall a b. NamesT m a -> NamesT m b -> NamesT m a
forall a b. NamesT m a -> NamesT m b -> NamesT m b
forall a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b
forall a b c.
(a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (m :: * -> *). Applicative m => Functor (NamesT m)
forall (m :: * -> *) a. Applicative m => a -> NamesT m a
forall (m :: * -> *) a b.
Applicative m =>
NamesT m a -> NamesT m b -> NamesT m a
forall (m :: * -> *) a b.
Applicative m =>
NamesT m a -> NamesT m b -> NamesT m b
forall (m :: * -> *) a b.
Applicative m =>
NamesT m (a -> b) -> NamesT m a -> NamesT m b
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
$cpure :: forall (m :: * -> *) a. Applicative m => a -> NamesT m a
pure :: forall a. a -> NamesT m a
$c<*> :: forall (m :: * -> *) a b.
Applicative m =>
NamesT m (a -> b) -> NamesT m a -> NamesT m b
<*> :: forall a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b
$cliftA2 :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
liftA2 :: forall a b c.
(a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c
$c*> :: forall (m :: * -> *) a b.
Applicative m =>
NamesT m a -> NamesT m b -> NamesT m b
*> :: forall a b. NamesT m a -> NamesT m b -> NamesT m b
$c<* :: forall (m :: * -> *) a b.
Applicative m =>
NamesT m a -> NamesT m b -> NamesT m a
<* :: forall a b. NamesT m a -> NamesT m b -> NamesT m a
Applicative
, Applicative (NamesT m)
Applicative (NamesT m) =>
(forall a b. NamesT m a -> (a -> NamesT m b) -> NamesT m b)
-> (forall a b. NamesT m a -> NamesT m b -> NamesT m b)
-> (forall a. a -> NamesT m a)
-> Monad (NamesT m)
forall a. a -> NamesT m a
forall a b. NamesT m a -> NamesT m b -> NamesT m b
forall a b. NamesT m a -> (a -> NamesT m b) -> NamesT m b
forall (m :: * -> *). Monad m => Applicative (NamesT m)
forall (m :: * -> *) a. Monad m => a -> NamesT m a
forall (m :: * -> *) a b.
Monad m =>
NamesT m a -> NamesT m b -> NamesT m b
forall (m :: * -> *) a b.
Monad m =>
NamesT m a -> (a -> NamesT m b) -> NamesT m b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
NamesT m a -> (a -> NamesT m b) -> NamesT m b
>>= :: forall a b. NamesT m a -> (a -> NamesT m b) -> NamesT m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
NamesT m a -> NamesT m b -> NamesT m b
>> :: forall a b. NamesT m a -> NamesT m b -> NamesT m b
$creturn :: forall (m :: * -> *) a. Monad m => a -> NamesT m a
return :: forall a. a -> NamesT m a
Monad
, Monad (NamesT m)
Monad (NamesT m) =>
(forall a. String -> NamesT m a) -> MonadFail (NamesT m)
forall a. String -> NamesT m a
forall (m :: * -> *).
Monad m =>
(forall a. String -> m a) -> MonadFail m
forall (m :: * -> *). MonadFail m => Monad (NamesT m)
forall (m :: * -> *) a. MonadFail m => String -> NamesT m a
$cfail :: forall (m :: * -> *) a. MonadFail m => String -> NamesT m a
fail :: forall a. String -> NamesT m a
MonadFail
, (forall (m :: * -> *). Monad m => Monad (NamesT m)) =>
(forall (m :: * -> *) a. Monad m => m a -> NamesT m a)
-> MonadTrans NamesT
forall (m :: * -> *). Monad m => Monad (NamesT m)
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *). Monad m => Monad (t m)) =>
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
$clift :: forall (m :: * -> *) a. Monad m => m a -> NamesT m a
lift :: forall (m :: * -> *) a. Monad m => m a -> NamesT m a
MonadTrans
, MonadState s
, Monad (NamesT m)
Monad (NamesT m) =>
(forall a. IO a -> NamesT m a) -> MonadIO (NamesT m)
forall a. IO a -> NamesT m a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
forall (m :: * -> *). MonadIO m => Monad (NamesT m)
forall (m :: * -> *) a. MonadIO m => IO a -> NamesT m a
$cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> NamesT m a
liftIO :: forall a. IO a -> NamesT m a
MonadIO
, Monad (NamesT m)
Functor (NamesT m)
Applicative (NamesT m)
NamesT m PragmaOptions
NamesT m CommandLineOptions
(Functor (NamesT m), Applicative (NamesT m), Monad (NamesT m)) =>
NamesT m PragmaOptions
-> NamesT m CommandLineOptions -> HasOptions (NamesT m)
forall (m :: * -> *).
(Functor m, Applicative m, Monad m) =>
m PragmaOptions -> m CommandLineOptions -> HasOptions m
forall (m :: * -> *). HasOptions m => Monad (NamesT m)
forall (m :: * -> *). HasOptions m => Functor (NamesT m)
forall (m :: * -> *). HasOptions m => Applicative (NamesT m)
forall (m :: * -> *). HasOptions m => NamesT m PragmaOptions
forall (m :: * -> *). HasOptions m => NamesT m CommandLineOptions
$cpragmaOptions :: forall (m :: * -> *). HasOptions m => NamesT m PragmaOptions
pragmaOptions :: NamesT m PragmaOptions
$ccommandLineOptions :: forall (m :: * -> *). HasOptions m => NamesT m CommandLineOptions
commandLineOptions :: NamesT m CommandLineOptions
HasOptions
, Monad (NamesT m)
Functor (NamesT m)
Applicative (NamesT m)
NamesT m Bool
NamesT m Verbosity
NamesT m ProfileOptions
(Functor (NamesT m), Applicative (NamesT m), Monad (NamesT m)) =>
(String -> VerboseLevel -> TCM Doc -> NamesT m String)
-> (forall a.
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a)
-> (forall a.
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a)
-> NamesT m Verbosity
-> NamesT m ProfileOptions
-> NamesT m Bool
-> (forall a. NamesT m a -> NamesT m a)
-> MonadDebug (NamesT m)
String -> VerboseLevel -> TCM Doc -> NamesT m String
forall a.
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
forall a. NamesT m a -> NamesT m a
forall (m :: * -> *).
(Functor m, Applicative m, Monad m) =>
(String -> VerboseLevel -> TCM Doc -> m String)
-> (forall a. String -> VerboseLevel -> String -> m a -> m a)
-> (forall a. String -> VerboseLevel -> String -> m a -> m a)
-> m Verbosity
-> m ProfileOptions
-> m Bool
-> (forall a. m a -> m a)
-> MonadDebug m
forall (m :: * -> *). MonadDebug m => Monad (NamesT m)
forall (m :: * -> *). MonadDebug m => Functor (NamesT m)
forall (m :: * -> *). MonadDebug m => Applicative (NamesT m)
forall (m :: * -> *). MonadDebug m => NamesT m Bool
forall (m :: * -> *). MonadDebug m => NamesT m Verbosity
forall (m :: * -> *). MonadDebug m => NamesT m ProfileOptions
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> NamesT m String
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
forall (m :: * -> *) a. MonadDebug m => NamesT m a -> NamesT m a
$cformatDebugMessage :: forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> NamesT m String
formatDebugMessage :: String -> VerboseLevel -> TCM Doc -> NamesT m String
$ctraceDebugMessage :: forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
traceDebugMessage :: forall a.
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
$cverboseBracket :: forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
verboseBracket :: forall a.
String -> VerboseLevel -> String -> NamesT m a -> NamesT m a
$cgetVerbosity :: forall (m :: * -> *). MonadDebug m => NamesT m Verbosity
getVerbosity :: NamesT m Verbosity
$cgetProfileOptions :: forall (m :: * -> *). MonadDebug m => NamesT m ProfileOptions
getProfileOptions :: NamesT m ProfileOptions
$cisDebugPrinting :: forall (m :: * -> *). MonadDebug m => NamesT m Bool
isDebugPrinting :: NamesT m Bool
$cnowDebugPrinting :: forall (m :: * -> *) a. MonadDebug m => NamesT m a -> NamesT m a
nowDebugPrinting :: forall a. NamesT m a -> NamesT m a
MonadDebug
, Monad (NamesT m)
NamesT m TCEnv
Monad (NamesT m) =>
NamesT m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a)
-> MonadTCEnv (NamesT m)
forall a. (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
forall (m :: * -> *).
Monad m =>
m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a) -> MonadTCEnv m
forall (m :: * -> *). MonadTCEnv m => Monad (NamesT m)
forall (m :: * -> *). MonadTCEnv m => NamesT m TCEnv
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
$caskTC :: forall (m :: * -> *). MonadTCEnv m => NamesT m TCEnv
askTC :: NamesT m TCEnv
$clocalTC :: forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
localTC :: forall a. (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a
MonadTCEnv
, Monad (NamesT m)
NamesT m TCState
Monad (NamesT m) =>
NamesT m TCState
-> (TCState -> NamesT m ())
-> ((TCState -> TCState) -> NamesT m ())
-> MonadTCState (NamesT m)
TCState -> NamesT m ()
(TCState -> TCState) -> NamesT m ()
forall (m :: * -> *).
Monad m =>
m TCState
-> (TCState -> m ())
-> ((TCState -> TCState) -> m ())
-> MonadTCState m
forall (m :: * -> *). MonadTCState m => Monad (NamesT m)
forall (m :: * -> *). MonadTCState m => NamesT m TCState
forall (m :: * -> *). MonadTCState m => TCState -> NamesT m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> NamesT m ()
$cgetTC :: forall (m :: * -> *). MonadTCState m => NamesT m TCState
getTC :: NamesT m TCState
$cputTC :: forall (m :: * -> *). MonadTCState m => TCState -> NamesT m ()
putTC :: TCState -> NamesT m ()
$cmodifyTC :: forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> NamesT m ()
modifyTC :: (TCState -> TCState) -> NamesT m ()
MonadTCState
, Applicative (NamesT m)
MonadIO (NamesT m)
HasOptions (NamesT m)
MonadTCState (NamesT m)
MonadTCEnv (NamesT m)
(Applicative (NamesT m), MonadIO (NamesT m), MonadTCEnv (NamesT m),
MonadTCState (NamesT m), HasOptions (NamesT m)) =>
(forall a. TCM a -> NamesT m a) -> MonadTCM (NamesT m)
forall a. TCM a -> NamesT m a
forall (tcm :: * -> *).
(Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm,
HasOptions tcm) =>
(forall a. TCM a -> tcm a) -> MonadTCM tcm
forall (m :: * -> *). MonadTCM m => Applicative (NamesT m)
forall (m :: * -> *). MonadTCM m => MonadIO (NamesT m)
forall (m :: * -> *). MonadTCM m => HasOptions (NamesT m)
forall (m :: * -> *). MonadTCM m => MonadTCState (NamesT m)
forall (m :: * -> *). MonadTCM m => MonadTCEnv (NamesT m)
forall (m :: * -> *) a. MonadTCM m => TCM a -> NamesT m a
$cliftTCM :: forall (m :: * -> *) a. MonadTCM m => TCM a -> NamesT m a
liftTCM :: forall a. TCM a -> NamesT m a
MonadTCM
, Monad (NamesT m)
NamesT m TCState
Monad (NamesT m) =>
NamesT m TCState
-> (forall a b.
Lens' TCState a -> (a -> a) -> NamesT m b -> NamesT m b)
-> (forall a. (TCState -> TCState) -> NamesT m a -> NamesT m a)
-> ReadTCState (NamesT m)
forall a. (TCState -> TCState) -> NamesT m a -> NamesT m a
forall a b. Lens' TCState a -> (a -> a) -> NamesT m b -> NamesT m b
forall (m :: * -> *).
Monad m =>
m TCState
-> (forall a b. Lens' TCState a -> (a -> a) -> m b -> m b)
-> (forall a. (TCState -> TCState) -> m a -> m a)
-> ReadTCState m
forall (m :: * -> *). ReadTCState m => Monad (NamesT m)
forall (m :: * -> *). ReadTCState m => NamesT m TCState
forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> NamesT m a -> NamesT m a
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> NamesT m b -> NamesT m b
$cgetTCState :: forall (m :: * -> *). ReadTCState m => NamesT m TCState
getTCState :: NamesT m TCState
$clocallyTCState :: forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> NamesT m b -> NamesT m b
locallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> NamesT m b -> NamesT m b
$cwithTCState :: forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> NamesT m a -> NamesT m a
withTCState :: forall a. (TCState -> TCState) -> NamesT m a -> NamesT m a
ReadTCState
, Applicative (NamesT m)
HasOptions (NamesT m)
MonadTCEnv (NamesT m)
ReadTCState (NamesT m)
(Applicative (NamesT m), MonadTCEnv (NamesT m),
ReadTCState (NamesT m), HasOptions (NamesT m)) =>
(forall a. ReduceM a -> NamesT m a) -> MonadReduce (NamesT m)
forall a. ReduceM a -> NamesT m a
forall (m :: * -> *).
(Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) =>
(forall a. ReduceM a -> m a) -> MonadReduce m
forall (m :: * -> *). MonadReduce m => Applicative (NamesT m)
forall (m :: * -> *). MonadReduce m => HasOptions (NamesT m)
forall (m :: * -> *). MonadReduce m => MonadTCEnv (NamesT m)
forall (m :: * -> *). MonadReduce m => ReadTCState (NamesT m)
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> NamesT m a
$cliftReduce :: forall (m :: * -> *) a. MonadReduce m => ReduceM a -> NamesT m a
liftReduce :: forall a. ReduceM a -> NamesT m a
MonadReduce
, MonadError e
, MonadTCEnv (NamesT m)
MonadTCEnv (NamesT m) =>
(forall a. Name -> Dom Type -> NamesT m a -> NamesT m a)
-> (forall a.
Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a)
-> (forall a.
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a)
-> (forall a.
Range -> String -> (Name -> NamesT m a) -> NamesT m a)
-> MonadAddContext (NamesT m)
forall a. Range -> String -> (Name -> NamesT m a) -> NamesT m a
forall a.
Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
forall a. Name -> Dom Type -> NamesT m a -> NamesT m a
forall a.
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
forall (m :: * -> *).
MonadTCEnv m =>
(forall a. Name -> Dom Type -> m a -> m a)
-> (forall a. Origin -> Name -> Term -> Dom Type -> m a -> m a)
-> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
-> (forall a. Range -> String -> (Name -> m a) -> m a)
-> MonadAddContext m
forall (m :: * -> *). MonadAddContext m => MonadTCEnv (NamesT m)
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> String -> (Name -> NamesT m a) -> NamesT m a
forall (m :: * -> *) a.
MonadAddContext m =>
Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> NamesT m a -> NamesT m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
$caddCtx :: forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> NamesT m a -> NamesT m a
addCtx :: forall a. Name -> Dom Type -> NamesT m a -> NamesT m a
$caddLetBinding' :: forall (m :: * -> *) a.
MonadAddContext m =>
Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
addLetBinding' :: forall a.
Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a
$cupdateContext :: forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
updateContext :: forall a.
Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a
$cwithFreshName :: forall (m :: * -> *) a.
MonadAddContext m =>
Range -> String -> (Name -> NamesT m a) -> NamesT m a
withFreshName :: forall a. Range -> String -> (Name -> NamesT m a) -> NamesT m a
MonadAddContext
, Functor (NamesT m)
MonadFail (NamesT m)
Applicative (NamesT m)
HasOptions (NamesT m)
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
)
type Names = [String]
runNamesT :: Names -> NamesT m a -> m a
runNamesT :: forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT Names
n NamesT m a
m = ReaderT Names m a -> Names -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (NamesT m a -> ReaderT Names m a
forall (m :: * -> *) a. NamesT m a -> ReaderT Names m a
unName NamesT m a
m) Names
n
runNames :: Names -> NamesT Fail a -> a
runNames :: forall a. Names -> NamesT Fail a -> a
runNames Names
n NamesT Fail a
m = Fail a -> a
forall a. Fail a -> a
runFail_ (Names -> NamesT Fail a -> Fail a
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT Names
n NamesT Fail a
m)
currentCxt :: Monad m => NamesT m Names
currentCxt :: forall (m :: * -> *). Monad m => NamesT m Names
currentCxt = ReaderT Names m Names -> NamesT m Names
forall (m :: * -> *) a. ReaderT Names m a -> NamesT m a
NamesT ReaderT Names m Names
forall r (m :: * -> *). MonadReader r m => m r
ask
{-# INLINABLE cxtSubst #-}
cxtSubst :: MonadFail m => Names -> NamesT m (Substitution' a)
cxtSubst :: forall (m :: * -> *) a.
MonadFail 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 fail $ "out of context (" ++ show ctx ++ " is not a sub context of " ++ show ctx' ++ ")"
{-# INLINABLE inCxt #-}
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
sigma <- Names -> NamesT m (Substitution' (SubstArg a))
forall (m :: * -> *) a.
MonadFail m =>
Names -> NamesT m (Substitution' a)
cxtSubst Names
ctx
return $ applySubst sigma a
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 :: (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
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
type Var m = forall b. (Subst b, DeBruijn b) => NamesT m b
{-# INLINE bind #-}
bind :: MonadFail m => ArgName -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a) -> NamesT m (Abs a)
bind :: forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
n (forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a
f = String -> a -> Abs a
forall a. String -> a -> Abs a
Abs String
n (a -> Abs a) -> NamesT m a -> NamesT m (Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m a
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m a
bind' String
n (forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a
f
{-# INLINABLE bind' #-}
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
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)))
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
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)
toAbsN :: Abs (AbsN a) -> AbsN a
toAbsN :: forall a. Abs (AbsN a) -> AbsN a
toAbsN (Abs String
n AbsN a
x') = Names -> a -> AbsN a
forall a. Names -> a -> AbsN a
AbsN (String
n String -> Names -> Names
forall a. a -> [a] -> [a]
: AbsN a -> Names
forall a. AbsN a -> Names
absNName AbsN a
x') (AbsN a -> a
forall a. AbsN a -> a
unAbsN AbsN a
x')
toAbsN NoAbs{} = AbsN a
forall a. HasCallStack => a
__IMPOSSIBLE__
{-# INLINABLE absAppN #-}
absAppN :: Subst a => AbsN a -> [SubstArg a] -> a
absAppN :: forall a. Subst a => AbsN a -> [SubstArg a] -> a
absAppN AbsN a
f [SubstArg a]
xs = [SubstArg a] -> Substitution' (SubstArg a)
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([SubstArg a] -> [SubstArg a]
forall a. [a] -> [a]
reverse [SubstArg a]
xs) Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` AbsN a -> a
forall a. AbsN a -> a
unAbsN AbsN a
f
type ArgVars m = (forall b. (Subst b, DeBruijn b) => [NamesT m (Arg b)])
type Vars m = (forall b. (Subst b, DeBruijn b) => [NamesT m b])
{-# INLINABLE bindN #-}
bindN :: ( MonadFail m
) =>
[ArgName] -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
bindN :: forall (m :: * -> *) a.
MonadFail m =>
Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
bindN [] Vars m -> NamesT m a
f = Names -> a -> AbsN a
forall a. Names -> a -> AbsN a
AbsN [] (a -> AbsN a) -> NamesT m a -> NamesT m (AbsN a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Vars m -> NamesT m a
f []
bindN (String
x:Names
xs) Vars m -> NamesT m a
f = Abs (AbsN a) -> AbsN a
forall a. Abs (AbsN a) -> AbsN a
toAbsN (Abs (AbsN a) -> AbsN a)
-> NamesT m (Abs (AbsN a)) -> NamesT m (AbsN a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
-> NamesT m (AbsN a))
-> NamesT m (Abs (AbsN a))
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
x (\ forall b. (Subst b, DeBruijn b) => NamesT m b
x -> Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
forall (m :: * -> *) a.
MonadFail m =>
Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
bindN Names
xs (\ Vars m
xs -> Vars m -> NamesT m a
f (NamesT m b
forall b. (Subst b, DeBruijn b) => NamesT m b
xNamesT m b -> [NamesT m b] -> [NamesT m b]
forall a. a -> [a] -> [a]
:[NamesT m b]
Vars m
xs)))
{-# INLINABLE bindNArg #-}
bindNArg :: ( MonadFail m
) =>
[Arg ArgName] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
bindNArg :: forall (m :: * -> *) a.
MonadFail m =>
[Arg String] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
bindNArg [] ArgVars m -> NamesT m a
f = Names -> a -> AbsN a
forall a. Names -> a -> AbsN a
AbsN [] (a -> AbsN a) -> NamesT m a -> NamesT m (AbsN a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgVars m -> NamesT m a
f []
bindNArg (Arg ArgInfo
i String
x:[Arg String]
xs) ArgVars m -> NamesT m a
f = Abs (AbsN a) -> AbsN a
forall a. Abs (AbsN a) -> AbsN a
toAbsN (Abs (AbsN a) -> AbsN a)
-> NamesT m (Abs (AbsN a)) -> NamesT m (AbsN a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
-> NamesT m (AbsN a))
-> NamesT m (Abs (AbsN a))
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
x (\ forall b. (Subst b, DeBruijn b) => NamesT m b
x -> [Arg String] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
forall (m :: * -> *) a.
MonadFail m =>
[Arg String] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
bindNArg [Arg String]
xs (\ ArgVars m
xs -> ArgVars m -> NamesT m a
f ((ArgInfo -> b -> Arg b
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (b -> Arg b) -> NamesT m b -> NamesT m (Arg b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT m b
forall b. (Subst b, DeBruijn b) => NamesT m b
x)NamesT m (Arg b) -> [NamesT m (Arg b)] -> [NamesT m (Arg b)]
forall a. a -> [a] -> [a]
:[NamesT m (Arg b)]
ArgVars m
xs)))
type Vars1 m = (forall b. (Subst b, DeBruijn b) => List1 (NamesT m b))
bindN1 :: MonadFail m
=> List1 ArgName -> (Vars1 m -> NamesT m a) -> NamesT m (AbsN a)
bindN1 :: forall (m :: * -> *) a.
MonadFail m =>
List1 String -> (Vars1 m -> NamesT m a) -> NamesT m (AbsN a)
bindN1 (String
x :| Names
xs) Vars1 m -> NamesT m a
f = Abs (AbsN a) -> AbsN a
forall a. Abs (AbsN a) -> AbsN a
toAbsN (Abs (AbsN a) -> AbsN a)
-> NamesT m (Abs (AbsN a)) -> NamesT m (AbsN a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
-> NamesT m (AbsN a))
-> NamesT m (Abs (AbsN a))
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind String
x (\ forall b. (Subst b, DeBruijn b) => NamesT m b
x -> Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
forall (m :: * -> *) a.
MonadFail m =>
Names -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
bindN Names
xs (\ Vars m
xs -> Vars1 m -> NamesT m a
f (NamesT m b
forall b. (Subst b, DeBruijn b) => NamesT m b
x NamesT m b -> [NamesT m b] -> NonEmpty (NamesT m b)
forall a. a -> [a] -> NonEmpty a
:| [NamesT m b]
Vars m
xs)))
glamN :: (Functor m, MonadFail m) =>
[Arg ArgName] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
glamN :: forall (m :: * -> *).
(Functor m, MonadFail m) =>
[Arg String] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
glamN [] NamesT m Args -> NamesT m Term
f = NamesT m Args -> NamesT m Term
f (NamesT m Args -> NamesT m Term) -> NamesT m Args -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ Args -> NamesT m Args
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
glamN (Arg ArgInfo
i String
n:[Arg String]
ns) NamesT m Args -> NamesT m Term
f = ArgInfo
-> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
ArgInfo
-> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam ArgInfo
i String
n ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
-> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
x -> [Arg String] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
(Functor m, MonadFail m) =>
[Arg String] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
glamN [Arg String]
ns (\ NamesT m Args
xs -> NamesT m Args -> NamesT m Term
f ((:) (Arg Term -> Args -> Args)
-> NamesT m (Arg Term) -> NamesT m (Args -> Args)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Term -> Arg Term) -> NamesT m Term -> NamesT m (Arg Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT m Term
x) NamesT m (Args -> Args) -> NamesT m Args -> NamesT m Args
forall a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT m Args
xs))
applyN :: ( Monad m
, Subst a
) =>
NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a
applyN :: forall (m :: * -> *) a.
(Monad m, Subst a) =>
NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a
applyN NamesT m (AbsN a)
f [NamesT m (SubstArg a)]
xs = do
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 :: ( 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
tel <- NamesT m Telescope
tel
u <- bindN (teleNames tel) f
return $ abstract tel $ unAbsN u
{-# INLINABLE abstractT #-}
abstractT :: ( MonadFail m
, Abstract a
) =>
String -> NamesT m Type -> (Var m -> NamesT m a) -> NamesT m a
abstractT :: forall (m :: * -> *) a.
(MonadFail m, Abstract a) =>
String -> NamesT m Type -> (Var m -> NamesT m a) -> NamesT m a
abstractT String
n NamesT m Type
ty Var m -> NamesT m a
f = do
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
ty <- ty
let tel = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
ty) (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ String -> Telescope -> Abs Telescope
forall a. String -> a -> Abs a
Abs String
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)