cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.ModuleSystem.Monad

Description

Synopsis

- data ImportSource
  - = FromModule ModName
  - | FromImport (Located Import)
- importedModule :: ImportSource -> ModName
- data ModuleError
  - = ModuleNotFound ModName [FilePath]
  - | CantFindFile FilePath
  - | OtherIOError FilePath IOException
  - | ModuleParseError FilePath ParseError
  - | RecursiveModules [ImportSource]
  - | RenamerErrors ImportSource [RenamerError]
  - | NoPatErrors ImportSource [Error]
  - | NoIncludeErrors ImportSource [IncludeError]
  - | TypeCheckingFailed ImportSource [(Range, Error)]
  - | OtherFailure String
  - | ModuleNameMismatch ModName (Located ModName)
  - | DuplicateModuleName ModName FilePath FilePath
- moduleNotFound :: ModName -> [FilePath] -> ModuleM a
- cantFindFile :: FilePath -> ModuleM a
- otherIOError :: FilePath -> IOException -> ModuleM a
- moduleParseError :: FilePath -> ParseError -> ModuleM a
- recursiveModules :: [ImportSource] -> ModuleM a
- renamerErrors :: [RenamerError] -> ModuleM a
- noPatErrors :: [Error] -> ModuleM a
- noIncludeErrors :: [IncludeError] -> ModuleM a
- typeCheckingFailed :: [(Range, Error)] -> ModuleM a
- moduleNameMismatch :: ModName -> Located ModName -> ModuleM a
- duplicateModuleName :: ModName -> FilePath -> FilePath -> ModuleM a
- data ModuleWarning
  - = TypeCheckWarnings [(Range, Warning)]
  - | RenamerWarnings [RenamerWarning]
- warn :: [ModuleWarning] -> ModuleM ()
- typeCheckWarnings :: [(Range, Warning)] -> ModuleM ()
- renamerWarnings :: [RenamerWarning] -> ModuleM ()
- data RO = RO {
  - roLoading :: [ImportSource]
  }
- emptyRO :: RO
- newtype ModuleT m a = ModuleT {
  - unModuleT :: ReaderT RO (StateT ModuleEnv (ExceptionT ModuleError (WriterT [ModuleWarning] m))) a
  }
- runModuleT :: Monad m => ModuleEnv -> ModuleT m a -> m (Either ModuleError (a, ModuleEnv), [ModuleWarning])
- type ModuleM = ModuleT IO
- runModuleM :: ModuleEnv -> ModuleM a -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
- io :: BaseM m IO => IO a -> ModuleT m a
- getModuleEnv :: Monad m => ModuleT m ModuleEnv
- setModuleEnv :: Monad m => ModuleEnv -> ModuleT m ()
- modifyModuleEnv :: Monad m => (ModuleEnv -> ModuleEnv) -> ModuleT m ()
- isLoaded :: ModName -> ModuleM Bool
- loadingImport :: Located Import -> ModuleM a -> ModuleM a
- loadingModule :: ModName -> ModuleM a -> ModuleM a
- interactive :: ModuleM a -> ModuleM a
- loading :: ImportSource -> ModuleM a -> ModuleM a
- getImportSource :: ModuleM ImportSource
- getIface :: ModName -> ModuleM Iface
- getNameSeeds :: ModuleM NameSeeds
- getSupply :: ModuleM Supply
- getMonoBinds :: ModuleM Bool
- setMonoBinds :: Bool -> ModuleM ()
- setNameSeeds :: NameSeeds -> ModuleM ()
- setSupply :: Supply -> ModuleM ()
- unloadModule :: FilePath -> ModuleM ()
- loadedModule :: FilePath -> Module -> ModuleM ()
- modifyEvalEnv :: (EvalEnv -> EvalEnv) -> ModuleM ()
- getEvalEnv :: ModuleM EvalEnv
- getFocusedModule :: ModuleM (Maybe ModName)
- setFocusedModule :: ModName -> ModuleM ()
- getSearchPath :: ModuleM [FilePath]
- withPrependedSearchPath :: [FilePath] -> ModuleM a -> ModuleM a
- getFocusedEnv :: ModuleM (IfaceDecls, NamingEnv, NameDisp)
- getQualifiedEnv :: ModuleM IfaceDecls
- getDynEnv :: ModuleM DynamicEnv
- setDynEnv :: DynamicEnv -> ModuleM ()
- setSolver :: SolverConfig -> ModuleM ()
- getSolverConfig :: ModuleM SolverConfig

# Documentation

data ImportSource Source #

Constructors

FromModule ModName |
FromImport (Located Import) |

Instances

Eq ImportSource Source # |
Methods (==) :: ImportSource -> ImportSource -> Bool # (/=) :: ImportSource -> ImportSource -> Bool #
Show ImportSource Source # |
Methods showsPrec :: Int -> ImportSource -> ShowS # show :: ImportSource -> String # showList :: [ImportSource] -> ShowS #
Generic ImportSource Source # |
Associated Types type Rep ImportSource :: * -> * # Methods from :: ImportSource -> Rep ImportSource x # to :: Rep ImportSource x -> ImportSource #
NFData ImportSource Source # |
Methods rnf :: ImportSource -> () #
PP ImportSource Source # |
Methods ppPrec :: Int -> ImportSource -> Doc Source #
type Rep ImportSource Source # |

type Rep ImportSource = D1 (MetaData "ImportSource" "Cryptol.ModuleSystem.Monad" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "FromModule" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ModName))) (C1 (MetaCons "FromImport" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Located Import)))))

importedModule :: ImportSource -> ModName Source #

data ModuleError Source #

Constructors

ModuleNotFound ModName [FilePath] | Unable to find the module given, tried looking in these paths
CantFindFile FilePath | Unable to open a file
OtherIOError FilePath IOException | Some other IO error occurred while reading this file
ModuleParseError FilePath ParseError | Generated this parse error when parsing the file for module m
RecursiveModules [ImportSource] | Recursive module group discovered
RenamerErrors ImportSource [RenamerError] | Problems during the renaming phase
NoPatErrors ImportSource [Error] | Problems during the NoPat phase
NoIncludeErrors ImportSource [IncludeError] | Problems during the NoInclude phase
TypeCheckingFailed ImportSource [(Range, Error)] | Problems during type checking
OtherFailure String | Problems after type checking, eg. specialization
ModuleNameMismatch ModName (Located ModName) | Module loaded by 'import' statement has the wrong module name
DuplicateModuleName ModName FilePath FilePath | Two modules loaded from different files have the same module name

Instances

Show ModuleError Source # |
Methods showsPrec :: Int -> ModuleError -> ShowS # show :: ModuleError -> String # showList :: [ModuleError] -> ShowS #
NFData ModuleError Source # |
Methods rnf :: ModuleError -> () #
PP ModuleError Source # |
Methods ppPrec :: Int -> ModuleError -> Doc Source #

moduleNotFound :: ModName -> [FilePath] -> ModuleM a Source #

cantFindFile :: FilePath -> ModuleM a Source #

otherIOError :: FilePath -> IOException -> ModuleM a Source #

moduleParseError :: FilePath -> ParseError -> ModuleM a Source #

recursiveModules :: [ImportSource] -> ModuleM a Source #

renamerErrors :: [RenamerError] -> ModuleM a Source #

noPatErrors :: [Error] -> ModuleM a Source #

noIncludeErrors :: [IncludeError] -> ModuleM a Source #

typeCheckingFailed :: [(Range, Error)] -> ModuleM a Source #

moduleNameMismatch :: ModName -> Located ModName -> ModuleM a Source #

duplicateModuleName :: ModName -> FilePath -> FilePath -> ModuleM a Source #

data ModuleWarning Source #

Constructors

TypeCheckWarnings [(Range, Warning)] |
RenamerWarnings [RenamerWarning] |

Instances

Show ModuleWarning Source # |
Methods showsPrec :: Int -> ModuleWarning -> ShowS # show :: ModuleWarning -> String # showList :: [ModuleWarning] -> ShowS #
Generic ModuleWarning Source # |
Associated Types type Rep ModuleWarning :: * -> * # Methods from :: ModuleWarning -> Rep ModuleWarning x # to :: Rep ModuleWarning x -> ModuleWarning #
NFData ModuleWarning Source # |
Methods rnf :: ModuleWarning -> () #
PP ModuleWarning Source # |
Methods ppPrec :: Int -> ModuleWarning -> Doc Source #
type Rep ModuleWarning Source # |

type Rep ModuleWarning = D1 (MetaData "ModuleWarning" "Cryptol.ModuleSystem.Monad" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "TypeCheckWarnings" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Range, Warning)]))) (C1 (MetaCons "RenamerWarnings" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [RenamerWarning]))))

warn :: [ModuleWarning] -> ModuleM () Source #

typeCheckWarnings :: [(Range, Warning)] -> ModuleM () Source #

renamerWarnings :: [RenamerWarning] -> ModuleM () Source #

data RO Source #

Constructors

RO |

Fields

- roLoading :: [ImportSource]

emptyRO :: RO Source #

newtype ModuleT m a Source #

Constructors

ModuleT |

Fields

- unModuleT :: ReaderT RO (StateT ModuleEnv (ExceptionT ModuleError (WriterT [ModuleWarning] m))) a

Instances

MonadT ModuleT Source # |
Methods lift :: Monad m => m a -> ModuleT m a #
Monad m => Monad (ModuleT m) Source # |
Methods (>>=) :: ModuleT m a -> (a -> ModuleT m b) -> ModuleT m b # (>>) :: ModuleT m a -> ModuleT m b -> ModuleT m b # return :: a -> ModuleT m a # fail :: String -> ModuleT m a #
Monad m => Functor (ModuleT m) Source # |
Methods fmap :: (a -> b) -> ModuleT m a -> ModuleT m b # (<$) :: a -> ModuleT m b -> ModuleT m a #
Monad m => Applicative (ModuleT m) Source # |
Methods pure :: a -> ModuleT m a # (<*>) :: ModuleT m (a -> b) -> ModuleT m a -> ModuleT m b # (*>) :: ModuleT m a -> ModuleT m b -> ModuleT m b # (<*) :: ModuleT m a -> ModuleT m b -> ModuleT m a #
Monad m => FreshM (ModuleT m) Source # |
Methods liftSupply :: (Supply -> (a, Supply)) -> ModuleT m a Source #

runModuleT :: Monad m => ModuleEnv -> ModuleT m a -> m (Either ModuleError (a, ModuleEnv), [ModuleWarning]) Source #

type ModuleM = ModuleT IO Source #

runModuleM :: ModuleEnv -> ModuleM a -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning]) Source #

io :: BaseM m IO => IO a -> ModuleT m a Source #

getModuleEnv :: Monad m => ModuleT m ModuleEnv Source #

setModuleEnv :: Monad m => ModuleEnv -> ModuleT m () Source #

modifyModuleEnv :: Monad m => (ModuleEnv -> ModuleEnv) -> ModuleT m () Source #

isLoaded :: ModName -> ModuleM Bool Source #

loadingImport :: Located Import -> ModuleM a -> ModuleM a Source #

loadingModule :: ModName -> ModuleM a -> ModuleM a Source #

interactive :: ModuleM a -> ModuleM a Source #

Push an "interactive" context onto the loading stack. A bit of a hack, as it uses a faked module name

loading :: ImportSource -> ModuleM a -> ModuleM a Source #

getImportSource :: ModuleM ImportSource Source #

Get the currently focused import source.

getIface :: ModName -> ModuleM Iface Source #

getNameSeeds :: ModuleM NameSeeds Source #

getSupply :: ModuleM Supply Source #

getMonoBinds :: ModuleM Bool Source #

setMonoBinds :: Bool -> ModuleM () Source #

setNameSeeds :: NameSeeds -> ModuleM () Source #

setSupply :: Supply -> ModuleM () Source #

unloadModule :: FilePath -> ModuleM () Source #

Remove a module from the set of loaded module, by its path.

loadedModule :: FilePath -> Module -> ModuleM () Source #

modifyEvalEnv :: (EvalEnv -> EvalEnv) -> ModuleM () Source #

getEvalEnv :: ModuleM EvalEnv Source #

getFocusedModule :: ModuleM (Maybe ModName) Source #

setFocusedModule :: ModName -> ModuleM () Source #

getSearchPath :: ModuleM [FilePath] Source #

withPrependedSearchPath :: [FilePath] -> ModuleM a -> ModuleM a Source #

Run a `ModuleM` action in a context with a prepended search path. Useful for temporarily looking in other places while resolving imports, for example.

getFocusedEnv :: ModuleM (IfaceDecls, NamingEnv, NameDisp) Source #

getQualifiedEnv :: ModuleM IfaceDecls Source #

getDynEnv :: ModuleM DynamicEnv Source #

setDynEnv :: DynamicEnv -> ModuleM () Source #

setSolver :: SolverConfig -> ModuleM () Source #

getSolverConfig :: ModuleM SolverConfig Source #