ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Concrete.Definitions.Monad

Contents

Handling the lone signatures, stored to infer mutual blocks.

Synopsis

newtype Nice
value runNice
data NiceEnv
data NiceState
data LoneSig
type LoneSigs
type NiceWarnings
value initNiceState
value lensNameId
value nextNameId
value loneSigs
value addLoneSig
value removeLoneSig
value getSig
value noLoneSigs
value forgetLoneSigs
value checkLoneSigs
value breakImplicitMutualBlock
value loneFuns
value loneSigsFromLoneNames
value terminationCheckPragma
value withTerminationCheckPragma
value coverageCheckPragma
value withCoverageCheckPragma
value positivityCheckPragma
value withPositivityCheckPragma
value universeCheckPragma
value withUniverseCheckPragma
value getUniverseCheckFromSig
value catchallPragma
value popCatchallPragma
value withCatchallPragma
value niceWarning
value declarationException
value declarationWarning'
value declarationWarning

PackageAgda-2.8.0.2
Exports36
LanguageHaskell2010
LicenceMIT
SourceMonad.hs

newtypenewtype Nice a

Source#

Nicifier monad. Preserve the state when throwing an exception.

Constructors

Nice
- unNice :: ReaderT NiceEnv (ExceptT DeclarationException (State NiceState)) a

Instances7Monad, Functor, Applicative, MonadError, MonadReader, MonadState, …

Monad NiceDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Monad
Functor NiceDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Monad
Applicative NiceDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Monad
MonadError DeclarationException NiceDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Monad
MonadReader NiceEnv NiceDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Monad
MonadState NiceState NiceDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Monad
Null a => Null (Nice a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Monad

valuerunNice

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

Source#

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

datadata NiceEnv

Source#

Nicifier parameters.

Constructors

NiceEnv
- safeButNotBuiltin :: Bool
  We are in a module declared --safe which is not a builtin module.
- checkingWhere :: WhereClause_
  Are we checking a where module?

Instances1MonadReader

MonadReader NiceEnv NiceDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Monad

datadata NiceState

Source#

Nicifier state.

Constructors

NiceState
- _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 NoNames (anonymous definitions) by a unique NameId.

Instances1MonadState

MonadState NiceState NiceDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Monad

datadata LoneSig

Constructors

LoneSig
- loneSigRange :: Range
- loneSigName :: Name
  If isNoName, this name can have a different NameId than the key of LoneSigs pointing to it.
- loneSigKind :: DataRecOrFun

Instances1Show

Show LoneSigDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Monad

typetype LoneSigs = Map Name LoneSig

typetype NiceWarnings = [DeclarationWarning]

valueinitNiceState :: NiceState

Source#

Initial nicifier state.

valuelensNameId :: Lens' NiceState NameId

valuenextNameId :: Nice NameId

Handling the lone signatures, stored to infer mutual blocks.

valueloneSigs :: Lens' NiceState LoneSigs

Source#

Lens for field _loneSigs.

valueaddLoneSig :: Range -> Name -> DataRecOrFun -> Nice Name

Source#

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

valueremoveLoneSig :: Name -> Nice ()

Source#

Remove a lone signature from the state.

valuegetSig :: Name -> Nice (Maybe DataRecOrFun)

Source#

Search for forward type signature.

valuenoLoneSigs :: Nice Bool

Source#

Check that no lone signatures are left in the state.

valueforgetLoneSigs :: Nice ()

valuecheckLoneSigs :: LoneSigs -> Nice ()

Source#

Ensure that all forward declarations have been given a definition.

valuebreakImplicitMutualBlock :: 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.

valueloneFuns :: LoneSigs -> [(Name, Name)]

Source#

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

valueloneSigsFromLoneNames :: [(Range, Name, DataRecOrFun)] -> LoneSigs

Source#

Create a LoneSigs map from an association list.

valueterminationCheckPragma :: Lens' NiceState TerminationCheck

Source#

Lens for field _termChk.

valuewithTerminationCheckPragma :: TerminationCheck -> Nice a -> Nice a

valuecoverageCheckPragma :: Lens' NiceState CoverageCheck

valuewithCoverageCheckPragma :: CoverageCheck -> Nice a -> Nice a

valuepositivityCheckPragma :: Lens' NiceState PositivityCheck

Source#

Lens for field _posChk.

valuewithPositivityCheckPragma :: PositivityCheck -> Nice a -> Nice a

valueuniverseCheckPragma :: Lens' NiceState UniverseCheck

Source#

Lens for field _uniChk.

valuewithUniverseCheckPragma :: UniverseCheck -> Nice a -> Nice a

valuegetUniverseCheckFromSig :: Name -> Nice UniverseCheck

Source#

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

valuecatchallPragma :: Lens' NiceState Catchall

Source#

Lens for field _catchall.

valuepopCatchallPragma :: Nice Catchall

Source#

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

valuewithCatchallPragma :: Catchall -> Nice a -> Nice a

valueniceWarning :: DeclarationWarning -> Nice ()

Source#

Add a new warning.

valuedeclarationException :: HasCallStack => DeclarationException' -> Nice a

valuedeclarationWarning' :: DeclarationWarning' -> CallStack -> Nice ()

valuedeclarationWarning :: HasCallStack => DeclarationWarning' -> Nice ()