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

Agda.Syntax.Internal

Contents

Synopsis

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) 
Sort Sort 
Level Level 
MetaV MetaId Args 
DontCare Term

irrelevant stuff

topSort :: TypeSource

Top sort (Setomega).

data Sort Source

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

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 Tele a Source

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.

data Abs a Source

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

Danger: doesn't shift variables properly

data Clause Source

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!

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

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.

Smart constructors

sSuc :: Sort -> SortSource

Get the next higher sort.