Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Concrete.Definitions.Types

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 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
- | 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
- | NiceUnquoteData Range Access IsAbstract PositivityCheck UniverseCheck Name [Name] Expr
- | NiceOpaque Range [QName] [NiceDeclaration]
type TerminationCheck = TerminationCheck Measure
type Measure = Name
type Catchall = Bool
type NiceConstructor = NiceTypeSignature
type NiceTypeSignature = NiceDeclaration
data Clause = Clause Name Catchall LHS RHS WhereClause [Clause]
data MutualChecks = MutualChecks {
- mutualTermination :: [TerminationCheck]
- mutualCoverage :: [CoverageCheck]
- mutualPositivity :: [PositivityCheck]
}
data InferredMutual = InferredMutual {
- inferredChecks :: MutualChecks
- inferredBlock :: [NiceDeclaration]
- inferredLeftovers :: [NiceDeclaration]
}
extendInferredBlock :: NiceDeclaration -> InferredMutual -> InferredMutual
type InterleavedMutual = Map Name InterleavedDecl
data InterleavedDecl
- = InterleavedData {
  - interleavedDeclNum :: DeclNum
  - interleavedDeclSig :: NiceDeclaration
  - interleavedDataCons :: Maybe (DeclNum, List1 [NiceConstructor])
  }
- | InterleavedFun {
  - interleavedDeclNum :: DeclNum
  - interleavedDeclSig :: NiceDeclaration
  - interleavedFunClauses :: Maybe (DeclNum, List1 ([Declaration], [Clause]))
  }
type DeclNum = Int
isInterleavedFun :: InterleavedDecl -> Maybe ()
isInterleavedData :: InterleavedDecl -> Maybe ()
interleavedDecl :: Name -> InterleavedDecl -> [(DeclNum, NiceDeclaration)]
data KindOfBlock
- = PostulateBlock
- | PrimitiveBlock
- | InstanceBlock
- | FieldBlock
- | DataBlock
- | ConstructorBlock
declName :: NiceDeclaration -> String
data InMutual
- = InMutual
- | NotInMutual
data DataRecOrFun
- = DataName {
  - _kindPosCheck :: PositivityCheck
  - _kindUniCheck :: UniverseCheck
  }
- | RecName {
  - _kindPosCheck :: PositivityCheck
  - _kindUniCheck :: UniverseCheck
  }
- | FunName TerminationCheck CoverageCheck
isFunName :: DataRecOrFun -> Bool
sameKind :: DataRecOrFun -> DataRecOrFun -> Bool
terminationCheck :: DataRecOrFun -> TerminationCheck
coverageCheck :: DataRecOrFun -> CoverageCheck
positivityCheck :: DataRecOrFun -> PositivityCheck
mutualChecks :: DataRecOrFun -> MutualChecks
universeCheck :: DataRecOrFun -> UniverseCheck

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 TerminationCheck = TerminationCheck Measure Source #

type Measure = Name Source #

Termination measure is, for now, a variable name.

type Catchall = Bool Source #

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.2-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.2-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 MutualChecks Source #

When processing a mutual block we collect the various checks present in the block before combining them.

Constructors

MutualChecks
Fields mutualTermination :: [TerminationCheck] mutualCoverage :: [CoverageCheck] mutualPositivity :: [PositivityCheck]

Instances

Instances details

Monoid MutualChecks Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods mempty :: MutualChecks # mappend :: MutualChecks -> MutualChecks -> MutualChecks # mconcat :: [MutualChecks] -> MutualChecks #
Semigroup MutualChecks Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods (<>) :: MutualChecks -> MutualChecks -> MutualChecks # sconcat :: NonEmpty MutualChecks -> MutualChecks # stimes :: Integral b => b -> MutualChecks -> MutualChecks #

data InferredMutual Source #

In an inferred mutual block we keep accumulating nice declarations until all of the lone signatures have an attached definition. The type is therefore a bit span-like: we return an initial segment (the inferred mutual block) together with leftovers.

Constructors

InferredMutual
Fields inferredChecks :: MutualChecks inferredBlock :: [NiceDeclaration] inferredLeftovers :: [NiceDeclaration]

extendInferredBlock :: NiceDeclaration -> InferredMutual -> InferredMutual Source #

type InterleavedMutual = Map Name InterleavedDecl Source #

In an `interleaved mutual' block we collect the data signatures, function signatures, as well as their associated constructors and function clauses respectively. Each signature is given a position in the block (from 0 onwards) and each set of constructor / clauses is given a *distinct* one. This allows for interleaved forward declarations similar to what one gets in a new-style mutual block.

data InterleavedDecl Source #

Constructors

InterleavedData
Fields interleavedDeclNum :: DeclNum Internal number of the data signature. interleavedDeclSig :: NiceDeclaration The data signature. interleavedDataCons :: Maybe (DeclNum, List1 [NiceConstructor]) Constructors associated to the data signature.
InterleavedFun
Fields interleavedDeclNum :: DeclNum Internal number of the data signature. interleavedDeclSig :: NiceDeclaration The data signature. interleavedFunClauses :: Maybe (DeclNum, List1 ([Declaration], [Clause])) Function clauses associated to the function signature.

type DeclNum = Int Source #

Numbering declarations in an interleaved mutual block.

isInterleavedFun :: InterleavedDecl -> Maybe () Source #

isInterleavedData :: InterleavedDecl -> Maybe () Source #

interleavedDecl :: Name -> InterleavedDecl -> [(DeclNum, NiceDeclaration)] Source #

data KindOfBlock Source #

Several declarations expect only type signatures as sub-declarations. These are:

Constructors

PostulateBlock	postulate
PrimitiveBlock	`primitive`. Ensured by parser.
InstanceBlock	`instance`. Actually, here all kinds of sub-declarations are allowed a priori.
FieldBlock	`field`. Ensured by parser.
DataBlock	`data ... where`. Here we got a bad error message for Agda-2.5 (Issue 1698).
ConstructorBlock	`constructor`, in `interleaved mutual`.

Instances

Instances details

Show KindOfBlock Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods showsPrec :: Int -> KindOfBlock -> ShowS # show :: KindOfBlock -> String # showList :: [KindOfBlock] -> ShowS #
Eq KindOfBlock Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods (==) :: KindOfBlock -> KindOfBlock -> Bool # (/=) :: KindOfBlock -> KindOfBlock -> Bool #
Ord KindOfBlock Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods compare :: KindOfBlock -> KindOfBlock -> Ordering # (<) :: KindOfBlock -> KindOfBlock -> Bool # (<=) :: KindOfBlock -> KindOfBlock -> Bool # (>) :: KindOfBlock -> KindOfBlock -> Bool # (>=) :: KindOfBlock -> KindOfBlock -> Bool # max :: KindOfBlock -> KindOfBlock -> KindOfBlock # min :: KindOfBlock -> KindOfBlock -> KindOfBlock #

declName :: NiceDeclaration -> String Source #

data InMutual Source #

Constructors

InMutual	we are nicifying a mutual block
NotInMutual	we are nicifying decls not in a mutual block

Instances

Instances details

Show InMutual Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods showsPrec :: Int -> InMutual -> ShowS # show :: InMutual -> String # showList :: [InMutual] -> ShowS #
Eq InMutual Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods (==) :: InMutual -> InMutual -> Bool # (/=) :: InMutual -> InMutual -> Bool #

data DataRecOrFun Source #

The kind of the forward declaration.

Constructors

DataName	Name of a data type
Fields _kindPosCheck :: PositivityCheck _kindUniCheck :: UniverseCheck
RecName	Name of a record type
Fields _kindPosCheck :: PositivityCheck _kindUniCheck :: UniverseCheck
FunName TerminationCheck CoverageCheck	Name of a function.

Instances

Instances details

Pretty DataRecOrFun Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods pretty :: DataRecOrFun -> Doc Source # prettyPrec :: Int -> DataRecOrFun -> Doc Source # prettyList :: [DataRecOrFun] -> Doc Source #
Show DataRecOrFun Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods showsPrec :: Int -> DataRecOrFun -> ShowS # show :: DataRecOrFun -> String # showList :: [DataRecOrFun] -> ShowS #
Eq DataRecOrFun Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods (==) :: DataRecOrFun -> DataRecOrFun -> Bool # (/=) :: DataRecOrFun -> DataRecOrFun -> Bool #

isFunName :: DataRecOrFun -> Bool Source #

sameKind :: DataRecOrFun -> DataRecOrFun -> Bool Source #

terminationCheck :: DataRecOrFun -> TerminationCheck Source #

coverageCheck :: DataRecOrFun -> CoverageCheck Source #

positivityCheck :: DataRecOrFun -> PositivityCheck Source #

mutualChecks :: DataRecOrFun -> MutualChecks Source #

universeCheck :: DataRecOrFun -> UniverseCheck Source #