Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Syntax.Internal
Contents
Views
Smart constructors
Synopsis
data Term
= Var Nat Args
| Lam Hiding (Abs Term)
| Lit Literal
| Def QName Args
| Con QName Args
| Pi (Arg Type) (Abs Type)
| Fun (Arg Type) Type
| Sort Sort
| MetaV MetaId Args
data Type = El Sort Term
data Sort
= Type Term
| Prop
| Lub Sort Sort
| Suc Sort
| MetaS MetaId Args
| Inf
| DLub Sort (Abs Sort)
data Blocked t
= Blocked MetaId t
| NotBlocked t
type Args = [Arg Term]
data Telescope
= EmptyTel
| ExtendTel (Arg Type) (Abs Telescope)
data Abs a = Abs {
absName :: String
absBody :: a
}
telFromList :: [Arg (String, Type)] -> Telescope
telToList :: Telescope -> [Arg (String, Type)]
data Clause = Clause {
clauseRange :: Range
clauseTel :: Telescope
clausePerm :: Permutation
clausePats :: [Arg Pattern]
clauseBody :: ClauseBody
}
data ClauseBody
= Body Term
| Bind (Abs ClauseBody)
| NoBind ClauseBody
| NoBody
data Pattern
= VarP String
| DotP Term
| ConP QName [Arg Pattern]
| LitP Literal
newtype MetaId = MetaId Nat
arity :: Type -> Nat
argName :: Type -> String
data FunView
= FunV (Arg Type) Term
| NoFunV Term
funView :: Term -> FunView
blockingMeta :: Blocked t -> Maybe MetaId
blocked :: MetaId -> a -> Blocked a
notBlocked :: a -> Blocked a
ignoreBlocking :: Blocked a -> a
teleLam :: Telescope -> Term -> Term
getSort :: Type -> Sort
unEl :: Type -> Term
sSuc :: Sort -> Sort
sLub :: Sort -> Sort -> Sort
impossibleTerm :: String -> Int -> Term
module Agda.Syntax.Abstract.Name
Documentation
data Term Source

Raw values.

Def is used for both defined and undefined constants. Assume there is a type declaration and a definition for every constant, even if the definition is an empty list of clauses.

Constructors
Var Nat Args
Lam Hiding (Abs Term)terms are beta normal
Lit Literal
Def QName Args
Con QName Args
Pi (Arg Type) (Abs Type)
Fun (Arg Type) Type
Sort Sort
MetaV MetaId Args
data Type Source
Constructors
El Sort Term
data Sort Source
Constructors
Type Term
Prop
Lub Sort Sort
Suc Sort
MetaS MetaId Args
Inf
DLub Sort (Abs Sort)if the free variable occurs in the second sort the whole thing should reduce to Inf, otherwise it's the normal Lub
data Blocked t Source
Something where a meta variable may block reduction.
Constructors
Blocked MetaId t
NotBlocked t
type Args = [Arg Term]Source
Type of argument lists.
data Telescope Source
Sequence of types. An argument of the first type is bound in later types and so on.
Constructors
EmptyTel
ExtendTel (Arg Type) (Abs Telescope)
data Abs a Source
The body has (at least) one free variable.
Constructors
Abs
absName :: String
absBody :: a
telFromList :: [Arg (String, Type)] -> TelescopeSource
telToList :: Telescope -> [Arg (String, Type)]Source
data Clause Source

A clause is a list of patterns and the clause body should Bind or NoBind in the order the variables occur in the patterns. The NoBind constructor is an optimisation to avoid substituting for variables that aren't used.

The telescope contains the types of the pattern variables and the permutation is how to get from the order the variables occur in the patterns to the order they occur in the telescope. For the purpose of the permutation dot patterns counts as variables. TODO: change this!

Constructors
Clause
clauseRange :: Range
clauseTel :: Telescope
clausePerm :: Permutation
clausePats :: [Arg Pattern]
clauseBody :: ClauseBody
data ClauseBody Source
Constructors
Body Term
Bind (Abs ClauseBody)
NoBind ClauseBody
NoBody
data Pattern Source
Patterns are variables, constructors, or wildcards. QName is used in ConP rather than Name since a constructor might come from a particular namespace. This also meshes well with the fact that values (i.e. the arguments we are matching with) use QName.
Constructors
VarP String
DotP Term
ConP QName [Arg Pattern]
LitP Literal
newtype MetaId Source
Constructors
MetaId Nat
arity :: Type -> NatSource
Doesn't do any reduction.
argName :: Type -> StringSource
Suggest a name for the first argument of a function of the given type.
Views
data FunView Source
Constructors
FunV (Arg Type) Termsecond arg is the entire type (Pi or Fun).
NoFunV Term
funView :: Term -> FunViewSource
Smart constructors
blockingMeta :: Blocked t -> Maybe MetaIdSource
blocked :: MetaId -> a -> Blocked aSource
notBlocked :: a -> Blocked aSource
ignoreBlocking :: Blocked a -> aSource
teleLam :: Telescope -> Term -> TermSource
getSort :: Type -> SortSource
unEl :: Type -> TermSource
sSuc :: Sort -> SortSource
Get the next higher sort.
sLub :: Sort -> Sort -> SortSource
impossibleTerm :: String -> Int -> TermSource
module Agda.Syntax.Abstract.Name
Produced by Haddock version 2.6.0