ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Concrete.Definitions.Monad

6 types
30 values

PackageAgda-2.8.0.2
Exports36
LanguageHaskell2010
LicenceMIT
SourceMonad.hs

newtypenewtype Nice a

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)

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

datadata NiceEnv

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

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

Initial nicifier state.

valuelensNameId :: Lens' NiceState NameId

valuenextNameId :: Nice NameId

Handling the lone signatures, stored to infer mutual blocks.

26 declarations

valueloneSigs :: Lens' NiceState LoneSigs

Lens for field _loneSigs.

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

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

valueremoveLoneSig :: Name -> Nice ()

Remove a lone signature from the state.

valuegetSig :: Name -> Nice (Maybe DataRecOrFun)

Search for forward type signature.

valuenoLoneSigs :: Nice Bool

Check that no lone signatures are left in the state.

valueforgetLoneSigs :: Nice ()

valuecheckLoneSigs :: LoneSigs -> Nice ()

Ensure that all forward declarations have been given a definition.

valuebreakImplicitMutualBlock :: KwRange -> String -> Nice ()

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)]

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

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

Create a LoneSigs map from an association list.

valueterminationCheckPragma :: Lens' NiceState TerminationCheck

Lens for field _termChk.

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

valuecoverageCheckPragma :: Lens' NiceState CoverageCheck

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

valuepositivityCheckPragma :: Lens' NiceState PositivityCheck

Lens for field _posChk.

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

valueuniverseCheckPragma :: Lens' NiceState UniverseCheck

Lens for field _uniChk.

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

valuegetUniverseCheckFromSig :: Name -> Nice UniverseCheck

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

valuecatchallPragma :: Lens' NiceState Catchall

Lens for field _catchall.

valuepopCatchallPragma :: Nice Catchall

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

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

valueniceWarning :: DeclarationWarning -> Nice ()

Add a new warning.

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

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

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