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 Fixity' Access IsAbstract IsInstance ArgInfo (Maybe [Occurrence]) Name Expr
- | NiceField Range Fixity' Access IsAbstract IsInstance Name (Arg Expr)
- | PrimitiveFunction Range Fixity' 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 Fixity' Access IsAbstract PositivityCheck Name [LamBinding] Expr
- | NiceDataSig Range Fixity' Access IsAbstract PositivityCheck Name [LamBinding] Expr
- | NiceFunClause Range Access IsAbstract TerminationCheck Catchall Declaration
- | FunSig Range Fixity' Access IsAbstract IsInstance IsMacro ArgInfo TerminationCheck Name Expr
- | FunDef Range [Declaration] Fixity' IsAbstract IsInstance TerminationCheck Name [Clause]
- | DataDef Range Fixity' IsAbstract PositivityCheck Name [LamBinding] [NiceConstructor]
- | RecDef Range Fixity' IsAbstract PositivityCheck Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (ThingWithFixity Name, IsInstance)) [LamBinding] [NiceDeclaration]
- | NicePatternSyn Range Fixity' Name [Arg Name] Pattern
- | NiceUnquoteDecl Range [Fixity'] Access IsAbstract IsInstance TerminationCheck [Name] Expr
- | NiceUnquoteDef Range [Fixity'] Access IsAbstract TerminationCheck [Name] Expr
- type NiceConstructor = NiceTypeSignature
- type NiceTypeSignature = NiceDeclaration
- data Clause = Clause Name Catchall LHS RHS WhereClause [Clause]
- data DeclarationException
- = MultipleFixityDecls [(Name, [Fixity'])]
- | MultiplePolarityPragmas [Name]
- | MultipleEllipses Pattern
- | InvalidName Name
- | DuplicateDefinition Name
- | MissingDefinition Name
- | MissingWithClauses Name
- | WrongDefinition Name DataRecOrFun DataRecOrFun
- | WrongParameters Name Params Params
- | NotAllowedInMutual NiceDeclaration
- | Codata Range
- | DeclarationPanic String
- | WrongContentBlock KindOfBlock Range
- | AmbiguousFunClauses LHS [Name]
- | InvalidMeasureMutual Range
- | PragmaNoTerminationCheck Range
- | UnquoteDefRequiresSignature [Name]
- | BadMacroDef NiceDeclaration
- data DeclarationWarning
- = UnknownNamesInFixityDecl [Name]
- | UnknownFixityInMixfixDecl [Name]
- | UnknownNamesInPolarityPragmas [Name]
- | PolarityPragmasButNotPostulates [Name]
- | UselessPrivate Range
- | UselessAbstract Range
- | UselessInstance Range
- | EmptyMutual Range
- | EmptyAbstract Range
- | EmptyPrivate Range
- | EmptyInstance Range
- | EmptyMacro Range
- | EmptyPostulate Range
- | InvalidTerminationCheckPragma Range
- | InvalidNoPositivityCheckPragma Range
- | InvalidCatchallPragma Range
- data Nice a
- runNice :: Nice a -> (Either DeclarationException a, NiceWarnings)
- niceDeclarations :: [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.
MultipleFixityDecls [(Name, [Fixity'])] | |
MultiplePolarityPragmas [Name] | |
MultipleEllipses Pattern | |
InvalidName Name | |
DuplicateDefinition Name | |
MissingDefinition Name | |
MissingWithClauses Name | |
WrongDefinition Name DataRecOrFun DataRecOrFun | |
WrongParameters Name Params Params |
|
NotAllowedInMutual NiceDeclaration | |
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. |
PragmaNoTerminationCheck Range | |
UnquoteDefRequiresSignature [Name] | |
BadMacroDef NiceDeclaration |
Instances
data DeclarationWarning Source #
Non-fatal errors encountered in the Nicifier
UnknownNamesInFixityDecl [Name] | |
UnknownFixityInMixfixDecl [Name] | |
UnknownNamesInPolarityPragmas [Name] | |
PolarityPragmasButNotPostulates [Name] | |
UselessPrivate Range | |
UselessAbstract Range | |
UselessInstance Range | |
EmptyMutual Range | Empty |
EmptyAbstract Range | Empty |
EmptyPrivate Range | Empty |
EmptyInstance Range | Empty |
EmptyMacro Range | Empty |
EmptyPostulate Range | Empty |
InvalidTerminationCheckPragma Range | |
InvalidNoPositivityCheckPragma Range | A {--} pragma that does not apply to any data or record type. |
InvalidCatchallPragma 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 :: [Declaration] -> Nice [NiceDeclaration] Source #
Main.
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
?