Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- 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
- type Type = Expr
- type Telescope = [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 [WithHiding 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 Assign = FieldAssignment' Expr
- type Constructor = TypeSignature
- type Pattern = Pattern' Expr
- pattern Def :: QName -> Expr
- data LHS = 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
- | InjectiveForInferencePragma QName
- | InlinePragma Bool QName
- | NotProjectionLikePragma QName
- | OverlapPragma QName OverlapMode
- | DisplayPragma QName [NamedArg Pattern] Expr
- type TacticAttribute = TacticAttribute' Expr
- type Clause = Clause' LHS
- data Clause' lhs = Clause {
- clauseLHS :: lhs
- clauseStrippedPats :: [ProblemEq]
- clauseRHS :: RHS
- clauseWhereDecls :: WhereDeclarations
- clauseCatchall :: Bool
- data Binder' a = Binder {
- binderPattern :: Maybe Pattern
- binderName :: a
- type Binder = Binder' BindName
- mkBinder_ :: Name -> Binder
- mkBinder :: a -> Binder' a
- data LamBinding
- data TypedBinding
- type Telescope1 = List1 TypedBinding
- mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
- mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding
- 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 Ren a = Map a (List1 a)
- type PatternSynDefn = ([WithHiding Name], Pattern' Void)
- type PatternSynDefns = Map QName PatternSynDefn
- data ProblemEq = ProblemEq {
- problemInPat :: Pattern
- problemInst :: Term
- problemType :: Dom Type
- data TypedBindingInfo = TypedBindingInfo {
- tbTacticAttr :: TacticAttribute
- tbFinite :: Bool
- type Args = [NamedArg Expr]
- app :: Expr -> [NamedArg Expr] -> Expr
- 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 ConPatInfo [FieldAssignment' (Pattern' e)]
- | EqualP PatInfo [(e, e)]
- | WithP PatInfo (Pattern' e)
- | AnnP PatInfo e (Pattern' e)
- type Field = TypeSignature
- data LHSCore' e
- type NAPs e = [NamedArg (Pattern' e)]
- type DefInfo = DefInfo' Expr
- newtype BindName = BindName {}
- mkBindName :: Name -> BindName
- data LetBinding
- type RecordAssigns = [RecordAssign]
- type Assigns = [Assign]
- generalized :: Set QName -> Type -> Type
- type RecordAssign = Either Assign ModuleName
- initCopyInfo :: ScopeCopyInfo
- data GeneralizeTelescope = GeneralizeTel {
- generalizeTelVars :: Map QName Name
- generalizeTel :: Telescope
- data DataDefParams = DataDefParams {
- dataDefGeneralizedParams :: Set Name
- dataDefParams :: [LamBinding]
- extractPattern :: Binder' a -> Maybe (Pattern, a)
- mkDomainFree :: NamedArg Binder -> LamBinding
- mkTBind :: Range -> List1 (NamedArg Binder) -> Type -> TypedBinding
- mkPi :: ExprInfo -> Telescope -> Type -> Type
- noDataDefParams :: DataDefParams
- data WhereDeclarations = WhereDecls {
- whereModule :: Maybe ModuleName
- whereAnywhere :: Bool
- whereDecls :: Maybe Declaration
- noWhereDecls :: WhereDeclarations
- type SpineClause = Clause' SpineLHS
- data SpineLHS = SpineLHS {}
- type WithExpr' e = Named BindName (Arg e)
- type NAPs1 e = List1 (NamedArg (Pattern' e))
- type Patterns = [NamedArg Pattern]
- axiomName :: Declaration -> QName
- class AnyAbstract a where
- anyAbstract :: a -> Bool
- class NameToExpr a where
- nameToExpr :: a -> Expr
- lambdaLiftExpr :: [WithHiding Name] -> Expr -> Expr
- class SubstExpr a where
- insertImplicitPatSynArgs :: HasRange a => (Hiding -> Range -> a) -> Range -> [WithHiding Name] -> [NamedArg a] -> Maybe ([(Name, a)], [WithHiding Name])
- 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)
- declarationSpine :: Declaration -> DeclarationSpine
- clauseSpine :: Clause -> ClauseSpine
- rhsSpine :: RHS -> RHSSpine
- whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine
- module Agda.Syntax.Abstract.Name
Documentation
Expressions after scope checking (operators parsed, names resolved).
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
SubstExpr Expr Source # | |||||
IsProjP Expr Source # | |||||
Defined in Agda.Syntax.Abstract isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName) Source # | |||||
MapNamedArgPattern NAP Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
ExprLike Expr Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m Expr Source # foldExpr :: FoldExprFn m Expr Source # | |||||
Underscore Expr Source # | |||||
Defined in Agda.Syntax.Abstract underscore :: Expr Source # isUnderscore :: Expr -> Bool Source # | |||||
HasRange Expr Source # | |||||
KillRange Expr Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
ToConcrete Expr Source # | |||||
ToConcrete LHSCore Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
| |||||
ToConcrete Pattern Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
| |||||
Reify Expr Source # | |||||
PrettyTCM Expr Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM Pattern Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
IsFlexiblePattern Pattern Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern -> m Bool Source # | |||||
NFData Expr Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
Generic Expr Source # | |||||
Defined in Agda.Syntax.Abstract
| |||||
Show Expr Source # | |||||
Eq Expr Source # | Does not compare | ||||
PatternToExpr Pattern Expr Source # | |||||
PrettyTCM (Arg Expr) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (NamedArg Expr) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
ToAbstract (Expr, Elim) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract
toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m (AbsOfRef (Expr, Elim)) Source # | |||||
ToAbstract (Expr, Elims) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract
toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m (AbsOfRef (Expr, Elims)) Source # | |||||
ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source # | |||||
type ConOfAbs Expr Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type ConOfAbs LHSCore Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type ConOfAbs Pattern Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type ReifiesTo Expr Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type Rep Expr Source # | |||||
Defined in Agda.Syntax.Abstract type Rep Expr = D1 ('MetaData "Expr" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) ((((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "Def'" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Suffix)) :+: C1 ('MetaCons "Proj" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)))) :+: (C1 ('MetaCons "Con" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: (C1 ('MetaCons "PatternSyn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: C1 ('MetaCons "Macro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: ((C1 ('MetaCons "Lit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: (C1 ('MetaCons "QuestionMark" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InteractionId)) :+: C1 ('MetaCons "Underscore" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaInfo)))) :+: ((C1 ('MetaCons "Dot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "App" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AppInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Expr))))) :+: (C1 ('MetaCons "WithApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr]))) :+: C1 ('MetaCons "Lam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LamBinding) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))))) :+: (((C1 ('MetaCons "AbsurdLam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Hiding)) :+: (C1 ('MetaCons "ExtendedLam" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Clause))))) :+: C1 ('MetaCons "Pi" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope1) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))) :+: (C1 ('MetaCons "Generalized" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set QName)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: (C1 ('MetaCons "Fun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: C1 ('MetaCons "Let" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 LetBinding)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))) :+: ((C1 ('MetaCons "Rec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordAssigns)) :+: (C1 ('MetaCons "RecUpdate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Assigns))) :+: C1 ('MetaCons "ScopedExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: ((C1 ('MetaCons "Quote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo)) :+: C1 ('MetaCons "QuoteTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo))) :+: (C1 ('MetaCons "Unquote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo)) :+: C1 ('MetaCons "DontCare" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))))) | |||||
type AbsOfRef (Expr, Elim) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |||||
type AbsOfRef (Expr, Elims) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |||||
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
Types are just expressions. Use this type synonym for hinting that an expression should be a type.
type Telescope = [TypedBinding] Source #
data Declaration Source #
Instances
AnyAbstract Declaration Source # | |||||
Defined in Agda.Syntax.Abstract anyAbstract :: Declaration -> Bool Source # | |||||
DeclaredNames Declaration Source # | |||||
Defined in Agda.Syntax.Abstract.Views declaredNames :: Collection KName m => Declaration -> m Source # | |||||
ExprLike Declaration Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m Declaration Source # foldExpr :: FoldExprFn m Declaration Source # traverseExpr :: TraverseExprFn m Declaration Source # mapExpr :: (Expr -> Expr) -> Declaration -> Declaration Source # | |||||
HasRange Declaration Source # | |||||
Defined in Agda.Syntax.Abstract getRange :: Declaration -> Range Source # | |||||
KillRange Declaration Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
ToConcrete Declaration Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
toConcrete :: Declaration -> AbsToCon (ConOfAbs Declaration) Source # bindToConcrete :: Declaration -> (ConOfAbs Declaration -> AbsToCon b) -> AbsToCon b Source # | |||||
ShowHead Declaration Source # | |||||
Defined in Agda.TypeChecking.Rules.Decl showHead :: Declaration -> String Source # | |||||
NFData Declaration Source # | |||||
Defined in Agda.Syntax.Abstract rnf :: Declaration -> () | |||||
Generic Declaration Source # | |||||
Defined in Agda.Syntax.Abstract
from :: Declaration -> Rep Declaration x to :: Rep Declaration x -> Declaration | |||||
Show Declaration Source # | |||||
Defined in Agda.Syntax.Abstract showsPrec :: Int -> Declaration -> ShowS show :: Declaration -> String showList :: [Declaration] -> ShowS | |||||
Eq Declaration Source # | Does not compare | ||||
Defined in Agda.Syntax.Abstract (==) :: Declaration -> Declaration -> Bool (/=) :: Declaration -> Declaration -> Bool | |||||
ToConcrete (Constr Constructor) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
toConcrete :: Constr Constructor -> AbsToCon (ConOfAbs (Constr Constructor)) Source # bindToConcrete :: Constr Constructor -> (ConOfAbs (Constr Constructor) -> AbsToCon b) -> AbsToCon b Source # | |||||
type ConOfAbs Declaration Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type Rep Declaration Source # | |||||
Defined in Agda.Syntax.Abstract type Rep Declaration = D1 ('MetaData "Declaration" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) ((((C1 ('MetaCons "Axiom" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [Occurrence])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: C1 ('MetaCons "Generalize" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set QName)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))) :+: (C1 ('MetaCons "Field" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Type)))) :+: (C1 ('MetaCons "Primitive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Type)))) :+: C1 ('MetaCons "Mutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MutualInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration]))))) :+: ((C1 ('MetaCons "Section" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))) :+: C1 ('MetaCons "Apply" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeCopyInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))))) :+: (C1 ('MetaCons "Import" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: (C1 ('MetaCons "Pragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pragma)) :+: C1 ('MetaCons "Open" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))))))) :+: (((C1 ('MetaCons "FunDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause]))) :+: C1 ('MetaCons "DataSig" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))) :+: (C1 ('MetaCons "DataDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataDefParams) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Constructor])))) :+: (C1 ('MetaCons "RecSig" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: C1 ('MetaCons "RecDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordDirectives) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataDefParams)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration]))))))) :+: ((C1 ('MetaCons "PatternSynDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [WithHiding BindName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' Void)))) :+: (C1 ('MetaCons "UnquoteDecl" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MutualInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "UnquoteDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: (C1 ('MetaCons "UnquoteData" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "ScopedDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])) :+: C1 ('MetaCons "UnfoldingDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]))))))) | |||||
type ConOfAbs (Constr Constructor) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete |
type Assign = FieldAssignment' Expr Source #
Record field assignment f = e
.
type Constructor = TypeSignature Source #
The lhs of a clause in focused (projection-application) view (outside-in).
Projection patters are represented as LHSProj
s.
Instances
DeclaredNames Clause Source # | |||||
Defined in Agda.Syntax.Abstract.Views declaredNames :: Collection KName m => Clause -> m Source # | |||||
ExprLike LHS Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m LHS Source # foldExpr :: FoldExprFn m LHS Source # traverseExpr :: TraverseExprFn m LHS Source # | |||||
HasRange LHS Source # | |||||
KillRange LHS Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
ToConcrete LHS Source # | |||||
NFData LHS Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
Generic LHS Source # | |||||
Defined in Agda.Syntax.Abstract
| |||||
Show LHS Source # | |||||
Eq LHS Source # | |||||
LHSToSpine Clause SpineClause Source # | Clause instance. | ||||
Defined in Agda.Syntax.Abstract.Pattern lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source # | |||||
LHSToSpine LHS SpineLHS Source # | LHS instance. | ||||
Defined in Agda.Syntax.Abstract.Pattern lhsToSpine :: LHS -> SpineLHS Source # spineToLhs :: SpineLHS -> LHS Source # | |||||
type ConOfAbs LHS Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type Rep LHS Source # | |||||
Defined in Agda.Syntax.Abstract type Rep LHS = D1 ('MetaData "LHS" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "LHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :*: S1 ('MetaSel ('Just "lhsCore") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSCore))) |
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 | |
InjectiveForInferencePragma QName | |
InlinePragma Bool QName | |
NotProjectionLikePragma QName | Mark the definition as not being projection-like |
OverlapPragma QName OverlapMode | If the definition is an instance, set its overlap mode. |
DisplayPragma QName [NamedArg Pattern] Expr |
Instances
DeclaredNames Pragma Source # | |||||
Defined in Agda.Syntax.Abstract.Views declaredNames :: Collection KName m => Pragma -> m Source # | |||||
ExprLike Pragma Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m Pragma Source # foldExpr :: FoldExprFn m Pragma Source # | |||||
NFData Pragma Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
Generic Pragma Source # | |||||
Defined in Agda.Syntax.Abstract
| |||||
Show Pragma Source # | |||||
Eq Pragma Source # | |||||
type Rep Pragma Source # | |||||
Defined in Agda.Syntax.Abstract type Rep Pragma = D1 ('MetaData "Pragma" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (((C1 ('MetaCons "OptionsPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :+: (C1 ('MetaCons "BuiltinPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ResolvedName)) :+: C1 ('MetaCons "BuiltinNoDefPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: (C1 ('MetaCons "RewritePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName])) :+: (C1 ('MetaCons "CompilePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: C1 ('MetaCons "StaticPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: ((C1 ('MetaCons "EtaPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "InjectivePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "InjectiveForInferencePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)))) :+: ((C1 ('MetaCons "InlinePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "NotProjectionLikePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "OverlapPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OverlapMode)) :+: C1 ('MetaCons "DisplayPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Pattern]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))))) |
type TacticAttribute = TacticAttribute' Expr 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 | |
|
Instances
DeclaredNames Clause Source # | |||||
Defined in Agda.Syntax.Abstract.Views declaredNames :: Collection KName m => Clause -> m Source # | |||||
Functor Clause' Source # | |||||
Foldable Clause' Source # | |||||
Defined in Agda.Syntax.Abstract fold :: Monoid m => Clause' m -> m foldMap :: Monoid m => (a -> m) -> Clause' a -> m foldMap' :: Monoid m => (a -> m) -> Clause' a -> m foldr :: (a -> b -> b) -> b -> Clause' a -> b foldr' :: (a -> b -> b) -> b -> Clause' a -> b foldl :: (b -> a -> b) -> b -> Clause' a -> b foldl' :: (b -> a -> b) -> b -> Clause' a -> b foldr1 :: (a -> a -> a) -> Clause' a -> a foldl1 :: (a -> a -> a) -> Clause' a -> a elem :: Eq a => a -> Clause' a -> Bool maximum :: Ord a => Clause' a -> a minimum :: Ord a => Clause' a -> a | |||||
Traversable Clause' Source # | |||||
LHSToSpine Clause SpineClause Source # | Clause instance. | ||||
Defined in Agda.Syntax.Abstract.Pattern lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source # | |||||
ExprLike a => ExprLike (Clause' a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m (Clause' a) Source # foldExpr :: FoldExprFn m (Clause' a) Source # traverseExpr :: TraverseExprFn m (Clause' a) Source # mapExpr :: (Expr -> Expr) -> Clause' a -> Clause' a Source # | |||||
HasRange a => HasRange (Clause' a) Source # | |||||
KillRange a => KillRange (Clause' a) Source # | |||||
Defined in Agda.Syntax.Abstract killRange :: KillRangeT (Clause' a) Source # | |||||
(ToConcrete a, ConOfAbs a ~ LHS) => ToConcrete (Clause' a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
| |||||
NFData lhs => NFData (Clause' lhs) Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
Generic (Clause' lhs) Source # | |||||
Defined in Agda.Syntax.Abstract
| |||||
Show lhs => Show (Clause' lhs) Source # | |||||
Eq lhs => Eq (Clause' lhs) Source # | |||||
type ConOfAbs (Clause' a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type Rep (Clause' lhs) Source # | |||||
Defined in Agda.Syntax.Abstract type Rep (Clause' lhs) = D1 ('MetaData "Clause'" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'True) ((S1 ('MetaSel ('Just "clauseLHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 lhs) :*: S1 ('MetaSel ('Just "clauseStrippedPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProblemEq])) :*: (S1 ('MetaSel ('Just "clauseRHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :*: (S1 ('MetaSel ('Just "clauseWhereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereDeclarations) :*: S1 ('MetaSel ('Just "clauseCatchall") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))) |
Binder | |
|
Instances
Functor Binder' Source # | |||||
Foldable Binder' Source # | |||||
Defined in Agda.Syntax.Abstract fold :: Monoid m => Binder' m -> m foldMap :: Monoid m => (a -> m) -> Binder' a -> m foldMap' :: Monoid m => (a -> m) -> Binder' a -> m foldr :: (a -> b -> b) -> b -> Binder' a -> b foldr' :: (a -> b -> b) -> b -> Binder' a -> b foldl :: (b -> a -> b) -> b -> Binder' a -> b foldl' :: (b -> a -> b) -> b -> Binder' a -> b foldr1 :: (a -> a -> a) -> Binder' a -> a foldl1 :: (a -> a -> a) -> Binder' a -> a elem :: Eq a => a -> Binder' a -> Bool maximum :: Ord a => Binder' a -> a minimum :: Ord a => Binder' a -> a | |||||
Traversable Binder' Source # | |||||
HasRange a => HasRange (Binder' a) Source # | |||||
KillRange a => KillRange (Binder' a) Source # | |||||
Defined in Agda.Syntax.Abstract killRange :: KillRangeT (Binder' a) Source # | |||||
ToConcrete a => ToConcrete (Binder' a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
| |||||
NFData a => NFData (Binder' a) Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
Generic (Binder' a) Source # | |||||
Defined in Agda.Syntax.Abstract
| |||||
Show a => Show (Binder' a) Source # | |||||
Eq a => Eq (Binder' a) Source # | |||||
type ConOfAbs (Binder' a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type Rep (Binder' a) Source # | |||||
Defined in Agda.Syntax.Abstract type Rep (Binder' a) = D1 ('MetaData "Binder'" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Binder" 'PrefixI 'True) (S1 ('MetaSel ('Just "binderPattern") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Pattern)) :*: S1 ('MetaSel ('Just "binderName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))) |
data LamBinding Source #
A lambda binding is either domain free or typed.
DomainFree TacticAttribute (NamedArg Binder) | . |
DomainFull TypedBinding | . |
Instances
ExprLike LamBinding Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m LamBinding Source # foldExpr :: FoldExprFn m LamBinding Source # traverseExpr :: TraverseExprFn m LamBinding Source # mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source # | |||||
LensHiding LamBinding Source # | |||||
Defined in Agda.Syntax.Abstract getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source # | |||||
HasRange LamBinding Source # | |||||
Defined in Agda.Syntax.Abstract getRange :: LamBinding -> Range Source # | |||||
KillRange LamBinding Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
ToConcrete LamBinding Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
toConcrete :: LamBinding -> AbsToCon (ConOfAbs LamBinding) Source # bindToConcrete :: LamBinding -> (ConOfAbs LamBinding -> AbsToCon b) -> AbsToCon b Source # | |||||
NFData LamBinding Source # | |||||
Defined in Agda.Syntax.Abstract rnf :: LamBinding -> () | |||||
Generic LamBinding Source # | |||||
Defined in Agda.Syntax.Abstract
from :: LamBinding -> Rep LamBinding x to :: Rep LamBinding x -> LamBinding | |||||
Show LamBinding Source # | |||||
Defined in Agda.Syntax.Abstract showsPrec :: Int -> LamBinding -> ShowS show :: LamBinding -> String showList :: [LamBinding] -> ShowS | |||||
Eq LamBinding Source # | |||||
Defined in Agda.Syntax.Abstract (==) :: LamBinding -> LamBinding -> Bool (/=) :: LamBinding -> LamBinding -> Bool | |||||
type ConOfAbs LamBinding Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type Rep LamBinding Source # | |||||
Defined in Agda.Syntax.Abstract type Rep LamBinding = D1 ('MetaData "LamBinding" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "DomainFree" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttribute) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Binder))) :+: C1 ('MetaCons "DomainFull" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypedBinding))) |
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
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.
TBind Range TypedBindingInfo (List1 (NamedArg Binder)) Type | As in telescope |
TLet Range (List1 LetBinding) | E.g. |
Instances
ExprLike TypedBinding Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m TypedBinding Source # foldExpr :: FoldExprFn m TypedBinding Source # traverseExpr :: TraverseExprFn m TypedBinding Source # mapExpr :: (Expr -> Expr) -> TypedBinding -> TypedBinding Source # | |||||
LensHiding TypedBinding Source # | |||||
Defined in Agda.Syntax.Abstract getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source # | |||||
HasRange TypedBinding Source # | |||||
Defined in Agda.Syntax.Abstract getRange :: TypedBinding -> Range Source # | |||||
KillRange TypedBinding Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
ToConcrete TypedBinding Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
toConcrete :: TypedBinding -> AbsToCon (ConOfAbs TypedBinding) Source # bindToConcrete :: TypedBinding -> (ConOfAbs TypedBinding -> AbsToCon b) -> AbsToCon b Source # | |||||
PrettyTCM TypedBinding Source # | |||||
Defined in Agda.TypeChecking.Pretty prettyTCM :: MonadPretty m => TypedBinding -> m Doc Source # | |||||
NFData TypedBinding Source # | |||||
Defined in Agda.Syntax.Abstract rnf :: TypedBinding -> () | |||||
Generic TypedBinding Source # | |||||
Defined in Agda.Syntax.Abstract
from :: TypedBinding -> Rep TypedBinding x to :: Rep TypedBinding x -> TypedBinding | |||||
Show TypedBinding Source # | |||||
Defined in Agda.Syntax.Abstract showsPrec :: Int -> TypedBinding -> ShowS show :: TypedBinding -> String showList :: [TypedBinding] -> ShowS | |||||
Eq TypedBinding Source # | |||||
Defined in Agda.Syntax.Abstract (==) :: TypedBinding -> TypedBinding -> Bool (/=) :: TypedBinding -> TypedBinding -> Bool | |||||
type ConOfAbs TypedBinding Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type Rep TypedBinding Source # | |||||
Defined in Agda.Syntax.Abstract type Rep TypedBinding = D1 ('MetaData "TypedBinding" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "TBind" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypedBindingInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (NamedArg Binder))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: C1 ('MetaCons "TLet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 LetBinding)))) |
type Telescope1 = List1 TypedBinding Source #
mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding Source #
data ModuleApplication Source #
SectionApp Telescope ModuleName [NamedArg Expr] |
|
RecordModuleInstance ModuleName | M {{...}} |
Instances
ExprLike ModuleApplication Source # | |||||
Defined in Agda.Syntax.Abstract.Views | |||||
KillRange ModuleApplication Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
ToConcrete ModuleApplication Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
toConcrete :: ModuleApplication -> AbsToCon (ConOfAbs ModuleApplication) Source # bindToConcrete :: ModuleApplication -> (ConOfAbs ModuleApplication -> AbsToCon b) -> AbsToCon b Source # | |||||
NFData ModuleApplication Source # | |||||
Defined in Agda.Syntax.Abstract rnf :: ModuleApplication -> () | |||||
Generic ModuleApplication Source # | |||||
Defined in Agda.Syntax.Abstract
from :: ModuleApplication -> Rep ModuleApplication x to :: Rep ModuleApplication x -> ModuleApplication | |||||
Show ModuleApplication Source # | |||||
Defined in Agda.Syntax.Abstract showsPrec :: Int -> ModuleApplication -> ShowS show :: ModuleApplication -> String showList :: [ModuleApplication] -> ShowS | |||||
Eq ModuleApplication Source # | |||||
Defined in Agda.Syntax.Abstract (==) :: ModuleApplication -> ModuleApplication -> Bool (/=) :: ModuleApplication -> ModuleApplication -> Bool | |||||
type ConOfAbs ModuleApplication Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type Rep ModuleApplication Source # | |||||
Defined in Agda.Syntax.Abstract type Rep ModuleApplication = D1 ('MetaData "ModuleApplication" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "SectionApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Expr]))) :+: C1 ('MetaCons "RecordModuleInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName))) |
type TypeSignature = Declaration Source #
Only Axiom
s.
type ImportedName = ImportedName' QName ModuleName Source #
type RewriteEqn = RewriteEqn' QName BindName Pattern Expr Source #
RHS | |
AbsurdRHS | |
WithRHS QName [WithExpr] (List1 Clause) | The |
RewriteRHS | |
|
Instances
DeclaredNames RHS Source # | |||||
Defined in Agda.Syntax.Abstract.Views declaredNames :: Collection KName m => RHS -> m Source # | |||||
ExprLike RHS Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m RHS Source # foldExpr :: FoldExprFn m RHS Source # traverseExpr :: TraverseExprFn m RHS Source # | |||||
HasRange RHS Source # | |||||
KillRange RHS Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
ToConcrete RHS Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
| |||||
NFData RHS Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
Generic RHS Source # | |||||
Defined in Agda.Syntax.Abstract
| |||||
Show RHS Source # | |||||
Eq RHS Source # | Ignore | ||||
type ConOfAbs RHS Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type Rep RHS Source # | |||||
Defined in Agda.Syntax.Abstract type Rep RHS = D1 ('MetaData "RHS" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) ((C1 ('MetaCons "RHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "rhsExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Just "rhsConcrete") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Expr))) :+: C1 ('MetaCons "AbsurdRHS" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WithRHS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [WithExpr]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Clause)))) :+: C1 ('MetaCons "RewriteRHS" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rewriteExprs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [RewriteEqn]) :*: S1 ('MetaSel ('Just "rewriteStrippedPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProblemEq])) :*: (S1 ('MetaSel ('Just "rewriteRHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :*: S1 ('MetaSel ('Just "rewriteWhereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereDeclarations))))) |
type HoleContent = HoleContent' () BindName Pattern Expr Source #
data ScopeCopyInfo Source #
Instances
Pretty ScopeCopyInfo Source # | |||||
Defined in Agda.Syntax.Abstract pretty :: ScopeCopyInfo -> Doc Source # prettyPrec :: Int -> ScopeCopyInfo -> Doc Source # prettyList :: [ScopeCopyInfo] -> Doc Source # | |||||
KillRange ScopeCopyInfo Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
NFData ScopeCopyInfo Source # | |||||
Defined in Agda.Syntax.Abstract rnf :: ScopeCopyInfo -> () | |||||
Generic ScopeCopyInfo Source # | |||||
Defined in Agda.Syntax.Abstract
from :: ScopeCopyInfo -> Rep ScopeCopyInfo x to :: Rep ScopeCopyInfo x -> ScopeCopyInfo | |||||
Show ScopeCopyInfo Source # | |||||
Defined in Agda.Syntax.Abstract showsPrec :: Int -> ScopeCopyInfo -> ShowS show :: ScopeCopyInfo -> String showList :: [ScopeCopyInfo] -> ShowS | |||||
Eq ScopeCopyInfo Source # | |||||
Defined in Agda.Syntax.Abstract (==) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool (/=) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool | |||||
type Rep ScopeCopyInfo Source # | |||||
Defined in Agda.Syntax.Abstract type Rep ScopeCopyInfo = D1 ('MetaData "ScopeCopyInfo" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "ScopeCopyInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "renModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Ren ModuleName)) :*: S1 ('MetaSel ('Just "renNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Ren QName)))) |
type PatternSynDefn = ([WithHiding Name], Pattern' Void) Source #
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.
ProblemEq | |
|
Instances
KillRange ProblemEq Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
PrettyTCM ProblemEq Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS.Problem | |||||
Subst ProblemEq Source # | |||||
Defined in Agda.TypeChecking.Substitute applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq Source # | |||||
NFData ProblemEq Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
Generic ProblemEq Source # | |||||
Defined in Agda.Syntax.Abstract
| |||||
Show ProblemEq Source # | |||||
Eq ProblemEq Source # | |||||
type SubstArg ProblemEq Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
type Rep ProblemEq Source # | |||||
Defined in Agda.Syntax.Abstract type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "ProblemEq" 'PrefixI 'True) (S1 ('MetaSel ('Just "problemInPat") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :*: (S1 ('MetaSel ('Just "problemInst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Just "problemType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type))))) |
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.
TypedBindingInfo | |
|
Instances
ExprLike TypedBindingInfo Source # | |||||
Defined in Agda.Syntax.Abstract.Views | |||||
KillRange TypedBindingInfo Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
Null TypedBindingInfo Source # | |||||
Defined in Agda.Syntax.Abstract empty :: TypedBindingInfo Source # null :: TypedBindingInfo -> Bool Source # | |||||
NFData TypedBindingInfo Source # | |||||
Defined in Agda.Syntax.Abstract rnf :: TypedBindingInfo -> () | |||||
Generic TypedBindingInfo Source # | |||||
Defined in Agda.Syntax.Abstract
from :: TypedBindingInfo -> Rep TypedBindingInfo x to :: Rep TypedBindingInfo x -> TypedBindingInfo | |||||
Show TypedBindingInfo Source # | |||||
Defined in Agda.Syntax.Abstract showsPrec :: Int -> TypedBindingInfo -> ShowS show :: TypedBindingInfo -> String showList :: [TypedBindingInfo] -> ShowS | |||||
Eq TypedBindingInfo Source # | |||||
Defined in Agda.Syntax.Abstract (==) :: TypedBindingInfo -> TypedBindingInfo -> Bool (/=) :: TypedBindingInfo -> TypedBindingInfo -> Bool | |||||
type Rep TypedBindingInfo Source # | |||||
Defined in Agda.Syntax.Abstract type Rep TypedBindingInfo = D1 ('MetaData "TypedBindingInfo" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "TypedBindingInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "tbTacticAttr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttribute) :*: S1 ('MetaSel ('Just "tbFinite") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) |
Parameterised over the type of dot patterns.
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 ConPatInfo [FieldAssignment' (Pattern' e)] | |
EqualP PatInfo [(e, e)] | |
WithP PatInfo (Pattern' e) |
|
AnnP PatInfo e (Pattern' e) | Pattern with type annotation |
Instances
MapNamedArgPattern NAP Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
ToConcrete Pattern Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
| |||||
PrettyTCM Pattern Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
IsFlexiblePattern Pattern Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern -> m Bool Source # | |||||
Functor Pattern' Source # | |||||
Foldable Pattern' Source # | |||||
Defined in Agda.Syntax.Abstract fold :: Monoid m => Pattern' m -> m foldMap :: Monoid m => (a -> m) -> Pattern' a -> m foldMap' :: Monoid m => (a -> m) -> Pattern' a -> m foldr :: (a -> b -> b) -> b -> Pattern' a -> b foldr' :: (a -> b -> b) -> b -> Pattern' a -> b foldl :: (b -> a -> b) -> b -> Pattern' a -> b foldl' :: (b -> a -> b) -> b -> Pattern' a -> b foldr1 :: (a -> a -> a) -> Pattern' a -> a foldl1 :: (a -> a -> a) -> Pattern' a -> a elem :: Eq a => a -> Pattern' a -> Bool maximum :: Ord a => Pattern' a -> a minimum :: Ord a => Pattern' a -> a | |||||
Traversable Pattern' Source # | |||||
PatternToExpr Pattern Expr Source # | |||||
IsProjP (Pattern' e) Source # | |||||
Defined in Agda.Syntax.Abstract isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) Source # | |||||
APatternLike (Pattern' a) Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern
foldrAPattern :: Monoid m => (Pattern' (ADotT (Pattern' a)) -> m -> m) -> Pattern' a -> m Source # traverseAPatternM :: Monad m => (Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))) -> (Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))) -> Pattern' a -> m (Pattern' a) Source # | |||||
ExprLike a => ExprLike (Pattern' a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m (Pattern' a) Source # foldExpr :: FoldExprFn m (Pattern' a) Source # traverseExpr :: TraverseExprFn m (Pattern' a) Source # mapExpr :: (Expr -> Expr) -> Pattern' a -> Pattern' a Source # | |||||
IsWithP (Pattern' e) Source # | Check for with-pattern. | ||||
NamesIn (Pattern' a) Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
HasRange (Pattern' e) Source # | |||||
KillRange e => KillRange (Pattern' e) Source # | |||||
Defined in Agda.Syntax.Abstract killRange :: KillRangeT (Pattern' e) Source # | |||||
SetRange (Pattern' a) Source # | |||||
ToAbstract (Pattern' Expr) Source # | |||||
ExpandPatternSynonyms (Pattern' e) Source # | |||||
Defined in Agda.TypeChecking.Patterns.Abstract | |||||
EmbPrj a => EmbPrj (Pattern' a) Source # | |||||
NFData e => NFData (Pattern' e) Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
Generic (Pattern' e) Source # | |||||
Defined in Agda.Syntax.Abstract
| |||||
Show e => Show (Pattern' e) Source # | |||||
Eq e => Eq (Pattern' e) Source # | |||||
ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source # | |||||
type ConOfAbs Pattern Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type ADotT (Pattern' a) Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
type AbsOfCon (Pattern' Expr) Source # | |||||
type Rep (Pattern' e) Source # | |||||
Defined in Agda.Syntax.Abstract type Rep (Pattern' e) = D1 ('MetaData "Pattern'" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (((C1 ('MetaCons "VarP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName)) :+: (C1 ('MetaCons "ConP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: C1 ('MetaCons "ProjP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName))))) :+: ((C1 ('MetaCons "DefP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: C1 ('MetaCons "WildP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo))) :+: (C1 ('MetaCons "AsP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e)))) :+: C1 ('MetaCons "DotP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e))))) :+: ((C1 ('MetaCons "AbsurdP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo)) :+: (C1 ('MetaCons "LitP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "PatternSynP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))))) :+: ((C1 ('MetaCons "RecP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FieldAssignment' (Pattern' e)])) :+: C1 ('MetaCons "EqualP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(e, e)]))) :+: (C1 ('MetaCons "WithP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e))) :+: C1 ('MetaCons "AnnP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e)))))))) | |||||
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
type Field = TypeSignature Source #
The lhs in projection-application and with-pattern view.
Parameterised over the type e
of dot patterns.
LHSHead | The head applied to ordinary patterns. |
| |
LHSProj | Projection. |
| |
LHSWith | With patterns. |
Instances
ToConcrete LHSCore Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
| |||||
Functor LHSCore' Source # | |||||
Foldable LHSCore' Source # | |||||
Defined in Agda.Syntax.Abstract fold :: Monoid m => LHSCore' m -> m foldMap :: Monoid m => (a -> m) -> LHSCore' a -> m foldMap' :: Monoid m => (a -> m) -> LHSCore' a -> m foldr :: (a -> b -> b) -> b -> LHSCore' a -> b foldr' :: (a -> b -> b) -> b -> LHSCore' a -> b foldl :: (b -> a -> b) -> b -> LHSCore' a -> b foldl' :: (b -> a -> b) -> b -> LHSCore' a -> b foldr1 :: (a -> a -> a) -> LHSCore' a -> a foldl1 :: (a -> a -> a) -> LHSCore' a -> a elem :: Eq a => a -> LHSCore' a -> Bool maximum :: Ord a => LHSCore' a -> a minimum :: Ord a => LHSCore' a -> a | |||||
Traversable LHSCore' Source # | |||||
ExprLike a => ExprLike (LHSCore' a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m (LHSCore' a) Source # foldExpr :: FoldExprFn m (LHSCore' a) Source # traverseExpr :: TraverseExprFn m (LHSCore' a) Source # mapExpr :: (Expr -> Expr) -> LHSCore' a -> LHSCore' a Source # | |||||
HasRange (LHSCore' e) Source # | |||||
KillRange e => KillRange (LHSCore' e) Source # | |||||
Defined in Agda.Syntax.Abstract killRange :: KillRangeT (LHSCore' e) Source # | |||||
ToAbstract (LHSCore' Expr) Source # | |||||
NFData e => NFData (LHSCore' e) Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
Generic (LHSCore' e) Source # | |||||
Defined in Agda.Syntax.Abstract
| |||||
Show e => Show (LHSCore' e) Source # | |||||
Eq e => Eq (LHSCore' e) Source # | |||||
type ConOfAbs LHSCore Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type AbsOfCon (LHSCore' Expr) Source # | |||||
type Rep (LHSCore' e) Source # | |||||
Defined in Agda.Syntax.Abstract type Rep (LHSCore' e) = D1 ('MetaData "LHSCore'" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "LHSHead" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsDefName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)])) :+: (C1 ('MetaCons "LHSProj" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsDestructor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: (S1 ('MetaSel ('Just "lhsFocus") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg (LHSCore' e))) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)]))) :+: C1 ('MetaCons "LHSWith" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsHead") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (LHSCore' e)) :*: (S1 ('MetaSel ('Just "lhsWithPatterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg (Pattern' e)]) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)]))))) |
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
mkBindName :: Name -> BindName Source #
data LetBinding Source #
Bindings that are valid in a let
.
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
ExprLike LetBinding Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m LetBinding Source # foldExpr :: FoldExprFn m LetBinding Source # traverseExpr :: TraverseExprFn m LetBinding Source # mapExpr :: (Expr -> Expr) -> LetBinding -> LetBinding Source # | |||||
HasRange LetBinding Source # | |||||
Defined in Agda.Syntax.Abstract getRange :: LetBinding -> Range Source # | |||||
KillRange LetBinding Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
ToConcrete LetBinding Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
toConcrete :: LetBinding -> AbsToCon (ConOfAbs LetBinding) Source # bindToConcrete :: LetBinding -> (ConOfAbs LetBinding -> AbsToCon b) -> AbsToCon b Source # | |||||
NFData LetBinding Source # | |||||
Defined in Agda.Syntax.Abstract rnf :: LetBinding -> () | |||||
Generic LetBinding Source # | |||||
Defined in Agda.Syntax.Abstract
from :: LetBinding -> Rep LetBinding x to :: Rep LetBinding x -> LetBinding | |||||
Show LetBinding Source # | |||||
Defined in Agda.Syntax.Abstract showsPrec :: Int -> LetBinding -> ShowS show :: LetBinding -> String showList :: [LetBinding] -> ShowS | |||||
Eq LetBinding Source # | |||||
Defined in Agda.Syntax.Abstract (==) :: LetBinding -> LetBinding -> Bool (/=) :: LetBinding -> LetBinding -> Bool | |||||
type ConOfAbs LetBinding Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type Rep LetBinding Source # | |||||
Defined in Agda.Syntax.Abstract type Rep LetBinding = D1 ('MetaData "LetBinding" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) ((C1 ('MetaCons "LetBind" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "LetPatBind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "LetApply" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeCopyInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: (C1 ('MetaCons "LetOpen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: C1 ('MetaCons "LetDeclaredVariable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName))))) |
type RecordAssigns = [RecordAssign] Source #
generalized :: Set QName -> Type -> Type Source #
Smart constructor for Generalized
.
type RecordAssign = Either Assign ModuleName Source #
data GeneralizeTelescope Source #
GeneralizeTel | |
|
Instances
ExprLike GeneralizeTelescope Source # | |||||
Defined in Agda.Syntax.Abstract.Views | |||||
KillRange GeneralizeTelescope Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
NFData GeneralizeTelescope Source # | |||||
Defined in Agda.Syntax.Abstract rnf :: GeneralizeTelescope -> () | |||||
Generic GeneralizeTelescope Source # | |||||
Defined in Agda.Syntax.Abstract
from :: GeneralizeTelescope -> Rep GeneralizeTelescope x to :: Rep GeneralizeTelescope x -> GeneralizeTelescope | |||||
Show GeneralizeTelescope Source # | |||||
Defined in Agda.Syntax.Abstract showsPrec :: Int -> GeneralizeTelescope -> ShowS show :: GeneralizeTelescope -> String showList :: [GeneralizeTelescope] -> ShowS | |||||
Eq GeneralizeTelescope Source # | |||||
Defined in Agda.Syntax.Abstract (==) :: GeneralizeTelescope -> GeneralizeTelescope -> Bool (/=) :: GeneralizeTelescope -> GeneralizeTelescope -> Bool | |||||
type Rep GeneralizeTelescope Source # | |||||
Defined in Agda.Syntax.Abstract type Rep GeneralizeTelescope = D1 ('MetaData "GeneralizeTelescope" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "GeneralizeTel" 'PrefixI 'True) (S1 ('MetaSel ('Just "generalizeTelVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName Name)) :*: S1 ('MetaSel ('Just "generalizeTel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope))) |
data DataDefParams Source #
DataDefParams | |
|
Instances
ExprLike DataDefParams Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m DataDefParams Source # foldExpr :: FoldExprFn m DataDefParams Source # traverseExpr :: TraverseExprFn m DataDefParams Source # mapExpr :: (Expr -> Expr) -> DataDefParams -> DataDefParams Source # | |||||
KillRange DataDefParams Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
NFData DataDefParams Source # | |||||
Defined in Agda.Syntax.Abstract rnf :: DataDefParams -> () | |||||
Generic DataDefParams Source # | |||||
Defined in Agda.Syntax.Abstract
from :: DataDefParams -> Rep DataDefParams x to :: Rep DataDefParams x -> DataDefParams | |||||
Show DataDefParams Source # | |||||
Defined in Agda.Syntax.Abstract showsPrec :: Int -> DataDefParams -> ShowS show :: DataDefParams -> String showList :: [DataDefParams] -> ShowS | |||||
Eq DataDefParams Source # | |||||
Defined in Agda.Syntax.Abstract (==) :: DataDefParams -> DataDefParams -> Bool (/=) :: DataDefParams -> DataDefParams -> Bool | |||||
type Rep DataDefParams Source # | |||||
Defined in Agda.Syntax.Abstract type Rep DataDefParams = D1 ('MetaData "DataDefParams" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "DataDefParams" 'PrefixI 'True) (S1 ('MetaSel ('Just "dataDefGeneralizedParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Name)) :*: S1 ('MetaSel ('Just "dataDefParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding]))) |
mkDomainFree :: NamedArg Binder -> LamBinding Source #
data WhereDeclarations Source #
WhereDecls | |
|
Instances
DeclaredNames WhereDeclarations Source # | |||||
Defined in Agda.Syntax.Abstract.Views declaredNames :: Collection KName m => WhereDeclarations -> m Source # | |||||
ExprLike WhereDeclarations Source # | |||||
Defined in Agda.Syntax.Abstract.Views | |||||
HasRange WhereDeclarations Source # | |||||
Defined in Agda.Syntax.Abstract getRange :: WhereDeclarations -> Range Source # | |||||
KillRange WhereDeclarations Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
ToConcrete WhereDeclarations Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
toConcrete :: WhereDeclarations -> AbsToCon (ConOfAbs WhereDeclarations) Source # bindToConcrete :: WhereDeclarations -> (ConOfAbs WhereDeclarations -> AbsToCon b) -> AbsToCon b Source # | |||||
Null WhereDeclarations Source # | |||||
Defined in Agda.Syntax.Abstract empty :: WhereDeclarations Source # null :: WhereDeclarations -> Bool Source # | |||||
NFData WhereDeclarations Source # | |||||
Defined in Agda.Syntax.Abstract rnf :: WhereDeclarations -> () | |||||
Generic WhereDeclarations Source # | |||||
Defined in Agda.Syntax.Abstract
from :: WhereDeclarations -> Rep WhereDeclarations x to :: Rep WhereDeclarations x -> WhereDeclarations | |||||
Show WhereDeclarations Source # | |||||
Defined in Agda.Syntax.Abstract showsPrec :: Int -> WhereDeclarations -> ShowS show :: WhereDeclarations -> String showList :: [WhereDeclarations] -> ShowS | |||||
Eq WhereDeclarations Source # | |||||
Defined in Agda.Syntax.Abstract (==) :: WhereDeclarations -> WhereDeclarations -> Bool (/=) :: WhereDeclarations -> WhereDeclarations -> Bool | |||||
type ConOfAbs WhereDeclarations Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type Rep WhereDeclarations Source # | |||||
Defined in Agda.Syntax.Abstract type Rep WhereDeclarations = D1 ('MetaData "WhereDeclarations" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "WhereDecls" 'PrefixI 'True) (S1 ('MetaSel ('Just "whereModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModuleName)) :*: (S1 ('MetaSel ('Just "whereAnywhere") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "whereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Declaration))))) |
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
.
Instances
ExprLike SpineLHS Source # | |||||
Defined in Agda.Syntax.Abstract.Views | |||||
HasRange SpineLHS Source # | |||||
KillRange SpineLHS Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
ToConcrete SpineLHS Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
| |||||
NFData SpineLHS Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
Generic SpineLHS Source # | |||||
Defined in Agda.Syntax.Abstract
| |||||
Show SpineLHS Source # | |||||
Eq SpineLHS Source # | |||||
LHSToSpine Clause SpineClause Source # | Clause instance. | ||||
Defined in Agda.Syntax.Abstract.Pattern lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source # | |||||
LHSToSpine LHS SpineLHS Source # | LHS instance. | ||||
Defined in Agda.Syntax.Abstract.Pattern lhsToSpine :: LHS -> SpineLHS Source # spineToLhs :: SpineLHS -> LHS Source # | |||||
type ConOfAbs SpineLHS Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type Rep SpineLHS Source # | |||||
Defined in Agda.Syntax.Abstract type Rep SpineLHS = D1 ('MetaData "SpineLHS" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "SpineLHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "spLhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :*: (S1 ('MetaSel ('Just "spLhsDefName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "spLhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Pattern])))) |
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.
anyAbstract :: a -> Bool Source #
Instances
AnyAbstract Declaration Source # | |
Defined in Agda.Syntax.Abstract anyAbstract :: Declaration -> Bool Source # | |
AnyAbstract a => AnyAbstract [a] Source # | |
Defined in Agda.Syntax.Abstract anyAbstract :: [a] -> Bool Source # |
class NameToExpr a where Source #
Turn a name into an expression.
nameToExpr :: a -> Expr Source #
Instances
NameToExpr AbstractName Source # | Turn an |
Defined in Agda.Syntax.Abstract nameToExpr :: AbstractName -> Expr Source # | |
NameToExpr ResolvedName Source # | Turn a Assumes name is not |
Defined in Agda.Syntax.Abstract nameToExpr :: ResolvedName -> Expr Source # |
lambdaLiftExpr :: [WithHiding Name] -> Expr -> Expr Source #
class SubstExpr a where Source #
Nothing
Instances
SubstExpr Expr Source # | |
SubstExpr ModuleName Source # | |
Defined in Agda.Syntax.Abstract 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 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 # | |
insertImplicitPatSynArgs Source #
:: HasRange a | |
=> (Hiding -> Range -> a) | Thing to insert (wildcard). |
-> Range | Range of the whole pattern synonym expression/pattern. |
-> [WithHiding Name] | The parameters of the pattern synonym (from its definition). |
-> [NamedArg a] | The arguments it is used with. |
-> Maybe ([(Name, a)], [WithHiding Name]) | Substitution and left-over parameters. |
data DeclarationSpine Source #
Declaration spines. Used in debugging to make it easy to see
where constructors such as ScopedDecl
and Mutual
are placed.
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 |
Instances
Show DeclarationSpine Source # | |
Defined in Agda.Syntax.Abstract showsPrec :: Int -> DeclarationSpine -> ShowS show :: DeclarationSpine -> String showList :: [DeclarationSpine] -> ShowS |
data ClauseSpine Source #
Clause spines.
Instances
Show ClauseSpine Source # | |
Defined in Agda.Syntax.Abstract showsPrec :: Int -> ClauseSpine -> ShowS show :: ClauseSpine -> String showList :: [ClauseSpine] -> ShowS |
Right-hand side spines.
data WhereDeclarationsSpine Source #
Spines corresponding to WhereDeclarations
values.
Instances
Show WhereDeclarationsSpine Source # | |
Defined in Agda.Syntax.Abstract showsPrec :: Int -> WhereDeclarationsSpine -> ShowS show :: WhereDeclarationsSpine -> String showList :: [WhereDeclarationsSpine] -> ShowS |
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