Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Concrete.Definitions.Monad

Synopsis

Documentation

newtype Nice a Source #

Nicifier monad. Preserve the state when throwing an exception.

Constructors

Nice 

Fields

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

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

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

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.

Handling the lone signatures, stored to infer mutual blocks.

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 #

Ensure that all forward declarations have been given a definition.

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.

getUniverseCheckFromSig :: Name -> Nice UniverseCheck Source #

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

popCatchallPragma :: Nice Catchall Source #

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

niceWarning :: DeclarationWarning -> Nice () Source #

Add a new warning.