| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Concrete.Definitions
Description
Preprocess Declarations, producing NiceDeclarations.
- Attach fixity and syntax declarations to the definition they refer to.
- Distribute the following attributes to the individual definitions:
abstract,instance,postulate,primitive,private, termination pragmas. - Gather the function clauses belonging to one function definition.
- Expand ellipsis
...in function clauses followingwith. - Infer mutual blocks. A block starts when a lone signature is encountered, and ends when all lone signatures have seen their definition.
- Handle interleaved mutual blocks. In an `interleaved mutual' block we:
- leave the data and fun sigs in place
- classify signatures in
constructorblock based on their return type and group them all as a data def at the position in the block where the first constructor for the data sig in question occured - classify fun clauses based on the declared function used and group them all as a fundef at the position in the block where the first such fun clause appeared
- Report basic well-formedness error, when one of the above transformation fails. When possible, errors should be deferred to the scope checking phase (ConcreteToAbstract), where we are in the TCM and can produce more informative error messages.
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 NiceConstructor = NiceTypeSignature
- type NiceTypeSignature = NiceDeclaration
- data Clause = Clause Name Catchall LHS RHS WhereClause [Clause]
- data DeclarationException = DeclarationException {}
- data DeclarationWarning = DeclarationWarning {}
- data DeclarationWarning'
- = EmptyAbstract Range
- | EmptyConstructor Range
- | EmptyField Range
- | EmptyGeneralize Range
- | EmptyInstance Range
- | EmptyMacro Range
- | EmptyMutual Range
- | EmptyPostulate Range
- | EmptyPrivate Range
- | EmptyPrimitive Range
- | HiddenGeneralize Range
- | InvalidCatchallPragma Range
- | InvalidConstructor Range
- | InvalidConstructorBlock Range
- | InvalidCoverageCheckPragma Range
- | InvalidNoPositivityCheckPragma Range
- | InvalidNoUniverseCheckPragma Range
- | InvalidRecordDirective Range
- | InvalidTerminationCheckPragma Range
- | MissingDeclarations [(Name, Range)]
- | MissingDefinitions [(Name, Range)]
- | NotAllowedInMutual Range String
- | OpenPublicPrivate Range
- | OpenPublicAbstract Range
- | PolarityPragmasButNotPostulates [Name]
- | PragmaNoTerminationCheck Range
- | PragmaCompiled Range
- | SafeFlagEta Range
- | SafeFlagInjective Range
- | SafeFlagNoCoverageCheck Range
- | SafeFlagNoPositivityCheck Range
- | SafeFlagNoUniverseCheck Range
- | SafeFlagNonTerminating Range
- | SafeFlagPolarity Range
- | SafeFlagTerminating Range
- | ShadowingInTelescope (List1 (Name, List2 Range))
- | UnknownFixityInMixfixDecl [Name]
- | UnknownNamesInFixityDecl [Name]
- | UnknownNamesInPolarityPragmas [Name]
- | UselessAbstract Range
- | UselessInstance Range
- | UselessPrivate Range
- unsafeDeclarationWarning :: DeclarationWarning -> Bool
- data Nice a
- data NiceEnv = NiceEnv {}
- runNice :: NiceEnv -> Nice a -> (Either DeclarationException a, NiceWarnings)
- niceDeclarations :: Fixities -> [Declaration] -> Nice [NiceDeclaration]
- notSoNiceDeclarations :: NiceDeclaration -> [Declaration]
- niceHasAbstract :: NiceDeclaration -> Maybe IsAbstract
- type Measure = Name
- declarationWarningName :: DeclarationWarning -> WarningName
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
data DeclarationException Source #
Exception with internal source code callstack
Constructors
| DeclarationException | |
Fields | |
Instances
| HasRange DeclarationException Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Errors Methods getRange :: DeclarationException -> Range Source # | |
| MonadError DeclarationException Nice Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Monad Methods throwError :: DeclarationException -> Nice a # catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a # | |
data DeclarationWarning Source #
Constructors
| DeclarationWarning | |
Fields | |
Instances
data DeclarationWarning' Source #
Non-fatal errors encountered in the Nicifier.
Constructors
| EmptyAbstract Range | Empty |
| EmptyConstructor Range | Empty |
| EmptyField Range | Empty |
| EmptyGeneralize Range | Empty |
| EmptyInstance Range | Empty |
| EmptyMacro Range | Empty |
| EmptyMutual Range | Empty |
| EmptyPostulate Range | Empty |
| EmptyPrivate Range | Empty |
| EmptyPrimitive Range | Empty |
| HiddenGeneralize Range | A |
| InvalidCatchallPragma Range | A {-# CATCHALL #-} pragma that does not precede a function clause. |
| InvalidConstructor Range | Invalid definition in a constructor block |
| InvalidConstructorBlock Range | Invalid constructor block (not inside an interleaved mutual block) |
| InvalidCoverageCheckPragma Range | A {-# NON_COVERING #-} pragma that does not apply to any function. |
| InvalidNoPositivityCheckPragma Range | A {-# NO_POSITIVITY_CHECK #-} pragma that does not apply to any data or record type. |
| InvalidNoUniverseCheckPragma Range | A {-# NO_UNIVERSE_CHECK #-} pragma that does not apply to a data or record type. |
| InvalidRecordDirective Range | A record directive outside of a record / below existing fields. |
| InvalidTerminationCheckPragma Range | A {-# TERMINATING #-} and {-# NON_TERMINATING #-} pragma that does not apply to any function. |
| MissingDeclarations [(Name, Range)] | Definitions (e.g. constructors or functions) without a declaration. |
| MissingDefinitions [(Name, Range)] | Declarations (e.g. type signatures) without a definition. |
| NotAllowedInMutual Range String | |
| OpenPublicPrivate Range |
|
| OpenPublicAbstract Range |
|
| PolarityPragmasButNotPostulates [Name] | |
| PragmaNoTerminationCheck Range | Pragma |
| PragmaCompiled Range |
|
| SafeFlagEta Range |
|
| SafeFlagInjective Range |
|
| SafeFlagNoCoverageCheck Range |
|
| SafeFlagNoPositivityCheck Range |
|
| SafeFlagNoUniverseCheck Range |
|
| SafeFlagNonTerminating Range |
|
| SafeFlagPolarity Range |
|
| SafeFlagTerminating Range |
|
| ShadowingInTelescope (List1 (Name, List2 Range)) | |
| UnknownFixityInMixfixDecl [Name] | |
| UnknownNamesInFixityDecl [Name] | |
| UnknownNamesInPolarityPragmas [Name] | |
| UselessAbstract Range |
|
| UselessInstance Range |
|
| UselessPrivate Range |
|
Instances
unsafeDeclarationWarning :: DeclarationWarning -> Bool Source #
Nicifier warnings turned into errors in --safe mode.
Nicifier monad. Preserve the state when throwing an exception.
Instances
| Applicative Nice Source # | |
| Functor Nice Source # | |
| Monad Nice Source # | |
| MonadError DeclarationException Nice Source # | |
Defined in Agda.Syntax.Concrete.Definitions.Monad Methods throwError :: DeclarationException -> Nice a # catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a # | |
| MonadReader NiceEnv Nice Source # | |
| MonadState NiceState Nice Source # | |
| Null a => Null (Nice a) Source # | |
Nicifier parameters.
Constructors
| NiceEnv | |
Fields
| |
runNice :: NiceEnv -> Nice a -> (Either DeclarationException a, NiceWarnings) Source #
Run a Nicifier computation, return result and warnings (in chronological order).
niceDeclarations :: Fixities -> [Declaration] -> Nice [NiceDeclaration] Source #
Main. Fixities (or more precisely syntax declarations) are needed when grouping function clauses.
notSoNiceDeclarations :: NiceDeclaration -> [Declaration] Source #
(Approximately) convert a NiceDeclaration back to a list of
Declarations.
niceHasAbstract :: NiceDeclaration -> Maybe IsAbstract Source #
Has the NiceDeclaration a field of type IsAbstract?