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

Agda.Syntax.Internal

Contents

Synopsis

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

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

data Blocked t

Something where a meta variable may block reduction.

Constructors

Blocked MetaId t 
NotBlocked t 

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.

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

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!

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 

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

blocked :: MetaId -> a -> Blocked a

sSuc :: Sort -> Sort

Get the next higher sort.

unEl :: Type -> Term