Agda.Syntax.Concrete.Definitions.Monad

Documentation

newtype Nice a

Nicifier monad. Preserve the state when throwing an exception.

Constructors

Nice

Fields

• unNice :: ReaderT NiceEnv (ExceptT DeclarationException (State NiceState)) a

Instances

Applicative Nice

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

Defined in Agda.Syntax.Concrete.Definitions.Monad

Methods

fmap :: (a -> b) -> Nice a -> Nice b

(<$) :: a -> Nice b -> Nice a

Monad Nice

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

Defined in Agda.Syntax.Concrete.Definitions.Monad

Methods

throwError :: DeclarationException -> Nice a

catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a

MonadReader NiceEnv Nice

Defined in Agda.Syntax.Concrete.Definitions.Monad

Methods

ask :: Nice NiceEnv

local :: (NiceEnv -> NiceEnv) -> Nice a -> Nice a

reader :: (NiceEnv -> a) -> Nice a

MonadState NiceState Nice

Defined in Agda.Syntax.Concrete.Definitions.Monad

Methods

get :: Nice NiceState

put :: NiceState -> Nice ()

state :: (NiceState -> (a, NiceState)) -> Nice a

Null a => Null (Nice a)

Defined in Agda.Syntax.Concrete.Definitions.Monad

Methods

empty :: Nice a

null :: Nice a -> Bool

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

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

data NiceEnv

Nicifier parameters.

Constructors

NiceEnv

Fields

• safeButNotBuiltin :: Bool

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

Instances

MonadReader NiceEnv Nice

Defined in Agda.Syntax.Concrete.Definitions.Monad

Methods

ask :: Nice NiceEnv

local :: (NiceEnv -> NiceEnv) -> Nice a -> Nice a

reader :: (NiceEnv -> a) -> Nice a

data NiceState

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

Instances

MonadState NiceState Nice

Defined in Agda.Syntax.Concrete.Definitions.Monad

Methods

get :: Nice NiceState

put :: NiceState -> Nice ()

state :: (NiceState -> (a, NiceState)) -> Nice a

data LoneSig

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

Show LoneSig

Defined in Agda.Syntax.Concrete.Definitions.Monad

Methods

showsPrec :: Int -> LoneSig -> ShowS

show :: LoneSig -> String

showList :: [LoneSig] -> ShowS

type LoneSigs

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

Arguments

 = [DeclarationWarning]

Stack of warnings. Head is last warning.

initNiceState :: NiceState

Initial nicifier state.

lensNameId :: Lens' NiceState NameId

nextNameId :: Nice NameId

Handling the lone signatures, stored to infer mutual blocks.

loneSigs :: Lens' NiceState LoneSigs

Lens for field _loneSigs.

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

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

removeLoneSig :: Name -> Nice ()

Remove a lone signature from the state.

getSig :: Name -> Nice (Maybe DataRecOrFun)

Search for forward type signature.

noLoneSigs :: Nice Bool

Check that no lone signatures are left in the state.

forgetLoneSigs :: Nice ()

checkLoneSigs :: LoneSigs -> Nice ()

Ensure that all forward declarations have been given a definition.

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

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

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

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

Create a LoneSigs map from an association list.

terminationCheckPragma :: Lens' NiceState TerminationCheck

Lens for field _termChk.

withTerminationCheckPragma :: TerminationCheck -> Nice a -> Nice a

coverageCheckPragma :: Lens' NiceState CoverageCheck

withCoverageCheckPragma :: CoverageCheck -> Nice a -> Nice a

positivityCheckPragma :: Lens' NiceState PositivityCheck

Lens for field _posChk.

withPositivityCheckPragma :: PositivityCheck -> Nice a -> Nice a

universeCheckPragma :: Lens' NiceState UniverseCheck

Lens for field _uniChk.

withUniverseCheckPragma :: UniverseCheck -> Nice a -> Nice a

getUniverseCheckFromSig :: Name -> Nice UniverseCheck

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

catchallPragma :: Lens' NiceState Catchall

Lens for field _catchall.

popCatchallPragma :: Nice Catchall

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

withCatchallPragma :: Catchall -> Nice a -> Nice a

niceWarning :: DeclarationWarning -> Nice ()

Add a new warning.

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

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

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