Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Syntax.Concrete.Definitions

Description

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 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
  - = Axiom Range Access IsAbstract IsInstance ArgInfo Name Expr
  - | 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 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 CoverageCheck Catchall Declaration
  - | FunSig Range Access IsAbstract IsInstance IsMacro ArgInfo TerminationCheck CoverageCheck Name Expr
  - | FunDef Range [Declaration] IsAbstract IsInstance TerminationCheck CoverageCheck Name [Clause]
  - | NiceDataDef Range Origin IsAbstract PositivityCheck UniverseCheck Name [LamBinding] [NiceConstructor]
  - | NiceLoneConstructor Range [NiceConstructor]
  - | NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name RecordDirectives [LamBinding] [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
- 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
  - | 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
  - | ShadowingInTelescope (List1 (Name, List2 Range))
  - | UnknownFixityInMixfixDecl [Name]
  - | UnknownNamesInFixityDecl [Name]
  - | UnknownNamesInPolarityPragmas [Name]
  - | UselessAbstract Range
  - | UselessInstance Range
  - | UselessPrivate Range
- unsafeDeclarationWarning :: DeclarationWarning -> Bool
- 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 ...)

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 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 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 |

#### Instances

Instances details

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 Source # Methods toAbstract :: NiceDeclaration -> ScopeM (AbsOfCon NiceDeclaration) Source #
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 #
Data NiceDeclaration Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NiceDeclaration Source #

toConstr :: NiceDeclaration -> Constr Source #

dataTypeOf :: NiceDeclaration -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NiceDeclaration) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NiceDeclaration) Source #

gmapT :: (forall b. Data b => b -> b) -> NiceDeclaration -> NiceDeclaration Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> NiceDeclaration -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NiceDeclaration -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NiceDeclaration -> m NiceDeclaration Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NiceDeclaration -> m NiceDeclaration Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NiceDeclaration -> m NiceDeclaration Source #

Generic NiceDeclaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Associated Types type Rep NiceDeclaration :: Type -> Type Source # Methods from :: NiceDeclaration -> Rep NiceDeclaration x Source # to :: Rep NiceDeclaration x -> NiceDeclaration Source #
Show NiceDeclaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods showsPrec :: Int -> NiceDeclaration -> ShowS Source # show :: NiceDeclaration -> String Source # showList :: [NiceDeclaration] -> ShowS Source #
NFData NiceDeclaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods rnf :: NiceDeclaration -> () Source #
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 Rep NiceDeclaration = D1 ('MetaData "NiceDeclaration" "Agda.Syntax.Concrete.Definitions.Types" "Agda-2.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) ((((C1 ('MetaCons "Axiom" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "NiceField" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttribute)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Expr)))))) :+: (C1 ('MetaCons "PrimitiveFunction" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Expr))))) :+: (C1 ('MetaCons "NiceMutual" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NiceDeclaration])))) :+: C1 ('MetaCons "NiceModule" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration]))))))) :+: ((C1 ('MetaCons "NiceModuleMacro" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpenShortHand) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: C1 ('MetaCons "NiceOpen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: (C1 ('MetaCons "NiceImport" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe AsName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpenShortHand) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: (C1 ('MetaCons "NicePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pragma)) :+: C1 ('MetaCons "NiceRecSig" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))))) :+: (((C1 ('MetaCons "NiceDataSig" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "NiceFunClause" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Catchall) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Declaration))))) :+: (C1 ('MetaCons "FunSig" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsMacro)))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: (C1 ('MetaCons "FunDef" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause])))) :+: C1 ('MetaCons "NiceDataDef" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Origin)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NiceConstructor]))))))) :+: ((C1 ('MetaCons "NiceLoneConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NiceConstructor])) :+: (C1 ('MetaCons "NiceRecDef" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Origin)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordDirectives) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration]))))) :+: C1 ('MetaCons "NicePatternSyn" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg Name]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern)))))) :+: (C1 ('MetaCons "NiceGeneralize" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttribute) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "NiceUnquoteDecl" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "NiceUnquoteDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))))))

type NiceConstructor = NiceTypeSignature Source #

Only `Axiom`s.

type NiceTypeSignature = NiceDeclaration Source #

Only `Axiom`s.

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 Source # Methods toAbstract :: Clause -> ScopeM (AbsOfCon Clause) Source #
Data Clause Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Clause -> c Clause Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Clause Source #

toConstr :: Clause -> Constr Source #

dataTypeOf :: Clause -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Clause) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause) Source #

gmapT :: (forall b. Data b => b -> b) -> Clause -> Clause Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Clause -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Clause -> m Clause Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause Source #

Generic Clause Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Associated Types type Rep Clause :: Type -> Type Source # Methods from :: Clause -> Rep Clause x Source # to :: Rep Clause x -> Clause Source #
Show Clause Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods showsPrec :: Int -> Clause -> ShowS Source # show :: Clause -> String Source # showList :: [Clause] -> ShowS Source #
NFData Clause Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods rnf :: Clause -> () Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 Source # catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a Source #

data DeclarationWarning Source #

Constructors

DeclarationWarning |

Fields

- dwLocation :: CallStack
- dwWarning :: DeclarationWarning'

#### Instances

Instances details

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 #
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 #
Generic DeclarationWarning Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Associated Types type Rep DeclarationWarning :: Type -> Type Source # Methods from :: DeclarationWarning -> Rep DeclarationWarning x Source # to :: Rep DeclarationWarning x -> DeclarationWarning Source #
Show DeclarationWarning Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods showsPrec :: Int -> DeclarationWarning -> ShowS Source # show :: DeclarationWarning -> String Source # showList :: [DeclarationWarning] -> ShowS Source #
NFData DeclarationWarning Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods rnf :: DeclarationWarning -> () Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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.
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
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

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 #
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 #
Data DeclarationWarning' Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DeclarationWarning' -> c DeclarationWarning' Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DeclarationWarning' Source #

toConstr :: DeclarationWarning' -> Constr Source #

dataTypeOf :: DeclarationWarning' -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DeclarationWarning') Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DeclarationWarning') Source #

gmapT :: (forall b. Data b => b -> b) -> DeclarationWarning' -> DeclarationWarning' Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DeclarationWarning' -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DeclarationWarning' -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> DeclarationWarning' -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DeclarationWarning' -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DeclarationWarning' -> m DeclarationWarning' Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclarationWarning' -> m DeclarationWarning' Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclarationWarning' -> m DeclarationWarning' Source #

Generic DeclarationWarning' Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Associated Types type Rep DeclarationWarning' :: Type -> Type Source # Methods from :: DeclarationWarning' -> Rep DeclarationWarning' x Source # to :: Rep DeclarationWarning' x -> DeclarationWarning' Source #
Show DeclarationWarning' Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods showsPrec :: Int -> DeclarationWarning' -> ShowS Source # show :: DeclarationWarning' -> String Source # showList :: [DeclarationWarning'] -> ShowS Source #
NFData DeclarationWarning' Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods rnf :: DeclarationWarning' -> () Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (((((C1 ('MetaCons "EmptyAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "EmptyConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "EmptyField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "EmptyGeneralize" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: ((C1 ('MetaCons "EmptyInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "EmptyMacro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "EmptyMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "EmptyPostulate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: (((C1 ('MetaCons "EmptyPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "EmptyPrimitive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "InvalidCatchallPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: ((C1 ('MetaCons "InvalidConstructorBlock" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidCoverageCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "InvalidNoPositivityCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidNoUniverseCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))) :+: ((((C1 ('MetaCons "InvalidRecordDirective" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "InvalidTerminationCheckPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "MissingDeclarations" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, Range)])) :+: C1 ('MetaCons "MissingDefinitions" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, Range)])))) :+: ((C1 ('MetaCons "NotAllowedInMutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "OpenPublicPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "OpenPublicAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "PolarityPragmasButNotPostulates" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))))) :+: (((C1 ('MetaCons "PragmaNoTerminationCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "PragmaCompiled" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "ShadowingInTelescope" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (Name, List2 Range)))) :+: C1 ('MetaCons "UnknownFixityInMixfixDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])))) :+: ((C1 ('MetaCons "UnknownNamesInFixityDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: C1 ('MetaCons "UnknownNamesInPolarityPragmas" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))) :+: (C1 ('MetaCons "UselessAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "UselessInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "UselessPrivate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))))))

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 Source # (<*>) :: Nice (a -> b) -> Nice a -> Nice b Source # liftA2 :: (a -> b -> c) -> Nice a -> Nice b -> Nice c Source # (*>) :: Nice a -> Nice b -> Nice b Source # (<*) :: Nice a -> Nice b -> Nice a Source #
Functor Nice Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods fmap :: (a -> b) -> Nice a -> Nice b Source # (<$) :: a -> Nice b -> Nice a Source #
Monad Nice Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods (>>=) :: Nice a -> (a -> Nice b) -> Nice b Source # (>>) :: Nice a -> Nice b -> Nice b Source # return :: a -> Nice a Source #
MonadError DeclarationException Nice Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods throwError :: DeclarationException -> Nice a Source # catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a Source #
MonadState NiceEnv Nice Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods get :: Nice NiceEnv Source # put :: NiceEnv -> Nice () Source # state :: (NiceEnv -> (a, NiceEnv)) -> Nice a Source #

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`?

type Measure = Name Source #

Termination measure is, for now, a variable name.

declarationWarningName :: DeclarationWarning -> WarningName Source #