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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Concrete.Definitions.Monad

Contents

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

Synopsis

- newtype Nice a = Nice {
  - unNice :: ReaderT NiceEnv (ExceptT DeclarationException (State NiceState)) a
  }
- runNice :: NiceEnv -> Nice a -> (Either DeclarationException a, NiceWarnings)
- data NiceEnv = NiceEnv {
  - safeButNotBuiltin :: Bool
  - checkingWhere :: WhereClause_
  }
- data NiceState = NiceState {
  - _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]
- initNiceState :: NiceState
- lensNameId :: Lens' NiceState NameId
- nextNameId :: Nice NameId
- loneSigs :: Lens' NiceState LoneSigs
- addLoneSig :: Range -> Name -> DataRecOrFun -> Nice Name
- removeLoneSig :: Name -> Nice ()
- getSig :: Name -> Nice (Maybe DataRecOrFun)
- noLoneSigs :: Nice Bool
- forgetLoneSigs :: Nice ()
- checkLoneSigs :: LoneSigs -> Nice ()
- breakImplicitMutualBlock :: KwRange -> String -> Nice ()
- loneFuns :: LoneSigs -> [(Name, Name)]
- loneSigsFromLoneNames :: [(Range, Name, DataRecOrFun)] -> LoneSigs
- terminationCheckPragma :: Lens' NiceState TerminationCheck
- withTerminationCheckPragma :: TerminationCheck -> Nice a -> Nice a
- coverageCheckPragma :: Lens' NiceState CoverageCheck
- withCoverageCheckPragma :: CoverageCheck -> Nice a -> Nice a
- positivityCheckPragma :: Lens' NiceState PositivityCheck
- withPositivityCheckPragma :: PositivityCheck -> Nice a -> Nice a
- universeCheckPragma :: Lens' NiceState UniverseCheck
- withUniverseCheckPragma :: UniverseCheck -> Nice a -> Nice a
- getUniverseCheckFromSig :: Name -> Nice UniverseCheck
- catchallPragma :: Lens' NiceState Catchall
- 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 :: ReaderT NiceEnv (ExceptT DeclarationException (State NiceState)) 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 #
MonadReader NiceEnv Nice Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods ask :: Nice NiceEnv Source # local :: (NiceEnv -> NiceEnv) -> Nice a -> Nice a Source # reader :: (NiceEnv -> a) -> Nice a Source #
MonadState NiceState Nice Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods get :: Nice NiceState Source # put :: NiceState -> Nice () Source # state :: (NiceState -> (a, NiceState)) -> Nice a Source #
Null a => Null (Nice a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods empty :: Nice a Source # null :: Nice a -> Bool Source #

runNice :: NiceEnv -> Nice a -> (Either DeclarationException a, NiceWarnings) Source #

Run a Nicifier computation, return result and warnings (in chronological order).

data NiceEnv Source #

Nicifier parameters.

Constructors

NiceEnv |

Fields

- safeButNotBuiltin :: Bool

  We are in a module declared `--safe` which is not a builtin module.

- checkingWhere :: WhereClause_

  Are we checking a `where` module?

#### Instances

Instances details

MonadReader NiceEnv Nice Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods ask :: Nice NiceEnv Source # local :: (NiceEnv -> NiceEnv) -> Nice a -> Nice a Source # reader :: (NiceEnv -> a) -> Nice a Source #

data NiceState Source #

Nicifier state.

Constructors

NiceState |

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 NiceState Nice Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods get :: Nice NiceState Source # put :: NiceState -> Nice () Source # state :: (NiceState -> (a, NiceState)) -> 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

#### Instances

Instances details

Show LoneSig Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods showsPrec :: Int -> LoneSig -> ShowS Source # show :: LoneSig -> String Source # showList :: [LoneSig] -> ShowS Source #

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.

initNiceState :: NiceState Source #

Initial nicifier state.

lensNameId :: Lens' NiceState NameId Source #

nextNameId :: Nice NameId Source #

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

loneSigs :: Lens' NiceState LoneSigs 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 #

checkLoneSigs :: LoneSigs -> Nice () Source #

Ensure that all forward declarations have been given a definition.

breakImplicitMutualBlock :: KwRange -> String -> Nice () Source #

Ensure that all forward declarations have been given a definition, raising an error indicating *why* they would have had to have been defined.

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' NiceState TerminationCheck Source #

Lens for field `_termChk`.

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

coverageCheckPragma :: Lens' NiceState CoverageCheck Source #

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

positivityCheckPragma :: Lens' NiceState PositivityCheck Source #

Lens for field `_posChk`.

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

universeCheckPragma :: Lens' NiceState UniverseCheck 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' NiceState Catchall 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 #