Agda.Syntax.Internal

Documentation

type Color = Term

type ArgInfo = ArgInfo Color

type Arg a = Arg Color a

type Dom a = Dom Color a

type NamedArg a = NamedArg Color a

type Args = [Arg Term]

Type of argument lists.

type NamedArgs = [NamedArg Term]

data ConHead

Store the names of the record fields in the constructor. This allows reduction of projection redexes outside of TCM. For instance, during substitution and application.

Constructors

ConHead

Fields

conName :: QName

The name of the constructor.

conInductive :: Induction

Record constructors can be coinductive.

conFields :: [QName]

The name of the record fields. Empty list for data constructors. Arg is not needed here since it is stored in the constructor args.

Instances

Eq ConHead

Ord ConHead

Show ConHead

KillRange ConHead

SetRange ConHead

HasRange ConHead

LensConName ConHead

PrettyTCM ConHead

Unquote ConHead

ShrinkC ConName ConHead

class LensConName a where

Minimal complete definition

getConName

Methods

getConName :: a -> QName

setConName :: QName -> a -> a

mapConName :: (QName -> QName) -> a -> a

Instances

LensConName ConHead

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 !Int Elims

x es neutral

Lam ArgInfo (Abs Term)

Terms are beta normal. Relevance is ignored

ExtLam [Clause] Args

Only used by unquote --> reify. Should never appear elsewhere.

Lit Literal

Def QName Elims

f es, possibly a delta/iota-redex

Con ConHead Args

c vs

Pi (Dom Type) (Abs Type)

dependent or non-dependent function space

Sort Sort

Level Level

MetaV !MetaId Elims

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

Instances

Show Term

Null ClauseBody

Pretty Type

Pretty Elim

Pretty Term

KillRange Term

TermSize Term

IsProjElim Elim

GetDefs ClauseBody

GetDefs Type

GetDefs Term

TermLike Type

TermLike Term

Free ClauseBody

Free Type

Free Term

GetBody ClauseBody

TeleNoAbs Telescope

TeleNoAbs ListTel

Subst ClauseBody

Subst Term

Abstract ClauseBody

Abstract Telescope

Abstract Type

Abstract Term

Apply ClauseBody

Apply Type

Apply Term

AbstractTerm Type

AbstractTerm Term

IsPrefixOf Elims

IsPrefixOf Term

IsPrefixOf Args

KillVar Telescope

KillVar Type

KillVar Term

GenC Telescope

GenC Type

GenC Term

HasOptions NLM

AddContext Telescope

UnFreezeMeta Type

UnFreezeMeta Term

IsInstantiatedMeta Term

PrettyTCM ClauseBody

PrettyTCM Telescope

PrettyTCM Type

PrettyTCM Elim

PrettyTCM Term

MentionsMeta Type

MentionsMeta Elim

MentionsMeta Term

InstantiateFull ClauseBody

InstantiateFull Term

Normalise ClauseBody

Normalise Type

Normalise Elim

Normalise Term

Simplify ClauseBody

Simplify Type

Simplify Elim

Simplify Term

Reduce Telescope

Reduce Type

Reduce Elim

Reduce Term

Instantiate Telescope

Instantiate Type

Instantiate Elim

Instantiate Term

Match Term

SynEq Type

Syntactic equality ignores sorts.

SynEq Term

Syntactic term equality ignores DontCare stuff.

DropArgs ClauseBody

NOTE: does not go into the body, so does not work for recursive functions.

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

Injectible Term

Evaluate Term

ComputeOccurrences Type

ComputeOccurrences Term

FoldRigid Type

FoldRigid Term

Occurs Type

Occurs Term

NoProjectedVar Term

HasPolarity Type

HasPolarity Term

ToTerm Type

ToTerm Term

ToTerm ArgInfo

PrimTerm Type

ApplyHH Type

ApplyHH Term

UReduce Type

UReduce Term

ForcedVariables Term

Assumes that the term is in normal form.

Unquote Type

Unquote Term

Unquote ArgInfo

UniverseBi Elims Pattern

UniverseBi Elims Term

UniverseBi Args Pattern

UniverseBi Args Term

Free' ClauseBody c

Free' Type c

Free' Term c

ShrinkC Telescope Telescope

ShrinkC Type Type

ShrinkC Term Term

Reify ClauseBody RHS

Reify Telescope Telescope

Reify Type Expr

Reify Elim Expr

Reify Term Expr

Reify ArgInfo ArgInfo

Match NLPat Term

PatternFrom Term NLPat

ConvColor ArgInfo ArgInfo

SubstHH Type (HomHet Type)

SubstHH Term (HomHet Term)

Pretty a => Pretty (Arg a)

SgTel (Dom (ArgName, Type))

SgTel (Dom Type)

TermLike a => TermLike (Dom a)

TermLike a => TermLike (Arg a)

Free a => Free (Dom a)

Free a => Free (Arg a)

Subst a => Subst (Dom a)

Subst a => Subst (Arg a)

AbstractTerm a => AbstractTerm (Dom a)

AbstractTerm a => AbstractTerm (Arg a)

KillVar a => KillVar (Dom a)

KillVar a => KillVar (Arg a)

AddContext (Dom (String, Type))

AddContext (Dom (Name, Type))

AddContext (Dom Type)

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a)

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a)

MentionsMeta t => MentionsMeta (Dom t)

MentionsMeta t => MentionsMeta (Arg t)

InstantiateFull t => InstantiateFull (Dom t)

InstantiateFull t => InstantiateFull (Arg t)

Normalise t => Normalise (Dom t)

Normalise t => Normalise (Arg t)

Simplify t => Simplify (Dom t)

Simplify t => Simplify (Arg t)

Reduce t => Reduce (Dom t)

Reduce t => Reduce (Arg t)

Instantiate t => Instantiate (Dom t)

Instantiate t => Instantiate (Arg t)

Match a => Match (Arg a)

Injectible a => Injectible (Arg a)

Evaluate a => Evaluate (Arg a)

ComputeOccurrences a => ComputeOccurrences (Dom a)

ComputeOccurrences a => ComputeOccurrences (Arg a)

FoldRigid a => FoldRigid (Dom a)

FoldRigid a => FoldRigid (Arg a)

Occurs a => Occurs (Dom a)

Occurs a => Occurs (Arg a)

NoProjectedVar a => NoProjectedVar (Arg a)

HasPolarity a => HasPolarity (Dom a)

HasPolarity a => HasPolarity (Arg a)

UReduce a => UReduce (Arg a)

Unquote a => Unquote (Arg a)

UniverseBi [Term] Term

Free' a c => Free' (Dom a) c

Free' a c => Free' (Arg a) c

ShrinkC a b => ShrinkC (Dom a) (Dom b)

ShrinkC a b => ShrinkC (Arg a) (Arg b)

Reify i a => Reify (Dom i) (Arg a)

Reify i a => Reify (Arg i) (Arg a)

Skip reification of implicit and irrelevant args if option is off.

Match a b => Match (Dom a) (Dom b)

Match a b => Match (Arg a) (Arg b)

PatternFrom a b => PatternFrom (Dom a) (Dom b)

PatternFrom a b => PatternFrom (Arg a) (Arg b)

SubstHH a b => SubstHH (Dom a) (Dom b)

SubstHH a b => SubstHH (Arg a) (Arg b)

ConvColor (Dom e) (Dom e)

ConvColor (Arg e) (Arg e)

SgTel (ArgName, Dom Type)

AddContext ([WithHiding Name], Dom Type)

AddContext ([Name], Dom Type)

AddContext (String, Dom Type)

AddContext (Name, Dom Type)

UniverseBi ([Type], [Clause]) Pattern

UniverseBi ([Type], [Clause]) Term

data Elim' a

Eliminations, subsuming applications and projections.

Constructors

Apply (Arg a)

Proj QName

name of a record projection

Instances

Functor Elim'

Foldable Elim'

Traversable Elim'

Pretty Elim

IsProjElim Elim

IsPrefixOf Elims

PrettyTCM Elim

MentionsMeta Elim

Normalise Elim

Simplify Elim

Reduce Elim

Instantiate Elim

UniverseBi Elims Pattern

UniverseBi Elims Term

Reify Elim Expr

Show a => Show (Elim' a)

KillRange a => KillRange (Elim' a)

GetDefs a => GetDefs (Elim' a)

TermLike a => TermLike (Elim' a)

Free a => Free (Elim' a)

Subst a => Subst (Elim' a)

AbstractTerm a => AbstractTerm (Elim' a)

KillVar a => KillVar (Elim' a)

GenC a => GenC (Elim' a)

PrettyTCM (Elim' NLPat)

PrettyTCM (Elim' DisplayTerm)

InstantiateFull a => InstantiateFull (Elim' a)

Match a => Match (Elim' a)

SynEq a => SynEq (Elim' a)

Injectible a => Injectible (Elim' a)

Evaluate a => Evaluate (Elim' a)

ComputeOccurrences a => ComputeOccurrences (Elim' a)

FoldRigid a => FoldRigid (Elim' a)

Occurs a => Occurs (Elim' a)

HasPolarity a => HasPolarity (Elim' a)

Unquote a => Unquote (Elim' a)

Free' a c => Free' (Elim' a) c

ShrinkC a b => ShrinkC (Elim' a) (Elim' b)

Match a b => Match (Elim' a) (Elim' b)

PatternFrom a b => PatternFrom (Elim' a) (Elim' b)

type Elim = Elim' Term

type Elims

Arguments

 = [Elim]

eliminations ordered left-to-right.

type ArgName = String

Names in binders and arguments.

argNameToString :: ArgName -> String

stringToArgName :: String -> ArgName

appendArgNames :: ArgName -> ArgName -> ArgName

nameToArgName :: Name -> ArgName

data Abs a

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.

Constructors

Abs

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

Fields

absName :: ArgName

unAbs :: a

NoAbs

Fields

absName :: ArgName

unAbs :: a

Instances

Functor Abs

Foldable Abs

Traversable Abs

Decoration Abs

Suggest String (Abs b)

Suggest Name (Abs b)

Show a => Show (Abs a)

Sized a => Sized (Abs a)

KillRange a => KillRange (Abs a)

LensSort a => LensSort (Abs a)

GetDefs a => GetDefs (Abs a)

TermLike a => TermLike (Abs a)

Free a => Free (Abs a)

Subst a => Subst (Abs a)

(Subst a, AbstractTerm a) => AbstractTerm (Abs a)

KillVar a => KillVar (Abs a)

GenC a => GenC (Abs a)

UnFreezeMeta a => UnFreezeMeta (Abs a)

IsInstantiatedMeta a => IsInstantiatedMeta (Abs a)

Does not worry about raising.

MentionsMeta t => MentionsMeta (Abs t)

(Subst t, InstantiateFull t) => InstantiateFull (Abs t)

(Subst t, Normalise t) => Normalise (Abs t)

(Subst t, Simplify t) => Simplify (Abs t)

(Subst t, Reduce t) => Reduce (Abs t)

Instantiate t => Instantiate (Abs t)

(Subst a, SynEq a) => SynEq (Abs a)

Evaluate a => Evaluate (Abs a)

ComputeOccurrences a => ComputeOccurrences (Abs a)

(Subst a, FoldRigid a) => FoldRigid (Abs a)

(Occurs a, Subst a) => Occurs (Abs a)

HasPolarity a => HasPolarity (Abs a)

Unquote a => Unquote (Abs a)

Free' a c => Free' (Abs a) c

Suggest (Abs a) (Abs b)

ShrinkC a b => ShrinkC (Abs a) (Abs b)

(Match a b, Subst b, Free b, PrettyTCM a, PrettyTCM b) => Match (Abs a) (Abs b)

PatternFrom a b => PatternFrom (Abs a) (Abs b)

SubstHH a b => SubstHH (Abs a) (Abs b)

(Free i, Reify i a) => Reify (Abs i) (Name, a)

data Type' a

Types are terms with a sort annotation.

Constructors

El

Fields

_getSort :: Sort

unEl :: a

Instances

Functor Type'

Foldable Type'

Traversable Type'

Decoration Type'

Pretty Type

GetDefs Type

TermLike Type

Free Type

TeleNoAbs Telescope

TeleNoAbs ListTel

Abstract Telescope

Abstract Type

Apply Type

AbstractTerm Type

KillVar Telescope

KillVar Type

GenC Telescope

GenC Type

AddContext Telescope

UnFreezeMeta Type

PrettyTCM Telescope

PrettyTCM Type

MentionsMeta Type

Normalise Type

Simplify Type

Reduce Telescope

Reduce Type

Instantiate Telescope

Instantiate Type

SynEq Type

Syntactic equality ignores sorts.

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

ComputeOccurrences Type

FoldRigid Type

Occurs Type

HasPolarity Type

ToTerm Type

PrimTerm Type

ApplyHH Type

UReduce Type

Unquote Type

Free' Type c

ShrinkC Telescope Telescope

ShrinkC Type Type

Reify Telescope Telescope

Reify Type Expr

SubstHH Type (HomHet Type)

Show a => Show (Type' a)

KillRange a => KillRange (Type' a)

SgTel (Dom (ArgName, Type))

SgTel (Dom Type)

LensSort (Type' a)

Subst a => Subst (Type' a)

AddContext (Dom (String, Type))

AddContext (Dom (Name, Type))

AddContext (Dom Type)

PrettyTCM (Type' NLPat)

InstantiateFull a => InstantiateFull (Type' a)

Match a b => Match (Type' a) (Type' b)

PatternFrom a b => PatternFrom (Type' a) (Type' b)

SgTel (ArgName, Dom Type)

AddContext ([WithHiding Name], Dom Type)

AddContext ([Name], Dom Type)

AddContext (String, Dom Type)

AddContext (Name, Dom Type)

UniverseBi ([Type], [Clause]) Pattern

UniverseBi ([Type], [Clause]) Term

type Type = Type' Term

class LensSort a where

Minimal complete definition

lensSort

Methods

lensSort :: Lens' Sort a

getSort :: a -> Sort

Instances

LensSort (Type' a)

LensSort a => LensSort (Abs a)

LensSort a => LensSort (Dom c a)

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

Foldable Tele

Traversable Tele

TeleNoAbs Telescope

Abstract Telescope

KillVar Telescope

GenC Telescope

AddContext Telescope

PrettyTCM Telescope

Reduce Telescope

Instantiate Telescope

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

ShrinkC Telescope Telescope

Reify Telescope Telescope

Show a => Show (Tele a)

Null (Tele a)

Sized (Tele a)

The size of a telescope is its length (as a list).

KillRange a => KillRange (Tele a)

Free a => Free (Tele a)

Subst a => Subst (Tele a)

Subst a => Apply (Tele a)

MentionsMeta a => MentionsMeta (Tele a)

(Subst a, InstantiateFull a) => InstantiateFull (Tele a)

(Subst a, Normalise a) => Normalise (Tele a)

(Subst a, Simplify a) => Simplify (Tele a)

ComputeOccurrences a => ComputeOccurrences (Tele a)

Free' a c => Free' (Tele a) c

SubstHH a b => SubstHH (Tele a) (Tele b)

type Telescope = Tele (Dom Type)

mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)

A traversal for the names in a telescope.

mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a

replaceEmptyName :: ArgName -> Tele a -> Tele a

data Sort

Sorts.

Constructors

Type Level

Set ℓ.

Prop

Dummy sort.

Inf

Setω.

SizeUniv

SizeUniv, a sort inhabited by type Size.

DLub Sort (Abs Sort)

Dependent least upper bound. If the free variable occurs in the second sort, the whole thing should reduce to Inf, otherwise it's the normal lub.

Instances

Show Sort

Pretty Sort

KillRange Sort

TermSize Sort

GetDefs Sort

Free Sort

Subst Sort

Abstract Sort

Apply Sort

AbstractTerm Sort

GenC Sort

UnFreezeMeta Sort

PrettyTCM Sort

MentionsMeta Sort

InstantiateFull Sort

Normalise Sort

Simplify Sort

Reduce Sort

Instantiate Sort

Match Sort

SynEq Sort

FoldRigid Sort

Occurs Sort

Unquote Sort

Free' Sort c

ShrinkC Sort Sort

Reify Sort Expr

newtype Level

A level is a maximum expression of 0..n PlusLevel expressions each of which is a number or an atom plus a number.

The empty maximum is the canonical representation for level 0.

Constructors

Max [PlusLevel]

Instances

Show Level

Pretty Level

KillRange Level

TermSize Level

GetDefs Level

TermLike Level

Free Level

Subst Level

AbstractTerm Level

UnFreezeMeta Level

IsInstantiatedMeta Level

PrettyTCM Level

MentionsMeta Level

InstantiateFull Level

Normalise Level

Simplify Level

Reduce Level

Instantiate Level

Match Level

SynEq Level

ComputeOccurrences Level

FoldRigid Level

Occurs Level

HasPolarity Level

Unquote Level

Free' Level c

Reify Level Expr

data PlusLevel

Constructors

ClosedLevel Integer

n, to represent Setₙ.

Plus Integer LevelAtom

n + ℓ.

Instances

Show PlusLevel

Pretty PlusLevel

KillRange PlusLevel

TermSize PlusLevel

GetDefs PlusLevel

TermLike PlusLevel

Free PlusLevel

Subst PlusLevel

AbstractTerm PlusLevel

UnFreezeMeta PlusLevel

IsInstantiatedMeta PlusLevel

MentionsMeta PlusLevel

InstantiateFull PlusLevel

Normalise PlusLevel

Simplify PlusLevel

Reduce PlusLevel

Instantiate PlusLevel

SynEq PlusLevel

ComputeOccurrences PlusLevel

FoldRigid PlusLevel

Occurs PlusLevel

HasPolarity PlusLevel

Free' PlusLevel c

data LevelAtom

An atomic term of type Level.

Constructors

MetaLevel MetaId Elims

A meta variable targeting Level under some eliminations.

BlockedLevel MetaId Term

A term of type Level whose reduction is blocked by a meta.

NeutralLevel NotBlocked Term

A neutral term of type Level.

UnreducedLevel Term

Introduced by instantiate, removed by reduce.

Instances

Show LevelAtom

Pretty LevelAtom

KillRange LevelAtom

TermSize LevelAtom

GetDefs LevelAtom

TermLike LevelAtom

Free LevelAtom

Subst LevelAtom

AbstractTerm LevelAtom

UnFreezeMeta LevelAtom

IsInstantiatedMeta LevelAtom

MentionsMeta LevelAtom

InstantiateFull LevelAtom

Normalise LevelAtom

Simplify LevelAtom

Reduce LevelAtom

Instantiate LevelAtom

SynEq LevelAtom

ComputeOccurrences LevelAtom

FoldRigid LevelAtom

Occurs LevelAtom

HasPolarity LevelAtom

Free' LevelAtom c

data NotBlocked

Even if we are not stuck on a meta during reduction we can fail to reduce a definition by pattern matching for another reason.

Constructors

StuckOn Elim

The Elim is neutral and blocks a pattern match.

Underapplied

Not enough arguments were supplied to complete the matching.

AbsurdMatch

We matched an absurd clause, results in a neutral Def.

MissingClauses

We ran out of clauses, all considered clauses produced an actual mismatch. This can happen when try to reduce a function application but we are still missing some function clauses. See Agda.TypeChecking.Patterns.Match.

ReallyNotBlocked

Reduction was not blocked, we reached a whnf which can be anything but a stuck Def.

Instances

Show NotBlocked

Monoid NotBlocked

ReallyNotBlocked is the unit. MissingClauses is dominant. StuckOn{} should be propagated, if tied, we take the left.

data Blocked t

Something where a meta variable may block reduction.

Constructors

Blocked

Fields

theBlockingMeta :: MetaId

ignoreBlocking :: t

NotBlocked

Fields

blockingStatus :: NotBlocked

ignoreBlocking :: t

Instances

Functor Blocked

Applicative Blocked

Blocking by a meta is dominant.

Foldable Blocked

Traversable Blocked

Monoid Blocked_

HasOptions NLM

Show t => Show (Blocked t)

KillRange a => KillRange (Blocked a)

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 Blocked_ = Blocked ()

Blocked t without the t.

stuckOn :: Elim -> NotBlocked -> NotBlocked

When trying to reduce f es, on match failed on one elimination e ∈ es that came with info r :: NotBlocked. stuckOn e r produces the new NotBlocked info.

MissingClauses must be propagated, as this is blockage that can be lifted in the future (as more clauses are added).

StuckOn e0 is also propagated, since it provides more precise information as StuckOn e (as e0 is the original reason why reduction got stuck and usually a subterm of e). An information like StuckOn (Apply (Arg info (Var i []))) (stuck on a variable) could be used by the lhs/coverage checker to trigger a split on that (pattern) variable.

In the remaining cases for r, we are terminally stuck due to StuckOn e. Propagating AbsurdMatch does not seem useful.

Underapplied must not be propagated, as this would mean that f es is underapplied, which is not the case (it is stuck). Note that Underapplied can only arise when projection patterns were missing to complete the original match (in e). (Missing ordinary pattern would mean the e is of function type, but we cannot match against something of function type.)

Definitions

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.

clauseTel ~ permute clausePerm (patternVars namedClausePats)

Terms in dot patterns are valid in the clause telescope.

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

Constructors

Clause

Fields

clauseRange :: Range

clauseTel :: Telescope

Δ: The types of the pattern variables.

clausePerm :: Permutation

π with Γ ⊢ renamingR π : Δ, which means Δ ⊢ renaming π : Γ.

namedClausePats :: [NamedArg Pattern]

let Γ = patternVars namedClausePats

clauseBody :: ClauseBody

λΓ.v

clauseType :: Maybe (Arg Type)

Δ ⊢ t. The type of the rhs under clauseTel. Used, e.g., by TermCheck. Can be Irrelevant if we encountered an irrelevant projection pattern on the lhs.

Instances

Show Clause

Null Clause

A null clause is one with no patterns and no rhs. Should not exist in practice.

KillRange Clause

HasRange Clause

GetDefs Clause

Free Clause

FunArity Clause

Get the number of initial Apply patterns in a clause.

GetBody Clause

Subst Clause

Abstract Clause

Abstract FunctionInverse

Apply Clause

Apply FunctionInverse

PrettyTCM Clause

PrettyTCM NamedClause

InstantiateFull Clause

InstantiateFull FunctionInverse

DropArgs Clause

NOTE: does not work for recursive functions.

DropArgs FunctionInverse

ComputeOccurrences Clause

Occurs Clause

Unquote Clause

Free' Clause c

Reify NamedClause Clause

FunArity [Clause]

Get the number of common initial Apply patterns in a list of clauses.

UniverseBi ([Type], [Clause]) Pattern

UniverseBi ([Type], [Clause]) Term

clausePats :: Clause -> [Arg Pattern]

data ClauseBodyF a

Constructors

Body a

Bind (Abs (ClauseBodyF a))

NoBody

for absurd clauses.

Instances

Functor ClauseBodyF

Foldable ClauseBodyF

Traversable ClauseBodyF

Null ClauseBody

GetDefs ClauseBody

Free ClauseBody

GetBody ClauseBody

Subst ClauseBody

Abstract ClauseBody

Apply ClauseBody

PrettyTCM ClauseBody

InstantiateFull ClauseBody

Normalise ClauseBody

Simplify ClauseBody

DropArgs ClauseBody

NOTE: does not go into the body, so does not work for recursive functions.

Free' ClauseBody c

Reify ClauseBody RHS

Show a => Show (ClauseBodyF a)

Pretty a => Pretty (ClauseBodyF a)

KillRange a => KillRange (ClauseBodyF a)

type ClauseBody = ClauseBodyF Term

imapClauseBody :: (Nat -> a -> b) -> ClauseBodyF a -> ClauseBodyF b

type PatVarName = ArgName

Pattern variables.

patVarNameToString :: PatVarName -> String

nameToPatVarName :: Name -> PatVarName

data Pattern' x

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 x

x

DotP Term

.t

ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]

c ps The subpatterns do not contain any projection copatterns.

LitP Literal

E.g. 5, "hello".

ProjP QName

Projection copattern. Can only appear by itself.

Instances

Functor Pattern'

Foldable Pattern'

Traversable Pattern'

KillRange Pattern

IsProjP Pattern

Subst Pattern

PrettyTCM DeBruijnPattern

PrettyTCM Pattern

InstantiateFull Pattern

Normalise Pattern

Unquote Pattern

UniverseBi Elims Pattern

UniverseBi Args Pattern

Show x => Show (Pattern' x)

Pretty a => Pretty (Pattern' a)

IsFlexiblePattern (Pattern' a)

LabelPatVars (Pattern' x) (Pattern' (i, x)) i

UniverseBi ([Type], [Clause]) Pattern

type Pattern

Arguments

 = Pattern' PatVarName

The PatVarName is a name suggestion.

type DeBruijnPattern = Pattern' (Int, PatVarName)

Type used when numbering pattern variables.

namedVarP :: PatVarName -> Named (Ranged PatVarName) Pattern

data ConPatternInfo

The ConPatternInfo states whether the constructor belongs to a record type (Just) or data type (Nothing). In the former case, the Bool says whether the record pattern orginates from the expansion of an implicit pattern. The Type is the type of the whole record pattern. The scope used for the type is given by any outer scope plus the clause's telescope (clauseTel).

Constructors

ConPatternInfo

Fields

conPRecord :: Maybe ConPOrigin

Nothing if data constructor. Just if record constructor.

conPType :: Maybe (Arg Type)

The type of the whole constructor pattern. Should be present (Just) if constructor pattern is is generated ordinarily by type-checking. Could be absent (Nothing) if pattern comes from some plugin (like Agsy). Needed e.g. for with-clause stripping.

Instances

Show ConPatternInfo

KillRange ConPatternInfo

Subst ConPatternInfo

InstantiateFull ConPatternInfo

Normalise ConPatternInfo

noConPatternInfo :: ConPatternInfo

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

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

properlyMatching :: Pattern -> Bool

Does the pattern perform a match that could fail?

Explicit substitutions

data Substitution

Substitutions.

Constructors

IdS

Identity substitution. Γ ⊢ IdS : Γ

EmptyS

Empty substitution, lifts from the empty context. Apply this to closed terms you want to use in a non-empty context. Γ ⊢ EmptyS : ()

Term :# Substitution infixr 4

Substitution extension, `cons'. Γ ⊢ u : Aρ Γ ⊢ ρ : Δ ---------------------- Γ ⊢ u :# ρ : Δ, A

Strengthen Empty Substitution

Strengthening substitution. First argument is IMPOSSIBLE. Apply this to a term which does not contain variable 0 to lower all de Bruijn indices by one. Γ ⊢ ρ : Δ --------------------------- Γ ⊢ Strengthen ρ : Δ, A

Wk !Int Substitution

Weakning substitution, lifts to an extended context. Γ ⊢ ρ : Δ ------------------- Γ, Ψ ⊢ Wk |Ψ| ρ : Δ

Lift !Int Substitution

Lifting substitution. Use this to go under a binder. Lift 1 ρ == var 0 :# Wk 1 ρ. Γ ⊢ ρ : Δ ------------------------- Γ, Ψρ ⊢ Lift |Ψ| ρ : Δ, Ψ

Instances

Show Substitution

Pretty Substitution

KillRange Substitution

TermSize Substitution

Subst Substitution

InstantiateFull Substitution

Absurd Lambda

absurdBody :: Abs Term

Absurd lambdas are internally represented as identity with variable name "()".

isAbsurdBody :: Abs Term -> Bool

absurdPatternName :: PatVarName

isAbsurdPatternName :: PatVarName -> Bool

Pointers and Sharing

ignoreSharing :: Term -> Term

ignoreSharingType :: Type -> Type

shared :: Term -> Term

Introduce sharing.

sharedType :: Type -> Type

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

Typically m would be TCM and f would be Blocked.

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

updateShared :: (Term -> Term) -> Term -> Term

pointerChain :: Term -> [Ptr Term]

compressPointerChain :: Term -> Term

Smart constructors

var :: Nat -> Term

An unapplied variable.

dontCare :: Term -> Term

Add DontCare is it is not already a DontCare.

typeDontCare :: Type

A dummy type.

topSort :: Type

Top sort (Setomega).

sort :: Sort -> Type

varSort :: Int -> Sort

sSuc :: Sort -> Sort

Get the next higher sort.

levelSuc :: Level -> Level

mkType :: Integer -> Sort

impossibleTerm :: String -> Int -> Term

class SgTel a where

Constructing a singleton telescope.

Methods

sgTel :: a -> Telescope

Instances

SgTel (Dom (ArgName, Type))

SgTel (Dom Type)

SgTel (ArgName, Dom Type)

hackReifyToMeta :: Term

isHackReifyToMeta :: Term -> Bool

Handling blocked terms.

blockingMeta :: Blocked t -> Maybe MetaId

blocked :: MetaId -> a -> Blocked a

notBlocked :: a -> Blocked a

Simple operations on terms and types.

stripDontCare :: Term -> Term

Removing a topmost DontCare constructor.

arity :: Type -> Nat

Doesn't do any reduction.

notInScopeName :: ArgName -> ArgName

Make a name that is not in scope.

class Suggest a b where

Pick the better name suggestion, i.e., the one that is not just underscore.

Methods

suggest :: a -> b -> String

Instances

Suggest String String

Suggest String (Abs b)

Suggest Name (Abs b)

Suggest (Abs a) (Abs b)

Eliminations.

unSpine :: Term -> Term

Convert top-level postfix projections into prefix projections.

hasElims :: Term -> Maybe (Elims -> Term, Elims)

A view distinguishing the neutrals Var, Def, and MetaV which can be projected.

argFromElim :: Elim -> Arg Term

Drop Apply constructor. (Unsafe!)

isApplyElim :: Elim -> Maybe (Arg Term)

Drop Apply constructor. (Safe)

allApplyElims :: Elims -> Maybe Args

Drop Apply constructors. (Safe)

splitApplyElims :: Elims -> (Args, Elims)

Split at first non-Apply

class IsProjElim e where

Methods

isProjElim :: e -> Maybe QName

Instances

IsProjElim Elim

IsProjElim e => IsProjElim (MaybeReduced e)

dropProjElims :: IsProjElim e => [e] -> [e]

Discard Proj f entries.

argsFromElims :: Elims -> Args

Discards Proj f entries.

Null instances.

Show instances.

Sized instances and TermSize.

class TermSize a where

The size of a term is roughly the number of nodes in its syntax tree. This number need not be precise for logical correctness of Agda, it is only used for reporting (and maybe decisions regarding performance).

Not counting towards the term size are:

• sort and color annotations,
• projections.

Minimal complete definition

tsize

Methods

termSize :: a -> Int

tsize :: a -> Sum Int

Instances

TermSize Substitution

TermSize LevelAtom

TermSize PlusLevel

TermSize Level

TermSize Sort

TermSize Term

(Foldable t, TermSize a) => TermSize (t a)

KillRange instances.

UniverseBi instances.

Simple pretty printing

module Agda.Syntax.Abstract.Name

module Agda.Utils.Pointer

newtype MetaId

A meta variable identifier is just a natural number.

Constructors

MetaId

Fields

metaId :: Nat

Instances

Enum MetaId

Eq MetaId

Integral MetaId

Num MetaId

Ord MetaId

Real MetaId

Show MetaId

Show non-record version of this newtype.

Pretty MetaId

GetDefs MetaId

HasFresh MetaId

UnFreezeMeta MetaId

IsInstantiatedMeta MetaId

PrettyTCM MetaId

Reify MetaId Expr