Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone





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.


Var !Int Args

x vs neutral

Lam Hiding (Abs Term)

terms are beta normal

Lit Literal 
Def QName Args

f vs, possibly a redex

Con QName Args
c vs
Pi (Dom Type) (Abs Type)

dependent or non-dependent function space

Sort Sort 
Level Level 
MetaV !MetaId Args 
DontCare Term

Irrelevant stuff in relevant position, but created in an irrelevant context. Basically, an internal version of the irrelevance axiom .irrAx : .A -> A.

Shared !(Ptr Term)

Explicit sharing

type Args = [Arg Term]Source

Type of argument lists.

data Elim Source

Eliminations, subsuming applications and projections. Used for a view which exposes the head of a neutral term.


Apply (Arg Term) 
Proj QName

name of a record projection

data Abs a Source

Binder. Abs: The bound variable might appear in the body. NoAbs is pseudo-binder, it does not introduce a fresh variable, similar to the const of Haskell.



The body has (at least) one free variable. Danger: unAbs doesn't shift variables properly


absName :: String
unAbs :: a


absName :: String
unAbs :: a


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

data Tele a Source

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


ExtendTel a (Abs (Tele a))

Abs is never NoAbs.

data Sort Source



Type Level 
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

newtype MetaId Source

A meta variable identifier is just a natural number.


MetaId Nat 

data Blocked t Source

Something where a meta variable may block reduction.


Blocked MetaId t 
NotBlocked t 


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.

clauseTel ~ permute clausePerm (patternVars clausPats)

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.


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 

patternVars :: Arg Pattern -> [Arg (Either String Term)]Source

Extract pattern variables in left-to-right order. A DotP is also treated as variable (see docu for Clause).

properlyMatching :: Pattern -> BoolSource

Does the pattern perform a match that could fail?

Smart constructors

updateSharedFM :: (Monad m, Applicative m, Traversable f) => (Term -> m (f Term)) -> Term -> m (f Term)Source

Typically m would be TCM and f would be Blocked.

updateSharedM :: Monad m => (Term -> m Term) -> Term -> m TermSource

var :: Nat -> TermSource

An unapplied variable.

typeDontCare :: TypeSource

A dummy type.

topSort :: TypeSource

Top sort (Setomega).

sSuc :: Sort -> SortSource

Get the next higher sort.

Handling blocked terms.

Simple operations on terms and types.

stripDontCare :: Term -> TermSource

Removing a topmost DontCare constructor.

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.

Show instances.

Sized instances.

KillRange instances.

UniverseBi instances.