| Safe Haskell | None |
|---|---|
| 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 {}
- data InferredMutual = InferredMutual {}
- extendInferredBlock :: NiceDeclaration -> InferredMutual -> InferredMutual
- type InterleavedMutual = Map Name InterleavedDecl
- data InterleavedDecl
- = InterleavedData { }
- | InterleavedFun { }
- type DeclNum = Int
- isInterleavedFun :: InterleavedDecl -> Maybe ()
- isInterleavedData :: InterleavedDecl -> Maybe ()
- interleavedDecl :: Name -> InterleavedDecl -> [(DeclNum, NiceDeclaration)]
- data KindOfBlock
- declName :: NiceDeclaration -> String
- data InMutual
- data DataRecOrFun
- 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
Instances
type NiceConstructor = NiceTypeSignature Source #
Only Axioms.
type NiceTypeSignature = NiceDeclaration Source #
Only Axioms.
One clause in a function definition. There is no guarantee that the LHS
actually declares the Name. We will have to check that later.
Instances
| ToAbstract Clause Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types
| |||||
| Generic Clause Source # | |||||
Defined in Agda.Syntax.Concrete.Definitions.Types Associated Types
| |||||
| Show Clause Source # | |||||
| NFData Clause Source # | |||||
Defined in Agda.Syntax.Concrete.Definitions.Types | |||||
| type AbsOfCon Clause Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |||||
| type Rep Clause Source # | |||||
Defined in Agda.Syntax.Concrete.Definitions.Types type Rep Clause = D1 ('MetaData "Clause" "Agda.Syntax.Concrete.Definitions.Types" "Agda-2.6.4.2-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 | |
Instances
| Monoid MutualChecks Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Types Methods mempty :: MutualChecks # mappend :: MutualChecks -> MutualChecks -> MutualChecks # mconcat :: [MutualChecks] -> MutualChecks # | |
| Semigroup MutualChecks Source # | |
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 | |
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
| |
| InterleavedFun | |
Fields
| |
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 |
|
| InstanceBlock |
|
| FieldBlock |
|
| DataBlock |
|
| ConstructorBlock |
|
Instances
| Show KindOfBlock Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Types Methods showsPrec :: Int -> KindOfBlock -> ShowS # show :: KindOfBlock -> String # showList :: [KindOfBlock] -> ShowS # | |
| Eq KindOfBlock Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Types | |
| Ord KindOfBlock Source # | |
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 #
Constructors
| InMutual | we are nicifying a mutual block |
| NotInMutual | we are nicifying decls not in a mutual block |
data DataRecOrFun Source #
The kind of the forward declaration.
Constructors
| DataName | Name of a data type |
Fields | |
| RecName | Name of a record type |
Fields | |
| FunName TerminationCheck CoverageCheck | Name of a function. |
Instances
| Pretty DataRecOrFun Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Types Methods pretty :: DataRecOrFun -> Doc Source # prettyPrec :: Int -> DataRecOrFun -> Doc Source # prettyList :: [DataRecOrFun] -> Doc Source # | |
| Show DataRecOrFun Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Types Methods showsPrec :: Int -> DataRecOrFun -> ShowS # show :: DataRecOrFun -> String # showList :: [DataRecOrFun] -> ShowS # | |
| Eq DataRecOrFun Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Types | |
isFunName :: DataRecOrFun -> Bool Source #
sameKind :: DataRecOrFun -> DataRecOrFun -> Bool Source #