Safe Haskell | None |
---|---|
Language | Haskell98 |
- data NiceDeclaration
- = Axiom Range Fixity' Access ArgInfo Name Expr
- | NiceField Range Fixity' Access IsAbstract Name (Arg Expr)
- | PrimitiveFunction Range Fixity' Access IsAbstract Name Expr
- | NiceMutual Range TerminationCheck [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 Name [LamBinding] Expr
- | NiceDataSig Range Fixity' Access Name [LamBinding] Expr
- | NiceFunClause Range Access IsAbstract TerminationCheck Declaration
- | FunSig Range Fixity' Access ArgInfo TerminationCheck Name Expr
- | FunDef Range [Declaration] Fixity' IsAbstract TerminationCheck Name [Clause]
- | DataDef Range Fixity' IsAbstract Name [LamBinding] [NiceConstructor]
- | RecDef Range Fixity' IsAbstract Name (Maybe (Ranged Induction)) (Maybe (ThingWithFixity Name)) [LamBinding] [NiceDeclaration]
- | NicePatternSyn Range Fixity' Name [Arg Name] Pattern
- type NiceConstructor = NiceTypeSignature
- type NiceTypeSignature = NiceDeclaration
- data Clause = Clause Name LHS RHS WhereClause [Clause]
- data DeclarationException
- = MultipleFixityDecls [(Name, [Fixity'])]
- | MissingDefinition Name
- | MissingWithClauses Name
- | MissingTypeSignature LHS
- | MissingDataSignature Name
- | WrongDefinition Name DataRecOrFun DataRecOrFun
- | WrongParameters Name
- | NotAllowedInMutual NiceDeclaration
- | UnknownNamesInFixityDecl [Name]
- | Codata Range
- | DeclarationPanic String
- | UselessPrivate Range
- | UselessAbstract Range
- | AmbiguousFunClauses LHS [Name]
- | InvalidNoTerminationCheckPragma Range
- type Nice = StateT NiceEnv (Either DeclarationException)
- runNice :: Nice a -> Either DeclarationException a
- niceDeclarations :: [Declaration] -> Nice [NiceDeclaration]
- notSoNiceDeclaration :: NiceDeclaration -> Declaration
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
, and abstract
modifiers have been distributed to the individual declarations.
type NiceConstructor = NiceTypeSignature Source
Only Axiom
s.
type NiceTypeSignature = NiceDeclaration Source
Only Axiom
s.
data DeclarationException Source
The exception type.
MultipleFixityDecls [(Name, [Fixity'])] | |
MissingDefinition Name | |
MissingWithClauses Name | |
MissingTypeSignature LHS | |
MissingDataSignature Name | |
WrongDefinition Name DataRecOrFun DataRecOrFun | |
WrongParameters Name | |
NotAllowedInMutual NiceDeclaration | |
UnknownNamesInFixityDecl [Name] | |
Codata Range | |
DeclarationPanic String | |
UselessPrivate Range | |
UselessAbstract Range | |
AmbiguousFunClauses LHS [Name] | in a mutual block, a clause could belong to any of the |
InvalidNoTerminationCheckPragma Range |
type Nice = StateT NiceEnv (Either DeclarationException) Source
runNice :: Nice a -> Either DeclarationException a Source
niceDeclarations :: [Declaration] -> Nice [NiceDeclaration] Source