cryptol-2.6.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 | Haskell2010

Cryptol.ModuleSystem.Monad

Description

Synopsis

- data ImportSource
  - = FromModule ModName
  - | FromImport (Located Import)
  - | FromModuleInstance (Located ModName)
- 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
  - | ImportedParamModule ModName
  - | FailedToParameterizeModDefs ModName [Name]
  - | NotAParameterizedModule ModName
  - | ErrorInFile FilePath ModuleError
- 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
- importParamModule :: ModName -> ModuleM a
- failedToParameterizeModDefs :: ModName -> [Name] -> ModuleM a
- notAParameterizedModule :: ModName -> ModuleM a
- errorInFile :: FilePath -> ModuleM a -> ModuleM a
- data ModuleWarning
  - = TypeCheckWarnings [(Range, Warning)]
  - | RenamerWarnings [RenamerWarning]
- warn :: [ModuleWarning] -> ModuleM ()
- typeCheckWarnings :: [(Range, Warning)] -> ModuleM ()
- renamerWarnings :: [RenamerWarning] -> ModuleM ()
- data RO = RO {
  - roLoading :: [ImportSource]
  - roEvalOpts :: EvalOpts
  }
- emptyRO :: EvalOpts -> RO
- newtype ModuleT m a = ModuleT {
  - unModuleT :: ReaderT RO (StateT ModuleEnv (ExceptionT ModuleError (WriterT [ModuleWarning] m))) a
  }
- runModuleT :: Monad m => (EvalOpts, ModuleEnv) -> ModuleT m a -> m (Either ModuleError (a, ModuleEnv), [ModuleWarning])
- type ModuleM = ModuleT IO
- runModuleM :: (EvalOpts, 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 ()
- getLoadedMaybe :: ModName -> ModuleM (Maybe LoadedModule)
- 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
- getIface :: ModName -> ModuleM Iface
- getLoaded :: ModName -> ModuleM Module
- getNameSeeds :: ModuleM NameSeeds
- getSupply :: ModuleM Supply
- getMonoBinds :: ModuleM Bool
- setMonoBinds :: Bool -> ModuleM ()
- setNameSeeds :: NameSeeds -> ModuleM ()
- setSupply :: Supply -> ModuleM ()
- unloadModule :: (LoadedModule -> Bool) -> ModuleM ()
- loadedModule :: FilePath -> FilePath -> Module -> ModuleM ()
- modifyEvalEnv :: (EvalEnv -> Eval EvalEnv) -> ModuleM ()
- getEvalEnv :: ModuleM EvalEnv
- getEvalOpts :: ModuleM EvalOpts
- getFocusedModule :: ModuleM (Maybe ModName)
- setFocusedModule :: ModName -> ModuleM ()
- getSearchPath :: ModuleM [FilePath]
- withPrependedSearchPath :: [FilePath] -> ModuleM a -> ModuleM a
- getFocusedEnv :: ModuleM (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
- getDynEnv :: ModuleM DynamicEnv
- setDynEnv :: DynamicEnv -> ModuleM ()
- setSolver :: SolverConfig -> ModuleM ()
- getSolverConfig :: ModuleM SolverConfig
- withLogger :: (Logger -> a -> IO b) -> a -> ModuleM b

# Documentation

data ImportSource Source #

Constructors

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

Instances

Eq ImportSource Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods (==) :: ImportSource -> ImportSource -> Bool Source # (/=) :: ImportSource -> ImportSource -> Bool 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 #
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 #
NFData ImportSource Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods rnf :: ImportSource -> () Source #
PP ImportSource Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods ppPrec :: Int -> ImportSource -> Doc Source #
type Rep ImportSource Source # |

Instance details

Defined in Cryptol.ModuleSystem.Monad

type Rep ImportSource = D1 (MetaData "ImportSource" "Cryptol.ModuleSystem.Monad" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" 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 "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
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
ImportedParamModule ModName | Attempt to import a parametrized module that was not instantiated.
FailedToParameterizeModDefs ModName [Name] | Failed to add the module parameters to all definitions in a module.
NotAParameterizedModule ModName |
ErrorInFile FilePath 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

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

importParamModule :: ModName -> ModuleM a Source #

failedToParameterizeModDefs :: ModName -> [Name] -> ModuleM a Source #

notAParameterizedModule :: ModName -> ModuleM a Source #

errorInFile :: FilePath -> 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 [(Range, Warning)] |
RenamerWarnings [RenamerWarning] |

Instances

Show ModuleWarning Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods showsPrec :: Int -> ModuleWarning -> ShowS Source # show :: ModuleWarning -> String Source # showList :: [ModuleWarning] -> ShowS Source #
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 #
NFData ModuleWarning Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods rnf :: ModuleWarning -> () Source #
PP ModuleWarning Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods ppPrec :: Int -> ModuleWarning -> Doc Source #
type Rep ModuleWarning Source # |

Instance details

Defined in Cryptol.ModuleSystem.Monad

type Rep ModuleWarning = D1 (MetaData "ModuleWarning" "Cryptol.ModuleSystem.Monad" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" False) (C1 (MetaCons "TypeCheckWarnings" PrefixI False) (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 :: [(Range, Warning)] -> ModuleM () Source #

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

data RO Source #

Constructors

RO |

Fields

- roLoading :: [ImportSource]
- roEvalOpts :: EvalOpts

emptyRO :: EvalOpts -> 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 # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods lift :: Monad m => m a -> 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 # fail :: String -> 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 => 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 #
MonadIO m => MonadIO (ModuleT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods liftIO :: IO 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 #

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

type ModuleM = ModuleT IO Source #

runModuleM :: (EvalOpts, 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 #

getLoadedMaybe :: ModName -> ModuleM (Maybe LoadedModule) Source #

isLoaded :: ModName -> ModuleM Bool Source #

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.

getIface :: ModName -> ModuleM Iface Source #

getLoaded :: ModName -> ModuleM Module 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 :: (LoadedModule -> Bool) -> ModuleM () Source #

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

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

getEvalEnv :: ModuleM EvalEnv Source #

getEvalOpts :: ModuleM EvalOpts 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 (IfaceParams, IfaceDecls, NamingEnv, NameDisp) Source #

getDynEnv :: ModuleM DynamicEnv Source #

setDynEnv :: DynamicEnv -> ModuleM () Source #

setSolver :: SolverConfig -> ModuleM () Source #

getSolverConfig :: ModuleM SolverConfig Source #

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

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