| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
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
- type Type = Expr
- type Constructor = TypeSignature
- type Clause = Clause' LHS
- data Pragma
- = OptionsPragma [String]
- | BuiltinPragma RString ResolvedName
- | BuiltinNoDefPragma RString KindOfName QName
- | RewritePragma Range [QName]
- | CompilePragma RString QName String
- | StaticPragma QName
- | EtaPragma QName
- | InjectivePragma QName
- | InlinePragma Bool QName
- | NotProjectionLikePragma QName
- | DisplayPragma QName [NamedArg Pattern] Expr
- type Telescope = [TypedBinding]
- type Pattern = Pattern' Expr
- type Assign = FieldAssignment' Expr
- data Expr
- = Var Name
- | Def' QName Suffix
- | Proj ProjOrigin AmbiguousQName
- | Con AmbiguousQName
- | PatternSyn AmbiguousQName
- | Macro QName
- | Lit ExprInfo Literal
- | QuestionMark MetaInfo InteractionId
- | Underscore MetaInfo
- | Dot ExprInfo Expr
- | App AppInfo Expr (NamedArg Expr)
- | WithApp ExprInfo Expr [Expr]
- | Lam ExprInfo LamBinding Expr
- | AbsurdLam ExprInfo Hiding
- | ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause)
- | Pi ExprInfo Telescope1 Type
- | Generalized (Set QName) Type
- | Fun ExprInfo (Arg Type) Type
- | Let ExprInfo (List1 LetBinding) Expr
- | Rec ExprInfo RecordAssigns
- | RecUpdate ExprInfo Expr Assigns
- | ScopedExpr ScopeInfo Expr
- | Quote ExprInfo
- | QuoteTerm ExprInfo
- | Unquote ExprInfo
- | DontCare Expr
- data LHS = LHS {}
- data Binder' a = Binder {
- binderPattern :: Maybe Pattern
- binderName :: a
- type Binder = Binder' BindName
- data LamBinding
- data TypedBinding
- type Telescope1 = List1 TypedBinding
- data Declaration
- = Axiom KindOfName DefInfo ArgInfo (Maybe [Occurrence]) QName Type
- | Generalize (Set QName) DefInfo ArgInfo QName Type
- | Field DefInfo QName (Arg Type)
- | Primitive DefInfo QName (Arg Type)
- | Mutual MutualInfo [Declaration]
- | Section Range Erased ModuleName GeneralizeTelescope [Declaration]
- | Apply ModuleInfo Erased ModuleName ModuleApplication ScopeCopyInfo ImportDirective
- | Import ModuleInfo ModuleName ImportDirective
- | Pragma Range Pragma
- | Open ModuleInfo ModuleName ImportDirective
- | FunDef DefInfo QName [Clause]
- | DataSig DefInfo Erased QName GeneralizeTelescope Type
- | DataDef DefInfo QName UniverseCheck DataDefParams [Constructor]
- | RecSig DefInfo Erased QName GeneralizeTelescope Type
- | RecDef DefInfo QName UniverseCheck RecordDirectives DataDefParams Type [Declaration]
- | PatternSynDef QName [Arg BindName] (Pattern' Void)
- | UnquoteDecl MutualInfo [DefInfo] [QName] Expr
- | UnquoteDef [DefInfo] [QName] Expr
- | UnquoteData [DefInfo] QName UniverseCheck [DefInfo] [QName] Expr
- | ScopedDecl ScopeInfo [Declaration]
- | UnfoldingDecl Range [QName]
- type RecordDirectives = RecordDirectives' QName
- data ModuleApplication
- type TypeSignature = Declaration
- type ImportDirective = ImportDirective' QName ModuleName
- type ImportedName = ImportedName' QName ModuleName
- type Renaming = Renaming' QName ModuleName
- type RewriteEqn = RewriteEqn' QName BindName Pattern Expr
- type WithExpr = WithExpr' Expr
- type LHSCore = LHSCore' Expr
- data RHS
- type HoleContent = HoleContent' () BindName Pattern Expr
- data ScopeCopyInfo = ScopeCopyInfo {
- renModules :: Ren ModuleName
- renNames :: Ren QName
- type Args = [NamedArg Expr]
- type Ren a = Map a (List1 a)
- type PatternSynDefn = ([Arg Name], Pattern' Void)
- type PatternSynDefns = Map QName PatternSynDefn
- data ProblemEq = ProblemEq {
- problemInPat :: Pattern
- problemInst :: Term
- problemType :: Dom Type
- data TypedBindingInfo = TypedBindingInfo {}
- type Field = TypeSignature
- type NAPs e = [NamedArg (Pattern' e)]
- data Pattern' e
- = VarP BindName
- | ConP ConPatInfo AmbiguousQName (NAPs e)
- | ProjP PatInfo ProjOrigin AmbiguousQName
- | DefP PatInfo AmbiguousQName (NAPs e)
- | WildP PatInfo
- | AsP PatInfo BindName (Pattern' e)
- | DotP PatInfo e
- | AbsurdP PatInfo
- | LitP PatInfo Literal
- | PatternSynP PatInfo AmbiguousQName (NAPs e)
- | RecP PatInfo [FieldAssignment' (Pattern' e)]
- | EqualP PatInfo [(e, e)]
- | WithP PatInfo (Pattern' e)
- | AnnP PatInfo e (Pattern' e)
- type DefInfo = DefInfo' Expr
- newtype BindName = BindName {}
- data LetBinding
- type RecordAssigns = [RecordAssign]
- type Assigns = [Assign]
- type RecordAssign = Either Assign ModuleName
- data GeneralizeTelescope = GeneralizeTel {}
- data DataDefParams = DataDefParams {}
- type TacticAttr = Maybe (Ranged Expr)
- data Clause' lhs = Clause {
- clauseLHS :: lhs
- clauseStrippedPats :: [ProblemEq]
- clauseRHS :: RHS
- clauseWhereDecls :: WhereDeclarations
- clauseCatchall :: Bool
- data WhereDeclarations = WhereDecls {}
- type SpineClause = Clause' SpineLHS
- data SpineLHS = SpineLHS {}
- type WithExpr' e = Named BindName (Arg e)
- data LHSCore' e
- type NAPs1 e = List1 (NamedArg (Pattern' e))
- type Patterns = [NamedArg Pattern]
- class AnyAbstract a where
- anyAbstract :: a -> Bool
- class NameToExpr a where
- nameToExpr :: a -> Expr
- class SubstExpr a where
- data DeclarationSpine
- = AxiomS
- | GeneralizeS
- | FieldS
- | PrimitiveS
- | MutualS [DeclarationSpine]
- | SectionS [DeclarationSpine]
- | ApplyS
- | ImportS
- | PragmaS
- | OpenS
- | FunDefS [ClauseSpine]
- | DataSigS
- | DataDefS
- | RecSigS
- | RecDefS [DeclarationSpine]
- | PatternSynDefS
- | UnquoteDeclS
- | UnquoteDefS
- | UnquoteDataS
- | ScopedDeclS [DeclarationSpine]
- | UnfoldingDeclS
- data ClauseSpine = ClauseS RHSSpine WhereDeclarationsSpine
- data RHSSpine
- data WhereDeclarationsSpine = WhereDeclsS (Maybe DeclarationSpine)
- pattern Def :: QName -> Expr
- app :: Expr -> [NamedArg Expr] -> Expr
- mkBinder_ :: Name -> Binder
- mkBinder :: a -> Binder' a
- mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
- mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding
- mkBindName :: Name -> BindName
- generalized :: Set QName -> Type -> Type
- initCopyInfo :: ScopeCopyInfo
- extractPattern :: Binder' a -> Maybe (Pattern, a)
- mkDomainFree :: NamedArg Binder -> LamBinding
- defaultTbInfo :: TypedBindingInfo
- mkTBind :: Range -> List1 (NamedArg Binder) -> Type -> TypedBinding
- mkPi :: ExprInfo -> Telescope -> Type -> Type
- noDataDefParams :: DataDefParams
- noWhereDecls :: WhereDeclarations
- axiomName :: Declaration -> QName
- patternToExpr :: Pattern -> Expr
- lambdaLiftExpr :: [Name] -> Expr -> Expr
- insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name])
- declarationSpine :: Declaration -> DeclarationSpine
- clauseSpine :: Clause -> ClauseSpine
- rhsSpine :: RHS -> RHSSpine
- whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine
- module Agda.Syntax.Abstract.Name
Documentation
Types are just expressions. Use this type synonym for hinting that an expression should be a type.
type Constructor = TypeSignature Source #
Constructors
| OptionsPragma [String] | |
| BuiltinPragma RString ResolvedName |
|
| BuiltinNoDefPragma RString KindOfName QName | Builtins that do not come with a definition, but declare a name for an Agda concept. |
| RewritePragma Range [QName] | Range is range of REWRITE keyword. |
| CompilePragma RString QName String | |
| StaticPragma QName | |
| EtaPragma QName | For coinductive records, use pragma instead of regular
|
| InjectivePragma QName | |
| InlinePragma Bool QName | |
| NotProjectionLikePragma QName | |
| DisplayPragma QName [NamedArg Pattern] Expr |
Instances
type Telescope = [TypedBinding] Source #
type Assign = FieldAssignment' Expr Source #
Record field assignment f = e.
Expressions after scope checking (operators parsed, names resolved).
Constructors
| Var Name | Bound variable. |
| Def' QName Suffix | Constant: axiom, function, data or record type, with a possible suffix. |
| Proj ProjOrigin AmbiguousQName | Projection (overloaded). |
| Con AmbiguousQName | Constructor (overloaded). |
| PatternSyn AmbiguousQName | Pattern synonym. |
| Macro QName | Macro. |
| Lit ExprInfo Literal | Literal. |
| QuestionMark MetaInfo InteractionId | Meta variable for interaction.
The |
| Underscore MetaInfo | Meta variable for hidden argument (must be inferred locally). |
| Dot ExprInfo Expr |
|
| App AppInfo Expr (NamedArg Expr) | Ordinary (binary) application. |
| WithApp ExprInfo Expr [Expr] | With application. |
| Lam ExprInfo LamBinding Expr |
|
| AbsurdLam ExprInfo Hiding |
|
| ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause) | |
| Pi ExprInfo Telescope1 Type | Dependent function space |
| Generalized (Set QName) Type | Like a Pi, but the ordering is not known |
| Fun ExprInfo (Arg Type) Type | Non-dependent function space. |
| Let ExprInfo (List1 LetBinding) Expr |
|
| Rec ExprInfo RecordAssigns | Record construction. |
| RecUpdate ExprInfo Expr Assigns | Record update. |
| ScopedExpr ScopeInfo Expr | Scope annotation. |
| Quote ExprInfo | Quote an identifier |
| QuoteTerm ExprInfo | Quote a term. |
| Unquote ExprInfo | The splicing construct: unquote ... |
| DontCare Expr | For printing |
Instances
The lhs of a clause in focused (projection-application) view (outside-in).
Projection patters are represented as LHSProjs.
Instances
Constructors
| Binder | |
Fields
| |
Instances
data LamBinding Source #
A lambda binding is either domain free or typed.
Constructors
| DomainFree TacticAttr (NamedArg Binder) | . |
| DomainFull TypedBinding | . |
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:
- We would have to typecheck the type
Aseveral times. - If
Acontains 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 TypedBindingInfo (List1 (NamedArg Binder)) Type | As in telescope |
| TLet Range (List1 LetBinding) | E.g. |
Instances
type Telescope1 = List1 TypedBinding Source #
data Declaration Source #
Constructors
Instances
data ModuleApplication Source #
Constructors
| SectionApp Telescope ModuleName [NamedArg Expr] |
|
| RecordModuleInstance ModuleName | M {{...}} |
Instances
type TypeSignature = Declaration Source #
Only Axioms.
type ImportedName = ImportedName' QName ModuleName Source #
type RewriteEqn = RewriteEqn' QName BindName Pattern Expr Source #
Constructors
| RHS | |
| AbsurdRHS | |
| WithRHS QName [WithExpr] (List1 Clause) | The |
| RewriteRHS | |
Fields
| |
Instances
type HoleContent = HoleContent' () BindName Pattern Expr Source #
data ScopeCopyInfo Source #
Constructors
| ScopeCopyInfo | |
Fields
| |
Instances
type PatternSynDefns = Map QName PatternSynDefn Source #
A user pattern together with an internal term that it should be equal to after splitting is complete. Special cases: * User pattern is a variable but internal term isn't: this will be turned into an as pattern. * User pattern is a dot pattern: this pattern won't trigger any splitting but will be checked for equality after all splitting is complete and as patterns have been bound. * User pattern is an absurd pattern: emptiness of the type will be checked after splitting is complete. * User pattern is an annotated wildcard: type annotation will be checked after splitting is complete.
Constructors
| ProblemEq | |
Fields
| |
Instances
data TypedBindingInfo Source #
Extra information that is attached to a typed binding, that plays a
role during type checking but strictly speaking is not part of the
name : type" relation which a makes up a binding.
Constructors
| TypedBindingInfo | |
Fields
| |
Instances
type Field = TypeSignature Source #
Parameterised over the type of dot patterns.
Constructors
| VarP BindName | |
| ConP ConPatInfo AmbiguousQName (NAPs e) | |
| ProjP PatInfo ProjOrigin AmbiguousQName | Destructor pattern |
| DefP PatInfo AmbiguousQName (NAPs e) | Defined pattern: function definition |
| WildP PatInfo | Underscore pattern entered by user. Or generated at type checking for implicit arguments. |
| AsP PatInfo BindName (Pattern' e) | |
| DotP PatInfo e | Dot pattern |
| AbsurdP PatInfo | |
| LitP PatInfo Literal | |
| PatternSynP PatInfo AmbiguousQName (NAPs e) | |
| RecP PatInfo [FieldAssignment' (Pattern' e)] | |
| EqualP PatInfo [(e, e)] | |
| WithP PatInfo (Pattern' e) |
|
| AnnP PatInfo e (Pattern' e) | Pattern with type annotation |
Instances
A name in a binding position: we also compare the nameConcrete when comparing the binders for equality.
With --caching on we compare abstract syntax to determine if we can
reuse previous typechecking results: during that comparison two
names can have the same nameId but be semantically different,
e.g. in {_ : A} -> .. vs. {r : A} -> ...
Instances
data LetBinding Source #
Bindings that are valid in a let.
Constructors
| LetBind LetInfo ArgInfo BindName Type Expr | LetBind info rel name type defn |
| LetPatBind LetInfo Pattern Expr | Irrefutable pattern binding. |
| LetApply ModuleInfo Erased ModuleName ModuleApplication ScopeCopyInfo ImportDirective |
|
| LetOpen ModuleInfo ModuleName ImportDirective | only for highlighting and abstractToConcrete |
| LetDeclaredVariable BindName | Only used for highlighting. Refers to the first occurrence of
|
Instances
type RecordAssigns = [RecordAssign] Source #
type RecordAssign = Either Assign ModuleName Source #
data GeneralizeTelescope Source #
Constructors
| GeneralizeTel | |
Fields
| |
Instances
data DataDefParams Source #
Constructors
| DataDefParams | |
Fields
| |
Instances
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
data WhereDeclarations Source #
Constructors
| WhereDecls | |
Fields
| |
Instances
type SpineClause = Clause' SpineLHS Source #
The lhs of a clause in spine view (inside-out).
Projection patterns are contained in spLhsPats,
represented as ProjP d.
Constructors
| SpineLHS | |
Instances
The lhs in projection-application and with-pattern view.
Parameterised over the type e of dot patterns.
Constructors
| LHSHead | The head applied to ordinary patterns. |
Fields
| |
| LHSProj | Projection. |
Fields
| |
| LHSWith | With patterns. |
Instances
class AnyAbstract a where Source #
Are we in an abstract block?
In that case some definition is abstract.
Methods
anyAbstract :: a -> Bool Source #
Instances
| AnyAbstract Declaration Source # | |
Defined in Agda.Syntax.Abstract Methods anyAbstract :: Declaration -> Bool Source # | |
| AnyAbstract a => AnyAbstract [a] Source # | |
Defined in Agda.Syntax.Abstract Methods anyAbstract :: [a] -> Bool Source # | |
class NameToExpr a where Source #
Turn a name into an expression.
Methods
nameToExpr :: a -> Expr Source #
Instances
| NameToExpr AbstractName Source # | Turn an |
Defined in Agda.Syntax.Abstract Methods nameToExpr :: AbstractName -> Expr Source # | |
| NameToExpr ResolvedName Source # | Turn a Assumes name is not |
Defined in Agda.Syntax.Abstract Methods nameToExpr :: ResolvedName -> Expr Source # | |
class SubstExpr a where Source #
Minimal complete definition
Nothing
Methods
Instances
| SubstExpr Expr Source # | |
| SubstExpr ModuleName Source # | |
Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName Source # | |
| SubstExpr Name Source # | |
| SubstExpr a => SubstExpr (Arg a) Source # | |
| SubstExpr a => SubstExpr (FieldAssignment' a) Source # | |
Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> FieldAssignment' a -> FieldAssignment' a Source # | |
| SubstExpr a => SubstExpr (List1 a) Source # | |
| SubstExpr a => SubstExpr (Maybe a) Source # | |
| SubstExpr a => SubstExpr [a] Source # | |
| SubstExpr a => SubstExpr (Named name a) Source # | |
| (SubstExpr a, SubstExpr b) => SubstExpr (Either a b) Source # | |
| (SubstExpr a, SubstExpr b) => SubstExpr (a, b) Source # | |
data DeclarationSpine Source #
Declaration spines. Used in debugging to make it easy to see
where constructors such as ScopedDecl and Mutual are placed.
Constructors
Instances
| Show DeclarationSpine Source # | |
Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> DeclarationSpine -> ShowS # show :: DeclarationSpine -> String # showList :: [DeclarationSpine] -> ShowS # | |
data ClauseSpine Source #
Clause spines.
Constructors
| ClauseS RHSSpine WhereDeclarationsSpine |
Instances
| Show ClauseSpine Source # | |
Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ClauseSpine -> ShowS # show :: ClauseSpine -> String # showList :: [ClauseSpine] -> ShowS # | |
Right-hand side spines.
Constructors
| RHSS | |
| AbsurdRHSS | |
| WithRHSS (List1 ClauseSpine) | |
| RewriteRHSS RHSSpine WhereDeclarationsSpine |
data WhereDeclarationsSpine Source #
Spines corresponding to WhereDeclarations values.
Constructors
| WhereDeclsS (Maybe DeclarationSpine) |
Instances
| Show WhereDeclarationsSpine Source # | |
Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> WhereDeclarationsSpine -> ShowS # show :: WhereDeclarationsSpine -> String # showList :: [WhereDeclarationsSpine] -> ShowS # | |
mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding Source #
mkBindName :: Name -> BindName Source #
generalized :: Set QName -> Type -> Type Source #
Smart constructor for Generalized.
mkDomainFree :: NamedArg Binder -> LamBinding Source #
axiomName :: Declaration -> QName Source #
The name defined by the given axiom.
Precondition: The declaration has to be a (scoped) Axiom.
patternToExpr :: Pattern -> Expr Source #
insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name]) Source #
declarationSpine :: Declaration -> DeclarationSpine Source #
The declaration spine corresponding to a declaration.
clauseSpine :: Clause -> ClauseSpine Source #
The clause spine corresponding to a clause.
whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine Source #
The spine corresponding to a WhereDeclarations value.
module Agda.Syntax.Abstract.Name