Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Syntax.Concrete.Definitions.Types

Synopsis

data NiceDeclaration
- = Axiom Range Access IsAbstract IsInstance ArgInfo Name Expr
- | NiceField Range Access IsAbstract IsInstance TacticAttribute Name (Arg Expr)
- | PrimitiveFunction Range Access IsAbstract Name (Arg Expr)
- | NiceMutual Range TerminationCheck CoverageCheck PositivityCheck [NiceDeclaration]
- | NiceModule Range Access IsAbstract Erased QName Telescope [Declaration]
- | NiceModuleMacro Range Access Erased Name ModuleApplication OpenShortHand ImportDirective
- | NiceOpen Range QName ImportDirective
- | NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
- | NicePragma Range Pragma
- | NiceRecSig Range Erased Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
- | NiceDataSig Range Erased Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
- | NiceFunClause Range Access IsAbstract TerminationCheck CoverageCheck Catchall Declaration
- | FunSig Range Access IsAbstract IsInstance IsMacro ArgInfo TerminationCheck CoverageCheck Name Expr
- | FunDef Range [Declaration] IsAbstract IsInstance TerminationCheck CoverageCheck Name [Clause]
- | NiceDataDef Range Origin IsAbstract PositivityCheck UniverseCheck Name [LamBinding] [NiceConstructor]
- | NiceLoneConstructor Range [NiceConstructor]
- | NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name RecordDirectives [LamBinding] [Declaration]
- | NicePatternSyn Range Access Name [Arg Name] Pattern
- | NiceGeneralize Range Access ArgInfo TacticAttribute Name Expr
- | NiceUnquoteDecl Range Access IsAbstract IsInstance TerminationCheck CoverageCheck [Name] Expr
- | NiceUnquoteDef Range Access IsAbstract TerminationCheck CoverageCheck [Name] Expr
- | NiceUnquoteData Range Access IsAbstract PositivityCheck UniverseCheck Name [Name] Expr
- | NiceOpaque Range [QName] [NiceDeclaration]
type TerminationCheck = TerminationCheck Measure
type Measure = Name
type Catchall = Bool
type NiceConstructor = NiceTypeSignature
type NiceTypeSignature = NiceDeclaration
data Clause = Clause Name Catchall LHS RHS WhereClause [Clause]
data MutualChecks = MutualChecks {
- mutualTermination :: [TerminationCheck]
- mutualCoverage :: [CoverageCheck]
- mutualPositivity :: [PositivityCheck]
}
data InferredMutual = InferredMutual {
- inferredChecks :: MutualChecks
- inferredBlock :: [NiceDeclaration]
- inferredLeftovers :: [NiceDeclaration]
}
extendInferredBlock :: NiceDeclaration -> InferredMutual -> InferredMutual
type InterleavedMutual = Map Name InterleavedDecl
data InterleavedDecl
- = InterleavedData {
  - interleavedDeclNum :: DeclNum
  - interleavedDeclSig :: NiceDeclaration
  - interleavedDataCons :: Maybe (DeclNum, List1 [NiceConstructor])
  }
- | InterleavedFun {
  - interleavedDeclNum :: DeclNum
  - interleavedDeclSig :: NiceDeclaration
  - interleavedFunClauses :: Maybe (DeclNum, List1 ([Declaration], [Clause]))
  }
type DeclNum = Int
isInterleavedFun :: InterleavedDecl -> Maybe ()
isInterleavedData :: InterleavedDecl -> Maybe ()
interleavedDecl :: Name -> InterleavedDecl -> [(DeclNum, NiceDeclaration)]
data KindOfBlock
- = PostulateBlock
- | PrimitiveBlock
- | InstanceBlock
- | FieldBlock
- | DataBlock
- | ConstructorBlock
declName :: NiceDeclaration -> String
data InMutual
- = InMutual
- | NotInMutual
data DataRecOrFun
- = DataName {
  - _kindPosCheck :: PositivityCheck
  - _kindUniCheck :: UniverseCheck
  }
- | RecName {
  - _kindPosCheck :: PositivityCheck
  - _kindUniCheck :: UniverseCheck
  }
- | FunName TerminationCheck CoverageCheck
isFunName :: DataRecOrFun -> Bool
sameKind :: DataRecOrFun -> DataRecOrFun -> Bool
terminationCheck :: DataRecOrFun -> TerminationCheck
coverageCheck :: DataRecOrFun -> CoverageCheck
positivityCheck :: DataRecOrFun -> PositivityCheck
mutualChecks :: DataRecOrFun -> MutualChecks
universeCheck :: DataRecOrFun -> UniverseCheck

Documentation

data NiceDeclaration Source #

The nice declarations. No fixity declarations and function definitions are contained in a single constructor instead of spread out between type signatures and clauses. The private, postulate, abstract and instance modifiers have been distributed to the individual declarations.

Observe the order of components:

Range Fixity' Access IsAbstract IsInstance TerminationCheck PositivityCheck

further attributes

(Q)Name

content (Expr, Declaration ...)

Constructors

Axiom Range Access IsAbstract IsInstance ArgInfo Name Expr	`IsAbstract` argument: We record whether a declaration was made in an `abstract` block. `ArgInfo` argument: Axioms and functions can be declared irrelevant. (`Hiding` should be `NotHidden`.)
NiceField Range Access IsAbstract IsInstance TacticAttribute Name (Arg Expr)
PrimitiveFunction Range Access IsAbstract Name (Arg Expr)
NiceMutual Range TerminationCheck CoverageCheck PositivityCheck [NiceDeclaration]
NiceModule Range Access IsAbstract Erased QName Telescope [Declaration]
NiceModuleMacro Range Access Erased Name ModuleApplication OpenShortHand ImportDirective
NiceOpen Range QName ImportDirective
NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
NicePragma Range Pragma
NiceRecSig Range Erased Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
NiceDataSig Range Erased Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
NiceFunClause Range Access IsAbstract TerminationCheck CoverageCheck Catchall Declaration	An uncategorized function clause, could be a function clause without type signature or a pattern lhs (e.g. for irrefutable let). The `Declaration` is the actual `FunClause`.
FunSig Range Access IsAbstract IsInstance IsMacro ArgInfo TerminationCheck CoverageCheck Name Expr
FunDef Range [Declaration] IsAbstract IsInstance TerminationCheck CoverageCheck Name [Clause]	Block of function clauses (we have seen the type signature before). The `Declaration`s are the original declarations that were processed into this `FunDef` and are only used in `notSoNiceDeclaration`. Andreas, 2017-01-01: Because of issue #2372, we add `IsInstance` here. An alias should know that it is an instance.
NiceDataDef Range Origin IsAbstract PositivityCheck UniverseCheck Name [LamBinding] [NiceConstructor]
NiceLoneConstructor Range [NiceConstructor]
NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name RecordDirectives [LamBinding] [Declaration]	`(Maybe Range)` gives range of the 'pattern' declaration.
NicePatternSyn Range Access Name [Arg Name] Pattern
NiceGeneralize Range Access ArgInfo TacticAttribute Name Expr
NiceUnquoteDecl Range Access IsAbstract IsInstance TerminationCheck CoverageCheck [Name] Expr
NiceUnquoteDef Range Access IsAbstract TerminationCheck CoverageCheck [Name] Expr
NiceUnquoteData Range Access IsAbstract PositivityCheck UniverseCheck Name [Name] Expr
NiceOpaque Range [QName] [NiceDeclaration]

Instances

Instances details

Pretty NiceDeclaration Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods pretty :: NiceDeclaration -> Doc Source # prettyPrec :: Int -> NiceDeclaration -> Doc Source # prettyList :: [NiceDeclaration] -> Doc Source #
HasRange NiceDeclaration Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods getRange :: NiceDeclaration -> Range Source #
ToAbstract NiceDeclaration Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon NiceDeclaration Source # Methods toAbstract :: NiceDeclaration -> ScopeM (AbsOfCon NiceDeclaration) Source #
Generic NiceDeclaration Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Associated Types type Rep NiceDeclaration :: Type -> Type Methods from :: NiceDeclaration -> Rep NiceDeclaration x to :: Rep NiceDeclaration x -> NiceDeclaration
Show NiceDeclaration Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods showsPrec :: Int -> NiceDeclaration -> ShowS show :: NiceDeclaration -> String showList :: [NiceDeclaration] -> ShowS
NFData NiceDeclaration Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods rnf :: NiceDeclaration -> ()
type AbsOfCon NiceDeclaration Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon NiceDeclaration = Declaration
type Rep NiceDeclaration Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types type Rep NiceDeclaration = D1 ('MetaData "NiceDeclaration" "Agda.Syntax.Concrete.Definitions.Types" "Agda-2.6.3.20230930-inplace" 'False) ((((C1 ('MetaCons "Axiom" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "NiceField" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttribute)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Expr)))))) :+: (C1 ('MetaCons "PrimitiveFunction" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Expr))))) :+: (C1 ('MetaCons "NiceMutual" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NiceDeclaration])))) :+: C1 ('MetaCons "NiceModule" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :: ((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 Telescope) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration]))))))) :+: ((C1 ('MetaCons "NiceModuleMacro" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased))) :: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpenShortHand) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: (C1 ('MetaCons "NiceOpen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: C1 ('MetaCons "NiceImport" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe AsName)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpenShortHand) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))))) :+: (C1 ('MetaCons "NicePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pragma)) :+: (C1 ('MetaCons "NiceRecSig" '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 Access) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: C1 ('MetaCons "NiceDataSig" '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 Access) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))))))) :+: (((C1 ('MetaCons "NiceFunClause" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Catchall) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Declaration)))) :+: (C1 ('MetaCons "FunSig" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsMacro)))) :: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: C1 ('MetaCons "FunDef" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance))) :: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause])))))) :+: (C1 ('MetaCons "NiceDataDef" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Origin)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck))) :: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NiceConstructor])))) :+: (C1 ('MetaCons "NiceLoneConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NiceConstructor])) :+: C1 ('MetaCons "NiceRecDef" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Origin)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck))) :: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordDirectives) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))))))) :+: ((C1 ('MetaCons "NicePatternSyn" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg Name]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern)))) :+: (C1 ('MetaCons "NiceGeneralize" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttribute) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "NiceUnquoteDecl" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance))) :: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))) :+: (C1 ('MetaCons "NiceUnquoteDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "NiceUnquoteData" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck))) :: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "NiceOpaque" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NiceDeclaration]))))))))

type TerminationCheck = TerminationCheck Measure Source #

type Measure = Name Source #

Termination measure is, for now, a variable name.

type Catchall = Bool Source #

type NiceConstructor = NiceTypeSignature Source #

Only Axioms.

type NiceTypeSignature = NiceDeclaration Source #

Only Axioms.

data Clause Source #

One clause in a function definition. There is no guarantee that the LHS actually declares the Name. We will have to check that later.

Constructors

Clause Name Catchall LHS RHS WhereClause [Clause]

Instances

Instances details

ToAbstract Clause Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon Clause Source # Methods toAbstract :: Clause -> ScopeM (AbsOfCon Clause) Source #
Generic Clause Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Associated Types type Rep Clause :: Type -> Type Methods from :: Clause -> Rep Clause x to :: Rep Clause x -> Clause
Show Clause Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods showsPrec :: Int -> Clause -> ShowS show :: Clause -> String showList :: [Clause] -> ShowS
NFData Clause Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods rnf :: Clause -> ()
type AbsOfCon Clause Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon Clause = Clause
type Rep Clause Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types type Rep Clause = D1 ('MetaData "Clause" "Agda.Syntax.Concrete.Definitions.Types" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Catchall) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHS))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereClause) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause])))))

data MutualChecks Source #

When processing a mutual block we collect the various checks present in the block before combining them.

Constructors

MutualChecks
Fields mutualTermination :: [TerminationCheck] mutualCoverage :: [CoverageCheck] mutualPositivity :: [PositivityCheck]

Instances

Instances details

Monoid MutualChecks Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods mempty :: MutualChecks mappend :: MutualChecks -> MutualChecks -> MutualChecks mconcat :: [MutualChecks] -> MutualChecks
Semigroup MutualChecks Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods (<>) :: MutualChecks -> MutualChecks -> MutualChecks # sconcat :: NonEmpty MutualChecks -> MutualChecks stimes :: Integral b => b -> MutualChecks -> MutualChecks

data InferredMutual Source #

In an inferred mutual block we keep accumulating nice declarations until all of the lone signatures have an attached definition. The type is therefore a bit span-like: we return an initial segment (the inferred mutual block) together with leftovers.

Constructors

InferredMutual
Fields inferredChecks :: MutualChecks inferredBlock :: [NiceDeclaration] inferredLeftovers :: [NiceDeclaration]

extendInferredBlock :: NiceDeclaration -> InferredMutual -> InferredMutual Source #

type InterleavedMutual = Map Name InterleavedDecl Source #

In an `interleaved mutual' block we collect the data signatures, function signatures, as well as their associated constructors and function clauses respectively. Each signature is given a position in the block (from 0 onwards) and each set of constructor / clauses is given a *distinct* one. This allows for interleaved forward declarations similar to what one gets in a new-style mutual block.

data InterleavedDecl Source #

Constructors

InterleavedData
Fields interleavedDeclNum :: DeclNum Internal number of the data signature. interleavedDeclSig :: NiceDeclaration The data signature. interleavedDataCons :: Maybe (DeclNum, List1 [NiceConstructor]) Constructors associated to the data signature.
InterleavedFun
Fields interleavedDeclNum :: DeclNum Internal number of the data signature. interleavedDeclSig :: NiceDeclaration The data signature. interleavedFunClauses :: Maybe (DeclNum, List1 ([Declaration], [Clause])) Function clauses associated to the function signature.

type DeclNum = Int Source #

Numbering declarations in an interleaved mutual block.

isInterleavedFun :: InterleavedDecl -> Maybe () Source #

isInterleavedData :: InterleavedDecl -> Maybe () Source #

interleavedDecl :: Name -> InterleavedDecl -> [(DeclNum, NiceDeclaration)] Source #

data KindOfBlock Source #

Several declarations expect only type signatures as sub-declarations. These are:

Constructors

PostulateBlock	postulate
PrimitiveBlock	`primitive`. Ensured by parser.
InstanceBlock	`instance`. Actually, here all kinds of sub-declarations are allowed a priori.
FieldBlock	`field`. Ensured by parser.
DataBlock	`data ... where`. Here we got a bad error message for Agda-2.5 (Issue 1698).
ConstructorBlock	`constructor`, in `interleaved mutual`.

Instances

Instances details

Show KindOfBlock Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods showsPrec :: Int -> KindOfBlock -> ShowS show :: KindOfBlock -> String showList :: [KindOfBlock] -> ShowS
Eq KindOfBlock Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods (==) :: KindOfBlock -> KindOfBlock -> Bool (/=) :: KindOfBlock -> KindOfBlock -> Bool
Ord KindOfBlock Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods compare :: KindOfBlock -> KindOfBlock -> Ordering (<) :: KindOfBlock -> KindOfBlock -> Bool (<=) :: KindOfBlock -> KindOfBlock -> Bool (>) :: KindOfBlock -> KindOfBlock -> Bool (>=) :: KindOfBlock -> KindOfBlock -> Bool max :: KindOfBlock -> KindOfBlock -> KindOfBlock min :: KindOfBlock -> KindOfBlock -> KindOfBlock

declName :: NiceDeclaration -> String Source #

data InMutual Source #

Constructors

InMutual	we are nicifying a mutual block
NotInMutual	we are nicifying decls not in a mutual block

Instances

Instances details

Show InMutual Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods showsPrec :: Int -> InMutual -> ShowS show :: InMutual -> String showList :: [InMutual] -> ShowS
Eq InMutual Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods (==) :: InMutual -> InMutual -> Bool (/=) :: InMutual -> InMutual -> Bool

data DataRecOrFun Source #

The kind of the forward declaration.

Constructors

DataName	Name of a data type
Fields _kindPosCheck :: PositivityCheck _kindUniCheck :: UniverseCheck
RecName	Name of a record type
Fields _kindPosCheck :: PositivityCheck _kindUniCheck :: UniverseCheck
FunName TerminationCheck CoverageCheck	Name of a function.

Instances

Instances details

Pretty DataRecOrFun Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods pretty :: DataRecOrFun -> Doc Source # prettyPrec :: Int -> DataRecOrFun -> Doc Source # prettyList :: [DataRecOrFun] -> Doc Source #
Show DataRecOrFun Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods showsPrec :: Int -> DataRecOrFun -> ShowS show :: DataRecOrFun -> String showList :: [DataRecOrFun] -> ShowS
Eq DataRecOrFun Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods (==) :: DataRecOrFun -> DataRecOrFun -> Bool (/=) :: DataRecOrFun -> DataRecOrFun -> Bool

isFunName :: DataRecOrFun -> Bool Source #

sameKind :: DataRecOrFun -> DataRecOrFun -> Bool Source #

terminationCheck :: DataRecOrFun -> TerminationCheck Source #

coverageCheck :: DataRecOrFun -> CoverageCheck Source #

positivityCheck :: DataRecOrFun -> PositivityCheck Source #

mutualChecks :: DataRecOrFun -> MutualChecks Source #

universeCheck :: DataRecOrFun -> UniverseCheck Source #