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 # (<>) :: Nice (a -> b) -> Nice a -> Nice b # liftA2 :: (a -> b -> c) -> Nice a -> Nice b -> Nice c # (>) :: Nice a -> Nice b -> Nice b # (<*) :: Nice a -> Nice b -> Nice a #
Functor Nice Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods fmap :: (a -> b) -> Nice a -> Nice b # (<$) :: a -> Nice b -> Nice a #
Monad Nice Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods (>>=) :: Nice a -> (a -> Nice b) -> Nice b # (>>) :: Nice a -> Nice b -> Nice b # return :: a -> Nice a #
MonadError DeclarationException Nice Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods throwError :: DeclarationException -> Nice a catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a
MonadState NiceEnv Nice Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Monad Methods get :: Nice NiceEnv put :: NiceEnv -> Nice () state :: (NiceEnv -> (a, NiceEnv)) -> Nice a

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 NoNames (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 put :: NiceEnv -> Nice () state :: (NiceEnv -> (a, NiceEnv)) -> Nice a

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 #