Safe Haskell | None |
---|---|
Language | Haskell2010 |
Preprocess Declaration
s, producing NiceDeclaration
s.
- 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.
- 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 Name (Arg Expr)
- | PrimitiveFunction Range Access IsAbstract Name Expr
- | NiceMutual Range TerminationCheck PositivityCheck [NiceDeclaration]
- | NiceModule Range Access IsAbstract QName Telescope [Declaration]
- | NiceModuleMacro Range Access Name ModuleApplication OpenShortHand ImportDirective
- | NiceOpen Range QName ImportDirective
- | NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
- | NicePragma Range Pragma
- | NiceRecSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
- | NiceDataSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
- | NiceFunClause Range Access IsAbstract TerminationCheck Catchall Declaration
- | FunSig Range Access IsAbstract IsInstance IsMacro ArgInfo TerminationCheck Name Expr
- | FunDef Range [Declaration] IsAbstract IsInstance TerminationCheck Name [Clause]
- | NiceDataDef Range Origin IsAbstract PositivityCheck UniverseCheck Name [LamBinding] [NiceConstructor]
- | NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] [Declaration]
- | NicePatternSyn Range Name [Arg Name] Pattern
- | NiceGeneralize Range Access ArgInfo Name Expr
- | NiceUnquoteDecl Range Access IsAbstract IsInstance TerminationCheck [Name] Expr
- | NiceUnquoteDef Range Access IsAbstract TerminationCheck [Name] Expr
- type NiceConstructor = NiceTypeSignature
- type NiceTypeSignature = NiceDeclaration
- data Clause = Clause Name Catchall LHS RHS WhereClause [Clause]
- data DeclarationException
- = MultipleEllipses Pattern
- | InvalidName Name
- | DuplicateDefinition Name
- | MissingWithClauses Name LHS
- | WrongDefinition Name DataRecOrFun DataRecOrFun
- | Codata Range
- | DeclarationPanic String
- | WrongContentBlock KindOfBlock Range
- | AmbiguousFunClauses LHS [Name]
- | InvalidMeasureMutual Range
- | UnquoteDefRequiresSignature [Name]
- | BadMacroDef NiceDeclaration
- data DeclarationWarning
- = EmptyAbstract Range
- | EmptyInstance Range
- | EmptyMacro Range
- | EmptyMutual Range
- | EmptyPostulate Range
- | EmptyPrivate Range
- | EmptyGeneralize Range
- | EmptyPrimitive Range
- | InvalidCatchallPragma Range
- | InvalidNoPositivityCheckPragma Range
- | InvalidNoUniverseCheckPragma Range
- | InvalidTerminationCheckPragma Range
- | MissingDefinitions [Name]
- | NotAllowedInMutual Range String
- | PolarityPragmasButNotPostulates [Name]
- | PragmaNoTerminationCheck Range
- | PragmaCompiled Range
- | UnknownFixityInMixfixDecl [Name]
- | UnknownNamesInFixityDecl [Name]
- | UnknownNamesInPolarityPragmas [Name]
- | UselessAbstract Range
- | UselessInstance Range
- | UselessPrivate Range
- data Nice a
- runNice :: 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 ...)
Instances
type NiceConstructor = NiceTypeSignature Source #
Only Axiom
s.
type NiceTypeSignature = NiceDeclaration Source #
Only Axiom
s.
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 Clause Source # | |
Defined in Agda.Syntax.Concrete.Definitions gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Clause -> c Clause # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Clause # toConstr :: Clause -> Constr # dataTypeOf :: Clause -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Clause) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause) # gmapT :: (forall b. Data b => b -> b) -> Clause -> Clause # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r # gmapQ :: (forall d. Data d => d -> u) -> Clause -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Clause -> m Clause # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause # | |
Show Clause Source # | |
ToAbstract Clause Clause Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
data DeclarationException Source #
The exception type.
MultipleEllipses Pattern | |
InvalidName Name | |
DuplicateDefinition Name | |
MissingWithClauses Name LHS | |
WrongDefinition Name DataRecOrFun DataRecOrFun | |
Codata Range | |
DeclarationPanic String | |
WrongContentBlock KindOfBlock Range | |
AmbiguousFunClauses LHS [Name] | in a mutual block, a clause could belong to any of the |
InvalidMeasureMutual Range | In a mutual block, all or none need a MEASURE pragma. Range is of mutual block. |
UnquoteDefRequiresSignature [Name] | |
BadMacroDef NiceDeclaration |
Instances
data DeclarationWarning Source #
Non-fatal errors encountered in the Nicifier
EmptyAbstract Range | Empty |
EmptyInstance Range | Empty |
EmptyMacro Range | Empty |
EmptyMutual Range | Empty |
EmptyPostulate Range | Empty |
EmptyPrivate Range | Empty |
EmptyGeneralize Range | Empty |
EmptyPrimitive Range | Empty |
InvalidCatchallPragma Range | A {-# CATCHALL #-} pragma that does not precede a function clause. |
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. |
InvalidTerminationCheckPragma Range | A {-# TERMINATING #-} and {-# NON_TERMINATING #-} pragma that does not apply to any function. |
MissingDefinitions [Name] | |
NotAllowedInMutual Range String | |
PolarityPragmasButNotPostulates [Name] | |
PragmaNoTerminationCheck Range | Pragma |
PragmaCompiled Range |
|
UnknownFixityInMixfixDecl [Name] | |
UnknownNamesInFixityDecl [Name] | |
UnknownNamesInPolarityPragmas [Name] | |
UselessAbstract Range | |
UselessInstance Range | |
UselessPrivate Range |
Instances
Nicifier monad. Preserve the state when throwing an exception.
Instances
Monad Nice Source # | |
Functor Nice Source # | |
Applicative Nice Source # | |
MonadError DeclarationException Nice Source # | |
Defined in Agda.Syntax.Concrete.Definitions throwError :: DeclarationException -> Nice a # catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a # |
runNice :: 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
Declaration
s.
niceHasAbstract :: NiceDeclaration -> Maybe IsAbstract Source #
Has the NiceDeclaration
a field of type IsAbstract
?