Safe Haskell | None |
---|
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
- | Con AmbiguousQName
- | 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
- | PatternSyn QName
- type Assign = (Name, Expr)
- type Assigns = [Assign]
- data Axiom
- type Ren a = Map 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
- | 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
- 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
- allNames :: Declaration -> Seq QName
- 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
- substExpr :: [(Name, Expr)] -> Expr -> Expr
- substLetBindings :: [(Name, Expr)] -> [LetBinding] -> [LetBinding]
- substLetBinding :: [(Name, Expr)] -> LetBinding -> LetBinding
- substTypedBindings :: [(Name, Expr)] -> TypedBindings -> TypedBindings
- substTypedBinding :: [(Name, Expr)] -> TypedBinding -> TypedBinding
- insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name])
- module Agda.Syntax.Abstract.Name
Documentation
Var Name | Bound variables |
Def QName | Constants (i.e. axioms, functions, projections, and datatypes) |
Con AmbiguousQName | Constructors |
Lit Literal | Literals |
QuestionMark MetaInfo InteractionId | Meta variable for interaction.
The |
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 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 DontCare from Syntax.Internal |
PatternSyn QName |
Is a type signature a postulate
or a function signature?
data Declaration Source
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 |
DataDef DefInfo QName [LamBinding] [Constructor] | the |
RecSig DefInfo QName Telescope Expr | lone record signature |
RecDef DefInfo QName (Maybe (Ranged Induction)) (Maybe QName) [LamBinding] Expr [Declaration] | The |
PatternSynDef QName [Arg Name] Pattern | Only for highlighting purposes |
UnquoteDecl MutualInfo DefInfo QName Expr | |
ScopedDecl ScopeInfo [Declaration] | scope annotation |
data ModuleApplication Source
SectionApp Telescope ModuleName [NamedArg Expr] |
|
RecordModuleIFS ModuleName | M {{...}} |
OptionsPragma [String] | |
BuiltinPragma String Expr | |
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 |
Show Pragma | |
Typeable Pragma | |
ToAbstract Pragma [Pragma] |
data LetBinding Source
Bindings that are valid in a let
.
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 = DeclarationSource
Only Axiom
s.
type Constructor = TypeSignatureSource
type Field = TypeSignatureSource
data LamBinding Source
A lambda binding is either domain free or typed.
DomainFree ArgInfo Name | . |
DomainFull TypedBindings | . |
data TypedBindings Source
Typed bindings with hiding information.
TypedBindings Range (Arg TypedBinding) | . |
data TypedBinding Source
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.
(Andreas, 2013-12-10: The more serious problem would that the translation
from (x y : ?)
to (x : ?) (y : ?)
duplicates the hole ?
.
type Telescope = [TypedBindings]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.
Clause | |
|
Functor Clause' | |
Typeable1 Clause' | |
Foldable Clause' | |
Traversable 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' SpineLHSSource
RHS Expr | |
AbsurdRHS | |
WithRHS QName [Expr] [Clause] | The |
RewriteRHS [QName] [Expr] RHS [Declaration] | The |
Show RHS | |
Typeable RHS | |
KillRange RHS | |
HasRange RHS | |
ToAbstract AbstractRHS RHS | |
Reify ClauseBody RHS | |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) |
The lhs of a clause in spine view (inside-out).
Projection patterns are contained in spLhsPats
,
represented as DefP d []
.
SpineLHS | |
|
Show SpineLHS | |
Typeable SpineLHS | |
KillRange SpineLHS | |
HasRange SpineLHS | |
LHSToSpine LHS SpineLHS | LHS instance. |
LHSToSpine Clause SpineClause | Clause instance. |
ToConcrete SpineLHS LHS |
The lhs of a clause in focused (projection-application) view (outside-in).
Projection patters are represented as LHSProj
s.
Eq LHS | |
Show LHS | |
Typeable LHS | |
KillRange LHS | |
HasRange LHS | |
LHSToSpine LHS SpineLHS | LHS instance. |
LHSToSpine Clause SpineClause | Clause instance. |
ToConcrete LHS LHS | |
ToAbstract Clause Clause | |
ToAbstract LeftHandSide LHS | |
Reify NamedClause Clause |
The lhs minus with
-patterns in projection-application view.
Parameterised over the type e
of dot patterns.
LHSHead | The head applied to ordinary patterns. |
| |
LHSProj | Projection |
|
class LHSToSpine a b whereSource
Convert a focused lhs to spine view and back.
lhsToSpine :: a -> bSource
spineToLhs :: b -> aSource
LHSToSpine LHS SpineLHS | LHS instance. |
LHSToSpine Clause SpineClause | Clause instance. |
LHSToSpine a b => LHSToSpine [a] [b] | List instance (for clauses). |
lhsCoreApp :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' eSource
Add applicative patterns (non-projection patterns) to the right.
lhsCoreAddSpine :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' eSource
Add projection and applicative patterns to the right.
lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e]Source
Used for checking pattern linearity.
lhsCoreToPattern :: LHSCore -> PatternSource
Used in AbstractToConcrete.
Patterns
Parameterised over the type of dot patterns.
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)] |
Functor Pattern' | |
Typeable1 Pattern' | |
Foldable Pattern' | |
Traversable Pattern' | |
EmbPrj Pattern | |
ExpandPatternSynonyms 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) | |
IsProjP (Pattern' e) | |
ExprLike (Pattern' a) | TODO: currently does not go into patterns. |
ToAbstract (Pattern' Expr) (Pattern' Expr) |
Check whether we are a projection pattern.
allNames :: Declaration -> Seq QNameSource
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 -> QNameSource
The name defined by the given axiom.
Precondition: The declaration has to be a (scoped) Axiom
.
class AnyAbstract a whereSource
Are we in an abstract block?
In that case some definition is abstract.
anyAbstract :: a -> BoolSource
AnyAbstract Declaration | |
AnyAbstract a => AnyAbstract [a] |
patternToExpr :: Pattern -> ExprSource
type PatternSynDefn = ([Arg Name], Pattern)Source
type PatternSynDefns = Map QName PatternSynDefnSource
lambdaLiftExpr :: [Name] -> Expr -> ExprSource
substLetBindings :: [(Name, Expr)] -> [LetBinding] -> [LetBinding]Source
substLetBinding :: [(Name, Expr)] -> LetBinding -> LetBindingSource
substTypedBindings :: [(Name, Expr)] -> TypedBindings -> TypedBindingsSource
substTypedBinding :: [(Name, Expr)] -> TypedBinding -> TypedBindingSource
insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name])Source
module Agda.Syntax.Abstract.Name