Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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

Methods

throwError :: DeclarationException -> Nice a

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

MonadReader NiceEnv Nice Source # 
Instance details

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 Source # 
Instance details

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) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Monad

Methods

empty :: Nice a Source #

null :: Nice a -> Bool Source #

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

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

data NiceEnv Source #

Nicifier parameters.

Constructors

NiceEnv 

Fields

  • safeButNotBuiltin :: Bool

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

Instances

Instances details
MonadReader NiceEnv Nice Source # 
Instance details

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 Source #

Nicifier state.

Constructors

NiceState 

Fields

Instances

Instances details
MonadState NiceState Nice Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Monad

Methods

get :: Nice NiceState

put :: NiceState -> Nice ()

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

data LoneSig Source #

Constructors

LoneSig 

Fields

Instances

Instances details
Show LoneSig Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Monad

Methods

showsPrec :: Int -> LoneSig -> ShowS

show :: LoneSig -> String

showList :: [LoneSig] -> ShowS

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.

initNiceState :: NiceState Source #

Initial nicifier state.

lensNameId :: Lens' NiceState NameId Source #

nextNameId :: Nice NameId Source #

Handling the lone signatures, stored to infer mutual blocks.

loneSigs :: Lens' NiceState LoneSigs Source #

Lens for field _loneSigs.

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 #

checkLoneSigs :: LoneSigs -> Nice () Source #

Ensure that all forward declarations have been given a definition.

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

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.

terminationCheckPragma :: Lens' NiceState TerminationCheck Source #

Lens for field _termChk.

withTerminationCheckPragma :: TerminationCheck -> Nice a -> Nice a Source #

coverageCheckPragma :: Lens' NiceState CoverageCheck Source #

withCoverageCheckPragma :: CoverageCheck -> Nice a -> Nice a Source #

positivityCheckPragma :: Lens' NiceState PositivityCheck Source #

Lens for field _posChk.

withPositivityCheckPragma :: PositivityCheck -> Nice a -> Nice a Source #

universeCheckPragma :: Lens' NiceState UniverseCheck Source #

Lens for field _uniChk.

withUniverseCheckPragma :: UniverseCheck -> Nice a -> Nice a Source #

getUniverseCheckFromSig :: Name -> Nice UniverseCheck Source #

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

catchallPragma :: Lens' NiceState Catchall Source #

Lens for field _catchall.

popCatchallPragma :: Nice Catchall Source #

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

withCatchallPragma :: Catchall -> Nice a -> Nice a Source #

niceWarning :: DeclarationWarning -> Nice () Source #

Add a new warning.

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

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

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