Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

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

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

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

toConstr :: NiceDeclaration -> Constr #

dataTypeOf :: NiceDeclaration -> DataType #

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

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

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

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

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

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

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

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

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

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

Show NiceDeclaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

Pretty NiceDeclaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

HasRange NiceDeclaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

ToAbstract NiceDeclaration Declaration Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

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

toConstr :: Clause -> Constr #

dataTypeOf :: Clause -> DataType #

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

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

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

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

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

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

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

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

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

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

Show Clause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

ToAbstract Clause Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data DeclarationException Source #

The exception type.

Constructors

MultipleEllipses Pattern 
InvalidName Name 
DuplicateDefinition Name 
MissingWithClauses Name LHS 
WrongDefinition Name DataRecOrFun DataRecOrFun 
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

Instances details
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 #

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

toConstr :: DeclarationException -> Constr #

dataTypeOf :: DeclarationException -> DataType #

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

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

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

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

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

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

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

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

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

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

Show DeclarationException Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

Pretty DeclarationException Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

HasRange DeclarationException Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

MonadError DeclarationException Nice Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

data DeclarationWarning Source #

Non-fatal errors encountered in the Nicifier.

Constructors

EmptyAbstract Range

Empty abstract 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.

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.

InvalidTerminationCheckPragma Range

A {-# TERMINATING #-} and {-# NON_TERMINATING #-} pragma that does not apply to any function.

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 [(Name, [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
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 #

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

toConstr :: DeclarationWarning -> Constr #

dataTypeOf :: DeclarationWarning -> DataType #

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

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

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

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

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

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

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

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

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

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

Show DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

Pretty DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

HasRange DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

EmbPrj DeclarationWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.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
Monad Nice Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

Methods

(>>=) :: Nice a -> (a -> Nice b) -> Nice b #

(>>) :: Nice a -> Nice b -> Nice b #

return :: a -> Nice a #

Functor Nice Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

Methods

fmap :: (a -> b) -> Nice a -> Nice b #

(<$) :: a -> Nice b -> Nice a #

Applicative Nice Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

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 #

MonadError DeclarationException Nice Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

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

type Measure = Name Source #

Termination measure is, for now, a variable name.