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

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
  - | DontCare
- 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 Tele a
  - = EmptyTel
  - | ExtendTel a (Abs (Tele a))
- type Telescope = Tele (Arg Type)
- data Abs a = Abs {
  - absName :: String
  - absBody :: a
  }
- telFromList :: [Arg (String, Type)] -> Telescope
- telToList :: Telescope -> [Arg (String, Type)]
- data Clauses = Clauses {
  - maybeOriginalClause :: Maybe Clause
  - translatedClause :: Clause
  }
- originalClause :: Clauses -> Clause
- 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 (Maybe (Arg Type)) [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

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 |
DontCare | nuked irrelevant and other stuff

Instances

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

data Type

Constructors

El Sort Term |

Instances

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

data Sort

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 |
Free Sort |
Strict Sort |
Raise Sort |
Subst Sort |
Abstract Sort |
Apply Sort |
AbstractTerm Sort |
GenC Sort |
EmbPrj Sort |
InstantiateFull Sort |
Normalise Sort |
Reduce Sort |
Instantiate Sort |
PrettyTCM Sort |
Occurs Sort |
HasMeta Sort |
ShrinkC Sort Sort |
Reify Sort Expr |

data Blocked t

Something where a meta variable may block reduction.

Constructors

Blocked MetaId t |
NotBlocked t |

Instances

Functor Blocked |
Typeable1 Blocked |
Applicative Blocked |
Foldable Blocked |
Traversable 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]

Type of argument lists.

data Tele a

Sequence of types. An argument of the first type is bound in later types and so on.

Constructors

EmptyTel |
ExtendTel a (Abs (Tele a)) |

Instances

Functor Tele |
Typeable1 Tele |
Abstract Telescope |
KillVar Telescope |
GenC Telescope |
EmbPrj Telescope |
Reduce Telescope |
Instantiate Telescope |
PrettyTCM Telescope |
ShrinkC Telescope Telescope |
Reify Telescope Telescope |
Eq a => Eq (Tele a) |
Data a => Data (Tele a) |
Ord a => Ord (Tele a) |
Show a => Show (Tele a) |
Sized (Tele a) |
KillRange a => KillRange (Tele a) |
Free a => Free (Tele a) |
Raise a => Raise (Tele a) |
Subst a => Subst (Tele a) |
Subst a => Apply (Tele a) |
InstantiateFull a => InstantiateFull (Tele a) |
Normalise a => Normalise (Tele a) |
ComputeOccurrences a => ComputeOccurrences (Tele a) |

type Telescope = Tele (Arg Type)

data Abs a

The body has (at least) one free variable.

Constructors

Abs |

Fields

absName :: String
absBody :: a

Instances

Functor Abs |
Typeable1 Abs |
Foldable Abs |
Traversable 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) |
Free a => Free (Abs a) |
TermLike a => TermLike (Abs a) |
Strict a => Strict (Abs a) |
Raise t => Raise (Abs t) |
Subst a => Subst (Abs a) |
(Subst a, AbstractTerm a) => AbstractTerm (Abs a) |
KillVar a => KillVar (Abs a) |
GenC a => GenC (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) |
ShrinkC a b => ShrinkC (Abs a) (Abs b) |
Reify i a => Reify (Abs i) (Name, a) |

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

telToList :: Telescope -> [Arg (String, Type)]

data Clauses

Pairs consisting of original and translated clauses.

Constructors

Clauses |

Fields

maybeOriginalClause :: Maybe Clause

  The original clause, before translation of record patterns. `Nothing` if the translated clause is identical to the original one.

translatedClause :: Clause

  The translated clause.

Instances

Data Clauses |
Show Clauses |
Typeable Clauses |
HasRange Clauses |
Abstract Clauses |
Apply Clauses |
EmbPrj Clauses |
InstantiateFull Clauses |

originalClause :: Clauses -> Clause

The original clause, before translation of record patterns.

data Clause

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. (Note: This optimisation has been disabled.)

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. The body binds the variables in the order they appear in the patterns.

For the purpose of the permutation and the body dot patterns count as variables. TODO: Change this!

Constructors

Clause |

Fields

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

Constructors

Body Term |
Bind (Abs ClauseBody) |
NoBind ClauseBody |
NoBody | for absurd clauses. A `NoBody` is never preceded by any `Bind` or `NoBind`.

Instances

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

data Pattern

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 (Maybe (Arg Type)) [Arg Pattern] | The type is ``Just` t`' iff the pattern is a record pattern. The scope used for the type is given by any outer scope plus the clause's telescope (`clauseTel`).
LitP Literal |

Instances

Data Pattern |
Show Pattern |
Typeable Pattern |
Raise Pattern |
Subst Pattern |
EmbPrj Pattern |
InstantiateFull Pattern |
Normalise Pattern |

newtype MetaId

Constructors

MetaId Nat |

Instances

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

arity :: Type -> Nat

Doesn't do any reduction.

argName :: Type -> String

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

# Views

data FunView

Constructors

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

funView :: Term -> FunView

# Smart constructors

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

Get the next higher sort.

sLub :: Sort -> Sort -> Sort

impossibleTerm :: String -> Int -> Term

module Agda.Syntax.Abstract.Name