| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 |

Instances

Eq Term
Data Term
Ord Term
Show Term
Typeable Term
Sized Term
KillRange Term
TermLike Term
Strict Term
Free Term
Raise Term
Subst Term
Abstract Term
Apply Term
AbstractTerm Term
EmbPrj Term
InstantiateFull Term
Normalise Term
Reduce Term
Instantiate Term
Match Term
PrettyTCM Term
Occurs Term
HasMeta Term
ComputeOccurrences Term
HasPolarity Term
KillVar Term
GenC Term
ShowAsOptimizedTerm Term
ShowAsOptimizedType Term
ShowAsOptimizedKind Term
ShowAsUntypedTerm Term
Reify Term Expr
ShrinkC Term Term

data Type | Source

Constructors

El Sort Term |

Instances

Eq Type
Data Type
Ord Type
Show Type
Typeable Type
Error Type
Sized Type
KillRange Type
TermLike Type
Strict Type
Free Type
Raise Type
Subst Type
Abstract Type
Apply Type
AbstractTerm Type
EmbPrj Type
InstantiateFull Type
Normalise Type
Reduce Type
Instantiate Type
PrettyTCM Type
Occurs Type
ComputeOccurrences Type
HasPolarity Type
KillVar Type
GenC Type
ShowAsOptimizedType Type
ShowAsOptimizedKind Type
Reify Type Expr
ShrinkC Type Type

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

Instances

Eq Sort
Data Sort
Ord Sort
Show Sort
Typeable Sort
KillRange Sort
Strict Sort
Free Sort
Raise Sort
Subst Sort
Abstract Sort
Apply Sort
EmbPrj Sort
InstantiateFull Sort
Normalise Sort
Reduce Sort
Instantiate Sort
PrettyTCM Sort
Occurs Sort
HasMeta Sort
GenC Sort
Reify Sort Expr
ShrinkC Sort Sort

data Blocked t | Source

Something where a meta variable may block reduction.
Constructors

Blocked MetaId t |
NotBlocked t |

Instances

Functor Blocked
Typeable1 Blocked
Traversable Blocked
Foldable Blocked
Applicative Blocked
Eq t => Eq (Blocked t)
Data t => Data (Blocked t)
Ord t => Ord (Blocked t)
Show t => Show (Blocked t)
KillRange a => KillRange (Blocked a)
Raise t => Raise (Blocked t)
Subst t => Subst (Blocked t)
Apply t => Apply (Blocked t)
Instantiate a => Instantiate (Blocked a)
PrettyTCM a => PrettyTCM (Blocked a)
ShrinkC a b => ShrinkC (Blocked a) (Blocked b)

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

Instances

Eq Telescope
Data Telescope
Ord Telescope
Show Telescope
Typeable Telescope
Sized Telescope
KillRange Telescope
Free Telescope
Raise Telescope
Subst Telescope
Abstract Telescope
Apply Telescope
EmbPrj Telescope
InstantiateFull Telescope
Normalise Telescope
Reduce Telescope
Instantiate Telescope
PrettyTCM Telescope
ComputeOccurrences Telescope
KillVar Telescope
GenC Telescope
Reify Telescope Telescope
ShrinkC Telescope Telescope

data Abs a | Source

The body has (at least) one free variable.
Constructors

Abs |

absName :: String |
absBody :: a |

Instances

Functor Abs
Typeable1 Abs
Traversable Abs
Foldable Abs
Eq a => Eq (Abs a)
Data a => Data (Abs a)
Ord a => Ord (Abs a)
Show a => Show (Abs a)
Sized a => Sized (Abs a)
KillRange a => KillRange (Abs a)
TermLike a => TermLike (Abs a)
Strict a => Strict (Abs a)
Free a => Free (Abs a)
Raise t => Raise (Abs t)
(Data a, Subst a) => Subst (Abs a)
(Subst a, AbstractTerm a) => AbstractTerm (Abs a)
EmbPrj a => EmbPrj (Abs a)
InstantiateFull t => InstantiateFull (Abs t)
Normalise t => Normalise (Abs t)
Reduce t => Reduce (Abs t)
Instantiate t => Instantiate (Abs t)
Occurs a => Occurs (Abs a)
ComputeOccurrences a => ComputeOccurrences (Abs a)
HasPolarity a => HasPolarity (Abs a)
KillVar a => KillVar (Abs a)
GenC a => GenC (Abs a)
ShrinkC a b => ShrinkC (Abs a) (Abs b)
Reify i a => Reify (Abs i) ((,) Name a)

telFromList :: [Arg (String, Type)] -> Telescope | Source

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 |

Instances

Data Clause
Show Clause
Typeable Clause
HasRange Clause
Abstract Clause
Apply Clause
EmbPrj Clause
InstantiateFull Clause
ComputeOccurrences Clause

data ClauseBody | Source

Constructors

Body Term |
Bind (Abs ClauseBody) |
NoBind ClauseBody |
NoBody |

Instances

Data ClauseBody
Show ClauseBody
Typeable ClauseBody
Strict ClauseBody
Free ClauseBody
Subst ClauseBody
Abstract ClauseBody
Apply ClauseBody
EmbPrj ClauseBody
InstantiateFull ClauseBody
Normalise ClauseBody
Reify ClauseBody RHS

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 |

Instances

Data Pattern
Show Pattern
Typeable Pattern
Subst Pattern
EmbPrj Pattern
Normalise Pattern

newtype MetaId | Source

Constructors

MetaId Nat |

Instances

Enum MetaId
Eq MetaId
Integral MetaId
Data MetaId
Num MetaId
Ord MetaId
Real MetaId
Show MetaId
Typeable MetaId
EmbPrj MetaId
HasFresh MetaId FreshThings
ToConcrete MetaId Expr
Reify MetaId Expr

arity :: Type -> Nat | Source

Doesn't do any reduction.

argName :: Type -> String | Source

Suggest a name for the first argument of a function of the given type.
Views

data FunView | Source

Constructors

FunV (Arg Type) Term | second arg is the entire type (`Pi` or `Fun`).
NoFunV Term |

funView :: Term -> FunView | Source

Smart constructors

blockingMeta :: Blocked t -> Maybe MetaId | Source

blocked :: MetaId -> a -> Blocked a | Source

notBlocked :: a -> Blocked a | Source

ignoreBlocking :: Blocked a -> a | Source

teleLam :: Telescope -> Term -> Term | Source

getSort :: Type -> Sort | Source

unEl :: Type -> Term | Source

sSuc :: Sort -> Sort | Source

Get the next higher sort.

sLub :: Sort -> Sort -> Sort | Source

impossibleTerm :: String -> Int -> Term | Source

module Agda.Syntax.Abstract.Name
Produced by Haddock version 2.4.2