Agda.Syntax.Abstract

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

Documentation

data Expr

Constructors

Var Name

Bound variables

Def QName

Constants (i.e. axioms, functions, projections, and datatypes)

Con AmbiguousQName

Constructors

Lit Literal

Literals

QuestionMark MetaInfo

meta variable for interaction

Underscore MetaInfo

meta variable for hidden argument (must be inferred locally)

App ExprInfo Expr (NamedArg Expr)

WithApp ExprInfo Expr [Expr]

with application

Lam ExprInfo LamBinding Expr

AbsurdLam ExprInfo Hiding

ExtendedLam ExprInfo DefInfo QName [Clause]

Pi ExprInfo Telescope Expr

Fun ExprInfo (Arg Expr) Expr

independent function space

Set ExprInfo Integer

Set, Set1, Set2, ...

Prop ExprInfo

Let ExprInfo [LetBinding] Expr

ETel Telescope

only used when printing telescopes

Rec ExprInfo [(Name, Expr)]

record construction

RecUpdate ExprInfo Expr [(Name, Expr)]

record update

ScopedExpr ScopeInfo Expr

scope annotation

QuoteGoal ExprInfo Name Expr

binds Name to current type in Expr

Quote ExprInfo

QuoteTerm ExprInfo

Unquote ExprInfo

The splicing construct: unquote ...

DontCare Expr

for printing DontCare from Syntax.Internal

PatternSyn QName

Instances

Show Expr

Typeable Expr

KillRange Expr

HasRange Expr

PrettyTCM Expr

EmbPrj Pattern

EmbPrj Expr

UniverseBi Declaration Pattern

UniverseBi Declaration Expr

ToConcrete Pattern Pattern

ToConcrete LHSCore Pattern

ToConcrete Expr Expr

ToAbstract Expr Expr

ToAbstract OldQName Expr

Reify Literal Expr

Reify MetaId Expr

Reify Level Expr

Reify Sort Expr

Reify Type Expr

Reify Elim Expr

Reify Term Expr

Reify Expr Expr

Reify DisplayTerm Expr

Reify i Expr => ReifyWhen i Expr

Reify ProblemConstraint (Closure (OutputForm Expr Expr))

Reify Constraint (OutputConstraint Expr Expr)

ToAbstract (Pattern' Expr) (Pattern' Expr)

ToAbstract (LHSCore' Expr) (LHSCore' Expr)

data Declaration

Constructors

Axiom DefInfo Relevance QName Expr

postulate

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 (Map QName QName) (Map ModuleName 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 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.

ScopedDecl ScopeInfo [Declaration]

scope annotation

Instances

Show Declaration

Typeable Declaration

KillRange Declaration

HasRange Declaration

GetDefInfo Declaration

AnyAbstract Declaration

UniverseBi Declaration AmbiguousQName

UniverseBi Declaration ModuleName

UniverseBi Declaration QName

UniverseBi Declaration ModuleInfo

UniverseBi Declaration Pattern

UniverseBi Declaration TypedBinding

UniverseBi Declaration LamBinding

UniverseBi Declaration LetBinding

UniverseBi Declaration Declaration

UniverseBi Declaration Expr

ToAbstract NiceDeclaration Declaration

ToConcrete Declaration [Declaration]

ToConcrete (Constr Constructor) Declaration

ToAbstract [Declaration] [Declaration]

class GetDefInfo a where

Methods

getDefInfo :: a -> Maybe DefInfo

Instances

GetDefInfo Declaration

data ModuleApplication

Constructors

SectionApp [TypedBindings] ModuleName [NamedArg Expr]

RecordModuleIFS ModuleName

Instances

Show ModuleApplication

Typeable ModuleApplication

KillRange ModuleApplication

ToConcrete ModuleApplication ModuleApplication

data Pragma

Constructors

OptionsPragma [String]

BuiltinPragma String Expr

CompiledPragma QName String

CompiledTypePragma QName String

CompiledDataPragma QName String [String]

CompiledEpicPragma QName String

CompiledJSPragma QName String

StaticPragma QName

EtaPragma QName

Instances

Show Pragma

Typeable Pragma

ToAbstract Pragma [Pragma]

data LetBinding

Constructors

LetBind LetInfo Relevance Name Expr Expr

LetBind info rel name type defn

LetPatBind LetInfo Pattern Expr

irrefutable pattern binding

LetApply ModuleInfo ModuleName ModuleApplication (Map QName QName) (Map ModuleName ModuleName)

LetOpen ModuleInfo ModuleName

only for highlighting and abstractToConcrete

Instances

Show LetBinding

Typeable LetBinding

KillRange LetBinding

HasRange LetBinding

EmbPrj LetBinding

UniverseBi Declaration LetBinding

ToConcrete LetBinding [Declaration]

ToAbstract LetDef [LetBinding]

ToAbstract LetDefs [LetBinding]

type TypeSignature = Declaration

Only Axioms.

type Constructor = TypeSignature

type Field = TypeSignature

data LamBinding

A lambda binding is either domain free or typed.

Constructors

DomainFree Hiding Relevance Name

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

DomainFull TypedBindings

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

Instances

Show LamBinding

Typeable LamBinding

KillRange LamBinding

HasRange LamBinding

EmbPrj LamBinding

UniverseBi Declaration LamBinding

ToConcrete LamBinding LamBinding

ToAbstract LamBinding LamBinding

data TypedBindings

Typed bindings with hiding information.

Constructors

TypedBindings Range (Arg TypedBinding)

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

Instances

Show TypedBindings

Typeable TypedBindings

KillRange TypedBindings

HasRange TypedBindings

EmbPrj TypedBindings

ToConcrete TypedBindings TypedBindings

ToAbstract TypedBindings TypedBindings

Reify Telescope Telescope

data TypedBinding

A typed binding. Appears in dependent function spaces, typed lambdas, and telescopes. I might be tempting to simplify this to only bind a single name at a time. This would mean that we would have to typecheck the type several times (x,y:A vs. x:A; y:A). In most cases this wouldn't really be a problem, but it's good principle to not do extra work unless you have to.

Constructors

TBind Range [Name] Expr

TNoBind Expr

Instances

Show TypedBinding

Typeable TypedBinding

KillRange TypedBinding

HasRange TypedBinding

EmbPrj TypedBinding

UniverseBi Declaration TypedBinding

ToConcrete TypedBinding TypedBinding

ToAbstract TypedBinding TypedBinding

type Telescope = [TypedBindings]

data Clause

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

Show Clause

Typeable Clause

KillRange Clause

HasRange Clause

ToAbstract Clause Clause

Reify NamedClause Clause

ToConcrete Clause [Declaration]

data RHS

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

Show RHS

Typeable RHS

KillRange RHS

HasRange RHS

ToAbstract AbstractRHS RHS

Reify ClauseBody RHS

ToConcrete RHS (RHS, [Expr], [Expr], [Declaration])

data SpineLHS

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

Show SpineLHS

Typeable SpineLHS

data LHS

The lhs of a clause in 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

Eq LHS

Show LHS

Typeable LHS

KillRange LHS

HasRange LHS

ToConcrete LHS LHS

ToAbstract LeftHandSide LHS

data LHSCore' e

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'

Typeable1 LHSCore'

Foldable LHSCore'

Traversable LHSCore'

ToConcrete LHSCore Pattern

ToAbstract LHSCore (LHSCore' Expr)

Eq (LHSCore' e)

Show e => Show (LHSCore' e)

KillRange e => KillRange (LHSCore' e)

HasRange (LHSCore' e)

ToAbstract (LHSCore' Expr) (LHSCore' Expr)

type LHSCore = LHSCore' Expr

lhsToSpine :: LHS -> SpineLHS

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

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

Used for checking pattern linearity.

lhsCoreToPattern :: LHSCore -> Pattern

Used in AbstractToConcrete.

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

data Pattern' e

Parameterised over the type of dot patterns.

Constructors

VarP Name

ConP PatInfo AmbiguousQName [NamedArg (Pattern' e)]

DefP PatInfo QName [NamedArg (Pattern' e)]

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

WildP PatInfo

AsP PatInfo Name (Pattern' e)

DotP PatInfo e

AbsurdP PatInfo

LitP Literal

ImplicitP PatInfo

Generated at type checking for implicit arguments.

PatternSynP PatInfo QName [NamedArg (Pattern' e)]

Instances

Functor Pattern'

Typeable1 Pattern'

Foldable Pattern'

Traversable Pattern'

EmbPrj Pattern

UniverseBi Declaration Pattern

ToConcrete Pattern Pattern

ToAbstract Pattern (Pattern' Expr)

Eq (Pattern' e)

Literal equality of patterns, ignoring dot patterns

Show e => Show (Pattern' e)

KillRange e => KillRange (Pattern' e)

SetRange (Pattern' a)

HasRange (Pattern' e)

ToAbstract (Pattern' Expr) (Pattern' Expr)

type Pattern = Pattern' Expr

type Patterns = [NamedArg Pattern]

allNames :: Declaration -> Seq QName

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.

axiomName :: Declaration -> QName

The name defined by the given axiom.

Precondition: The declaration has to be an Axiom.

class AnyAbstract a where

Are we in an abstract block?

In that case some definition is abstract.

Methods

anyAbstract :: a -> Bool

Instances

AnyAbstract Declaration

AnyAbstract a => AnyAbstract [a]

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

patternToExpr :: Pattern -> Expr

type PatternSynDefn = ([Name], Pattern)

type PatternSynDefns = Map QName PatternSynDefn

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

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

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

substLetBinding :: [(Name, Expr)] -> LetBinding -> LetBinding

substTypedBindings :: [(Name, Expr)] -> TypedBindings -> TypedBindings

substTypedBinding :: [(Name, Expr)] -> TypedBinding -> TypedBinding

module Agda.Syntax.Abstract.Name