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

Safe Haskell | None
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.
- 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 Name (Arg Expr)
  - | PrimitiveFunction Range 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 Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
  - | NiceDataSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
  - | NiceFunClause Range Access IsAbstract TerminationCheck Catchall Declaration
  - | FunSig Range Access IsAbstract IsInstance IsMacro ArgInfo TerminationCheck Name Expr
  - | FunDef Range [Declaration] IsAbstract IsInstance TerminationCheck Name [Clause]
  - | NiceDataDef Range Origin IsAbstract PositivityCheck UniverseCheck Name [LamBinding] [NiceConstructor]
  - | NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] [Declaration]
  - | NicePatternSyn Range Name [Arg Name] Pattern
  - | NiceGeneralize Range Access ArgInfo Name Expr
  - | NiceUnquoteDecl Range Access IsAbstract IsInstance TerminationCheck [Name] Expr
  - | NiceUnquoteDef Range Access IsAbstract TerminationCheck [Name] Expr
- type NiceConstructor = NiceTypeSignature
- type NiceTypeSignature = NiceDeclaration
- data Clause = Clause Name Catchall LHS RHS WhereClause [Clause]
- data DeclarationException
  - = MultipleEllipses Pattern
  - | InvalidName Name
  - | DuplicateDefinition Name
  - | MissingWithClauses Name LHS
  - | WrongDefinition Name DataRecOrFun DataRecOrFun
  - | Codata Range
  - | DeclarationPanic String
  - | WrongContentBlock KindOfBlock Range
  - | AmbiguousFunClauses LHS [Name]
  - | InvalidMeasureMutual Range
  - | UnquoteDefRequiresSignature [Name]
  - | BadMacroDef NiceDeclaration
- data DeclarationWarning
  - = EmptyAbstract Range
  - | EmptyInstance Range
  - | EmptyMacro Range
  - | EmptyMutual Range
  - | EmptyPostulate Range
  - | EmptyPrivate Range
  - | EmptyGeneralize Range
  - | EmptyPrimitive Range
  - | InvalidCatchallPragma Range
  - | InvalidNoPositivityCheckPragma Range
  - | InvalidNoUniverseCheckPragma Range
  - | InvalidTerminationCheckPragma Range
  - | MissingDefinitions [Name]
  - | NotAllowedInMutual Range String
  - | PolarityPragmasButNotPostulates [Name]
  - | PragmaNoTerminationCheck Range
  - | PragmaCompiled Range
  - | UnknownFixityInMixfixDecl [Name]
  - | UnknownNamesInFixityDecl [Name]
  - | UnknownNamesInPolarityPragmas [Name]
  - | UselessAbstract Range
  - | UselessInstance Range
  - | UselessPrivate Range
- 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 Name (Arg Expr) |
PrimitiveFunction Range 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 Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr |
NiceDataSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr |
NiceFunClause Range Access IsAbstract TerminationCheck 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 Name Expr |
FunDef Range [Declaration] IsAbstract IsInstance TerminationCheck 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] |
NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] [Declaration] |
NicePatternSyn Range Name [Arg Name] Pattern |
NiceGeneralize Range Access ArgInfo Name Expr |
NiceUnquoteDecl Range Access IsAbstract IsInstance TerminationCheck [Name] Expr |
NiceUnquoteDef Range Access IsAbstract TerminationCheck [Name] Expr |

Instances

Data NiceDeclaration Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions

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 :: (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 #

Show NiceDeclaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods showsPrec :: Int -> NiceDeclaration -> ShowS Source # show :: NiceDeclaration -> String Source # showList :: [NiceDeclaration] -> ShowS Source #
Pretty NiceDeclaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions 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 Methods getRange :: NiceDeclaration -> Range Source #
ToAbstract NiceDeclaration Declaration Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NiceDeclaration -> ScopeM Declaration Source #

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

Data Clause Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions

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 :: (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 #

Show Clause Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods showsPrec :: Int -> Clause -> ShowS Source # show :: Clause -> String Source # showList :: [Clause] -> ShowS Source #
ToAbstract Clause Clause Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Clause -> ScopeM Clause0 Source #

data DeclarationException Source #

The exception type.

Constructors

MultipleEllipses Pattern |
InvalidName Name |
DuplicateDefinition Name |
MissingWithClauses Name LHS |
WrongDefinition Name DataRecOrFun DataRecOrFun |
Codata Range |
DeclarationPanic String |
WrongContentBlock KindOfBlock Range |
AmbiguousFunClauses LHS [Name] | in a mutual block, a clause could belong to any of the `[Name]` type signatures
InvalidMeasureMutual Range | In a mutual block, all or none need a MEASURE pragma. Range is of mutual block.
UnquoteDefRequiresSignature [Name] |
BadMacroDef NiceDeclaration |

Instances

Data DeclarationException Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions

Methods

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

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

toConstr :: DeclarationException -> Constr Source #

dataTypeOf :: DeclarationException -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show DeclarationException Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods showsPrec :: Int -> DeclarationException -> ShowS Source # show :: DeclarationException -> String Source # showList :: [DeclarationException] -> ShowS Source #
Pretty DeclarationException Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods pretty :: DeclarationException -> Doc Source # prettyPrec :: Int -> DeclarationException -> Doc Source # prettyList :: [DeclarationException] -> Doc Source #
HasRange DeclarationException Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods getRange :: DeclarationException -> Range Source #
MonadError DeclarationException Nice Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods throwError :: DeclarationException -> Nice a Source # catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a Source #

data DeclarationWarning Source #

Non-fatal errors encountered in the Nicifier

Constructors

EmptyAbstract Range | Empty `abstract` 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.
EmptyGeneralize Range | Empty `variable` block.
EmptyPrimitive Range | Empty `primitive` block.
InvalidCatchallPragma Range | A {-# CATCHALL #-} pragma that does not precede a function clause.
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.
InvalidTerminationCheckPragma Range | A {-# TERMINATING #-} and {-# NON_TERMINATING #-} pragma that does not apply to any function.
MissingDefinitions [Name] |
NotAllowedInMutual Range String |
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
UnknownFixityInMixfixDecl [Name] |
UnknownNamesInFixityDecl [Name] |
UnknownNamesInPolarityPragmas [Name] |
UselessAbstract Range |
UselessInstance Range |
UselessPrivate Range |

Instances

Data DeclarationWarning Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions

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 :: (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 #

Show DeclarationWarning Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods showsPrec :: Int -> DeclarationWarning -> ShowS Source # show :: DeclarationWarning -> String Source # showList :: [DeclarationWarning] -> ShowS Source #
Pretty DeclarationWarning Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions 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 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 #

data Nice a Source #

Nicifier monad. Preserve the state when throwing an exception.

Instances

Monad Nice Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods (>>=) :: Nice a -> (a -> Nice b) -> Nice b Source # (>>) :: Nice a -> Nice b -> Nice b Source # return :: a -> Nice a Source # fail :: String -> Nice a Source #
Functor Nice Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods fmap :: (a -> b) -> Nice a -> Nice b Source # (<$) :: a -> Nice b -> Nice a Source #
Applicative Nice Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions 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 #
MonadError DeclarationException Nice Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods throwError :: DeclarationException -> Nice a Source # catchError :: Nice a -> (DeclarationException -> Nice a) -> 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 #