cryptol-3.0.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-Inferred
Language | Haskell2010

Cryptol.ModuleSystem.Monad

Description

Synopsis

- data ImportSource
  - = FromModule ModName
  - | FromImport (Located Import)
  - | FromSigImport (Located ModName)
  - | FromModuleInstance (Located ModName)
- importedModule :: ImportSource -> ModName
- data ModuleError
  - = ModuleNotFound ModName [FilePath]
  - | CantFindFile FilePath
  - | BadUtf8 ModulePath UnicodeException
  - | OtherIOError FilePath IOException
  - | ModuleParseError ModulePath ParseError
  - | RecursiveModules [ImportSource]
  - | RenamerErrors ImportSource [RenamerError]
  - | NoPatErrors ImportSource [Error]
  - | ExpandPropGuardsError ImportSource Error
  - | NoIncludeErrors ImportSource [IncludeError]
  - | TypeCheckingFailed ImportSource NameMap [(Range, Error)]
  - | OtherFailure String
  - | ModuleNameMismatch ModName (Located ModName)
  - | DuplicateModuleName ModName FilePath FilePath
  - | FFILoadErrors ModName [FFILoadError]
  - | ErrorInFile ModulePath ModuleError
- moduleNotFound :: ModName -> [FilePath] -> ModuleM a
- cantFindFile :: FilePath -> ModuleM a
- badUtf8 :: ModulePath -> UnicodeException -> ModuleM a
- otherIOError :: FilePath -> IOException -> ModuleM a
- moduleParseError :: ModulePath -> ParseError -> ModuleM a
- recursiveModules :: [ImportSource] -> ModuleM a
- renamerErrors :: [RenamerError] -> ModuleM a
- noPatErrors :: [Error] -> ModuleM a
- expandPropGuardsError :: Error -> ModuleM a
- noIncludeErrors :: [IncludeError] -> ModuleM a
- typeCheckingFailed :: NameMap -> [(Range, Error)] -> ModuleM a
- moduleNameMismatch :: ModName -> Located ModName -> ModuleM a
- duplicateModuleName :: ModName -> FilePath -> FilePath -> ModuleM a
- ffiLoadErrors :: ModName -> [FFILoadError] -> ModuleM a
- errorInFile :: ModulePath -> ModuleM a -> ModuleM a
- data ModuleWarning
  - = TypeCheckWarnings NameMap [(Range, Warning)]
  - | RenamerWarnings [RenamerWarning]
- warn :: [ModuleWarning] -> ModuleM ()
- typeCheckWarnings :: NameMap -> [(Range, Warning)] -> ModuleM ()
- renamerWarnings :: [RenamerWarning] -> ModuleM ()
- data RO m = RO {
  - roLoading :: [ImportSource]
  - roEvalOpts :: m EvalOpts
  - roCallStacks :: Bool
  - roFileReader :: FilePath -> m ByteString
  - roTCSolver :: Solver
  }
- emptyRO :: ModuleInput m -> RO m
- newtype ModuleT m a = ModuleT {
  - unModuleT :: ReaderT (RO m) (StateT ModuleEnv (ExceptionT ModuleError (WriterT [ModuleWarning] m))) a
  }
- data ModuleInput m = ModuleInput {
  - minpCallStacks :: Bool
  - minpEvalOpts :: m EvalOpts
  - minpByteReader :: FilePath -> m ByteString
  - minpModuleEnv :: ModuleEnv
  - minpTCSolver :: Solver
  }
- runModuleT :: Monad m => ModuleInput m -> ModuleT m a -> m (Either ModuleError (a, ModuleEnv), [ModuleWarning])
- type ModuleM = ModuleT IO
- runModuleM :: ModuleInput IO -> ModuleM a -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
- io :: BaseM m IO => IO a -> ModuleT m a
- getByteReader :: Monad m => ModuleT m (FilePath -> m ByteString)
- getCallStacks :: Monad m => ModuleT m Bool
- readBytes :: Monad m => FilePath -> ModuleT m ByteString
- getModuleEnv :: Monad m => ModuleT m ModuleEnv
- getTCSolver :: Monad m => ModuleT m Solver
- setModuleEnv :: Monad m => ModuleEnv -> ModuleT m ()
- modifyModuleEnv :: Monad m => (ModuleEnv -> ModuleEnv) -> ModuleT m ()
- getLoadedMaybe :: ModName -> ModuleM (Maybe (LoadedModuleG TCTopEntity))
- isLoaded :: ModName -> ModuleM Bool
- loadingImport :: Located Import -> ModuleM a -> ModuleM a
- loadingModule :: ModName -> ModuleM a -> ModuleM a
- loadingModInstance :: Located ModName -> ModuleM a -> ModuleM a
- interactive :: ModuleM a -> ModuleM a
- loading :: ImportSource -> ModuleM a -> ModuleM a
- getImportSource :: ModuleM ImportSource
- getIfaces :: ModuleM (Map ModName (Either ModParamNames Iface))
- getLoaded :: ModName -> ModuleM Module
- getAllLoaded :: ModuleM (ModName -> Maybe (ModuleG (), IfaceG ()))
- getAllLoadedSignatures :: ModuleM (ModName -> Maybe ModParamNames)
- getNameSeeds :: ModuleM NameSeeds
- getSupply :: ModuleM Supply
- getMonoBinds :: ModuleM Bool
- setMonoBinds :: Bool -> ModuleM ()
- setNameSeeds :: NameSeeds -> ModuleM ()
- setSupply :: Supply -> ModuleM ()
- unloadModule :: (forall a. LoadedModuleG a -> Bool) -> ModuleM ()
- loadedModule :: ModulePath -> FileInfo -> NamingEnv -> Maybe ForeignSrc -> TCTopEntity -> ModuleM ()
- modifyEvalEnvM :: Traversable t => (EvalEnv -> Eval (t EvalEnv)) -> ModuleM (t ())
- modifyEvalEnv :: (EvalEnv -> Eval EvalEnv) -> ModuleM ()
- getEvalEnv :: ModuleM EvalEnv
- getEvalOptsAction :: ModuleM (IO EvalOpts)
- getEvalOpts :: ModuleM EvalOpts
- getNewtypes :: ModuleM (Map Name Newtype)
- getFocusedModule :: ModuleM (Maybe ModName)
- setFocusedModule :: ModName -> ModuleM ()
- getSearchPath :: ModuleM [FilePath]
- withPrependedSearchPath :: [FilePath] -> ModuleM a -> ModuleM a
- getFocusedEnv :: ModuleM ModContext
- getDynEnv :: ModuleM DynamicEnv
- setDynEnv :: DynamicEnv -> ModuleM ()
- withLogger :: (Logger -> a -> IO b) -> a -> ModuleM b

# Documentation

data ImportSource Source #

Constructors

FromModule ModName |
FromImport (Located Import) |
FromSigImport (Located ModName) |
FromModuleInstance (Located ModName) |

#### Instances

Instances details

Generic ImportSource Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Associated Types type Rep ImportSource :: Type -> Type Source # Methods from :: ImportSource -> Rep ImportSource x Source # to :: Rep ImportSource x -> ImportSource Source #
Show ImportSource Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods showsPrec :: Int -> ImportSource -> ShowS Source # show :: ImportSource -> String Source # showList :: [ImportSource] -> ShowS Source #
PP ImportSource Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods ppPrec :: Int -> ImportSource -> Doc Source #
NFData ImportSource Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods rnf :: ImportSource -> () Source #
Eq ImportSource Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods (==) :: ImportSource -> ImportSource -> Bool Source # (/=) :: ImportSource -> ImportSource -> Bool Source #
type Rep ImportSource Source # |

Instance details

Defined in Cryptol.ModuleSystem.Monad

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

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
BadUtf8 ModulePath UnicodeException | Bad UTF-8 encoding in while decoding this file
OtherIOError FilePath IOException | Some other IO error occurred while reading this file
ModuleParseError ModulePath 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
ExpandPropGuardsError ImportSource Error | Problems during the ExpandPropGuards phase
NoIncludeErrors ImportSource [IncludeError] | Problems during the NoInclude phase
TypeCheckingFailed ImportSource NameMap [(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
FFILoadErrors ModName [FFILoadError] | Errors loading foreign function implementations
ErrorInFile ModulePath ModuleError | This is just a tag on the error, indicating the file containing it. It is convenient when we had to look for the module, and we'd like to communicate the location of pthe problematic module to the handler.

#### Instances

Instances details

Show ModuleError Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods showsPrec :: Int -> ModuleError -> ShowS Source # show :: ModuleError -> String Source # showList :: [ModuleError] -> ShowS Source #
PP ModuleError Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods ppPrec :: Int -> ModuleError -> Doc Source #
NFData ModuleError Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods rnf :: ModuleError -> () Source #

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

cantFindFile :: FilePath -> ModuleM a Source #

badUtf8 :: ModulePath -> UnicodeException -> ModuleM a Source #

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

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

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

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

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

expandPropGuardsError :: Error -> ModuleM a Source #

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

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

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

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

ffiLoadErrors :: ModName -> [FFILoadError] -> ModuleM a Source #

errorInFile :: ModulePath -> ModuleM a -> ModuleM a Source #

Run the computation, and if it caused and error, tag the error with the given file.

data ModuleWarning Source #

Constructors

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

#### Instances

Instances details

Generic ModuleWarning Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Associated Types type Rep ModuleWarning :: Type -> Type Source # Methods from :: ModuleWarning -> Rep ModuleWarning x Source # to :: Rep ModuleWarning x -> ModuleWarning Source #
Show ModuleWarning Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods showsPrec :: Int -> ModuleWarning -> ShowS Source # show :: ModuleWarning -> String Source # showList :: [ModuleWarning] -> ShowS Source #
PP ModuleWarning Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods ppPrec :: Int -> ModuleWarning -> Doc Source #
NFData ModuleWarning Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods rnf :: ModuleWarning -> () Source #
type Rep ModuleWarning Source # |

Instance details

Defined in Cryptol.ModuleSystem.Monad

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

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

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

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

data RO m Source #

Constructors

RO |

Fields

- roLoading :: [ImportSource]
- roEvalOpts :: m EvalOpts
- roCallStacks :: Bool
- roFileReader :: FilePath -> m ByteString
- roTCSolver :: Solver

emptyRO :: ModuleInput m -> RO m Source #

newtype ModuleT m a Source #

Constructors

ModuleT |

Fields

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

#### Instances

Instances details

MonadT ModuleT Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods lift :: Monad m => m a -> ModuleT m a Source #
MonadFail m => MonadFail (ModuleT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods fail :: String -> ModuleT m a Source #
MonadIO m => MonadIO (ModuleT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods liftIO :: IO a -> ModuleT m a Source #
Monad m => Applicative (ModuleT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods pure :: a -> ModuleT m a Source # (<*>) :: ModuleT m (a -> b) -> ModuleT m a -> ModuleT m b Source # liftA2 :: (a -> b -> c) -> ModuleT m a -> ModuleT m b -> ModuleT m c Source # (*>) :: ModuleT m a -> ModuleT m b -> ModuleT m b Source # (<*) :: ModuleT m a -> ModuleT m b -> ModuleT m a Source #
Monad m => Functor (ModuleT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods fmap :: (a -> b) -> ModuleT m a -> ModuleT m b Source # (<$) :: a -> ModuleT m b -> ModuleT m a Source #
Monad m => Monad (ModuleT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods (>>=) :: ModuleT m a -> (a -> ModuleT m b) -> ModuleT m b Source # (>>) :: ModuleT m a -> ModuleT m b -> ModuleT m b Source # return :: a -> ModuleT m a Source #
Monad m => FreshM (ModuleT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods liftSupply :: (Supply -> (a, Supply)) -> ModuleT m a Source #

data ModuleInput m Source #

Constructors

ModuleInput |

Fields

- minpCallStacks :: Bool
- minpEvalOpts :: m EvalOpts
- minpByteReader :: FilePath -> m ByteString
- minpModuleEnv :: ModuleEnv
- minpTCSolver :: Solver

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

type ModuleM = ModuleT IO Source #

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

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

getByteReader :: Monad m => ModuleT m (FilePath -> m ByteString) Source #

getCallStacks :: Monad m => ModuleT m Bool Source #

readBytes :: Monad m => FilePath -> ModuleT m ByteString Source #

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

getTCSolver :: Monad m => ModuleT m Solver Source #

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

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

getLoadedMaybe :: ModName -> ModuleM (Maybe (LoadedModuleG TCTopEntity)) Source #

isLoaded :: ModName -> ModuleM Bool Source #

This checks if the given name is loaded---it might refer to either a module or a signature.

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

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

loadingModInstance :: Located 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.

getIfaces :: ModuleM (Map ModName (Either ModParamNames Iface)) Source #

getLoaded :: ModName -> ModuleM Module Source #

getAllLoaded :: ModuleM (ModName -> Maybe (ModuleG (), IfaceG ())) Source #

getAllLoadedSignatures :: ModuleM (ModName -> Maybe ModParamNames) 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 :: (forall a. LoadedModuleG a -> Bool) -> ModuleM () Source #

loadedModule :: ModulePath -> FileInfo -> NamingEnv -> Maybe ForeignSrc -> TCTopEntity -> ModuleM () Source #

modifyEvalEnvM :: Traversable t => (EvalEnv -> Eval (t EvalEnv)) -> ModuleM (t ()) Source #

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

getEvalEnv :: ModuleM EvalEnv Source #

getEvalOptsAction :: ModuleM (IO EvalOpts) Source #

getEvalOpts :: ModuleM EvalOpts Source #

getNewtypes :: ModuleM (Map Name Newtype) 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 ModContext Source #

getDynEnv :: ModuleM DynamicEnv Source #

setDynEnv :: DynamicEnv -> ModuleM () Source #

withLogger :: (Logger -> a -> IO b) -> a -> ModuleM b Source #

Usefule for logging. For example: `withLogger logPutStrLn Hello`