Safe Haskell	None
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 following with.
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 constructor block 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
type NiceConstructor = NiceTypeSignature
type NiceTypeSignature = NiceDeclaration
data Clause = Clause Name Catchall LHS RHS WhereClause [Clause]
data DeclarationException = DeclarationException {
- deLocation :: CallStack
- deException :: DeclarationException'
}
data DeclarationWarning = DeclarationWarning {
- dwLocation :: CallStack
- dwWarning :: 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 {
- safeButNotBuiltin :: Bool
}
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

Axiom Range Access IsAbstract IsInstance ArgInfo Name Expr	`IsAbstract` argument: We record whether a declaration was made in an `abstract` block. `ArgInfo` argument: Axioms and functions can be declared irrelevant. (`Hiding` should be `NotHidden`.)
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	An uncategorized function clause, could be a function clause without type signature or a pattern lhs (e.g. for irrefutable let). The `Declaration` is the actual `FunClause`.
FunSig Range Access IsAbstract IsInstance IsMacro ArgInfo TerminationCheck CoverageCheck Name Expr
FunDef Range [Declaration] IsAbstract IsInstance TerminationCheck CoverageCheck Name [Clause]	Block of function clauses (we have seen the type signature before). The `Declaration`s are the original declarations that were processed into this `FunDef` and are only used in `notSoNiceDeclaration`. Andreas, 2017-01-01: Because of issue #2372, we add `IsInstance` here. An alias should know that it is an instance.
NiceDataDef Range Origin IsAbstract PositivityCheck UniverseCheck Name [LamBinding] [NiceConstructor]
NiceLoneConstructor Range [NiceConstructor]
NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name RecordDirectives [LamBinding] [Declaration]	`(Maybe Range)` gives range of the 'pattern' 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]

Instances

Instances details

Pretty NiceDeclaration Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

pretty :: NiceDeclaration -> Doc Source #

prettyPrec :: Int -> NiceDeclaration -> Doc Source #

prettyList :: [NiceDeclaration] -> Doc Source #

HasRange NiceDeclaration Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

getRange :: NiceDeclaration -> Range Source #

ToAbstract NiceDeclaration Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon NiceDeclaration
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon NiceDeclaration = Declaration

Methods

toAbstract :: NiceDeclaration -> ScopeM (AbsOfCon NiceDeclaration) Source #

Generic NiceDeclaration Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Associated Types

type Rep NiceDeclaration

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

from :: NiceDeclaration -> Rep NiceDeclaration x #

to :: Rep NiceDeclaration x -> NiceDeclaration #

Show NiceDeclaration Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

showsPrec :: Int -> NiceDeclaration -> ShowS #

show :: NiceDeclaration -> String #

showList :: [NiceDeclaration] -> ShowS #

NFData NiceDeclaration Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

rnf :: NiceDeclaration -> () #

type AbsOfCon NiceDeclaration Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon NiceDeclaration = Declaration

type Rep NiceDeclaration Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

type NiceConstructor = NiceTypeSignature Source #

Only Axioms.

type NiceTypeSignature = NiceDeclaration Source #

Only Axioms.

data Clause Source #

One clause in a function definition. There is no guarantee that the LHS actually declares the Name. We will have to check that later.

Constructors

Clause Name Catchall LHS RHS WhereClause [Clause]

Instances

Instances details

ToAbstract Clause Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Clause
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon Clause = Clause

Methods

toAbstract :: Clause -> ScopeM (AbsOfCon Clause) Source #

Generic Clause Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Associated Types

type Rep Clause

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

type Rep Clause = D1 ('MetaData "Clause" "Agda.Syntax.Concrete.Definitions.Types" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Catchall) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHS))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereClause) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause])))))

Methods

from :: Clause -> Rep Clause x #

to :: Rep Clause x -> Clause #

Show Clause Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

showsPrec :: Int -> Clause -> ShowS #

show :: Clause -> String #

showList :: [Clause] -> ShowS #

NFData Clause Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

rnf :: Clause -> () #

type AbsOfCon Clause Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon Clause = Clause

type Rep Clause Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

type Rep Clause = D1 ('MetaData "Clause" "Agda.Syntax.Concrete.Definitions.Types" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Catchall) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHS))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereClause) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause])))))

data DeclarationException Source #

Exception with internal source code callstack

Constructors

DeclarationException
Fields deLocation :: CallStack deException :: DeclarationException'

Instances

Instances details

HasRange DeclarationException Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods getRange :: DeclarationException -> Range Source #
MonadError DeclarationException Nice Source #
Instance details 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 dwLocation :: CallStack dwWarning :: DeclarationWarning'

Instances

Instances details

Pretty DeclarationWarning Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

pretty :: DeclarationWarning -> Doc Source #

prettyPrec :: Int -> DeclarationWarning -> Doc Source #

prettyList :: [DeclarationWarning] -> Doc Source #

HasRange DeclarationWarning Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationWarning -> Range Source #

EmbPrj DeclarationWarning Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: DeclarationWarning -> S Int32 Source #

icod_ :: DeclarationWarning -> S Int32 Source #

value :: Int32 -> R DeclarationWarning Source #

Generic DeclarationWarning Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Associated Types

type Rep DeclarationWarning

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

type Rep DeclarationWarning = D1 ('MetaData "DeclarationWarning" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "DeclarationWarning" 'PrefixI 'True) (S1 ('MetaSel ('Just "dwLocation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CallStack) :*: S1 ('MetaSel ('Just "dwWarning") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeclarationWarning')))

Methods

from :: DeclarationWarning -> Rep DeclarationWarning x #

to :: Rep DeclarationWarning x -> DeclarationWarning #

Show DeclarationWarning Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

showsPrec :: Int -> DeclarationWarning -> ShowS #

show :: DeclarationWarning -> String #

showList :: [DeclarationWarning] -> ShowS #

NFData DeclarationWarning Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

rnf :: DeclarationWarning -> () #

type Rep DeclarationWarning Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

type Rep DeclarationWarning = D1 ('MetaData "DeclarationWarning" "Agda.Syntax.Concrete.Definitions.Errors" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "DeclarationWarning" 'PrefixI 'True) (S1 ('MetaSel ('Just "dwLocation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CallStack) :*: S1 ('MetaSel ('Just "dwWarning") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeclarationWarning')))

data DeclarationWarning' Source #

Non-fatal errors encountered in the Nicifier.

Constructors

EmptyAbstract Range	Empty `abstract` block.
EmptyConstructor Range	Empty `constructor` block.
EmptyField Range	Empty `field` block.
EmptyGeneralize Range	Empty `variable` block.
EmptyInstance Range	Empty `instance` block
EmptyMacro Range	Empty `macro` block.
EmptyMutual Range	Empty `mutual` block.
EmptyPostulate Range	Empty `postulate` block.
EmptyPrivate Range	Empty `private` block.
EmptyPrimitive Range	Empty `primitive` block.
HiddenGeneralize Range	A `Hidden` identifier in a `variable` declaration. Hiding has no effect there as generalized variables are always hidden (or instance variables).
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	`private` has no effect on `open public`. (But the user might think so.)
OpenPublicAbstract Range	`abstract` has no effect on `open public`. (But the user might think so.)
PolarityPragmasButNotPostulates [Name]
PragmaNoTerminationCheck Range	Pragma `{-# NO_TERMINATION_CHECK #-}` has been replaced by `{-# TERMINATING #-}` and `{-# NON_TERMINATING #-}`.
PragmaCompiled Range	`COMPILE` pragmas are not allowed in safe mode.
SafeFlagEta Range	`ETA` pragma is unsafe.
SafeFlagInjective Range	`INJECTIVE` pragma is unsafe.
SafeFlagNoCoverageCheck Range	`NON_COVERING` pragma is unsafe.
SafeFlagNoPositivityCheck Range	`NO_POSITIVITY_CHECK` pragma is unsafe.
SafeFlagNoUniverseCheck Range	`NO_UNIVERSE_CHECK` pragma is unsafe.
SafeFlagNonTerminating Range	`NON_TERMINATING` pragma is unsafe.
SafeFlagPolarity Range	`POLARITY` pragma is unsafe.
SafeFlagTerminating Range	`TERMINATING` pragma is unsafe.
ShadowingInTelescope (List1 (Name, List2 Range))
UnknownFixityInMixfixDecl [Name]
UnknownNamesInFixityDecl [Name]
UnknownNamesInPolarityPragmas [Name]
UselessAbstract Range	`abstract` block with nothing that can (newly) be made abstract.
UselessInstance Range	`instance` block with nothing that can (newly) become an instance.
UselessPrivate Range	`private` block with nothing that can (newly) be made private.

Instances

Instances details

Pretty DeclarationWarning' Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

pretty :: DeclarationWarning' -> Doc Source #

prettyPrec :: Int -> DeclarationWarning' -> Doc Source #

prettyList :: [DeclarationWarning'] -> Doc Source #

HasRange DeclarationWarning' Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

getRange :: DeclarationWarning' -> Range Source #

EmbPrj DeclarationWarning' Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: DeclarationWarning' -> S Int32 Source #

icod_ :: DeclarationWarning' -> S Int32 Source #

value :: Int32 -> R DeclarationWarning' Source #

Generic DeclarationWarning' Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Associated Types

type Rep DeclarationWarning'

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

from :: DeclarationWarning' -> Rep DeclarationWarning' x #

to :: Rep DeclarationWarning' x -> DeclarationWarning' #

Show DeclarationWarning' Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

showsPrec :: Int -> DeclarationWarning' -> ShowS #

show :: DeclarationWarning' -> String #

showList :: [DeclarationWarning'] -> ShowS #

NFData DeclarationWarning' Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

rnf :: DeclarationWarning' -> () #

type Rep DeclarationWarning' Source #

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

unsafeDeclarationWarning :: DeclarationWarning -> Bool Source #

Nicifier warnings turned into errors in --safe mode.

data Nice a Source #

Nicifier monad. Preserve the state when throwing an exception.

Instances

Instances details

Applicative Nice Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods pure :: a -> Nice a # (<>) :: Nice (a -> b) -> Nice a -> Nice b # liftA2 :: (a -> b -> c) -> Nice a -> Nice b -> Nice c # (>) :: Nice a -> Nice b -> Nice b # (<*) :: Nice a -> Nice b -> Nice a #
Functor Nice Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods fmap :: (a -> b) -> Nice a -> Nice b # (<$) :: a -> Nice b -> Nice a #
Monad Nice Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods (>>=) :: Nice a -> (a -> Nice b) -> Nice b # (>>) :: Nice a -> Nice b -> Nice b # return :: a -> Nice a #
MonadError DeclarationException Nice Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods throwError :: DeclarationException -> Nice a # catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a #
MonadReader NiceEnv Nice Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods ask :: Nice NiceEnv # local :: (NiceEnv -> NiceEnv) -> Nice a -> Nice a # reader :: (NiceEnv -> a) -> Nice a #
MonadState NiceState Nice Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods get :: Nice NiceState # put :: NiceState -> Nice () # state :: (NiceState -> (a, NiceState)) -> Nice a #
Null a => Null (Nice a) Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods empty :: Nice a Source # null :: Nice a -> Bool Source #

data NiceEnv Source #

Nicifier parameters.

Constructors

NiceEnv
Fields safeButNotBuiltin :: Bool We are in a module declared `--safe` which is not a builtin module.

Instances

Instances details

MonadReader NiceEnv Nice Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods ask :: Nice NiceEnv # local :: (NiceEnv -> NiceEnv) -> Nice a -> Nice a # reader :: (NiceEnv -> a) -> Nice a #

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?

type Measure = Name Source #

Termination measure is, for now, a variable name.

declarationWarningName :: DeclarationWarning -> WarningName Source #