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 Fingerprint UnicodeException
- | OtherIOError FilePath IOException
- | ModuleParseError ModulePath Fingerprint 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]
- | ConfigLoadError ConfigLoadError
- | ErrorInFile ModulePath ModuleError
moduleNotFound :: ModName -> [FilePath] -> ModuleM a
cantFindFile :: FilePath -> ModuleM a
badUtf8 :: ModulePath -> Fingerprint -> UnicodeException -> ModuleM a
otherIOError :: FilePath -> IOException -> ModuleM a
moduleParseError :: ModulePath -> Fingerprint -> 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
tryModule :: ModuleM a -> ModuleM (Either ModuleError 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
isLoadedStrict :: ModName -> ModulePath -> 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
getEvalForeignPolicy :: ModuleM EvalForeignPolicy
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
getNominalTypes :: ModuleM (Map Name NominalType)
getFocusedModule :: ModuleM (Maybe (ImpName Name))
setFocusedModule :: ImpName Name -> ModuleM ()
setMaybeFocusedModule :: Maybe (ImpName Name) -> 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 # Methods from :: ImportSource -> Rep ImportSource x # to :: Rep ImportSource x -> ImportSource #
Show ImportSource Source #
Instance details Defined in Cryptol.ModuleSystem.Monad Methods showsPrec :: Int -> ImportSource -> ShowS # show :: ImportSource -> String # showList :: [ImportSource] -> ShowS #
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 -> () #
Eq ImportSource Source #
Instance details Defined in Cryptol.ModuleSystem.Monad Methods (==) :: ImportSource -> ImportSource -> Bool # (/=) :: ImportSource -> ImportSource -> Bool #
type Rep ImportSource Source #
Instance details Defined in Cryptol.ModuleSystem.Monad type Rep ImportSource = D1 ('MetaData "ImportSource" "Cryptol.ModuleSystem.Monad" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" '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 Fingerprint UnicodeException	Bad UTF-8 encoding in while decoding this file
OtherIOError FilePath IOException	Some other IO error occurred while reading this file
ModuleParseError ModulePath Fingerprint 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
ConfigLoadError ConfigLoadError
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 the problematic module to the handler.

Instances

Instances details

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

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

cantFindFile :: FilePath -> ModuleM a Source #

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

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

moduleParseError :: ModulePath -> Fingerprint -> 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.

tryModule :: ModuleM a -> ModuleM (Either ModuleError a) Source #

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 # Methods from :: ModuleWarning -> Rep ModuleWarning x # to :: Rep ModuleWarning x -> ModuleWarning #
Show ModuleWarning Source #
Instance details Defined in Cryptol.ModuleSystem.Monad Methods showsPrec :: Int -> ModuleWarning -> ShowS # show :: ModuleWarning -> String # showList :: [ModuleWarning] -> ShowS #
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 -> () #
type Rep ModuleWarning Source #
Instance details Defined in Cryptol.ModuleSystem.Monad type Rep ModuleWarning = D1 ('MetaData "ModuleWarning" "Cryptol.ModuleSystem.Monad" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" '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 #
MonadFail m => MonadFail (ModuleT m) Source #
Instance details Defined in Cryptol.ModuleSystem.Monad Methods fail :: String -> 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 => 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 #
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 => 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 #
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.

isLoadedStrict :: ModName -> ModulePath -> 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.

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 #

getEvalForeignPolicy :: ModuleM EvalForeignPolicy 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 #

getNominalTypes :: ModuleM (Map Name NominalType) Source #

getFocusedModule :: ModuleM (Maybe (ImpName Name)) Source #

setFocusedModule :: ImpName Name -> ModuleM () Source #

setMaybeFocusedModule :: Maybe (ImpName Name) -> 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