Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Names

Contents

- Helpers to build lambda abstractions.
- Combinators for n-ary binders.

Description

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

Synopsis

- newtype NamesT (m :: Type -> Type) a = NamesT {
  - unName :: ReaderT Names m a
  }
- type Names = [String]
- runNamesT :: Names -> NamesT m a -> m a
- runNames :: Names -> NamesT Identity a -> a
- currentCxt :: forall (m :: Type -> Type). Monad m => NamesT m Names
- cxtSubst :: forall (m :: Type -> Type) a. Monad m => Names -> NamesT m (Substitution' a)
- inCxt :: forall (m :: Type -> Type) a. (Monad m, Subst a) => Names -> a -> NamesT m a
- cl' :: forall (m :: Type -> Type) a. Applicative m => a -> NamesT m a
- cl :: Monad m => m a -> NamesT m a
- open :: forall (m :: Type -> Type) a. (Monad m, Subst a) => a -> NamesT m (NamesT m a)
- type Var (m :: Type -> Type) = forall b. (Subst b, DeBruijn b) => NamesT m b
- bind :: forall (m :: Type -> Type) a. Monad m => ArgName -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a) -> NamesT m (Abs a)
- bind' :: forall (m :: Type -> Type) a. Monad m => ArgName -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a) -> NamesT m a
- glam :: forall (m :: Type -> Type). Monad m => ArgInfo -> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
- lam :: forall (m :: Type -> Type). Monad m => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
- ilam :: forall (m :: Type -> Type). Monad m => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
- data AbsN a = AbsN {
  - absNName :: [ArgName]
  - unAbsN :: a
  }
- toAbsN :: Abs (AbsN a) -> AbsN a
- absAppN :: Subst a => AbsN a -> [SubstArg a] -> a
- type ArgVars (m :: Type -> Type) = forall b. (Subst b, DeBruijn b) => [NamesT m (Arg b)]
- type Vars (m :: Type -> Type) = forall b. (Subst b, DeBruijn b) => [NamesT m b]
- bindN :: forall (m :: Type -> Type) a. Monad m => [ArgName] -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)
- bindNArg :: forall (m :: Type -> Type) a. Monad m => [Arg ArgName] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)
- type Vars1 (m :: Type -> Type) = forall b. (Subst b, DeBruijn b) => List1 (NamesT m b)
- bindN1 :: forall (m :: Type -> Type) a. Monad m => List1 ArgName -> (Vars1 m -> NamesT m a) -> NamesT m (AbsN a)
- glamN :: forall (m :: Type -> Type). (Functor m, Monad m) => [Arg ArgName] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term
- applyN :: forall (m :: Type -> Type) a. (Monad m, Subst a) => NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a
- applyN' :: forall (m :: Type -> Type) a. (Monad m, Subst a) => NamesT m (AbsN a) -> NamesT m [SubstArg a] -> NamesT m a
- abstractN :: forall (m :: Type -> Type) a. (Monad m, Abstract a) => NamesT m Telescope -> (Vars m -> NamesT m a) -> NamesT m a
- abstractT :: forall (m :: Type -> Type) a. (Monad m, Abstract a) => String -> NamesT m Type -> (Var m -> NamesT m a) -> NamesT m a
- lamTel :: forall (m :: Type -> Type). Monad m => NamesT m (Abs [Term]) -> NamesT m [Term]
- appTel :: forall (m :: Type -> Type). Monad m => NamesT m [Term] -> NamesT m Term -> NamesT m [Term]

# Documentation

newtype NamesT (m :: Type -> Type) a Source #

Constructors

NamesT |

Fields

- unName :: ReaderT Names m a

#### Instances

Instances details

MonadTrans NamesT Source # |
Instance details Defined in Agda.TypeChecking.Names Methods lift :: Monad m => m a -> NamesT m a Source #
MonadError e m => MonadError e (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods throwError :: e -> NamesT m a Source # catchError :: NamesT m a -> (e -> NamesT m a) -> NamesT m a Source #
MonadState s m => MonadState s (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods get :: NamesT m s Source # put :: s -> NamesT m () Source # state :: (s -> (a, s)) -> NamesT m a Source #
HasOptions m => HasOptions (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods pragmaOptions :: NamesT m PragmaOptions Source # commandLineOptions :: NamesT m CommandLineOptions Source #
MonadReduce m => MonadReduce (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods liftReduce :: ReduceM a -> NamesT m a Source #
MonadTCEnv m => MonadTCEnv (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods askTC :: NamesT m TCEnv Source # localTC :: (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a Source #
MonadTCM m => MonadTCM (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods liftTCM :: TCM a -> NamesT m a Source #
MonadTCState m => MonadTCState (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods getTC :: NamesT m TCState Source # putTC :: TCState -> NamesT m () Source # modifyTC :: (TCState -> TCState) -> NamesT m () Source #
ReadTCState m => ReadTCState (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods getTCState :: NamesT m TCState Source # locallyTCState :: Lens' TCState a -> (a -> a) -> NamesT m b -> NamesT m b Source # withTCState :: (TCState -> TCState) -> NamesT m a -> NamesT m a Source #
HasBuiltins m => HasBuiltins (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods getBuiltinThing :: SomeBuiltin -> NamesT m (Maybe (Builtin PrimFun)) Source #
MonadAddContext m => MonadAddContext (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods addCtx :: Name -> Dom Type -> NamesT m a -> NamesT m a Source # addLetBinding' :: Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a Source # updateContext :: Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a Source # withFreshName :: Range -> ArgName -> (Name -> NamesT m a) -> NamesT m a Source #
MonadDebug m => MonadDebug (NamesT m) Source # |

Instance details

Defined in Agda.TypeChecking.Names

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m String Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> NamesT m a -> NamesT m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> NamesT m a -> NamesT m a Source #

getVerbosity :: NamesT m Verbosity Source #

getProfileOptions :: NamesT m ProfileOptions Source #

isDebugPrinting :: NamesT m Bool Source #

nowDebugPrinting :: NamesT m a -> NamesT m a Source #

(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names
HasConstInfo m => HasConstInfo (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods getConstInfo :: QName -> NamesT m Definition Source # getConstInfo' :: QName -> NamesT m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> NamesT m RewriteRules Source #
MonadIO m => MonadIO (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods liftIO :: IO a -> NamesT m a Source #
Applicative m => Applicative (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods pure :: a -> NamesT m a Source # (<*>) :: NamesT m (a -> b) -> NamesT m a -> NamesT m b Source # liftA2 :: (a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c Source # (*>) :: NamesT m a -> NamesT m b -> NamesT m b Source # (<*) :: NamesT m a -> NamesT m b -> NamesT m a Source #
Functor m => Functor (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods fmap :: (a -> b) -> NamesT m a -> NamesT m b Source # (<$) :: a -> NamesT m b -> NamesT m a Source #
Monad m => Monad (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods (>>=) :: NamesT m a -> (a -> NamesT m b) -> NamesT m b Source # (>>) :: NamesT m a -> NamesT m b -> NamesT m b Source # return :: a -> NamesT m a Source #

type Names = [String] Source #

A list of variable names from a context.

runNamesT :: Names -> NamesT m a -> m a Source #

runNames :: Names -> NamesT Identity a -> a Source #

currentCxt :: forall (m :: Type -> Type). Monad m => NamesT m Names Source #

cxtSubst :: forall (m :: Type -> Type) a. Monad m => Names -> NamesT m (Substitution' a) Source #

`cxtSubst Γ` returns the substitution needed to go from Γ to the current context.

Precondition `Γ` is not a subcontext of the current one.

inCxt :: forall (m :: Type -> Type) a. (Monad m, Subst a) => Names -> a -> NamesT m a Source #

`inCxt Γ t` takes a `t` in context `Γ` and produce an action that will return `t` weakened to the current context.

Fails whenever `cxtSubst Γ` would.

cl' :: forall (m :: Type -> Type) a. Applicative m => a -> NamesT m a Source #

Closed terms

cl :: Monad m => m a -> NamesT m a Source #

open :: forall (m :: Type -> Type) a. (Monad m, Subst a) => a -> NamesT m (NamesT m a) Source #

Open terms in the current context.

type Var (m :: Type -> Type) = forall b. (Subst b, DeBruijn b) => NamesT m b Source #

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.

bind :: forall (m :: Type -> Type) a. Monad m => ArgName -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a) -> NamesT m (Abs a) Source #

`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' :: forall (m :: Type -> Type) a. Monad m => ArgName -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a) -> NamesT m a Source #

Like `bind` but returns a bare term.

# Helpers to build lambda abstractions.

glam :: forall (m :: Type -> Type). Monad m => ArgInfo -> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term Source #

lam :: forall (m :: Type -> Type). Monad m => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term Source #

ilam :: forall (m :: Type -> Type). Monad m => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term Source #

# Combinators for n-ary binders.

data AbsN a Source #

Constructors

AbsN |

Fields

- absNName :: [ArgName]
- unAbsN :: a

#### Instances

Instances details

Functor AbsN Source # |
Instance details Defined in Agda.TypeChecking.Names Methods fmap :: (a -> b) -> AbsN a -> AbsN b Source # (<$) :: a -> AbsN b -> AbsN a Source #
Foldable AbsN Source # |

Instance details

Defined in Agda.TypeChecking.Names

Methods

fold :: Monoid m => AbsN m -> m Source #

foldMap :: Monoid m => (a -> m) -> AbsN a -> m Source #

foldMap' :: Monoid m => (a -> m) -> AbsN a -> m Source #

foldr :: (a -> b -> b) -> b -> AbsN a -> b Source #

foldr' :: (a -> b -> b) -> b -> AbsN a -> b Source #

foldl :: (b -> a -> b) -> b -> AbsN a -> b Source #

foldl' :: (b -> a -> b) -> b -> AbsN a -> b Source #

foldr1 :: (a -> a -> a) -> AbsN a -> a Source #

foldl1 :: (a -> a -> a) -> AbsN a -> a Source #

toList :: AbsN a -> [a] Source #

null :: AbsN a -> Bool Source #

length :: AbsN a -> Int Source #

elem :: Eq a => a -> AbsN a -> Bool Source #

maximum :: Ord a => AbsN a -> a Source #

minimum :: Ord a => AbsN a -> a Source #

sum :: Num a => AbsN a -> a Source #

product :: Num a => AbsN a -> a Source #

Traversable AbsN Source # |
Instance details Defined in Agda.TypeChecking.Names Methods traverse :: Applicative f => (a -> f b) -> AbsN a -> f (AbsN b) Source # sequenceA :: Applicative f => AbsN (f a) -> f (AbsN a) Source # mapM :: Monad m => (a -> m b) -> AbsN a -> m (AbsN b) Source # sequence :: Monad m => AbsN (m a) -> m (AbsN a) Source #
Subst a => Subst (AbsN a) Source # |

Instance details

Defined in Agda.TypeChecking.Names

Associated Types

type SubstArg (AbsN a) |
Instance details Defined in Agda.TypeChecking.Names type SubstArg (AbsN a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (AbsN a)) -> AbsN a -> AbsN a Source #

type SubstArg (AbsN a) Source # |
Instance details Defined in Agda.TypeChecking.Names type SubstArg (AbsN a) = SubstArg a

toAbsN :: Abs (AbsN a) -> AbsN a Source #

Will crash on `NoAbs`

absAppN :: Subst a => AbsN a -> [SubstArg a] -> a Source #

type ArgVars (m :: Type -> Type) = forall b. (Subst b, DeBruijn b) => [NamesT m (Arg b)] Source #

type Vars (m :: Type -> Type) = forall b. (Subst b, DeBruijn b) => [NamesT m b] Source #

bindN :: forall (m :: Type -> Type) a. Monad m => [ArgName] -> (Vars m -> NamesT m a) -> NamesT m (AbsN a) Source #

bindNArg :: forall (m :: Type -> Type) a. Monad m => [Arg ArgName] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a) Source #

type Vars1 (m :: Type -> Type) = forall b. (Subst b, DeBruijn b) => List1 (NamesT m b) Source #

bindN1 :: forall (m :: Type -> Type) a. Monad m => List1 ArgName -> (Vars1 m -> NamesT m a) -> NamesT m (AbsN a) Source #

glamN :: forall (m :: Type -> Type). (Functor m, Monad m) => [Arg ArgName] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term Source #

applyN :: forall (m :: Type -> Type) a. (Monad m, Subst a) => NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a Source #

applyN' :: forall (m :: Type -> Type) a. (Monad m, Subst a) => NamesT m (AbsN a) -> NamesT m [SubstArg a] -> NamesT m a Source #

abstractN :: forall (m :: Type -> Type) a. (Monad m, Abstract a) => NamesT m Telescope -> (Vars m -> NamesT m a) -> NamesT m a Source #

abstractT :: forall (m :: Type -> Type) a. (Monad m, Abstract a) => String -> NamesT m Type -> (Var m -> NamesT m a) -> NamesT m a Source #

lamTel :: forall (m :: Type -> Type). Monad m => NamesT m (Abs [Term]) -> NamesT m [Term] Source #

appTel :: forall (m :: Type -> Type). Monad m => NamesT m [Term] -> NamesT m Term -> NamesT m [Term] Source #