Cryptol.ModuleSystem.Monad

Documentation

data ImportSource

Constructors

FromModule ModName

FromImport (Located Import)

FromModuleInstance (Located ModName)

Instances

Eq ImportSource

Defined in Cryptol.ModuleSystem.Monad

Methods

(==) :: ImportSource -> ImportSource -> Bool

(/=) :: ImportSource -> ImportSource -> Bool

Show ImportSource

Defined in Cryptol.ModuleSystem.Monad

Methods

showsPrec :: Int -> ImportSource -> ShowS

show :: ImportSource -> String

showList :: [ImportSource] -> ShowS

Generic ImportSource

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

Defined in Cryptol.ModuleSystem.Monad

Methods

rnf :: ImportSource -> ()

PP ImportSource

Defined in Cryptol.ModuleSystem.Monad

Methods

ppPrec :: Int -> ImportSource -> Doc

type Rep ImportSource

Defined in Cryptol.ModuleSystem.Monad

type Rep ImportSource = D1 ('MetaData "ImportSource" "Cryptol.ModuleSystem.Monad" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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

data ModuleError

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 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

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

Defined in Cryptol.ModuleSystem.Monad

Methods

showsPrec :: Int -> ModuleError -> ShowS

show :: ModuleError -> String

showList :: [ModuleError] -> ShowS

NFData ModuleError

Defined in Cryptol.ModuleSystem.Monad

Methods

rnf :: ModuleError -> ()

PP ModuleError

Defined in Cryptol.ModuleSystem.Monad

Methods

ppPrec :: Int -> ModuleError -> Doc

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 :: NameMap -> [(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

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

data ModuleWarning

Constructors

TypeCheckWarnings NameMap [(Range, Warning)]

RenamerWarnings [RenamerWarning]

Instances

Show ModuleWarning

Defined in Cryptol.ModuleSystem.Monad

Methods

showsPrec :: Int -> ModuleWarning -> ShowS

show :: ModuleWarning -> String

showList :: [ModuleWarning] -> ShowS

Generic ModuleWarning

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

Defined in Cryptol.ModuleSystem.Monad

Methods

rnf :: ModuleWarning -> ()

PP ModuleWarning

Defined in Cryptol.ModuleSystem.Monad

Methods

ppPrec :: Int -> ModuleWarning -> Doc

type Rep ModuleWarning

Defined in Cryptol.ModuleSystem.Monad

type Rep ModuleWarning = D1 ('MetaData "ModuleWarning" "Cryptol.ModuleSystem.Monad" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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 ()

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

renamerWarnings :: [RenamerWarning] -> ModuleM ()

data RO m

Constructors

RO

Fields

• roLoading :: [ImportSource]
• roEvalOpts :: EvalOpts
• roFileReader :: FilePath -> m ByteString

emptyRO :: EvalOpts -> (FilePath -> m ByteString) -> RO m

newtype ModuleT m a

Constructors

ModuleT

Fields

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

Instances

MonadT ModuleT

Defined in Cryptol.ModuleSystem.Monad

Methods

lift :: Monad m => m a -> ModuleT m a

Monad m => Monad (ModuleT m)

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 => Functor (ModuleT m)

Defined in Cryptol.ModuleSystem.Monad

Methods

fmap :: (a -> b) -> ModuleT m a -> ModuleT m b

(<$) :: a -> ModuleT m b -> ModuleT m a

MonadFail m => MonadFail (ModuleT m)

Defined in Cryptol.ModuleSystem.Monad

Methods

fail :: String -> ModuleT m a

Monad m => Applicative (ModuleT m)

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)

Defined in Cryptol.ModuleSystem.Monad

Methods

liftIO :: IO a -> ModuleT m a

Monad m => FreshM (ModuleT m)

Defined in Cryptol.ModuleSystem.Monad

Methods

liftSupply :: (Supply -> (a, Supply)) -> ModuleT m a

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

type ModuleM = ModuleT IO

runModuleM :: (EvalOpts, FilePath -> IO ByteString, ModuleEnv) -> 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)

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

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

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

getImportSource :: ModuleM ImportSource

Get the currently focused import source.

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

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

getDynEnv :: ModuleM DynamicEnv

setDynEnv :: DynamicEnv -> ModuleM ()

setSolver :: SolverConfig -> ModuleM ()

getSolverConfig :: ModuleM SolverConfig

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

Usefule for logging. For example: withLogger logPutStrLn Hello