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

Safe HaskellNone
LanguageHaskell98

Agda.Syntax.Internal

Contents

Synopsis

Documentation

type Args = [Arg Term] Source

Type of argument lists.

type NamedArgs = [NamedArg Term] Source

data ConHead Source

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

class LensConName a where Source

Minimal complete definition

getConName

Methods

getConName :: a -> QName Source

setConName :: QName -> a -> a Source

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

Instances

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

x es neutral

Lam ArgInfo (Abs Term)

Terms are beta normal. Relevance is ignored

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 Source 
Pretty Substitution Source 
Pretty Type Source 
Pretty Elim Source 
Pretty Term Source 
Null ClauseBody Source 
KillRange Substitution Source 
KillRange Term Source 
TermSize Term Source 
IsProjElim Elim Source 
GetDefs ClauseBody Source 
GetDefs Type Source 
GetDefs Term Source 
TermLike Type Source 
TermLike Term Source 
Free ClauseBody Source 
Free Type Source 
Free Term Source 
GetBody ClauseBody Source 
TeleNoAbs Telescope Source 
TeleNoAbs ListTel Source 
DeBruijn Term Source 
Abstract ClauseBody Source 
Abstract Telescope Source 
Abstract Type Source 
Abstract Term Source 
Apply ClauseBody Source 
Apply Term Source 
KillVar Telescope Source 
KillVar Type Source 
KillVar Term Source 
GenC Telescope Source 
GenC Type Source 
GenC Term Source 
HasOptions NLM Source 
NamesIn Term Source 
AddContext Telescope Source 
IsSizeType Term Source 
UnFreezeMeta Type Source 
UnFreezeMeta Term Source 
IsInstantiatedMeta Term Source 
PrettyTCM ClauseBody Source 
PrettyTCM Telescope Source 
PrettyTCM Type Source 
PrettyTCM Elim Source 
PrettyTCM Term Source 
MentionsMeta Type Source 
MentionsMeta Elim Source 
MentionsMeta Term Source 
InstantiateFull Substitution Source 
InstantiateFull ClauseBody Source 
InstantiateFull Term Source 
Normalise ClauseBody Source 
Normalise Type Source 
Normalise Elim Source 
Normalise Term Source 
Simplify ClauseBody Source 
Simplify Type Source 
Simplify Elim Source 
Simplify Term Source 
Reduce Telescope Source 
Reduce Type Source 
Reduce Elim Source 
Reduce Term Source 
Instantiate Telescope Source 
Instantiate Type Source 
Instantiate Elim Source 
Instantiate Term Source 
Match Term Source 
SynEq Type Source

Syntactic equality ignores sorts.

SynEq Term Source

Syntactic term equality ignores DontCare stuff.

DropArgs ClauseBody Source

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

DropArgs Telescope Source

NOTE: This creates telescopes with unbound de Bruijn indices.

Injectible Term Source 
Evaluate Term Source 
ComputeOccurrences Type Source 
ComputeOccurrences Term Source 
FoldRigid Type Source 
FoldRigid Term Source 
Occurs Type Source 
Occurs Term Source 
NoProjectedVar Term Source 
HasPolarity Type Source 
HasPolarity Term Source 
ToTerm Type Source 
ToTerm Term Source 
PrimTerm Type Source 
AbsTerm Type Source 
AbsTerm Term Source 
IsPrefixOf Elims Source 
IsPrefixOf Term Source 
IsPrefixOf Args Source 
ForcedVariables Term Source

Assumes that the term is in normal form.

UniverseBi Elims Pattern Source 
UniverseBi Elims Term Source 
UniverseBi Args Pattern Source 
UniverseBi Args Term Source 
Free' ClauseBody c Source 
Free' Type c Source 
Free' Term c Source 
Subst Term String Source 
Subst Term () Source 
Subst Term Name Source 
Subst Term EqualityView Source 
Subst Term ConPatternInfo Source 
Subst Term Pattern Source 
Subst Term ClauseBody Source 
Subst Term LevelAtom Source 
Subst Term PlusLevel Source 
Subst Term Level Source 
Subst Term Sort Source 
Subst Term Term Source 
Subst Term Candidate Source 
Subst Term RewriteRule Source 
Subst Term NLPat Source 
Subst Term DisplayTerm Source 
Subst Term DisplayForm Source 
Subst Term Constraint Source 
Subst Term AsBinding Source 
Subst Term DotPatternInst Source 
Subst Term ProblemRest Source 
Subst Term SizeConstraint Source 
Subst Term SizeMeta Source 
ShrinkC Telescope Telescope Source 
ShrinkC Type Type Source 
ShrinkC Term Term Source 
Reify ClauseBody RHS Source 
Reify Telescope Telescope Source 
Reify Type Expr Source 
Reify Elim Expr Source 
Reify Term Expr Source 
Match NLPat Term Source 
PatternFrom Term NLPat Source 
Subst Term a => Subst Term (Type' a) Source 
Subst Term (Problem' p) Source 
Subst Term (SizeExpr' NamedRigid SizeMeta) Source

Only for raise.

SgTel (Dom (ArgName, Type)) Source 
SgTel (Dom Type) Source 
AddContext (Dom (String, Type)) Source 
AddContext (Dom (Name, Type)) Source 
AddContext (Dom Type) Source 
UniverseBi [Term] Term Source 
SgTel (ArgName, Dom Type) Source 
AddContext ([WithHiding Name], Dom Type) Source 
AddContext ([Name], Dom Type) Source 
AddContext (String, Dom Type) Source 
AddContext (Name, Dom Type) Source 
UniverseBi ([Type], [Clause]) Pattern Source 
UniverseBi ([Type], [Clause]) Term Source 

data Elim' a Source

Eliminations, subsuming applications and projections.

Constructors

Apply (Arg a) 
Proj QName

name of a record projection

Instances

Functor Elim' Source 
Foldable Elim' Source 
Traversable Elim' Source 
Pretty Elim Source 
IsProjElim Elim Source 
PrettyTCM Elim Source 
MentionsMeta Elim Source 
Normalise Elim Source 
Simplify Elim Source 
Reduce Elim Source 
Instantiate Elim Source 
IsPrefixOf Elims Source 
UniverseBi Elims Pattern Source 
UniverseBi Elims Term Source 
Reify Elim Expr Source 
Subst t a => Subst t (Elim' a) Source 
Show a => Show (Elim' a) Source 
KillRange a => KillRange (Elim' a) Source 
GetDefs a => GetDefs (Elim' a) Source 
TermLike a => TermLike (Elim' a) Source 
Free a => Free (Elim' a) Source 
KillVar a => KillVar (Elim' a) Source 
GenC a => GenC (Elim' a) Source 
NamesIn a => NamesIn (Elim' a) Source 
PrettyTCM (Elim' NLPat) Source 
PrettyTCM (Elim' DisplayTerm) Source 
InstantiateFull a => InstantiateFull (Elim' a) Source 
Match a => Match (Elim' a) Source 
SynEq a => SynEq (Elim' a) Source 
Injectible a => Injectible (Elim' a) Source 
Evaluate a => Evaluate (Elim' a) Source 
RaiseNLP a => RaiseNLP (Elim' a) Source 
ComputeOccurrences a => ComputeOccurrences (Elim' a) Source 
FoldRigid a => FoldRigid (Elim' a) Source 
Occurs a => Occurs (Elim' a) Source 
HasPolarity a => HasPolarity (Elim' a) Source 
AbsTerm a => AbsTerm (Elim' a) Source 
Free' a c => Free' (Elim' a) c Source 
ShrinkC a b => ShrinkC (Elim' a) (Elim' b) Source 
Match a b => Match (Elim' a) (Elim' b) Source 
PatternFrom a b => PatternFrom (Elim' a) (Elim' b) Source 

type Elim = Elim' Term Source

type Elims Source

Arguments

 = [Elim]

eliminations ordered left-to-right.

type ArgName = String Source

Names in binders and arguments.

argNameToString :: ArgName -> String Source

stringToArgName :: String -> ArgName Source

appendArgNames :: ArgName -> ArgName -> ArgName Source

nameToArgName :: Name -> ArgName Source

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.

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 Source 
Foldable Abs Source 
Traversable Abs Source 
Decoration Abs Source 
Suggest String (Abs b) Source 
Suggest Name (Abs b) Source 
Subst t a => Subst t (Abs a) Source 
Show a => Show (Abs a) Source 
Sized a => Sized (Abs a) Source 
KillRange a => KillRange (Abs a) Source 
LensSort a => LensSort (Abs a) Source 
GetDefs a => GetDefs (Abs a) Source 
TermLike a => TermLike (Abs a) Source 
Free a => Free (Abs a) Source 
KillVar a => KillVar (Abs a) Source 
GenC a => GenC (Abs a) Source 
NamesIn a => NamesIn (Abs a) Source 
UnFreezeMeta a => UnFreezeMeta (Abs a) Source 
IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source

Does not worry about raising.

MentionsMeta t => MentionsMeta (Abs t) Source 
(Subst t a, InstantiateFull a) => InstantiateFull (Abs a) Source 
(Subst t a, Normalise a) => Normalise (Abs a) Source 
(Subst t a, Simplify a) => Simplify (Abs a) Source 
(Subst t a, Reduce a) => Reduce (Abs a) Source 
Instantiate t => Instantiate (Abs t) Source 
(Subst t a, SynEq a) => SynEq (Abs a) Source 
Evaluate a => Evaluate (Abs a) Source 
RaiseNLP a => RaiseNLP (Abs a) Source 
ComputeOccurrences a => ComputeOccurrences (Abs a) Source 
(Subst t a, FoldRigid a) => FoldRigid (Abs a) Source 
(Occurs a, Subst t a) => Occurs (Abs a) Source 
HasPolarity a => HasPolarity (Abs a) Source 
(Subst Term a, AbsTerm a) => AbsTerm (Abs a) Source 
Free' a c => Free' (Abs a) c Source 
Suggest (Abs a) (Abs b) Source 
ShrinkC a b => ShrinkC (Abs a) (Abs b) Source 
(Match a b, Subst t1 a, Subst t2 b) => Match (Abs a) (Abs b) Source 
PatternFrom a b => PatternFrom (Abs a) (Abs b) Source 
(Free i, Reify i a) => Reify (Abs i) (Name, a) Source 

data Type' a Source

Types are terms with a sort annotation.

Constructors

El 

Fields

_getSort :: Sort
 
unEl :: a
 

Instances

Functor Type' Source 
Foldable Type' Source 
Traversable Type' Source 
Pretty Type Source 
Decoration Type' Source 
GetDefs Type Source 
TermLike Type Source 
Free Type Source 
TeleNoAbs Telescope Source 
TeleNoAbs ListTel Source 
Abstract Telescope Source 
Abstract Type Source 
KillVar Telescope Source 
KillVar Type Source 
GenC Telescope Source 
GenC Type Source 
AddContext Telescope Source 
UnFreezeMeta Type Source 
PrettyTCM Telescope Source 
PrettyTCM Type Source 
MentionsMeta Type Source 
Normalise Type Source 
Simplify Type Source 
Reduce Telescope Source 
Reduce Type Source 
Instantiate Telescope Source 
Instantiate Type Source 
SynEq Type Source

Syntactic equality ignores sorts.

DropArgs Telescope Source

NOTE: This creates telescopes with unbound de Bruijn indices.

ComputeOccurrences Type Source 
FoldRigid Type Source 
Occurs Type Source 
HasPolarity Type Source 
ToTerm Type Source 
PrimTerm Type Source 
AbsTerm Type Source 
Free' Type c Source 
ShrinkC Telescope Telescope Source 
ShrinkC Type Type Source 
Reify Telescope Telescope Source 
Reify Type Expr Source 
Subst Term a => Subst Term (Type' a) Source 
Show a => Show (Type' a) Source 
KillRange a => KillRange (Type' a) Source 
SgTel (Dom (ArgName, Type)) Source 
SgTel (Dom Type) Source 
LensSort (Type' a) Source 
NamesIn a => NamesIn (Type' a) Source 
AddContext (Dom (String, Type)) Source 
AddContext (Dom (Name, Type)) Source 
AddContext (Dom Type) Source 
IsSizeType a => IsSizeType (Type' a) Source 
PrettyTCM (Type' NLPat) Source 
InstantiateFull a => InstantiateFull (Type' a) Source 
RaiseNLP a => RaiseNLP (Type' a) Source 
Match a b => Match (Type' a) (Type' b) Source 
PatternFrom a b => PatternFrom (Type' a) (Type' b) Source 
SgTel (ArgName, Dom Type) Source 
AddContext ([WithHiding Name], Dom Type) Source 
AddContext ([Name], Dom Type) Source 
AddContext (String, Dom Type) Source 
AddContext (Name, Dom Type) Source 
UniverseBi ([Type], [Clause]) Pattern Source 
UniverseBi ([Type], [Clause]) Term Source 

type Type = Type' Term Source

class LensSort a where Source

Minimal complete definition

lensSort

Methods

lensSort :: Lens' Sort a Source

getSort :: a -> Sort Source

Instances

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.

Instances

type Telescope = Tele (Dom Type) Source

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

A traversal for the names in a telescope.

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

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

data Sort Source

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

newtype Level Source

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

data PlusLevel Source

Constructors

ClosedLevel Integer

n, to represent Setₙ.

Plus Integer LevelAtom

n + ℓ.

Instances

data LevelAtom Source

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

Blocked Terms

data NotBlocked Source

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 Source 
Monoid NotBlocked Source

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

data Blocked t Source

Something where a meta variable may block reduction.

Constructors

Blocked 

Fields

theBlockingMeta :: MetaId
 
ignoreBlocking :: t
 
NotBlocked 

Fields

blockingStatus :: NotBlocked
 
ignoreBlocking :: t
 

Instances

type Blocked_ = Blocked () Source

Blocked t without the t.

stuckOn :: Elim -> NotBlocked -> NotBlocked Source

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 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 de Bruijn indices say 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.

namedClausePats :: [NamedArg DeBruijnPattern]
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.

clauseCatchall :: Bool
 

Instances

clausePats :: Clause -> [Arg DeBruijnPattern] Source

data ClauseBodyF a Source

Constructors

Body a 
Bind (Abs (ClauseBodyF a)) 
NoBody

for absurd clauses.

Instances

type ClauseBody = ClauseBodyF Term Source

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

type PatVarName = ArgName Source

Pattern variables.

patVarNameToString :: PatVarName -> String Source

nameToPatVarName :: Name -> PatVarName Source

data Pattern' x 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 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' Source 
Foldable Pattern' Source 
Traversable Pattern' Source 
PrettyTCM DeBruijnPattern Source 
PrettyTCM Pattern Source 
UniverseBi Elims Pattern Source 
UniverseBi Args Pattern Source 
Subst Term Pattern Source 
Show x => Show (Pattern' x) Source 
Pretty a => Pretty (Pattern' a) Source 
KillRange a => KillRange (Pattern' a) Source 
IsProjP (Pattern' a) Source 
NamesIn (Pattern' a) Source 
InstantiateFull a => InstantiateFull (Pattern' a) Source 
Normalise a => Normalise (Pattern' a) Source 
IsFlexiblePattern (Pattern' a) Source 
LabelPatVars (Pattern' x) (Pattern' (i, x)) i Source 
UniverseBi ([Type], [Clause]) Pattern Source 

type Pattern Source

Arguments

 = Pattern' PatVarName

The PatVarName is a name suggestion.

type DeBruijnPattern = Pattern' (Int, PatVarName) Source

Type used when numbering pattern variables.

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

namedDBVarP :: Int -> PatVarName -> Named (Ranged PatVarName) DeBruijnPattern Source

data ConPatternInfo Source

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

noConPatternInfo :: ConPatternInfo Source

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

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

properlyMatching :: Pattern' a -> Bool Source

Does the pattern perform a match that could fail?

Explicit substitutions

data Substitution' a Source

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

a :# (Substitution' a) infixr 4

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

Strengthen Empty (Substitution' a)

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' a)

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

Lift !Int (Substitution' a)

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

Instances

Functor Substitution' Source 
Foldable Substitution' Source 
Traversable Substitution' Source 
Pretty Substitution Source 
KillRange Substitution Source 
InstantiateFull Substitution Source 
Subst a a => Subst a (Substitution' a) Source 
Show a => Show (Substitution' a) Source 
TermSize a => TermSize (Substitution' a) Source 
(Show a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) Source 

type Substitution = Substitution' Term Source

type PatternSubstitution = Substitution' DeBruijnPattern Source

Views

data EqualityView Source

View type as equality type.

Constructors

EqualityType 

Fields

eqtSort :: Sort

Sort of this type.

eqtName :: QName

Builtin EQUALITY.

eqtLevel :: Arg Term

Hidden

eqtType :: Arg Term

Hidden

eqtLhs :: Arg Term

NotHidden

eqtRhs :: Arg Term

NotHidden

OtherType Type

reduced

Instances

isEqualityType :: EqualityView -> Bool Source

Absurd Lambda

absurdBody :: Abs Term Source

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

isAbsurdBody :: Abs Term -> Bool Source

absurdPatternName :: PatVarName Source

isAbsurdPatternName :: PatVarName -> Bool Source

Pointers and Sharing

ignoreSharing :: Term -> Term Source

Remove top-level Shared data constructors.

ignoreSharingType :: Type -> Type Source

shared_ :: Term -> Term Source

Introduce sharing.

updateSharedFM :: (Monad 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 Term Source

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

pointerChain :: Term -> [Ptr Term] Source

compressPointerChain :: Term -> Term Source

Smart constructors

var :: Nat -> Term Source

An unapplied variable.

dontCare :: Term -> Term Source

Add DontCare is it is not already a DontCare.

typeDontCare :: Type Source

A dummy type.

topSort :: Type Source

Top sort (Setomega).

sort :: Sort -> Type Source

varSort :: Int -> Sort Source

sSuc :: Sort -> Sort Source

Get the next higher sort.

levelSuc :: Level -> Level Source

mkType :: Integer -> Sort Source

impossibleTerm :: String -> Int -> Term Source

class SgTel a where Source

Constructing a singleton telescope.

Methods

sgTel :: a -> Telescope Source

Instances

hackReifyToMeta :: Term Source

isHackReifyToMeta :: Term -> Bool Source

Handling blocked terms.

blockingMeta :: Blocked t -> Maybe MetaId Source

blocked :: MetaId -> a -> Blocked a Source

notBlocked :: a -> Blocked a Source

Simple operations on terms and types.

stripDontCare :: Term -> Term Source

Removing a topmost DontCare constructor.

arity :: Type -> Nat Source

Doesn't do any reduction.

notInScopeName :: ArgName -> ArgName Source

Make a name that is not in scope.

class Suggest a b where Source

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

Methods

suggest :: a -> b -> String Source

Instances

Eliminations.

unSpine :: Term -> Term Source

Convert top-level postfix projections into prefix projections.

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

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

argFromElim :: Elim -> Arg Term Source

Drop Apply constructor. (Unsafe!)

isApplyElim :: Elim -> Maybe (Arg Term) Source

Drop Apply constructor. (Safe)

allApplyElims :: Elims -> Maybe Args Source

Drop Apply constructors. (Safe)

splitApplyElims :: Elims -> (Args, Elims) Source

Split at first non-Apply

class IsProjElim e where Source

Methods

isProjElim :: e -> Maybe QName Source

Instances

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

Discard Proj f entries.

argsFromElims :: Elims -> Args Source

Discards Proj f entries.

allProjElims :: Elims -> Maybe [QName] Source

Drop Proj constructors. (Safe)

Null instances.

Show instances.

Sized instances and TermSize.

class TermSize a where Source

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 Source

tsize :: a -> Sum Int Source

Instances

KillRange instances.

UniverseBi instances.

Simple pretty printing

module Agda.Syntax.Abstract.Name

module Agda.Utils.Pointer

newtype MetaId Source

A meta variable identifier is just a natural number.

Constructors

MetaId 

Fields

metaId :: Nat
 

Instances