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

Safe HaskellNone
LanguageHaskell98

Agda.Syntax.Internal

Contents

Synopsis

Documentation

type Color = Term

type Arg a = Arg Color a

type Dom a = Dom Color a

type Args = [Arg Term]

Type of argument lists.

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.

class LensConName a where

Minimal complete definition

getConName

Methods

getConName :: a -> QName

setConName :: QName -> a -> a

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

Instances

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 Type 
KillRange Term 
TermSize Term 
IsProjElim Elim 
Free ClauseBody 
Free Type 
Free Term 
GetDefs ClauseBody 
GetDefs Type 
GetDefs Term 
TermLike Type 
TermLike Term 
GetBody ClauseBody 
TeleNoAbs Telescope 
TeleNoAbs ListTel 
Subst ClauseBody 
Subst Type 
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 
AddContext Telescope 
UnFreezeMeta Type 
UnFreezeMeta Term 
IsInstantiatedMeta Term 
PrettyTCM ClauseBody 
PrettyTCM Telescope 
PrettyTCM Type 
PrettyTCM Elim 
PrettyTCM Term 
EmbPrj ClauseBody 
EmbPrj Telescope 
EmbPrj Type 
EmbPrj Term 
MentionsMeta Type 
MentionsMeta Elim 
MentionsMeta Term 
InstantiateFull ClauseBody 
InstantiateFull Type 
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 
FoldRigid Type 
FoldRigid Term 
Occurs Type 
Occurs Term 
NoProjectedVar Term 
HasPolarity Type 
HasPolarity Term 
ComputeOccurrences Type 
ComputeOccurrences 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 
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 
AmbMatch 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)) 
Free a => Free (Dom a) 
Free a => Free (Arg a) 
TermLike a => TermLike (Dom a) 
TermLike a => TermLike (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)) 
(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) 
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) 
ComputeOccurrences a => ComputeOccurrences (Dom a) 
ComputeOccurrences a => ComputeOccurrences (Arg a) 
UReduce a => UReduce (Arg a) 
Unquote a => Unquote (Arg a) 
UniverseBi [Term] Term 
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.

AmbMatch a b => AmbMatch (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 ([Name], Dom Type) 
AddContext ([WithHiding Name], Dom Type) 
AddContext (String, Dom Type) 
AddContext (Name, Dom Type) 
UniverseBi ([Type], [Clause]) Pattern 
UniverseBi ([Type], [Clause]) Term 
Singleton (Int, Term) AmbSubst 

type Elim = Elim' Term

type Elims

Arguments

 = [Elim]

eliminations ordered left-to-right.

type ArgName = String

Names in binders and arguments.

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) 
Free a => Free (Abs a) 
GetDefs a => GetDefs (Abs a) 
TermLike a => TermLike (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.

EmbPrj a => EmbPrj (Abs a) 
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) 
(Subst a, FoldRigid a) => FoldRigid (Abs a) 
(Occurs a, Subst a) => Occurs (Abs a) 
HasPolarity a => HasPolarity (Abs a) 
ComputeOccurrences a => ComputeOccurrences (Abs a) 
Unquote a => Unquote (Abs a) 
Suggest (Abs a) (Abs b) 
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) 

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.

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

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.

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] 

newtype MetaId

A meta variable identifier is just a natural number.

Constructors

MetaId 

Fields

metaId :: Nat
 

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 block 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.

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 
Free Clause 
GetDefs 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 
EmbPrj Clause 
EmbPrj FunctionInverse 
InstantiateFull Clause 
InstantiateFull FunctionInverse 
DropArgs Clause

NOTE: does not work for recursive functions.

DropArgs FunctionInverse 
Occurs Clause 
ComputeOccurrences Clause 
Unquote Clause 
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 

type PatVarName = ArgName

Pattern variables.

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.

type Pattern

Arguments

 = Pattern' PatVarName

The PatVarName is a name suggestion.

type DeBruijnPattern = Pattern' (Int, PatVarName)

Type used when numbering pattern variables.

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 Bool

Nothing if data constructor. Just if record constructor, then True if pattern was expanded from an implicit pattern.

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.

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 |Ψ| ρ : Δ, Ψ

Absurd Lambda

absurdBody :: Abs Term

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

Pointers and Sharing

shared :: Term -> Term

Introduce sharing.

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

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

sSuc :: Sort -> Sort

Get the next higher sort.

class SgTel a where

Constructing a singleton telescope.

Methods

sgTel :: a -> Telescope

Instances

Handling blocked terms.

blocked :: MetaId -> 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.

argName :: Type -> String

Suggest a name for the first argument of a function of the given type.

class Suggest a b where

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

Methods

suggest :: a -> b -> String

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

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

KillRange instances.

UniverseBi instances.

Simple pretty printing