Safe Haskell | None |
---|---|
Language | Haskell98 |
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).
- type Color = Expr
- type Arg a = Arg Color a
- type Dom a = Dom Color a
- type NamedArg a = NamedArg Color a
- type ArgInfo = ArgInfo Color
- type Args = [NamedArg Expr]
- data Expr
- = Var Name
- | Def QName
- | Proj QName
- | Con AmbiguousQName
- | PatternSyn QName
- | Lit Literal
- | QuestionMark MetaInfo InteractionId
- | Underscore MetaInfo
- | App ExprInfo Expr (NamedArg Expr)
- | WithApp ExprInfo Expr [Expr]
- | Lam ExprInfo LamBinding Expr
- | AbsurdLam ExprInfo Hiding
- | ExtendedLam ExprInfo DefInfo QName [Clause]
- | Pi ExprInfo Telescope Expr
- | Fun ExprInfo (Arg Expr) Expr
- | Set ExprInfo Integer
- | Prop ExprInfo
- | Let ExprInfo [LetBinding] Expr
- | ETel Telescope
- | Rec ExprInfo Assigns
- | RecUpdate ExprInfo Expr Assigns
- | ScopedExpr ScopeInfo Expr
- | QuoteGoal ExprInfo Name Expr
- | QuoteContext ExprInfo Name Expr
- | Quote ExprInfo
- | QuoteTerm ExprInfo
- | Unquote ExprInfo
- | DontCare Expr
- type Assign = (Name, Expr)
- type Assigns = [Assign]
- data Axiom
- type Ren a = [(a, a)]
- data Declaration
- = Axiom Axiom DefInfo ArgInfo QName Expr
- | Field DefInfo QName (Arg Expr)
- | Primitive DefInfo QName Expr
- | Mutual MutualInfo [Declaration]
- | Section ModuleInfo ModuleName [TypedBindings] [Declaration]
- | Apply ModuleInfo ModuleName ModuleApplication (Ren QName) (Ren ModuleName)
- | Import ModuleInfo ModuleName
- | Pragma Range Pragma
- | Open ModuleInfo ModuleName
- | FunDef DefInfo QName Delayed [Clause]
- | DataSig DefInfo QName Telescope Expr
- | DataDef DefInfo QName [LamBinding] [Constructor]
- | RecSig DefInfo QName Telescope Expr
- | RecDef DefInfo QName (Maybe (Ranged Induction)) (Maybe QName) [LamBinding] Expr [Declaration]
- | PatternSynDef QName [Arg Name] Pattern
- | UnquoteDecl MutualInfo DefInfo QName Expr
- | ScopedDecl ScopeInfo [Declaration]
- class GetDefInfo a where
- getDefInfo :: a -> Maybe DefInfo
- data ModuleApplication
- data Pragma
- = OptionsPragma [String]
- | BuiltinPragma String Expr
- | BuiltinNoDefPragma String QName
- | 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
- data LetBinding
- type TypeSignature = Declaration
- type Constructor = TypeSignature
- type Field = TypeSignature
- data LamBinding
- data TypedBindings = TypedBindings Range (Arg TypedBinding)
- data TypedBinding
- = TBind Range [WithHiding Name] Expr
- | TLet Range [LetBinding]
- type Telescope = [TypedBindings]
- data Clause' lhs = Clause {
- clauseLHS :: lhs
- clauseRHS :: RHS
- clauseWhereDecls :: [Declaration]
- type Clause = Clause' LHS
- type SpineClause = Clause' SpineLHS
- data RHS
- data SpineLHS = SpineLHS {
- spLhsInfo :: LHSInfo
- spLhsDefName :: QName
- spLhsPats :: [NamedArg Pattern]
- spLhsWithPats :: [Pattern]
- data LHS = LHS {}
- data LHSCore' e
- = LHSHead {
- lhsDefName :: QName
- lhsPats :: [NamedArg (Pattern' e)]
- | LHSProj {
- lhsDestructor :: QName
- lhsPatsLeft :: [NamedArg (Pattern' e)]
- lhsFocus :: NamedArg (LHSCore' e)
- lhsPatsRight :: [NamedArg (Pattern' e)]
- = LHSHead {
- type LHSCore = LHSCore' Expr
- class LHSToSpine a b where
- lhsToSpine :: a -> b
- spineToLhs :: b -> a
- lhsCoreToSpine :: LHSCore' e -> QNamed [NamedArg (Pattern' e)]
- spineToLhsCore :: QNamed [NamedArg (Pattern' e)] -> LHSCore' e
- lhsCoreApp :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
- lhsCoreAddSpine :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
- lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e]
- lhsCoreToPattern :: LHSCore -> Pattern
- mapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore
- data Pattern' e
- type Pattern = Pattern' Expr
- type Patterns = [NamedArg Pattern]
- class IsProjP a where
- class AllNames a where
- axiomName :: Declaration -> QName
- class AnyAbstract a where
- anyAbstract :: a -> Bool
- app :: Expr -> [NamedArg Expr] -> Expr
- patternToExpr :: Pattern -> Expr
- type PatternSynDefn = ([Arg Name], Pattern)
- type PatternSynDefns = Map QName PatternSynDefn
- lambdaLiftExpr :: [Name] -> Expr -> Expr
- substPattern :: [(Name, Pattern)] -> Pattern -> Pattern
- class SubstExpr a where
- insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name])
- module Agda.Syntax.Abstract.Name
Documentation
data Expr
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 |
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 |
|
AbsurdLam ExprInfo Hiding |
|
ExtendedLam ExprInfo DefInfo QName [Clause] | |
Pi ExprInfo Telescope Expr | Dependent function space |
Fun ExprInfo (Arg Expr) Expr | Non-dependent function space. |
Set ExprInfo Integer |
|
Prop ExprInfo |
|
Let ExprInfo [LetBinding] Expr |
|
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 |
QuoteContext ExprInfo Name Expr | Binds |
Quote ExprInfo | Quote an identifier |
QuoteTerm ExprInfo | Quote a term. |
Unquote ExprInfo | The splicing construct: unquote ... |
DontCare Expr | For printing |
Instances
data Axiom
Is a type signature a postulate
or a function signature?
type Ren a = [(a, a)]
Renaming (generic).
data Declaration
Constructors
Instances
data ModuleApplication
Constructors
SectionApp Telescope ModuleName [NamedArg Expr] |
|
RecordModuleIFS ModuleName | M {{...}} |
data Pragma
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
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) |
|
LetOpen ModuleInfo ModuleName | only for highlighting and abstractToConcrete |
type TypeSignature = Declaration
Only Axiom
s.
type Constructor = TypeSignature
type Field = TypeSignature
data LamBinding
A lambda binding is either domain free or typed.
Constructors
DomainFree ArgInfo Name | . |
DomainFull TypedBindings | . |
data TypedBindings
Typed bindings with hiding information.
Constructors
TypedBindings Range (Arg TypedBinding) | . |
data TypedBinding
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:
- We would have to typecheck the type
A
several times. - 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 |
TLet Range [LetBinding] | E.g. |
type Telescope = [TypedBindings]
data Clause' lhs
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
|
Instances
Functor Clause' | |
Foldable Clause' | |
Traversable Clause' | |
AllNames Clause | |
LHSToSpine Clause SpineClause | Clause instance. |
ToAbstract Clause Clause | |
Reify NamedClause Clause | |
Show lhs => Show (Clause' lhs) | |
KillRange a => KillRange (Clause' a) | |
HasRange a => HasRange (Clause' a) | |
ExprLike (Clause' a) | TODO: currently does not go into clauses. |
ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] |
type SpineClause = Clause' SpineLHS
data RHS
Constructors
RHS Expr | |
AbsurdRHS | |
WithRHS QName [Expr] [Clause] | The |
RewriteRHS [(QName, Expr)] RHS [Declaration] | The |
Instances
Show RHS | |
KillRange RHS | |
HasRange RHS | |
AllNames 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
|
Instances
Show SpineLHS | |
KillRange SpineLHS | |
HasRange SpineLHS | |
LHSToSpine LHS SpineLHS | LHS instance. |
LHSToSpine Clause SpineClause | Clause instance. |
ToConcrete SpineLHS LHS |
data LHS
The lhs of a clause in focused (projection-application) view (outside-in).
Projection patters are represented as LHSProj
s.
Constructors
LHS | |
Instances
Show LHS | |
KillRange LHS | |
HasRange LHS | |
AllNames Clause | |
LHSToSpine LHS SpineLHS | LHS instance. |
LHSToSpine Clause SpineClause | Clause instance. |
ToConcrete LHS LHS | |
ToAbstract Clause Clause | |
ToAbstract LeftHandSide LHS | |
Reify NamedClause Clause |
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
| |
LHSProj | Projection |
Fields
|
class LHSToSpine a b where
Convert a focused lhs to spine view and back.
Instances
LHSToSpine LHS SpineLHS | LHS instance. |
LHSToSpine Clause SpineClause | Clause instance. |
LHSToSpine a b => LHSToSpine [a] [b] | List instance (for clauses). |
lhsCoreToSpine :: LHSCore' e -> QNamed [NamedArg (Pattern' e)]
spineToLhsCore :: QNamed [NamedArg (Pattern' e)] -> LHSCore' e
lhsCoreApp :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
Add applicative patterns (non-projection patterns) to the right.
lhsCoreAddSpine :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
Add projection and applicative patterns to the right.
lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e]
Used for checking pattern linearity.
lhsCoreToPattern :: LHSCore -> Pattern
Used in AbstractToConcrete.
Patterns
data Pattern' e
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 |
WildP PatInfo | Underscore pattern entered by user. |
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' | |
Foldable Pattern' | |
Traversable Pattern' | |
EmbPrj Pattern | |
ExpandPatternSynonyms Pattern | |
UniverseBi Declaration Pattern | |
ToConcrete Pattern Pattern | |
ToAbstract Pattern (Pattern' Expr) | |
Show e => Show (Pattern' e) | |
KillRange e => KillRange (Pattern' e) | |
SetRange (Pattern' a) | |
HasRange (Pattern' e) | |
IsProjP (Pattern' e) | |
ExprLike (Pattern' a) | TODO: currently does not go into patterns. |
ToAbstract (Pattern' Expr) (Pattern' Expr) |
class IsProjP a where
Check whether we are a projection pattern.
class AllNames a where
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.
Instances
AllNames QName | |
AllNames RHS | |
AllNames Clause | |
AllNames TypedBinding | |
AllNames TypedBindings | |
AllNames LamBinding | |
AllNames LetBinding | |
AllNames ModuleApplication | |
AllNames Declaration | |
AllNames Expr | |
AllNames CallInfo | |
AllNames CallPath | |
AllNames a => AllNames [a] | |
AllNames a => AllNames (Maybe a) | |
AllNames a => AllNames (Arg a) | |
(AllNames a, AllNames b) => AllNames (a, b) | |
AllNames a => AllNames (Named name a) |
axiomName :: Declaration -> QName
The name defined by the given axiom.
Precondition: The declaration has to be a (scoped) 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] |
patternToExpr :: Pattern -> Expr
type PatternSynDefn = ([Arg Name], Pattern)
type PatternSynDefns = Map QName PatternSynDefn
lambdaLiftExpr :: [Name] -> Expr -> Expr
substPattern :: [(Name, Pattern)] -> Pattern -> Pattern
class SubstExpr a where
insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name])
module Agda.Syntax.Abstract.Name