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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Syntax.Concrete.Definitions.Monad

Contents

- Handling the lone signatures, stored to infer mutual blocks.

Synopsis

- newtype Nice a = Nice {
  - unNice :: ExceptT DeclarationException (State NiceEnv) a
  }
- runNice :: Nice a -> (Either DeclarationException a, NiceWarnings)
- data NiceEnv = NiceEnv {
  - _loneSigs :: LoneSigs
  - _termChk :: TerminationCheck
  - _posChk :: PositivityCheck
  - _uniChk :: UniverseCheck
  - _catchall :: Catchall
  - _covChk :: CoverageCheck
  - niceWarn :: NiceWarnings
  - _nameId :: NameId
  }
- data LoneSig = LoneSig {
  - loneSigRange :: Range
  - loneSigName :: Name
  - loneSigKind :: DataRecOrFun
  }
- type LoneSigs = Map Name LoneSig
- type NiceWarnings = [DeclarationWarning]
- initNiceEnv :: NiceEnv
- lensNameId :: Lens' NameId NiceEnv
- nextNameId :: Nice NameId
- loneSigs :: Lens' LoneSigs NiceEnv
- addLoneSig :: Range -> Name -> DataRecOrFun -> Nice Name
- removeLoneSig :: Name -> Nice ()
- getSig :: Name -> Nice (Maybe DataRecOrFun)
- noLoneSigs :: Nice Bool
- forgetLoneSigs :: Nice ()
- checkLoneSigs :: LoneSigs -> Nice ()
- loneFuns :: LoneSigs -> [(Name, Name)]
- loneSigsFromLoneNames :: [(Range, Name, DataRecOrFun)] -> LoneSigs
- terminationCheckPragma :: Lens' TerminationCheck NiceEnv
- withTerminationCheckPragma :: TerminationCheck -> Nice a -> Nice a
- coverageCheckPragma :: Lens' CoverageCheck NiceEnv
- withCoverageCheckPragma :: CoverageCheck -> Nice a -> Nice a
- positivityCheckPragma :: Lens' PositivityCheck NiceEnv
- withPositivityCheckPragma :: PositivityCheck -> Nice a -> Nice a
- universeCheckPragma :: Lens' UniverseCheck NiceEnv
- withUniverseCheckPragma :: UniverseCheck -> Nice a -> Nice a
- getUniverseCheckFromSig :: Name -> Nice UniverseCheck
- catchallPragma :: Lens' Catchall NiceEnv
- popCatchallPragma :: Nice Catchall
- withCatchallPragma :: Catchall -> Nice a -> Nice a
- niceWarning :: DeclarationWarning -> Nice ()
- declarationException :: HasCallStack => DeclarationException' -> Nice a
- declarationWarning' :: DeclarationWarning' -> CallStack -> Nice ()
- declarationWarning :: HasCallStack => DeclarationWarning' -> Nice ()

# Documentation

newtype Nice a Source #

Nicifier monad. Preserve the state when throwing an exception.

Constructors

Nice |

Fields

- unNice :: ExceptT DeclarationException (State NiceEnv) a

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

data NiceEnv Source #

Nicifier state.

Constructors

NiceEnv |

Fields

- _loneSigs :: LoneSigs

  Lone type signatures that wait for their definition.

- _termChk :: TerminationCheck

  Termination checking pragma waiting for a definition.

- _posChk :: PositivityCheck

  Positivity checking pragma waiting for a definition.

- _uniChk :: UniverseCheck

  Universe checking pragma waiting for a data/rec signature or definition.

- _catchall :: Catchall

  Catchall pragma waiting for a function clause.

- _covChk :: CoverageCheck

  Coverage pragma waiting for a definition.

- niceWarn :: NiceWarnings

  Stack of warnings. Head is last warning.

- _nameId :: NameId

  We distinguish different `NoName`s (anonymous definitions) by a unique `NameId`.

#### Instances

Instances details

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 #

data LoneSig Source #

Constructors

LoneSig |

Fields

- loneSigRange :: Range
- loneSigName :: Name

  If `isNoName`, this name can have a different `NameId` than the key of `LoneSigs` pointing to it.

- loneSigKind :: DataRecOrFun

type LoneSigs Source #

Arguments

= Map Name LoneSig

We retain the `Name` also in the codomain since `Name` as a key is up to `Eq Name` which ignores the range. However, without range names are not unique in case the user gives a second definition of the same name. This causes then problems in `replaceSigs` which might replace the wrong signature.

Another reason is that we want to distinguish different occurrences of `NoName` in a mutual block (issue #4157). The `NoName` in the codomain will have a unique `NameId`.

type NiceWarnings Source #

Arguments

= [DeclarationWarning] | Stack of warnings. Head is last warning.

initNiceEnv :: NiceEnv Source #

Initial nicifier state.

lensNameId :: Lens' NameId NiceEnv Source #

nextNameId :: Nice NameId Source #

# Handling the lone signatures, stored to infer mutual blocks.

loneSigs :: Lens' LoneSigs NiceEnv Source #

Lens for field `_loneSigs`.

addLoneSig :: Range -> Name -> DataRecOrFun -> Nice Name Source #

Adding a lone signature to the state. Return the name (which is made unique if `isNoName`).

removeLoneSig :: Name -> Nice () Source #

Remove a lone signature from the state.

getSig :: Name -> Nice (Maybe DataRecOrFun) Source #

Search for forward type signature.

noLoneSigs :: Nice Bool Source #

Check that no lone signatures are left in the state.

forgetLoneSigs :: Nice () Source #

Ensure that all forward declarations have been given a definition.

checkLoneSigs :: LoneSigs -> Nice () Source #

loneFuns :: LoneSigs -> [(Name, Name)] Source #

Get names of lone function signatures, plus their unique names.

loneSigsFromLoneNames :: [(Range, Name, DataRecOrFun)] -> LoneSigs Source #

Create a `LoneSigs` map from an association list.

terminationCheckPragma :: Lens' TerminationCheck NiceEnv Source #

Lens for field `_termChk`.

withTerminationCheckPragma :: TerminationCheck -> Nice a -> Nice a Source #

coverageCheckPragma :: Lens' CoverageCheck NiceEnv Source #

withCoverageCheckPragma :: CoverageCheck -> Nice a -> Nice a Source #

positivityCheckPragma :: Lens' PositivityCheck NiceEnv Source #

Lens for field `_posChk`.

withPositivityCheckPragma :: PositivityCheck -> Nice a -> Nice a Source #

universeCheckPragma :: Lens' UniverseCheck NiceEnv Source #

Lens for field `_uniChk`.

withUniverseCheckPragma :: UniverseCheck -> Nice a -> Nice a Source #

getUniverseCheckFromSig :: Name -> Nice UniverseCheck Source #

Get universe check pragma from a data/rec signature. Defaults to `YesUniverseCheck`.

catchallPragma :: Lens' Catchall NiceEnv Source #

Lens for field `_catchall`.

popCatchallPragma :: Nice Catchall Source #

Get current catchall pragma, and reset it for the next clause.

withCatchallPragma :: Catchall -> Nice a -> Nice a Source #

niceWarning :: DeclarationWarning -> Nice () Source #

Add a new warning.

declarationException :: HasCallStack => DeclarationException' -> Nice a Source #

declarationWarning' :: DeclarationWarning' -> CallStack -> Nice () Source #

declarationWarning :: HasCallStack => DeclarationWarning' -> Nice () Source #