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

Safe HaskellNone
LanguageHaskell98

Agda.Syntax.Abstract

Contents

Description

The abstract syntax. This is what you get after desugaring and scope analysis of the concrete syntax. The type checker works on abstract syntax, producing internal syntax (Agda.Syntax.Internal).

Synopsis

Documentation

type Color = Expr Source

type Arg a = Arg Color a Source

type Dom a = Dom Color a Source

type NamedArg a = NamedArg Color a Source

type ArgInfo = ArgInfo Color Source

type Args = [NamedArg Expr] Source

data Expr Source

Expressions after scope checking (operators parsed, names resolved).

Constructors

Var Name

Bound variable.

Def QName

Constant: axiom, function, data or record type.

Proj QName

Projection.

Con AmbiguousQName

Constructor.

PatternSyn QName

Pattern synonym.

Lit Literal

Literal.

QuestionMark MetaInfo InteractionId

Meta variable for interaction. The InteractionId is usually identical with the metaNumber of MetaInfo. However, if you want to print an interaction meta as just ? instead of ?n, you should set the metaNumber to Nothing while keeping the InteractionId.

Underscore MetaInfo

Meta variable for hidden argument (must be inferred locally).

App ExprInfo Expr (NamedArg Expr)

Ordinary (binary) application.

WithApp ExprInfo Expr [Expr]

With application.

Lam ExprInfo LamBinding Expr

λ bs → e.

AbsurdLam ExprInfo Hiding

λ() or λ{}.

ExtendedLam ExprInfo DefInfo QName [Clause] 
Pi ExprInfo Telescope Expr

Dependent function space Γ → A.

Fun ExprInfo (Arg Expr) Expr

Non-dependent function space.

Set ExprInfo Integer

Set, Set1, Set2, ...

Prop ExprInfo

Prop (no longer supported, used as dummy type).

Let ExprInfo [LetBinding] Expr

let bs in e.

ETel Telescope

Only used when printing telescopes.

Rec ExprInfo Assigns

Record construction.

RecUpdate ExprInfo Expr Assigns

Record update.

ScopedExpr ScopeInfo Expr

Scope annotation.

QuoteGoal ExprInfo Name Expr

Binds Name to current type in Expr.

QuoteContext ExprInfo Name Expr

Binds Name to current context in Expr.

Quote ExprInfo

Quote an identifier QName.

QuoteTerm ExprInfo

Quote a term.

Unquote ExprInfo

The splicing construct: unquote ...

DontCare Expr

For printing DontCare from Syntax.Internal.

Instances

type Assign = (Name, Expr) Source

Record field assignment f = e.

type Assigns = [Assign] Source

data Axiom Source

Is a type signature a postulate or a function signature?

Constructors

FunSig

A function signature.

NoFunSig

Not a function signature, i.e., a postulate (in user input) or another (e.g. data/record) type signature (internally).

Instances

type Ren a = [(a, a)] Source

Renaming (generic).

data Declaration Source

Constructors

Axiom Axiom DefInfo ArgInfo QName Expr

type signature (can be irrelevant and colored, but not hidden)

Field DefInfo QName (Arg Expr)

record field

Primitive DefInfo QName Expr

primitive function

Mutual MutualInfo [Declaration]

a bunch of mutually recursive definitions

Section ModuleInfo ModuleName [TypedBindings] [Declaration] 
Apply ModuleInfo ModuleName ModuleApplication (Ren QName) (Ren ModuleName) 
Import ModuleInfo ModuleName 
Pragma Range Pragma 
Open ModuleInfo ModuleName

only retained for highlighting purposes

FunDef DefInfo QName Delayed [Clause]

sequence of function clauses

DataSig DefInfo QName Telescope Expr

lone data signature ^ the LamBindings are DomainFree and binds the parameters of the datatype.

DataDef DefInfo QName [LamBinding] [Constructor]

the LamBindings are DomainFree and binds the parameters of the datatype.

RecSig DefInfo QName Telescope Expr

lone record signature

RecDef DefInfo QName (Maybe (Ranged Induction)) (Maybe QName) [LamBinding] Expr [Declaration]

The Expr gives the constructor type telescope, (x1 : A1)..(xn : An) -> Prop, and the optional name is the constructor's name.

PatternSynDef QName [Arg Name] Pattern

Only for highlighting purposes

UnquoteDecl MutualInfo DefInfo QName Expr 
ScopedDecl ScopeInfo [Declaration]

scope annotation

Instances

class GetDefInfo a where Source

Methods

getDefInfo :: a -> Maybe DefInfo Source

Instances

data ModuleApplication Source

Constructors

SectionApp Telescope ModuleName [NamedArg Expr]

tel. M args: applies M to args and abstracts tel.

RecordModuleIFS ModuleName
M {{...}}

Instances

data Pragma Source

Constructors

OptionsPragma [String] 
BuiltinPragma String Expr 
BuiltinNoDefPragma String QName

Builtins that do not come with a definition, but declare a name for an Agda concept.

RewritePragma QName 
CompiledPragma QName String 
CompiledExportPragma QName String 
CompiledTypePragma QName String 
CompiledDataPragma QName String [String] 
CompiledEpicPragma QName String 
CompiledJSPragma QName String 
StaticPragma QName 
EtaPragma QName 

Instances

data LetBinding Source

Bindings that are valid in a let.

Constructors

LetBind LetInfo ArgInfo Name Expr Expr
LetBind info rel name type defn
LetPatBind LetInfo Pattern Expr

Irrefutable pattern binding.

LetApply ModuleInfo ModuleName ModuleApplication (Ren QName) (Ren ModuleName)

LetApply mi newM (oldM args) renaming moduleRenaming.

LetOpen ModuleInfo ModuleName

only for highlighting and abstractToConcrete

Instances

type TypeSignature = Declaration Source

Only Axioms.

type Constructor = TypeSignature Source

type Field = TypeSignature Source

data LamBinding Source

A lambda binding is either domain free or typed.

Constructors

DomainFree ArgInfo Name

. x or {x} or .x or .{x}

DomainFull TypedBindings

. (xs:e) or {xs:e} or (let Ds)

Instances

data TypedBindings Source

Typed bindings with hiding information.

Constructors

TypedBindings Range (Arg TypedBinding)

. (xs : e) or {xs : e}

Instances

data TypedBinding Source

A typed binding. Appears in dependent function spaces, typed lambdas, and telescopes. It might be tempting to simplify this to only bind a single name at a time, and translate, say, (x y : A) to (x : A)(y : A) before type-checking. However, this would be slightly problematic:

  1. We would have to typecheck the type A several times.
  2. If A contains a meta variable or hole, it would be duplicated by such a translation.

While 1. is only slightly inefficient, 2. would be an outright bug. Duplicating A could not be done naively, we would have to make sure that the metas of the copy are aliases of the metas of the original.

Constructors

TBind Range [WithHiding Name] Expr

As in telescope (x y z : A) or type (x y z : A) -> B.

TLet Range [LetBinding]

E.g. (let x = e) or (let open M).

Instances

type Telescope = [TypedBindings] Source

data Clause' lhs Source

We could throw away where clauses at this point and translate them to let. It's not obvious how to remember that the let was really a where clause though, so for the time being we keep it here.

Constructors

Clause 

Fields

clauseLHS :: lhs
 
clauseRHS :: RHS
 
clauseWhereDecls :: [Declaration]
 

Instances

Functor Clause' Source 
Foldable Clause' Source 
Traversable Clause' Source 
AllNames Clause Source 
LHSToSpine Clause SpineClause Source

Clause instance.

Reify NamedClause Clause Source 
ToAbstract Clause Clause Source 
Show lhs => Show (Clause' lhs) Source 
KillRange a => KillRange (Clause' a) Source 
HasRange a => HasRange (Clause' a) Source 
ExprLike (Clause' a) Source

TODO: currently does not go into clauses.

ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] Source 

type Clause = Clause' LHS Source

type SpineClause = Clause' SpineLHS Source

data RHS Source

Constructors

RHS Expr 
AbsurdRHS 
WithRHS QName [Expr] [Clause]

The QName is the name of the with function.

RewriteRHS [(QName, Expr)] RHS [Declaration]

The QNames are the names of the generated with functions. One for each Expr. The RHS shouldn't be another RewriteRHS.

Instances

data SpineLHS Source

The lhs of a clause in spine view (inside-out). Projection patterns are contained in spLhsPats, represented as DefP d [].

Constructors

SpineLHS 

Fields

spLhsInfo :: LHSInfo

Range.

spLhsDefName :: QName

Name of function we are defining.

spLhsPats :: [NamedArg Pattern]

Function parameters (patterns).

spLhsWithPats :: [Pattern]

with patterns (after |).

Instances

data LHS Source

The lhs of a clause in focused (projection-application) view (outside-in). Projection patters are represented as LHSProjs.

Constructors

LHS 

Fields

lhsInfo :: LHSInfo

Range.

lhsCore :: LHSCore

Copatterns.

lhsWithPats :: [Pattern]

with patterns (after |).

Instances

data LHSCore' e Source

The lhs minus with-patterns in projection-application view. Parameterised over the type e of dot patterns.

Constructors

LHSHead

The head applied to ordinary patterns.

Fields

lhsDefName :: QName

Head f.

lhsPats :: [NamedArg (Pattern' e)]

Applied to patterns ps.

LHSProj

Projection

Fields

lhsDestructor :: QName

Record projection identifier.

lhsPatsLeft :: [NamedArg (Pattern' e)]

Indices of the projection. Currently none [], since we do not have indexed records.

lhsFocus :: NamedArg (LHSCore' e)

Main branch.

lhsPatsRight :: [NamedArg (Pattern' e)]

Further applied to patterns.

Instances

Functor LHSCore' Source 
Foldable LHSCore' Source 
Traversable LHSCore' Source 
ToConcrete LHSCore Pattern Source 
ToAbstract LHSCore (LHSCore' Expr) Source 
Eq (LHSCore' e) Source 
Show e => Show (LHSCore' e) Source 
KillRange e => KillRange (LHSCore' e) Source 
HasRange (LHSCore' e) Source 
ToAbstract (LHSCore' Expr) (LHSCore' Expr) Source 

type LHSCore = LHSCore' Expr Source

class LHSToSpine a b where Source

Convert a focused lhs to spine view and back.

Methods

lhsToSpine :: a -> b Source

spineToLhs :: b -> a Source

Instances

LHSToSpine LHS SpineLHS Source

LHS instance.

LHSToSpine Clause SpineClause Source

Clause instance.

LHSToSpine a b => LHSToSpine [a] [b] Source

List instance (for clauses).

lhsCoreToSpine :: LHSCore' e -> QNamed [NamedArg (Pattern' e)] Source

spineToLhsCore :: QNamed [NamedArg (Pattern' e)] -> LHSCore' e Source

lhsCoreApp :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e Source

Add applicative patterns (non-projection patterns) to the right.

lhsCoreAddSpine :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e Source

Add projection and applicative patterns to the right.

lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e] Source

Used for checking pattern linearity.

lhsCoreToPattern :: LHSCore -> Pattern Source

Used in AbstractToConcrete.

mapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore Source

Patterns

data Pattern' e Source

Parameterised over the type of dot patterns.

Constructors

VarP Name 
ConP ConPatInfo AmbiguousQName [NamedArg (Pattern' e)] 
DefP PatInfo QName [NamedArg (Pattern' e)]

Defined pattern: function definition f ps or destructor pattern d p ps.

WildP PatInfo

Underscore pattern entered by user. Or generated at type checking for implicit arguments.

AsP PatInfo Name (Pattern' e) 
DotP PatInfo e 
AbsurdP PatInfo 
LitP Literal 
PatternSynP PatInfo QName [NamedArg (Pattern' e)] 

Instances

Functor Pattern' Source 
Foldable Pattern' Source 
Traversable Pattern' Source 
EmbPrj Pattern Source 
ExpandPatternSynonyms Pattern Source 
IsFlexiblePattern Pattern Source 
UniverseBi Declaration Pattern Source 
ToConcrete Pattern Pattern Source 
ToAbstract Pattern (Pattern' Expr) Source 
Eq (Pattern' e) Source

Literal equality of patterns, ignoring dot patterns

Show e => Show (Pattern' e) Source 
KillRange e => KillRange (Pattern' e) Source 
SetRange (Pattern' a) Source 
HasRange (Pattern' e) Source 
IsProjP (Pattern' e) Source 
ExprLike a => ExprLike (Pattern' a) Source 
ToAbstract (Pattern' Expr) (Pattern' Expr) Source 

type Pattern = Pattern' Expr Source

type Patterns = [NamedArg Pattern] Source

class IsProjP a where Source

Check whether we are a projection pattern.

Methods

isProjP :: a -> Maybe QName Source

Instances

class AllNames a where Source

Extracts all the names which are declared in a Declaration. This does not include open public or let expressions, but it does include local modules, where clauses and the names of extended lambdas.

Methods

allNames :: a -> Seq QName Source

Instances

axiomName :: Declaration -> QName Source

The name defined by the given axiom.

Precondition: The declaration has to be a (scoped) Axiom.

class AnyAbstract a where Source

Are we in an abstract block?

In that case some definition is abstract.

Methods

anyAbstract :: a -> Bool Source

Instances

app :: Expr -> [NamedArg Expr] -> Expr Source

patternToExpr :: Pattern -> Expr Source

type PatternSynDefn = ([Arg Name], Pattern) Source

type PatternSynDefns = Map QName PatternSynDefn Source

lambdaLiftExpr :: [Name] -> Expr -> Expr Source

substPattern :: [(Name, Pattern)] -> Pattern -> Pattern Source

class SubstExpr a where Source

Methods

substExpr :: [(Name, Expr)] -> a -> a Source

Instances

insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name]) Source

module Agda.Syntax.Abstract.Name