- data NiceDeclaration
- = Axiom Range Fixity' Access Relevance Name Expr
- | NiceField Range Fixity' Access IsAbstract Name (Arg Expr)
- | PrimitiveFunction Range Fixity' Access IsAbstract Name Expr
- | NiceMutual Range [NiceDeclaration]
- | NiceModule Range Access IsAbstract QName Telescope [Declaration]
- | NiceModuleMacro Range Access IsAbstract 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
- | FunSig Range Fixity' Access Relevance Name Expr
- | FunDef Range [Declaration] Fixity' IsAbstract Name [Clause]
- | DataDef Range Fixity' IsAbstract Name [LamBinding] [NiceConstructor]
- | RecDef Range Fixity' IsAbstract Name (Maybe (ThingWithFixity Name)) [LamBinding] [NiceDeclaration]
- 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
- | NotAllowedInMutual NiceDeclaration
- | UnknownNamesInFixityDecl [Name]
- | Codata Range
- | DeclarationPanic String
- | UselessPrivate Range
- | UselessAbstract Range
- | AmbiguousFunClauses LHS [Name]
- type Nice = StateT NiceEnv (Either DeclarationException)
- runNice :: Nice a -> Either DeclarationException a
- niceDeclarations :: [Declaration] -> Nice [NiceDeclaration]
- notSoNiceDeclarations :: [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.
Axiom Range Fixity' Access Relevance Name Expr | Axioms and functions can be declared irrelevant. |
NiceField Range Fixity' Access IsAbstract Name (Arg Expr) | |
PrimitiveFunction Range Fixity' Access IsAbstract Name Expr | |
NiceMutual Range [NiceDeclaration] | |
NiceModule Range Access IsAbstract QName Telescope [Declaration] | |
NiceModuleMacro Range Access IsAbstract 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 | |
FunSig Range Fixity' Access Relevance Name Expr | |
FunDef Range [Declaration] Fixity' IsAbstract Name [Clause] | block of function clauses (we have seen the type signature before) |
DataDef Range Fixity' IsAbstract Name [LamBinding] [NiceConstructor] | |
RecDef Range Fixity' IsAbstract Name (Maybe (ThingWithFixity Name)) [LamBinding] [NiceDeclaration] |
type NiceConstructor = NiceTypeSignatureSource
Only Axiom
s.
type NiceTypeSignature = NiceDeclarationSource
Only Axiom
s.
data DeclarationException Source
The exception type.
MultipleFixityDecls [(Name, [Fixity'])] | |
MissingDefinition Name | |
MissingWithClauses Name | |
MissingTypeSignature LHS | |
MissingDataSignature 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 |
type Nice = StateT NiceEnv (Either DeclarationException)Source
runNice :: Nice a -> Either DeclarationException aSource
niceDeclarations :: [Declaration] -> Nice [NiceDeclaration]Source