Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Syntax.Abstract

Contents

Orphan instances

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 Telescope = [TypedBinding]
type Pattern = Pattern' Expr
type Type = Expr
type Assign = FieldAssignment' Expr
type Constructor = TypeSignature
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 {
- lhsInfo :: LHSInfo
- lhsCore :: LHSCore
}
type Clause = Clause' LHS
data Binder' a = Binder {
- binderPattern :: Maybe Pattern
- binderName :: a
}
type Binder = Binder' BindName
data LamBinding
- = DomainFree TacticAttr (NamedArg Binder)
- | DomainFull TypedBinding
data TypedBinding
- = TBind Range TypedBindingInfo (List1 (NamedArg Binder)) Type
- | TLet Range (List1 LetBinding)
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
- = SectionApp Telescope ModuleName [NamedArg Expr]
- | RecordModuleInstance ModuleName
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
- = RHS {
  - rhsExpr :: Expr
  - rhsConcrete :: Maybe Expr
  }
- | AbsurdRHS
- | WithRHS QName [WithExpr] (List1 Clause)
- | RewriteRHS {
  - rewriteExprs :: [RewriteEqn]
  - rewriteStrippedPats :: [ProblemEq]
  - rewriteRHS :: RHS
  - rewriteWhereDecls :: WhereDeclarations
  }
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 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 {
- tbTacticAttr :: TacticAttr
- tbFinite :: Bool
}
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 {
- unBind :: Name
}
data LetBinding
- = LetBind LetInfo ArgInfo BindName Type Expr
- | LetPatBind LetInfo Pattern Expr
- | LetApply ModuleInfo Erased ModuleName ModuleApplication ScopeCopyInfo ImportDirective
- | LetOpen ModuleInfo ModuleName ImportDirective
- | LetDeclaredVariable BindName
type RecordAssigns = [RecordAssign]
type Assigns = [Assign]
type RecordAssign = Either Assign ModuleName
data GeneralizeTelescope = GeneralizeTel {
- generalizeTelVars :: Map QName Name
- generalizeTel :: Telescope
}
data DataDefParams = DataDefParams {
- dataDefGeneralizedParams :: Set Name
- dataDefParams :: [LamBinding]
}
type TacticAttr = Maybe (Ranged Expr)
data Clause' lhs = Clause {
- clauseLHS :: lhs
- clauseStrippedPats :: [ProblemEq]
- clauseRHS :: RHS
- clauseWhereDecls :: WhereDeclarations
- clauseCatchall :: Bool
}
data WhereDeclarations = WhereDecls {
- whereModule :: Maybe ModuleName
- whereAnywhere :: Bool
- whereDecls :: Maybe Declaration
}
type SpineClause = Clause' SpineLHS
data SpineLHS = SpineLHS {
- spLhsInfo :: LHSInfo
- spLhsDefName :: QName
- spLhsPats :: [NamedArg Pattern]
}
type WithExpr' e = Named BindName (Arg e)
data LHSCore' e
- = LHSHead {
  - lhsDefName :: QName
  - lhsPats :: [NamedArg (Pattern' e)]
  }
- | LHSProj {
  - lhsDestructor :: AmbiguousQName
  - lhsFocus :: NamedArg (LHSCore' e)
  - lhsPats :: [NamedArg (Pattern' e)]
  }
- | LHSWith {
  - lhsHead :: LHSCore' e
  - lhsWithPatterns :: [Arg (Pattern' e)]
  - lhsPats :: [NamedArg (Pattern' 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
- substExpr :: [(Name, Expr)] -> a -> a
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
- = RHSS
- | AbsurdRHSS
- | WithRHSS (List1 ClauseSpine)
- | RewriteRHSS RHSSpine WhereDeclarationsSpine
data WhereDeclarationsSpine = WhereDeclsS (Maybe DeclarationSpine)
pattern Def :: QName -> Expr
mkBinder_ :: Name -> Binder
mkBinder :: a -> Binder' a
mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding
app :: Expr -> [NamedArg Expr] -> Expr
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

type Telescope = [TypedBinding] Source #

type Pattern = Pattern' Expr Source #

type Type = Expr Source #

Types are just expressions. Use this type synonym for hinting that an expression should be a type.

type Assign = FieldAssignment' Expr Source #

Record field assignment f = e.

type Constructor = TypeSignature Source #

data Expr Source #

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 `InteractionId` is usually identical with the `metaNumber` of `MetaInfo`. However, if you want to print an interaction meta as just `?` instead of `?n`, you should set the `metaNumber` to `Nothing` while keeping the `InteractionId`.
Underscore MetaInfo	Meta variable for hidden argument (must be inferred locally).
Dot ExprInfo Expr	`.e`, for postfix projection.
App AppInfo Expr (NamedArg Expr)	Ordinary (binary) application.
WithApp ExprInfo Expr [Expr]	With application.
Lam ExprInfo LamBinding Expr	`λ bs → e`.
AbsurdLam ExprInfo Hiding	`λ()` or `λ{}`.
ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause)
Pi ExprInfo Telescope1 Type	Dependent function space `Γ → A`.
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	`let bs in e`.
Rec ExprInfo RecordAssigns	Record construction.
RecUpdate ExprInfo Expr Assigns	Record update.
ScopedExpr ScopeInfo Expr	Scope annotation.
Quote ExprInfo	Quote an identifier `QName`.
QuoteTerm ExprInfo	Quote a term.
Unquote ExprInfo	The splicing construct: unquote ...
DontCare Expr	For printing `DontCare` from `Syntax.Internal`.

Instances

Instances details

SubstExpr Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Expr -> Expr Source #
IsProjP Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName) Source #
MapNamedArgPattern NAP Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
ExprLike Expr Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m Expr Source # foldExpr :: FoldExprFn m Expr Source # traverseExpr :: TraverseExprFn m Expr Source # mapExpr :: (Expr -> Expr) -> Expr -> Expr Source #
Underscore Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods underscore :: Expr Source # isUnderscore :: Expr -> Bool Source #
HasRange Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Expr -> Range Source #
KillRange Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT Expr Source #
ToConcrete Expr Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs Expr Source # Methods toConcrete :: Expr -> AbsToCon (ConOfAbs Expr) Source # bindToConcrete :: Expr -> (ConOfAbs Expr -> AbsToCon b) -> AbsToCon b Source #
ToConcrete LHSCore Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs LHSCore Source # Methods toConcrete :: LHSCore -> AbsToCon (ConOfAbs LHSCore) Source # bindToConcrete :: LHSCore -> (ConOfAbs LHSCore -> AbsToCon b) -> AbsToCon b Source #
ToConcrete Pattern Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs Pattern Source # Methods toConcrete :: Pattern -> AbsToCon (ConOfAbs Pattern) Source # bindToConcrete :: Pattern -> (ConOfAbs Pattern -> AbsToCon b) -> AbsToCon b Source #
Reify Expr Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo Expr Source # Methods reify :: MonadReify m => Expr -> m (ReifiesTo Expr) Source # reifyWhen :: MonadReify m => Bool -> Expr -> m (ReifiesTo Expr) Source #
PrettyTCM Expr Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Expr -> m Doc Source #
PrettyTCM Pattern Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Pattern -> m Doc Source #
IsFlexiblePattern Pattern Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern -> m Bool Source #
Generic Expr Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep Expr :: Type -> Type Methods from :: Expr -> Rep Expr x to :: Rep Expr x -> Expr
Show Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Expr -> ShowS show :: Expr -> String showList :: [Expr] -> ShowS
NFData Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Expr -> ()
Eq Expr Source #	Does not compare `ScopeInfo` fields. Does not distinguish between prefix and postfix projections.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Expr -> Expr -> Bool (/=) :: Expr -> Expr -> Bool
ToConcrete (Maybe Pattern) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Maybe Pattern) Source # Methods toConcrete :: Maybe Pattern -> AbsToCon (ConOfAbs (Maybe Pattern)) Source # bindToConcrete :: Maybe Pattern -> (ConOfAbs (Maybe Pattern) -> AbsToCon b) -> AbsToCon b Source #
PrettyTCM (Arg Expr) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Arg Expr -> m Doc Source #
PrettyTCM (NamedArg Expr) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedArg Expr -> m Doc Source #
ToAbstract (Expr, Elim) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Expr, Elim) Source # Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m (AbsOfRef (Expr, Elim)) Source #
ToAbstract (Expr, Elims) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Expr, Elims) Source # Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m (AbsOfRef (Expr, Elims)) Source #
ToAbstract (RewriteEqn' () BindName Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # Methods toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source #
type ConOfAbs Expr Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Expr = Expr
type ConOfAbs LHSCore Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHSCore = Pattern
type ConOfAbs Pattern Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Pattern = Pattern
type ReifiesTo Expr Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Expr = Expr
type Rep Expr Source #
Instance details Defined in Agda.Syntax.Abstract type Rep Expr = D1 ('MetaData "Expr" "Agda.Syntax.Abstract" "Agda-2.6.4-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 ConOfAbs (Maybe Pattern) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Maybe Pattern) = Maybe Pattern
type AbsOfRef (Expr, Elim) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elim) = Expr
type AbsOfRef (Expr, Elims) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elims) = Expr
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

data LHS Source #

The lhs of a clause in focused (projection-application) view (outside-in). Projection patters are represented as LHSProjs.

Constructors

LHS
Fields lhsInfo :: LHSInfo Range. lhsCore :: LHSCore Copatterns.

Instances

Instances details

DeclaredNames Clause Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Clause -> m Source #
ExprLike LHS Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m LHS Source # foldExpr :: FoldExprFn m LHS Source # traverseExpr :: TraverseExprFn m LHS Source # mapExpr :: (Expr -> Expr) -> LHS -> LHS Source #
HasRange LHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LHS -> Range Source #
KillRange LHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LHS Source #
ToConcrete LHS Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs LHS Source # Methods toConcrete :: LHS -> AbsToCon (ConOfAbs LHS) Source # bindToConcrete :: LHS -> (ConOfAbs LHS -> AbsToCon b) -> AbsToCon b Source #
Generic LHS Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep LHS :: Type -> Type Methods from :: LHS -> Rep LHS x to :: Rep LHS x -> LHS
Show LHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LHS -> ShowS show :: LHS -> String showList :: [LHS] -> ShowS
NFData LHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: LHS -> ()
Eq LHS Source #	Ignore `Range'` when comparing `LHS`s.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LHS -> LHS -> Bool (/=) :: LHS -> LHS -> Bool
LHSToSpine Clause SpineClause Source #	Clause instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
LHSToSpine LHS SpineLHS Source #	LHS instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: LHS -> SpineLHS Source # spineToLhs :: SpineLHS -> LHS Source #
type ConOfAbs LHS Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHS = LHS
type Rep LHS Source #
Instance details Defined in Agda.Syntax.Abstract type Rep LHS = D1 ('MetaData "LHS" "Agda.Syntax.Abstract" "Agda-2.6.4-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)))

type Clause = Clause' LHS Source #

data Binder' a Source #

Constructors

Binder
Fields binderPattern :: Maybe Pattern binderName :: a

Instances

Instances details

Foldable Binder' Source #
Instance details Defined in Agda.Syntax.Abstract Methods 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 toList :: Binder' a -> [a] null :: Binder' a -> Bool length :: Binder' a -> Int elem :: Eq a => a -> Binder' a -> Bool maximum :: Ord a => Binder' a -> a minimum :: Ord a => Binder' a -> a sum :: Num a => Binder' a -> a product :: Num a => Binder' a -> a
Traversable Binder' Source #
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> Binder' a -> f (Binder' b) sequenceA :: Applicative f => Binder' (f a) -> f (Binder' a) mapM :: Monad m => (a -> m b) -> Binder' a -> m (Binder' b) sequence :: Monad m => Binder' (m a) -> m (Binder' a)
Functor Binder' Source #
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> Binder' a -> Binder' b (<$) :: a -> Binder' b -> Binder' a #
HasRange a => HasRange (Binder' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Binder' a -> Range Source #
KillRange a => KillRange (Binder' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Binder' a) Source #
ToConcrete a => ToConcrete (Binder' a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Binder' a) Source # Methods toConcrete :: Binder' a -> AbsToCon (ConOfAbs (Binder' a)) Source # bindToConcrete :: Binder' a -> (ConOfAbs (Binder' a) -> AbsToCon b) -> AbsToCon b Source #
Generic (Binder' a) Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep (Binder' a) :: Type -> Type Methods from :: Binder' a -> Rep (Binder' a) x to :: Rep (Binder' a) x -> Binder' a
Show a => Show (Binder' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Binder' a -> ShowS show :: Binder' a -> String showList :: [Binder' a] -> ShowS
NFData a => NFData (Binder' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Binder' a -> ()
Eq a => Eq (Binder' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Binder' a -> Binder' a -> Bool (/=) :: Binder' a -> Binder' a -> Bool
type ConOfAbs (Binder' a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Binder' a) = Binder' (ConOfAbs a)
type Rep (Binder' a) Source #
Instance details Defined in Agda.Syntax.Abstract type Rep (Binder' a) = D1 ('MetaData "Binder'" "Agda.Syntax.Abstract" "Agda-2.6.4-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)))

type Binder = Binder' BindName Source #

data LamBinding Source #

A lambda binding is either domain free or typed.

Constructors

DomainFree TacticAttr (NamedArg Binder)	. `x` or `{x}` or `.x` or `{x = y}` or `x@p` or `(p)`
DomainFull TypedBinding	. `(xs:e)` or `{xs:e}` or `(let Ds)`

Instances

Instances details

ExprLike LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m LamBinding Source # foldExpr :: FoldExprFn m LamBinding Source # traverseExpr :: TraverseExprFn m LamBinding Source # mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source #
LensHiding LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source #
HasRange LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LamBinding -> Range Source #
KillRange LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LamBinding Source #
ToConcrete LamBinding Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs LamBinding Source # Methods toConcrete :: LamBinding -> AbsToCon (ConOfAbs LamBinding) Source # bindToConcrete :: LamBinding -> (ConOfAbs LamBinding -> AbsToCon b) -> AbsToCon b Source #
Generic LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep LamBinding :: Type -> Type Methods from :: LamBinding -> Rep LamBinding x to :: Rep LamBinding x -> LamBinding
Show LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LamBinding -> ShowS show :: LamBinding -> String showList :: [LamBinding] -> ShowS
NFData LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: LamBinding -> ()
Eq LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LamBinding -> LamBinding -> Bool (/=) :: LamBinding -> LamBinding -> Bool
type ConOfAbs LamBinding Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LamBinding = Maybe LamBinding
type Rep LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract type Rep LamBinding = D1 ('MetaData "LamBinding" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "DomainFree" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttr) :*: 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.

Constructors

TBind Range TypedBindingInfo (List1 (NamedArg Binder)) Type	As in telescope `(x y z : A)` or type `(x y z : A) -> B`.
TLet Range (List1 LetBinding)	E.g. `(let x = e)` or `(let open M)`.

Instances

Instances details

ExprLike TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m TypedBinding Source # foldExpr :: FoldExprFn m TypedBinding Source # traverseExpr :: TraverseExprFn m TypedBinding Source # mapExpr :: (Expr -> Expr) -> TypedBinding -> TypedBinding Source #
LensHiding TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source #
HasRange TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: TypedBinding -> Range Source #
KillRange TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT TypedBinding Source #
ToConcrete TypedBinding Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs TypedBinding Source # Methods toConcrete :: TypedBinding -> AbsToCon (ConOfAbs TypedBinding) Source # bindToConcrete :: TypedBinding -> (ConOfAbs TypedBinding -> AbsToCon b) -> AbsToCon b Source #
PrettyTCM TypedBinding Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TypedBinding -> m Doc Source #
Generic TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep TypedBinding :: Type -> Type Methods from :: TypedBinding -> Rep TypedBinding x to :: Rep TypedBinding x -> TypedBinding
Show TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> TypedBinding -> ShowS show :: TypedBinding -> String showList :: [TypedBinding] -> ShowS
NFData TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: TypedBinding -> ()
Eq TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: TypedBinding -> TypedBinding -> Bool (/=) :: TypedBinding -> TypedBinding -> Bool
type ConOfAbs TypedBinding Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs TypedBinding = Maybe TypedBinding
type Rep TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract type Rep TypedBinding = D1 ('MetaData "TypedBinding" "Agda.Syntax.Abstract" "Agda-2.6.4-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 #

data Declaration Source #

Constructors

Axiom KindOfName DefInfo ArgInfo (Maybe [Occurrence]) QName Type	Type signature (can be irrelevant, but not hidden). The fourth argument contains an optional assignment of polarities to arguments.
Generalize (Set QName) DefInfo ArgInfo QName Type	First argument is set of generalizable variables used in the type.
Field DefInfo QName (Arg Type)	record field
Primitive DefInfo QName (Arg Type)	primitive function
Mutual MutualInfo [Declaration]	a bunch of mutually recursive definitions
Section Range Erased ModuleName GeneralizeTelescope [Declaration]
Apply ModuleInfo Erased ModuleName ModuleApplication ScopeCopyInfo ImportDirective	The `ImportDirective` is for highlighting purposes.
Import ModuleInfo ModuleName ImportDirective	The `ImportDirective` is for highlighting purposes.
Pragma Range Pragma
Open ModuleInfo ModuleName ImportDirective
FunDef DefInfo QName [Clause]	sequence of function clauses
DataSig DefInfo Erased QName GeneralizeTelescope Type	lone data signature
DataDef DefInfo QName UniverseCheck DataDefParams [Constructor]
RecSig DefInfo Erased QName GeneralizeTelescope Type	lone record signature
RecDef DefInfo QName UniverseCheck RecordDirectives DataDefParams Type [Declaration]	The `Type` gives the constructor type telescope, `(x1 : A1)..(xn : An) -> Dummy`, and the optional name is the constructor's name. The optional `Range'` is for the `pattern` attribute.
PatternSynDef QName [Arg BindName] (Pattern' Void)	Only for highlighting purposes
UnquoteDecl MutualInfo [DefInfo] [QName] Expr
UnquoteDef [DefInfo] [QName] Expr
UnquoteData [DefInfo] QName UniverseCheck [DefInfo] [QName] Expr
ScopedDecl ScopeInfo [Declaration]	scope annotation
UnfoldingDecl Range [QName]	Only for highlighting the unfolded names

Instances

Instances details

AnyAbstract Declaration Source #
Instance details Defined in Agda.Syntax.Abstract Methods anyAbstract :: Declaration -> Bool Source #
DeclaredNames Declaration Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Declaration -> m Source #
ExprLike Declaration Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m Declaration Source # foldExpr :: FoldExprFn m Declaration Source # traverseExpr :: TraverseExprFn m Declaration Source # mapExpr :: (Expr -> Expr) -> Declaration -> Declaration Source #
HasRange Declaration Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Declaration -> Range Source #
KillRange Declaration Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT Declaration Source #
ToConcrete Declaration Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs Declaration Source # Methods toConcrete :: Declaration -> AbsToCon (ConOfAbs Declaration) Source # bindToConcrete :: Declaration -> (ConOfAbs Declaration -> AbsToCon b) -> AbsToCon b Source #
ShowHead Declaration Source #
Instance details Defined in Agda.TypeChecking.Rules.Decl Methods showHead :: Declaration -> String Source #
Generic Declaration Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep Declaration :: Type -> Type Methods from :: Declaration -> Rep Declaration x to :: Rep Declaration x -> Declaration
Show Declaration Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Declaration -> ShowS show :: Declaration -> String showList :: [Declaration] -> ShowS
NFData Declaration Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Declaration -> ()
Eq Declaration Source #	Does not compare `ScopeInfo` fields.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Declaration -> Declaration -> Bool (/=) :: Declaration -> Declaration -> Bool
ToConcrete (Constr Constructor) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Constr Constructor) Source # Methods toConcrete :: Constr Constructor -> AbsToCon (ConOfAbs (Constr Constructor)) Source # bindToConcrete :: Constr Constructor -> (ConOfAbs (Constr Constructor) -> AbsToCon b) -> AbsToCon b Source #
type ConOfAbs Declaration Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Declaration = [Declaration]
type Rep Declaration Source #
Instance details Defined in Agda.Syntax.Abstract type Rep Declaration = D1 ('MetaData "Declaration" "Agda.Syntax.Abstract" "Agda-2.6.4-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 [Arg 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 #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Constr Constructor) = Declaration

type RecordDirectives = RecordDirectives' QName Source #

data ModuleApplication Source #

Constructors

SectionApp Telescope ModuleName [NamedArg Expr]	`tel. M args`: applies `M` to `args` and abstracts `tel`.
RecordModuleInstance ModuleName	M {{...}}

Instances

Instances details

ExprLike ModuleApplication Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m ModuleApplication Source # foldExpr :: FoldExprFn m ModuleApplication Source # traverseExpr :: TraverseExprFn m ModuleApplication Source # mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication Source #
KillRange ModuleApplication Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ModuleApplication Source #
ToConcrete ModuleApplication Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs ModuleApplication Source # Methods toConcrete :: ModuleApplication -> AbsToCon (ConOfAbs ModuleApplication) Source # bindToConcrete :: ModuleApplication -> (ConOfAbs ModuleApplication -> AbsToCon b) -> AbsToCon b Source #
Generic ModuleApplication Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep ModuleApplication :: Type -> Type Methods from :: ModuleApplication -> Rep ModuleApplication x to :: Rep ModuleApplication x -> ModuleApplication
Show ModuleApplication Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ModuleApplication -> ShowS show :: ModuleApplication -> String showList :: [ModuleApplication] -> ShowS
NFData ModuleApplication Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: ModuleApplication -> ()
Eq ModuleApplication Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: ModuleApplication -> ModuleApplication -> Bool (/=) :: ModuleApplication -> ModuleApplication -> Bool
type ConOfAbs ModuleApplication Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs ModuleApplication = ModuleApplication
type Rep ModuleApplication Source #
Instance details Defined in Agda.Syntax.Abstract type Rep ModuleApplication = D1 ('MetaData "ModuleApplication" "Agda.Syntax.Abstract" "Agda-2.6.4-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 Axioms.

type ImportDirective = ImportDirective' QName ModuleName Source #

type ImportedName = ImportedName' QName ModuleName Source #

type Renaming = Renaming' QName ModuleName Source #

type RewriteEqn = RewriteEqn' QName BindName Pattern Expr Source #

type WithExpr = WithExpr' Expr Source #

type LHSCore = LHSCore' Expr Source #

data RHS Source #

Constructors

RHS
Fields rhsExpr :: Expr rhsConcrete :: Maybe Expr We store the original concrete expression in case we have to reproduce it during interactive case splitting. `Nothing` for internally generated rhss.
AbsurdRHS
WithRHS QName [WithExpr] (List1 Clause)	The `QName` is the name of the with function.
RewriteRHS
Fields rewriteExprs :: [RewriteEqn] The `QName`s are the names of the generated with functions, one for each `Expr`. rewriteStrippedPats :: [ProblemEq] The patterns stripped by with-desugaring. These are only present if this rewrite follows a with. rewriteRHS :: RHS The RHS should not be another `RewriteRHS`. rewriteWhereDecls :: WhereDeclarations The where clauses are attached to the `RewriteRHS` by

Instances

Instances details

DeclaredNames RHS Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => RHS -> m Source #
ExprLike RHS Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m RHS Source # foldExpr :: FoldExprFn m RHS Source # traverseExpr :: TraverseExprFn m RHS Source # mapExpr :: (Expr -> Expr) -> RHS -> RHS Source #
HasRange RHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: RHS -> Range Source #
KillRange RHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT RHS Source #
ToConcrete RHS Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs RHS Source # Methods toConcrete :: RHS -> AbsToCon (ConOfAbs RHS) Source # bindToConcrete :: RHS -> (ConOfAbs RHS -> AbsToCon b) -> AbsToCon b Source #
Generic RHS Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep RHS :: Type -> Type Methods from :: RHS -> Rep RHS x to :: Rep RHS x -> RHS
Show RHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> RHS -> ShowS show :: RHS -> String showList :: [RHS] -> ShowS
NFData RHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: RHS -> ()
Eq RHS Source #	Ignore `rhsConcrete` when comparing `RHS`s.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: RHS -> RHS -> Bool (/=) :: RHS -> RHS -> Bool
type ConOfAbs RHS Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs RHS = (RHS, [RewriteEqn], [WithExpr], [Declaration])
type Rep RHS Source #
Instance details Defined in Agda.Syntax.Abstract type Rep RHS = D1 ('MetaData "RHS" "Agda.Syntax.Abstract" "Agda-2.6.4-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)))))

data Pragma Source #

Constructors

OptionsPragma [String]
BuiltinPragma RString ResolvedName	`ResolvedName` is not `UnknownName`. Name can be ambiguous e.g. for built-in constructors.
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 `eta-equality` definition (as it is might make Agda loop).
InjectivePragma QName
InlinePragma Bool QName
NotProjectionLikePragma QName
DisplayPragma QName [NamedArg Pattern] Expr

Instances

Instances details

DeclaredNames Pragma Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Pragma -> m Source #
ExprLike Pragma Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m Pragma Source # foldExpr :: FoldExprFn m Pragma Source # traverseExpr :: TraverseExprFn m Pragma Source # mapExpr :: (Expr -> Expr) -> Pragma -> Pragma Source #
Generic Pragma Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep Pragma :: Type -> Type Methods from :: Pragma -> Rep Pragma x to :: Rep Pragma x -> Pragma
Show Pragma Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Pragma -> ShowS show :: Pragma -> String showList :: [Pragma] -> ShowS
NFData Pragma Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Pragma -> ()
Eq Pragma Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Pragma -> Pragma -> Bool (/=) :: Pragma -> Pragma -> Bool
type Rep Pragma Source #
Instance details Defined in Agda.Syntax.Abstract type Rep Pragma = D1 ('MetaData "Pragma" "Agda.Syntax.Abstract" "Agda-2.6.4-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 "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 "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 HoleContent = HoleContent' () BindName Pattern Expr Source #

data ScopeCopyInfo Source #

Constructors

ScopeCopyInfo
Fields renModules :: Ren ModuleName renNames :: Ren QName

Instances

Instances details

Pretty ScopeCopyInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods pretty :: ScopeCopyInfo -> Doc Source # prettyPrec :: Int -> ScopeCopyInfo -> Doc Source # prettyList :: [ScopeCopyInfo] -> Doc Source #
KillRange ScopeCopyInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ScopeCopyInfo Source #
Generic ScopeCopyInfo Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep ScopeCopyInfo :: Type -> Type Methods from :: ScopeCopyInfo -> Rep ScopeCopyInfo x to :: Rep ScopeCopyInfo x -> ScopeCopyInfo
Show ScopeCopyInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ScopeCopyInfo -> ShowS show :: ScopeCopyInfo -> String showList :: [ScopeCopyInfo] -> ShowS
NFData ScopeCopyInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: ScopeCopyInfo -> ()
Eq ScopeCopyInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool (/=) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
type Rep ScopeCopyInfo Source #
Instance details Defined in Agda.Syntax.Abstract type Rep ScopeCopyInfo = D1 ('MetaData "ScopeCopyInfo" "Agda.Syntax.Abstract" "Agda-2.6.4-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 Args = [NamedArg Expr] Source #

type Ren a = Map a (List1 a) Source #

Renaming (generic).

type PatternSynDefn = ([Arg Name], Pattern' Void) Source #

type PatternSynDefns = Map QName PatternSynDefn Source #

data ProblemEq 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 problemInPat :: Pattern problemInst :: Term problemType :: Dom Type

Instances

Instances details

KillRange ProblemEq Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ProblemEq Source #
PrettyTCM ProblemEq Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => ProblemEq -> m Doc Source #
Subst ProblemEq Source #
Instance details Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg ProblemEq Source # Methods applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq Source #
Generic ProblemEq Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep ProblemEq :: Type -> Type Methods from :: ProblemEq -> Rep ProblemEq x to :: Rep ProblemEq x -> ProblemEq
Show ProblemEq Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ProblemEq -> ShowS show :: ProblemEq -> String showList :: [ProblemEq] -> ShowS
NFData ProblemEq Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: ProblemEq -> ()
Eq ProblemEq Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: ProblemEq -> ProblemEq -> Bool (/=) :: ProblemEq -> ProblemEq -> Bool
type SubstArg ProblemEq Source #
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ProblemEq = Term
type Rep ProblemEq Source #
Instance details Defined in Agda.Syntax.Abstract type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.6.4-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.

Constructors

TypedBindingInfo
Fields tbTacticAttr :: TacticAttr Does this binding have a tactic annotation? tbFinite :: Bool Does this binding correspond to a Partial binder, rather than to a Pi binder? Must be present here to be reflected into abstract syntax later (and to be printed to the user later).

Instances

Instances details

ExprLike TypedBindingInfo Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m TypedBindingInfo Source # foldExpr :: FoldExprFn m TypedBindingInfo Source # traverseExpr :: TraverseExprFn m TypedBindingInfo Source # mapExpr :: (Expr -> Expr) -> TypedBindingInfo -> TypedBindingInfo Source #
KillRange TypedBindingInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT TypedBindingInfo Source #
Generic TypedBindingInfo Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep TypedBindingInfo :: Type -> Type Methods from :: TypedBindingInfo -> Rep TypedBindingInfo x to :: Rep TypedBindingInfo x -> TypedBindingInfo
Show TypedBindingInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> TypedBindingInfo -> ShowS show :: TypedBindingInfo -> String showList :: [TypedBindingInfo] -> ShowS
NFData TypedBindingInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: TypedBindingInfo -> ()
Eq TypedBindingInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: TypedBindingInfo -> TypedBindingInfo -> Bool (/=) :: TypedBindingInfo -> TypedBindingInfo -> Bool
type Rep TypedBindingInfo Source #
Instance details Defined in Agda.Syntax.Abstract type Rep TypedBindingInfo = D1 ('MetaData "TypedBindingInfo" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "TypedBindingInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "tbTacticAttr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttr) :*: S1 ('MetaSel ('Just "tbFinite") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

type Field = TypeSignature Source #

type NAPs e = [NamedArg (Pattern' e)] Source #

data Pattern' e Source #

Parameterised over the type of dot patterns.

Constructors

VarP BindName
ConP ConPatInfo AmbiguousQName (NAPs e)
ProjP PatInfo ProjOrigin AmbiguousQName	Destructor pattern `d`.
DefP PatInfo AmbiguousQName (NAPs e)	Defined pattern: function definition `f ps`. It is also abused to convert destructor patterns into concrete syntax thus, we put AmbiguousQName here as well.
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 `.e`
AbsurdP PatInfo
LitP PatInfo Literal
PatternSynP PatInfo AmbiguousQName (NAPs e)
RecP PatInfo [FieldAssignment' (Pattern' e)]
EqualP PatInfo [(e, e)]
WithP PatInfo (Pattern' e)	`\| p`, for with-patterns.
AnnP PatInfo e (Pattern' e)	Pattern with type annotation

Instances

Instances details

MapNamedArgPattern NAP Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
ToConcrete Pattern Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs Pattern Source # Methods toConcrete :: Pattern -> AbsToCon (ConOfAbs Pattern) Source # bindToConcrete :: Pattern -> (ConOfAbs Pattern -> AbsToCon b) -> AbsToCon b Source #
PrettyTCM Pattern Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Pattern -> m Doc Source #
IsFlexiblePattern Pattern Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern -> m Bool Source #
Foldable Pattern' Source #
Instance details Defined in Agda.Syntax.Abstract Methods 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 toList :: Pattern' a -> [a] null :: Pattern' a -> Bool length :: Pattern' a -> Int elem :: Eq a => a -> Pattern' a -> Bool maximum :: Ord a => Pattern' a -> a minimum :: Ord a => Pattern' a -> a sum :: Num a => Pattern' a -> a product :: Num a => Pattern' a -> a
Traversable Pattern' Source #
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> Pattern' a -> f (Pattern' b) sequenceA :: Applicative f => Pattern' (f a) -> f (Pattern' a) mapM :: Monad m => (a -> m b) -> Pattern' a -> m (Pattern' b) sequence :: Monad m => Pattern' (m a) -> m (Pattern' a)
Functor Pattern' Source #
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> Pattern' a -> Pattern' b (<$) :: a -> Pattern' b -> Pattern' a #
IsProjP (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) Source #
APatternLike (Pattern' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Associated Types type ADotT (Pattern' a) Source # Methods 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 #
Instance details Defined in Agda.Syntax.Abstract.Views Methods 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.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods isWithP :: Pattern' e -> Maybe (Pattern' e) Source #
NamesIn (Pattern' a) Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Pattern' a -> m Source #
HasRange (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Pattern' e -> Range Source #
KillRange e => KillRange (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Pattern' e) Source #
SetRange (Pattern' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods setRange :: Range -> Pattern' a -> Pattern' a Source #
ToConcrete (Maybe Pattern) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Maybe Pattern) Source # Methods toConcrete :: Maybe Pattern -> AbsToCon (ConOfAbs (Maybe Pattern)) Source # bindToConcrete :: Maybe Pattern -> (ConOfAbs (Maybe Pattern) -> AbsToCon b) -> AbsToCon b Source #
ToAbstract (Pattern' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Pattern' Expr) Source # Methods toAbstract :: Pattern' Expr -> ScopeM (AbsOfCon (Pattern' Expr)) Source #
ExpandPatternSynonyms (Pattern' e) Source #
Instance details Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: Pattern' e -> TCM (Pattern' e) Source #
EmbPrj a => EmbPrj (Pattern' a) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Pattern' a -> S Int32 Source # icod_ :: Pattern' a -> S Int32 Source # value :: Int32 -> R (Pattern' a) Source #
Generic (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep (Pattern' e) :: Type -> Type Methods from :: Pattern' e -> Rep (Pattern' e) x to :: Rep (Pattern' e) x -> Pattern' e
Show e => Show (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Pattern' e -> ShowS show :: Pattern' e -> String showList :: [Pattern' e] -> ShowS
NFData e => NFData (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Pattern' e -> ()
Eq e => Eq (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Pattern' e -> Pattern' e -> Bool (/=) :: Pattern' e -> Pattern' e -> Bool
ToAbstract (RewriteEqn' () BindName Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # Methods toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source #
type ConOfAbs Pattern Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Pattern = Pattern
type ADotT (Pattern' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern type ADotT (Pattern' a) = a
type ConOfAbs (Maybe Pattern) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Maybe Pattern) = Maybe Pattern
type AbsOfCon (Pattern' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Pattern' Expr) = Pattern' Expr
type Rep (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract type Rep (Pattern' e) = D1 ('MetaData "Pattern'" "Agda.Syntax.Abstract" "Agda-2.6.4-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 PatInfo) :: 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 #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

type DefInfo = DefInfo' Expr Source #

newtype BindName Source #

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

Constructors

BindName
Fields unBind :: Name

Instances

Instances details

ExprLike BindName Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m BindName Source # foldExpr :: FoldExprFn m BindName Source # traverseExpr :: TraverseExprFn m BindName Source # mapExpr :: (Expr -> Expr) -> BindName -> BindName Source #
HasRange BindName Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: BindName -> Range Source #
KillRange BindName Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT BindName Source #
SetRange BindName Source #
Instance details Defined in Agda.Syntax.Abstract Methods setRange :: Range -> BindName -> BindName Source #
ToConcrete BindName Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs BindName Source # Methods toConcrete :: BindName -> AbsToCon (ConOfAbs BindName) Source # bindToConcrete :: BindName -> (ConOfAbs BindName -> AbsToCon b) -> AbsToCon b Source #
EmbPrj BindName Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: BindName -> S Int32 Source # icod_ :: BindName -> S Int32 Source # value :: Int32 -> R BindName Source #
Show BindName Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> BindName -> ShowS show :: BindName -> String showList :: [BindName] -> ShowS
NFData BindName Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: BindName -> ()
Eq BindName Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: BindName -> BindName -> Bool (/=) :: BindName -> BindName -> Bool
Ord BindName Source #
Instance details Defined in Agda.Syntax.Abstract Methods compare :: BindName -> BindName -> Ordering (<) :: BindName -> BindName -> Bool (<=) :: BindName -> BindName -> Bool (>) :: BindName -> BindName -> Bool (>=) :: BindName -> BindName -> Bool max :: BindName -> BindName -> BindName min :: BindName -> BindName -> BindName
ToConcrete (Maybe BindName) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Maybe BindName) Source # Methods toConcrete :: Maybe BindName -> AbsToCon (ConOfAbs (Maybe BindName)) Source # bindToConcrete :: Maybe BindName -> (ConOfAbs (Maybe BindName) -> AbsToCon b) -> AbsToCon b Source #
(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (RewriteEqn' qn BindName p a) Source # Methods toConcrete :: RewriteEqn' qn BindName p a -> AbsToCon (ConOfAbs (RewriteEqn' qn BindName p a)) Source # bindToConcrete :: RewriteEqn' qn BindName p a -> (ConOfAbs (RewriteEqn' qn BindName p a) -> AbsToCon b) -> AbsToCon b Source #
ToAbstract (RewriteEqn' () BindName Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # Methods toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source #
type ConOfAbs BindName Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs BindName = BoundName
type ConOfAbs (Maybe BindName) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Maybe BindName) = Maybe Name
type ConOfAbs (RewriteEqn' qn BindName p a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (RewriteEqn' qn BindName p a) = RewriteEqn' () Name (ConOfAbs p) (ConOfAbs a)
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

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	`LetApply mi newM (oldM args) renamings dir`. The `ImportDirective` is for highlighting purposes.
LetOpen ModuleInfo ModuleName ImportDirective	only for highlighting and abstractToConcrete
LetDeclaredVariable BindName	Only used for highlighting. Refers to the first occurrence of `x` in `let x : A; x = e`.

Instances

Instances details

ExprLike LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m LetBinding Source # foldExpr :: FoldExprFn m LetBinding Source # traverseExpr :: TraverseExprFn m LetBinding Source # mapExpr :: (Expr -> Expr) -> LetBinding -> LetBinding Source #
HasRange LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LetBinding -> Range Source #
KillRange LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LetBinding Source #
ToConcrete LetBinding Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs LetBinding Source # Methods toConcrete :: LetBinding -> AbsToCon (ConOfAbs LetBinding) Source # bindToConcrete :: LetBinding -> (ConOfAbs LetBinding -> AbsToCon b) -> AbsToCon b Source #
Generic LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep LetBinding :: Type -> Type Methods from :: LetBinding -> Rep LetBinding x to :: Rep LetBinding x -> LetBinding
Show LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LetBinding -> ShowS show :: LetBinding -> String showList :: [LetBinding] -> ShowS
NFData LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: LetBinding -> ()
Eq LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LetBinding -> LetBinding -> Bool (/=) :: LetBinding -> LetBinding -> Bool
type ConOfAbs LetBinding Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LetBinding = [Declaration]
type Rep LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract type Rep LetBinding = D1 ('MetaData "LetBinding" "Agda.Syntax.Abstract" "Agda-2.6.4-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 #

type Assigns = [Assign] Source #

type RecordAssign = Either Assign ModuleName Source #

data GeneralizeTelescope Source #

Constructors

GeneralizeTel
Fields generalizeTelVars :: Map QName Name Maps generalize variables to the corresponding bound variable (to be introduced by the generalisation). generalizeTel :: Telescope

Instances

Instances details

ExprLike GeneralizeTelescope Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m GeneralizeTelescope Source # foldExpr :: FoldExprFn m GeneralizeTelescope Source # traverseExpr :: TraverseExprFn m GeneralizeTelescope Source # mapExpr :: (Expr -> Expr) -> GeneralizeTelescope -> GeneralizeTelescope Source #
KillRange GeneralizeTelescope Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT GeneralizeTelescope Source #
Generic GeneralizeTelescope Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep GeneralizeTelescope :: Type -> Type Methods from :: GeneralizeTelescope -> Rep GeneralizeTelescope x to :: Rep GeneralizeTelescope x -> GeneralizeTelescope
Show GeneralizeTelescope Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> GeneralizeTelescope -> ShowS show :: GeneralizeTelescope -> String showList :: [GeneralizeTelescope] -> ShowS
NFData GeneralizeTelescope Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: GeneralizeTelescope -> ()
Eq GeneralizeTelescope Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: GeneralizeTelescope -> GeneralizeTelescope -> Bool (/=) :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
type Rep GeneralizeTelescope Source #
Instance details Defined in Agda.Syntax.Abstract type Rep GeneralizeTelescope = D1 ('MetaData "GeneralizeTelescope" "Agda.Syntax.Abstract" "Agda-2.6.4-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 #

Constructors

DataDefParams
Fields dataDefGeneralizedParams :: Set Name We don't yet know the position of generalized parameters from the data sig, so we keep these in a set on the side. dataDefParams :: [LamBinding]

Instances

Instances details

ExprLike DataDefParams Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m DataDefParams Source # foldExpr :: FoldExprFn m DataDefParams Source # traverseExpr :: TraverseExprFn m DataDefParams Source # mapExpr :: (Expr -> Expr) -> DataDefParams -> DataDefParams Source #
KillRange DataDefParams Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT DataDefParams Source #
Generic DataDefParams Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep DataDefParams :: Type -> Type Methods from :: DataDefParams -> Rep DataDefParams x to :: Rep DataDefParams x -> DataDefParams
Show DataDefParams Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> DataDefParams -> ShowS show :: DataDefParams -> String showList :: [DataDefParams] -> ShowS
NFData DataDefParams Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: DataDefParams -> ()
Eq DataDefParams Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: DataDefParams -> DataDefParams -> Bool (/=) :: DataDefParams -> DataDefParams -> Bool
type Rep DataDefParams Source #
Instance details Defined in Agda.Syntax.Abstract type Rep DataDefParams = D1 ('MetaData "DataDefParams" "Agda.Syntax.Abstract" "Agda-2.6.4-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])))

type TacticAttr = Maybe (Ranged Expr) Source #

data Clause' lhs 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.

Constructors

Clause
Fields clauseLHS :: lhs clauseStrippedPats :: [ProblemEq] Only in with-clauses where we inherit some already checked patterns from the parent. These live in the context of the parent clause left-hand side. clauseRHS :: RHS clauseWhereDecls :: WhereDeclarations clauseCatchall :: Bool

Instances

Instances details

DeclaredNames Clause Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Clause -> m Source #
Foldable Clause' Source #
Instance details Defined in Agda.Syntax.Abstract Methods 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 toList :: Clause' a -> [a] null :: Clause' a -> Bool length :: Clause' a -> Int elem :: Eq a => a -> Clause' a -> Bool maximum :: Ord a => Clause' a -> a minimum :: Ord a => Clause' a -> a sum :: Num a => Clause' a -> a product :: Num a => Clause' a -> a
Traversable Clause' Source #
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> Clause' a -> f (Clause' b) sequenceA :: Applicative f => Clause' (f a) -> f (Clause' a) mapM :: Monad m => (a -> m b) -> Clause' a -> m (Clause' b) sequence :: Monad m => Clause' (m a) -> m (Clause' a)
Functor Clause' Source #
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> Clause' a -> Clause' b (<$) :: a -> Clause' b -> Clause' a #
LHSToSpine Clause SpineClause Source #	Clause instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
ExprLike a => ExprLike (Clause' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods 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 #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Clause' a -> Range Source #
KillRange a => KillRange (Clause' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Clause' a) Source #
(ToConcrete a, ConOfAbs a ~ LHS) => ToConcrete (Clause' a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Clause' a) Source # Methods toConcrete :: Clause' a -> AbsToCon (ConOfAbs (Clause' a)) Source # bindToConcrete :: Clause' a -> (ConOfAbs (Clause' a) -> AbsToCon b) -> AbsToCon b Source #
Generic (Clause' lhs) Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep (Clause' lhs) :: Type -> Type Methods from :: Clause' lhs -> Rep (Clause' lhs) x to :: Rep (Clause' lhs) x -> Clause' lhs
Show lhs => Show (Clause' lhs) Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Clause' lhs -> ShowS show :: Clause' lhs -> String showList :: [Clause' lhs] -> ShowS
NFData lhs => NFData (Clause' lhs) Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Clause' lhs -> ()
Eq lhs => Eq (Clause' lhs) Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Clause' lhs -> Clause' lhs -> Bool (/=) :: Clause' lhs -> Clause' lhs -> Bool
type ConOfAbs (Clause' a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Clause' a) = List1 Declaration
type Rep (Clause' lhs) Source #
Instance details Defined in Agda.Syntax.Abstract type Rep (Clause' lhs) = D1 ('MetaData "Clause'" "Agda.Syntax.Abstract" "Agda-2.6.4-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)))))

data WhereDeclarations Source #

Constructors

WhereDecls
Fields whereModule :: Maybe ModuleName whereAnywhere :: Bool is it an ordinary unnamed `where`? whereDecls :: Maybe Declaration The declaration is a `Section`.

Instances

Instances details

DeclaredNames WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => WhereDeclarations -> m Source #
ExprLike WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m WhereDeclarations Source # foldExpr :: FoldExprFn m WhereDeclarations Source # traverseExpr :: TraverseExprFn m WhereDeclarations Source # mapExpr :: (Expr -> Expr) -> WhereDeclarations -> WhereDeclarations Source #
HasRange WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: WhereDeclarations -> Range Source #
KillRange WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT WhereDeclarations Source #
ToConcrete WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs WhereDeclarations Source # Methods toConcrete :: WhereDeclarations -> AbsToCon (ConOfAbs WhereDeclarations) Source # bindToConcrete :: WhereDeclarations -> (ConOfAbs WhereDeclarations -> AbsToCon b) -> AbsToCon b Source #
Null WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Methods empty :: WhereDeclarations Source # null :: WhereDeclarations -> Bool Source #
Generic WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep WhereDeclarations :: Type -> Type Methods from :: WhereDeclarations -> Rep WhereDeclarations x to :: Rep WhereDeclarations x -> WhereDeclarations
Show WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> WhereDeclarations -> ShowS show :: WhereDeclarations -> String showList :: [WhereDeclarations] -> ShowS
NFData WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: WhereDeclarations -> ()
Eq WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: WhereDeclarations -> WhereDeclarations -> Bool (/=) :: WhereDeclarations -> WhereDeclarations -> Bool
type ConOfAbs WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs WhereDeclarations = WhereClause
type Rep WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract type Rep WhereDeclarations = D1 ('MetaData "WhereDeclarations" "Agda.Syntax.Abstract" "Agda-2.6.4-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 #

data SpineLHS Source #

The lhs of a clause in spine view (inside-out). Projection patterns are contained in spLhsPats, represented as ProjP d.

Constructors

SpineLHS
Fields spLhsInfo :: LHSInfo Range. spLhsDefName :: QName Name of function we are defining. spLhsPats :: [NamedArg Pattern] Elimination by pattern, projections, with-patterns.

Instances

Instances details

ExprLike SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m SpineLHS Source # foldExpr :: FoldExprFn m SpineLHS Source # traverseExpr :: TraverseExprFn m SpineLHS Source # mapExpr :: (Expr -> Expr) -> SpineLHS -> SpineLHS Source #
HasRange SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: SpineLHS -> Range Source #
KillRange SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT SpineLHS Source #
ToConcrete SpineLHS Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs SpineLHS Source # Methods toConcrete :: SpineLHS -> AbsToCon (ConOfAbs SpineLHS) Source # bindToConcrete :: SpineLHS -> (ConOfAbs SpineLHS -> AbsToCon b) -> AbsToCon b Source #
Generic SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep SpineLHS :: Type -> Type Methods from :: SpineLHS -> Rep SpineLHS x to :: Rep SpineLHS x -> SpineLHS
Show SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> SpineLHS -> ShowS show :: SpineLHS -> String showList :: [SpineLHS] -> ShowS
NFData SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: SpineLHS -> ()
Eq SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: SpineLHS -> SpineLHS -> Bool (/=) :: SpineLHS -> SpineLHS -> Bool
LHSToSpine Clause SpineClause Source #	Clause instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
LHSToSpine LHS SpineLHS Source #	LHS instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: LHS -> SpineLHS Source # spineToLhs :: SpineLHS -> LHS Source #
type ConOfAbs SpineLHS Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs SpineLHS = LHS
type Rep SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract type Rep SpineLHS = D1 ('MetaData "SpineLHS" "Agda.Syntax.Abstract" "Agda-2.6.4-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]))))

type WithExpr' e = Named BindName (Arg e) Source #

data LHSCore' e Source #

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 lhsDefName :: QName Head `f`. lhsPats :: [NamedArg (Pattern' e)] Applied to patterns `ps`.
LHSProj	Projection.
Fields lhsDestructor :: AmbiguousQName Record projection identifier. lhsFocus :: NamedArg (LHSCore' e) Main argument of projection. lhsPats :: [NamedArg (Pattern' e)] Applied to patterns `ps`.
LHSWith	With patterns.
Fields lhsHead :: LHSCore' e E.g. the `LHSHead`. lhsWithPatterns :: [Arg (Pattern' e)] Applied to with patterns `\| p1 \| ... \| pn`. These patterns are not prefixed with `WithP`! lhsPats :: [NamedArg (Pattern' e)] Applied to patterns `ps`.

Instances

Instances details

ToConcrete LHSCore Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs LHSCore Source # Methods toConcrete :: LHSCore -> AbsToCon (ConOfAbs LHSCore) Source # bindToConcrete :: LHSCore -> (ConOfAbs LHSCore -> AbsToCon b) -> AbsToCon b Source #
Foldable LHSCore' Source #
Instance details Defined in Agda.Syntax.Abstract Methods 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 toList :: LHSCore' a -> [a] null :: LHSCore' a -> Bool length :: LHSCore' a -> Int elem :: Eq a => a -> LHSCore' a -> Bool maximum :: Ord a => LHSCore' a -> a minimum :: Ord a => LHSCore' a -> a sum :: Num a => LHSCore' a -> a product :: Num a => LHSCore' a -> a
Traversable LHSCore' Source #
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> LHSCore' a -> f (LHSCore' b) sequenceA :: Applicative f => LHSCore' (f a) -> f (LHSCore' a) mapM :: Monad m => (a -> m b) -> LHSCore' a -> m (LHSCore' b) sequence :: Monad m => LHSCore' (m a) -> m (LHSCore' a)
Functor LHSCore' Source #
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> LHSCore' a -> LHSCore' b (<$) :: a -> LHSCore' b -> LHSCore' a #
ExprLike a => ExprLike (LHSCore' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods 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 #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LHSCore' e -> Range Source #
KillRange e => KillRange (LHSCore' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (LHSCore' e) Source #
ToAbstract (LHSCore' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (LHSCore' Expr) Source # Methods toAbstract :: LHSCore' Expr -> ScopeM (AbsOfCon (LHSCore' Expr)) Source #
Generic (LHSCore' e) Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep (LHSCore' e) :: Type -> Type Methods from :: LHSCore' e -> Rep (LHSCore' e) x to :: Rep (LHSCore' e) x -> LHSCore' e
Show e => Show (LHSCore' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LHSCore' e -> ShowS show :: LHSCore' e -> String showList :: [LHSCore' e] -> ShowS
NFData e => NFData (LHSCore' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: LHSCore' e -> ()
Eq e => Eq (LHSCore' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LHSCore' e -> LHSCore' e -> Bool (/=) :: LHSCore' e -> LHSCore' e -> Bool
type ConOfAbs LHSCore Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHSCore = Pattern
type AbsOfCon (LHSCore' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (LHSCore' Expr) = LHSCore' Expr
type Rep (LHSCore' e) Source #
Instance details Defined in Agda.Syntax.Abstract type Rep (LHSCore' e) = D1 ('MetaData "LHSCore'" "Agda.Syntax.Abstract" "Agda-2.6.4-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)])))))

type NAPs1 e = List1 (NamedArg (Pattern' e)) Source #

type Patterns = [NamedArg Pattern] Source #

class AnyAbstract a where Source #

Are we in an abstract block?

In that case some definition is abstract.

Methods

anyAbstract :: a -> Bool Source #

Instances

Instances details

AnyAbstract Declaration Source #
Instance details Defined in Agda.Syntax.Abstract Methods anyAbstract :: Declaration -> Bool Source #
AnyAbstract a => AnyAbstract [a] Source #
Instance details 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

Instances details

NameToExpr AbstractName Source #	Turn an `AbstractName` into an expression.
Instance details Defined in Agda.Syntax.Abstract Methods nameToExpr :: AbstractName -> Expr Source #
NameToExpr ResolvedName Source #	Turn a `ResolvedName` into an expression. Assumes name is not `UnknownName`.
Instance details Defined in Agda.Syntax.Abstract Methods nameToExpr :: ResolvedName -> Expr Source #

class SubstExpr a where Source #

Minimal complete definition

Nothing

Methods

substExpr :: [(Name, Expr)] -> a -> a Source #

default substExpr :: (Functor t, SubstExpr b, t b ~ a) => [(Name, Expr)] -> a -> a Source #

Instances

Instances details

SubstExpr Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Expr -> Expr Source #
SubstExpr ModuleName Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName Source #
SubstExpr Name Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name0, Expr)] -> Name -> Name Source #
SubstExpr a => SubstExpr (Arg a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Arg a -> Arg a Source #
SubstExpr a => SubstExpr (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> FieldAssignment' a -> FieldAssignment' a Source #
SubstExpr a => SubstExpr (List1 a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> List1 a -> List1 a Source #
SubstExpr a => SubstExpr (Maybe a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Maybe a -> Maybe a Source #
SubstExpr a => SubstExpr [a] Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> [a] -> [a] Source #
SubstExpr a => SubstExpr (Named name a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Named name a -> Named name a Source #
(SubstExpr a, SubstExpr b) => SubstExpr (Either a b) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Either a b -> Either a b Source #
(SubstExpr a, SubstExpr b) => SubstExpr (a, b) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> (a, b) -> (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.

Instances

Instances details

Show DeclarationSpine Source #
Instance details 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

Instances details

Show ClauseSpine Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ClauseSpine -> ShowS show :: ClauseSpine -> String showList :: [ClauseSpine] -> ShowS

data RHSSpine Source #

Right-hand side spines.

Constructors

RHSS
AbsurdRHSS
WithRHSS (List1 ClauseSpine)
RewriteRHSS RHSSpine WhereDeclarationsSpine

Instances

Instances details

Show RHSSpine Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> RHSSpine -> ShowS show :: RHSSpine -> String showList :: [RHSSpine] -> ShowS

data WhereDeclarationsSpine Source #

Spines corresponding to WhereDeclarations values.

Constructors

WhereDeclsS (Maybe DeclarationSpine)

Instances

Instances details

Show WhereDeclarationsSpine Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> WhereDeclarationsSpine -> ShowS show :: WhereDeclarationsSpine -> String showList :: [WhereDeclarationsSpine] -> ShowS

pattern Def :: QName -> Expr Source #

Pattern synonym for regular Def.

mkBinder_ :: Name -> Binder Source #

mkBinder :: a -> Binder' a Source #

mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr Source #

mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding Source #

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

mkBindName :: Name -> BindName Source #

generalized :: Set QName -> Type -> Type Source #

Smart constructor for Generalized.

initCopyInfo :: ScopeCopyInfo Source #

extractPattern :: Binder' a -> Maybe (Pattern, a) Source #

mkDomainFree :: NamedArg Binder -> LamBinding Source #

defaultTbInfo :: TypedBindingInfo Source #

mkTBind :: Range -> List1 (NamedArg Binder) -> Type -> TypedBinding Source #

mkPi :: ExprInfo -> Telescope -> Type -> Type Source #

noDataDefParams :: DataDefParams Source #

noWhereDecls :: WhereDeclarations 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 #

lambdaLiftExpr :: [Name] -> Expr -> 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.

rhsSpine :: RHS -> RHSSpine Source #

The right-hand side spine corresponding to a right-hand side.

whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine Source #

The spine corresponding to a WhereDeclarations value.

module Agda.Syntax.Abstract.Name

Orphan instances

KillRange Suffix Source #
Instance details Methods killRange :: KillRangeT Suffix Source #

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