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

Safe Haskell | None

Agda.Syntax.Internal

Contents

- 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)
  - | Sort Sort
  - | Level Level
  - | MetaV MetaId Args
  - | DontCare Term
- data Type = El Sort Term
- data Elim
  - = Apply (Arg Term)
  - | Proj QName
- topSort :: Type
- data Sort
  - = Type Level
  - | Prop
  - | Inf
  - | DLub Sort (Abs Sort)
- newtype Level = Max [PlusLevel]
- data PlusLevel
  - = ClosedLevel Integer
  - | Plus Integer LevelAtom
- data LevelAtom
  - = MetaLevel MetaId Args
  - | BlockedLevel MetaId Term
  - | NeutralLevel Term
  - | UnreducedLevel Term
- 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 String a
  - | NoAbs String a
- unAbs :: Abs a -> a
- absName :: Abs a -> String
- data Clause = Clause {
  - clauseRange :: Range
  - clauseTel :: Telescope
  - clausePerm :: Permutation
  - clausePats :: [Arg Pattern]
  - clauseBody :: ClauseBody
  }
- data ClauseBody
  - = Body Term
  - | Bind (Abs 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
- blockingMeta :: Blocked t -> Maybe MetaId
- blocked :: MetaId -> a -> Blocked a
- notBlocked :: a -> Blocked a
- ignoreBlocking :: Blocked a -> a
- set0 :: Type
- set :: Integer -> Type
- prop :: Type
- sort :: Sort -> Type
- varSort :: Nat -> Sort
- sSuc :: Sort -> Sort
- levelSuc :: Level -> Level
- mkType :: Integer -> Sort
- getSort :: Type -> Sort
- unEl :: Type -> Term
- 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) |
Sort Sort |
Level Level |
MetaV MetaId Args |
DontCare Term | irrelevant stuff

Instances

Eq Term | Syntactic equality, ignores stuff below `DontCare`.
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 |
PrettyTCM Term |
InstantiateFull Term |
Normalise Term |
Reduce Term |
Instantiate Term |
Match Term |
MentionsMeta Term |
Occurs Term |
ComputeOccurrences Term |
HasPolarity Term |
Unquote Term |
ApplyHH Term |
UReduce Term |
StripAllProjections Term |
ShrinkC Term Term |
Reify Term Expr |
SubstHH Term (HomHet Term) |

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 |
PrettyTCM Telescope |
PrettyTCM Type |
InstantiateFull Type |
Normalise Type |
Reduce Telescope |
Reduce Type |
Instantiate Telescope |
Instantiate Type |
MentionsMeta Type |
Occurs Type |
ComputeOccurrences Type |
HasPolarity Type |
Unquote Type |
ToTerm Type |
PrimTerm Type |
ApplyHH Type |
UReduce Type |
ShrinkC Telescope Telescope |
ShrinkC Type Type |
Reify Telescope Telescope |
Reify Type Expr |
SubstHH Type (HomHet Type) |

data Elim

Constructors

Apply (Arg Term) |
Proj QName | name of a record projection

Instances

Eq Elim |
Ord Elim |
Show Elim |
Raise Elim |
PrettyTCM Elim |
InstantiateFull Elim |
Normalise Elim |
Reduce Elim |
Instantiate Elim |
MentionsMeta Elim |
Reify Elim Expr |

topSort :: Type

Top sort (Setomega).

data Sort

Constructors

Type Level |
Prop |
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 |
PrettyTCM Sort |
InstantiateFull Sort |
Normalise Sort |
Reduce Sort |
Instantiate Sort |
MentionsMeta Sort |
Occurs Sort |
Unquote Sort |
ShrinkC Sort Sort |
Reify Sort Expr |

newtype Level

Constructors

Max [PlusLevel] |

Instances

Eq Level |
Data Level |
Ord Level |
Show Level |
Typeable Level |
Sized Level |
KillRange Level |
Free Level |
TermLike Level |
Strict Level |
Raise Level |
Subst Level |
AbstractTerm Level |
EmbPrj Level |
PrettyTCM Level |
InstantiateFull Level |
Normalise Level |
Reduce Level |
Instantiate Level |
MentionsMeta Level |
Occurs Level |
ComputeOccurrences Level |
HasPolarity Level |
Unquote Level |
Reify Level Expr |

data PlusLevel

Constructors

ClosedLevel Integer |
Plus Integer LevelAtom |

Instances

Eq PlusLevel |
Data PlusLevel |
Ord PlusLevel |
Show PlusLevel |
Typeable PlusLevel |
Sized PlusLevel |
KillRange PlusLevel |
Free PlusLevel |
TermLike PlusLevel |
Strict PlusLevel |
Raise PlusLevel |
Subst PlusLevel |
AbstractTerm PlusLevel |
EmbPrj PlusLevel |
InstantiateFull PlusLevel |
Normalise PlusLevel |
Reduce PlusLevel |
Instantiate PlusLevel |
MentionsMeta PlusLevel |
Occurs PlusLevel |
ComputeOccurrences PlusLevel |
HasPolarity PlusLevel |

data LevelAtom

Constructors

MetaLevel MetaId Args |
BlockedLevel MetaId Term |
NeutralLevel Term |
UnreducedLevel Term |

Instances

Eq LevelAtom |
Data LevelAtom |
Ord LevelAtom |
Show LevelAtom |
Typeable LevelAtom |
Sized LevelAtom |
KillRange LevelAtom |
Free LevelAtom |
TermLike LevelAtom |
Strict LevelAtom |
Raise LevelAtom |
Subst LevelAtom |
AbstractTerm LevelAtom |
EmbPrj LevelAtom |
InstantiateFull LevelAtom |
Normalise LevelAtom |
Reduce LevelAtom |
Instantiate LevelAtom |
MentionsMeta LevelAtom |
Occurs LevelAtom |
ComputeOccurrences LevelAtom |
HasPolarity LevelAtom |

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) |
PrettyTCM a => PrettyTCM (Blocked a) |
Instantiate a => Instantiate (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)) | Abs is never NoAbs.

Instances

Functor Tele |
Typeable1 Tele |
Foldable Tele |
Traversable Tele |
Abstract Telescope |
KillVar Telescope |
GenC Telescope |
EmbPrj Telescope |
PrettyTCM Telescope |
Reduce Telescope |
Instantiate Telescope |
ShrinkC Telescope Telescope |
Reify Telescope Telescope |
(Raise a, Eq a) => Eq (Tele a) |
Data a => Data (Tele a) |
(Raise 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) |
(Raise a, InstantiateFull a) => InstantiateFull (Tele a) |
(Raise a, Normalise a) => Normalise (Tele a) |
MentionsMeta a => MentionsMeta (Tele a) |
ComputeOccurrences a => ComputeOccurrences (Tele a) |
SubstHH a b => SubstHH (Tele a) (Tele b) |

type Telescope = Tele (Arg Type)

data Abs a

The body has (at least) one free variable.

Constructors

Abs String a |
NoAbs String a |

Instances

Functor Abs |
Typeable1 Abs |
Foldable Abs |
Traversable Abs |
(Raise a, Eq a) => Eq (Abs a) |
Data a => Data (Abs a) |
(Raise 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) |
(Raise a, AbstractTerm a) => AbstractTerm (Abs a) |
KillVar a => KillVar (Abs a) |
GenC a => GenC (Abs a) |
EmbPrj a => EmbPrj (Abs a) |
(Raise t, InstantiateFull t) => InstantiateFull (Abs t) |
(Raise t, Normalise t) => Normalise (Abs t) |
(Raise t, Reduce t) => Reduce (Abs t) |
Instantiate t => Instantiate (Abs t) |
MentionsMeta t => MentionsMeta (Abs t) |
Occurs a => Occurs (Abs a) |
ComputeOccurrences a => ComputeOccurrences (Abs a) |
HasPolarity a => HasPolarity (Abs a) |
Unquote a => Unquote (Abs a) |
ShrinkC a b => ShrinkC (Abs a) (Abs b) |
SubstHH a b => SubstHH (Abs a) (Abs b) |
(Free i, Reify i a) => Reify (Abs i) (Name, a) |

unAbs :: Abs a -> a

Danger: doesn't shift variables properly

absName :: Abs a -> String

data Clause

A clause is a list of patterns and the clause body should `Bind`.

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) |
NoBody | for absurd clauses.

Instances

Data ClauseBody |
Show ClauseBody |
Typeable ClauseBody |
Free ClauseBody |
Strict ClauseBody |
Raise ClauseBody |
Subst ClauseBody |
Abstract ClauseBody |
Apply ClauseBody |
EmbPrj ClauseBody |
PrettyTCM ClauseBody |
InstantiateFull ClauseBody |
Normalise 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.

# Smart constructors

blockingMeta :: Blocked t -> Maybe MetaId

blocked :: MetaId -> a -> Blocked a

notBlocked :: a -> Blocked a

ignoreBlocking :: Blocked a -> a

set0 :: Type

set :: Integer -> Type

prop :: Type

sort :: Sort -> Type

varSort :: Nat -> Sort

sSuc :: Sort -> Sort

Get the next higher sort.

levelSuc :: Level -> Level

mkType :: Integer -> Sort

getSort :: Type -> Sort

unEl :: Type -> Term

impossibleTerm :: String -> Int -> Term

module Agda.Syntax.Abstract.Name