Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	None
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
- | BadUtf8 ModulePath UnicodeException
- | OtherIOError FilePath IOException
- | ModuleParseError ModulePath 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 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
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 :: ModulePath -> 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 :: ModulePath -> Fingerprint -> 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 # (/=) :: ImportSource -> ImportSource -> Bool #
Show ImportSource Source #
Instance details Defined in Cryptol.ModuleSystem.Monad Methods showsPrec :: Int -> ImportSource -> ShowS # show :: ImportSource -> String # showList :: [ImportSource] -> ShowS #
Generic ImportSource Source #
Instance details Defined in Cryptol.ModuleSystem.Monad Associated Types type Rep ImportSource :: Type -> Type # Methods from :: ImportSource -> Rep ImportSource x # to :: Rep ImportSource x -> ImportSource #
NFData ImportSource Source #
Instance details Defined in Cryptol.ModuleSystem.Monad Methods rnf :: ImportSource -> () #
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.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" 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
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
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 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

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

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 #

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

Instances

Show ModuleWarning Source #
Instance details Defined in Cryptol.ModuleSystem.Monad Methods showsPrec :: Int -> ModuleWarning -> ShowS # show :: ModuleWarning -> String # showList :: [ModuleWarning] -> ShowS #
Generic ModuleWarning Source #
Instance details Defined in Cryptol.ModuleSystem.Monad Associated Types type Rep ModuleWarning :: Type -> Type # Methods from :: ModuleWarning -> Rep ModuleWarning x # to :: Rep ModuleWarning x -> ModuleWarning #
NFData ModuleWarning Source #
Instance details Defined in Cryptol.ModuleSystem.Monad Methods rnf :: ModuleWarning -> () #
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.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" 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 #
Monad m => Monad (ModuleT m) Source #
Instance details Defined in Cryptol.ModuleSystem.Monad 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 #
Instance details Defined in Cryptol.ModuleSystem.Monad Methods fmap :: (a -> b) -> ModuleT m a -> ModuleT m b # (<$) :: a -> ModuleT m b -> ModuleT m a #
Monad m => Applicative (ModuleT m) Source #
Instance details Defined in Cryptol.ModuleSystem.Monad Methods pure :: a -> ModuleT m a # (<>) :: ModuleT m (a -> b) -> ModuleT m a -> ModuleT m b # liftA2 :: (a -> b -> c) -> ModuleT m a -> ModuleT m b -> ModuleT m c # (>) :: ModuleT m a -> ModuleT m b -> ModuleT m b # (<*) :: ModuleT m a -> ModuleT m b -> ModuleT m a #
MonadIO m => MonadIO (ModuleT m) Source #
Instance details Defined in Cryptol.ModuleSystem.Monad Methods liftIO :: IO a -> ModuleT m a #
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 :: ModulePath -> Fingerprint -> 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