Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
Cryptol.ModuleSystem
Contents
Description
Synopsis
- data ModuleEnv = ModuleEnv {
- meLoadedModules :: LoadedModules
- meNameSeeds :: NameSeeds
- meSolverConfig :: SolverConfig
- meEvalEnv :: EvalEnv
- meCoreLint :: CoreLint
- meMonoBinds :: !Bool
- meFocusedModule :: Maybe ModName
- meSearchPath :: [FilePath]
- meDynEnv :: DynamicEnv
- meSupply :: !Supply
- initialModuleEnv :: IO ModuleEnv
- data DynamicEnv = DEnv {}
- 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
- data ModuleWarning
- type ModuleCmd a = (EvalOpts, ModuleEnv) -> IO (ModuleRes a)
- type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning])
- findModule :: ModName -> ModuleCmd ModulePath
- loadModuleByPath :: FilePath -> ModuleCmd (ModulePath, Module)
- loadModuleByName :: ModName -> ModuleCmd (ModulePath, Module)
- checkExpr :: Expr PName -> ModuleCmd (Expr Name, Expr, Schema)
- evalExpr :: Expr -> ModuleCmd Value
- checkDecls :: [TopDecl PName] -> ModuleCmd (NamingEnv, [DeclGroup])
- evalDecls :: [DeclGroup] -> ModuleCmd ()
- noPat :: RemovePatterns a => a -> ModuleCmd a
- focusedEnv :: ModuleEnv -> (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
- getPrimMap :: ModuleCmd PrimMap
- renameVar :: NamingEnv -> PName -> ModuleCmd Name
- renameType :: NamingEnv -> PName -> ModuleCmd Name
- data Iface = Iface {}
- data IfaceParams = IfaceParams {
- ifParamTypes :: Map Name ModTParam
- ifParamConstraints :: [Located Prop]
- ifParamFuns :: Map Name ModVParam
- data IfaceDecls = IfaceDecls {
- ifTySyns :: Map Name IfaceTySyn
- ifNewtypes :: Map Name IfaceNewtype
- ifAbstractTypes :: Map Name IfaceAbstractType
- ifDecls :: Map Name IfaceDecl
- genIface :: Module -> Iface
- type IfaceTySyn = TySyn
- data IfaceDecl = IfaceDecl {
- ifDeclName :: !Name
- ifDeclSig :: Schema
- ifDeclPragmas :: [Pragma]
- ifDeclInfix :: Bool
- ifDeclFixity :: Maybe Fixity
- ifDeclDoc :: Maybe String
Module System
This is the current state of the interpreter.
Constructors
ModuleEnv | |
Fields
|
Instances
Generic ModuleEnv Source # | |
NFData ModuleEnv Source # | |
Defined in Cryptol.ModuleSystem.Env | |
type Rep ModuleEnv Source # | |
Defined in Cryptol.ModuleSystem.Env type Rep ModuleEnv = D1 ('MetaData "ModuleEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "ModuleEnv" 'PrefixI 'True) (((S1 ('MetaSel ('Just "meLoadedModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LoadedModules) :*: S1 ('MetaSel ('Just "meNameSeeds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameSeeds)) :*: (S1 ('MetaSel ('Just "meSolverConfig") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SolverConfig) :*: (S1 ('MetaSel ('Just "meEvalEnv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 EvalEnv) :*: S1 ('MetaSel ('Just "meCoreLint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoreLint)))) :*: ((S1 ('MetaSel ('Just "meMonoBinds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool) :*: S1 ('MetaSel ('Just "meFocusedModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModName))) :*: (S1 ('MetaSel ('Just "meSearchPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]) :*: (S1 ('MetaSel ('Just "meDynEnv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DynamicEnv) :*: S1 ('MetaSel ('Just "meSupply") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Supply)))))) |
initialModuleEnv :: IO ModuleEnv Source #
data DynamicEnv Source #
Extra information we need to carry around to dynamically extend
an environment outside the context of a single module. Particularly
useful when dealing with interactive declarations as in :let
or
it
.
Instances
Generic DynamicEnv Source # | |
Defined in Cryptol.ModuleSystem.Env Associated Types type Rep DynamicEnv :: Type -> Type | |
Semigroup DynamicEnv Source # | |
Defined in Cryptol.ModuleSystem.Env Methods (<>) :: DynamicEnv -> DynamicEnv -> DynamicEnv # sconcat :: NonEmpty DynamicEnv -> DynamicEnv # stimes :: Integral b => b -> DynamicEnv -> DynamicEnv # | |
Monoid DynamicEnv Source # | |
Defined in Cryptol.ModuleSystem.Env Methods mempty :: DynamicEnv # mappend :: DynamicEnv -> DynamicEnv -> DynamicEnv # mconcat :: [DynamicEnv] -> DynamicEnv # | |
NFData DynamicEnv Source # | |
Defined in Cryptol.ModuleSystem.Env Methods rnf :: DynamicEnv -> () | |
type Rep DynamicEnv Source # | |
Defined in Cryptol.ModuleSystem.Env type Rep DynamicEnv = D1 ('MetaData "DynamicEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "DEnv" 'PrefixI 'True) (S1 ('MetaSel ('Just "deNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NamingEnv) :*: (S1 ('MetaSel ('Just "deDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DeclGroup]) :*: S1 ('MetaSel ('Just "deEnv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 EvalEnv)))) |
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 # | |
Defined in Cryptol.ModuleSystem.Monad Methods showsPrec :: Int -> ModuleError -> ShowS show :: ModuleError -> String showList :: [ModuleError] -> ShowS | |
NFData ModuleError Source # | |
Defined in Cryptol.ModuleSystem.Monad Methods rnf :: ModuleError -> () | |
PP ModuleError Source # | |
Defined in Cryptol.ModuleSystem.Monad Methods ppPrec :: Int -> ModuleError -> Doc Source # |
data ModuleWarning Source #
Constructors
TypeCheckWarnings [(Range, Warning)] | |
RenamerWarnings [RenamerWarning] |
Instances
Show ModuleWarning Source # | |
Defined in Cryptol.ModuleSystem.Monad Methods showsPrec :: Int -> ModuleWarning -> ShowS show :: ModuleWarning -> String showList :: [ModuleWarning] -> ShowS | |
Generic ModuleWarning Source # | |
Defined in Cryptol.ModuleSystem.Monad Associated Types type Rep ModuleWarning :: Type -> Type | |
NFData ModuleWarning Source # | |
Defined in Cryptol.ModuleSystem.Monad Methods rnf :: ModuleWarning -> () | |
PP ModuleWarning Source # | |
Defined in Cryptol.ModuleSystem.Monad Methods ppPrec :: Int -> ModuleWarning -> Doc Source # | |
type Rep ModuleWarning Source # | |
Defined in Cryptol.ModuleSystem.Monad type Rep ModuleWarning = D1 ('MetaData "ModuleWarning" "Cryptol.ModuleSystem.Monad" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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]))) |
type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning]) Source #
findModule :: ModName -> ModuleCmd ModulePath Source #
Find the file associated with a module name in the module search path.
loadModuleByPath :: FilePath -> ModuleCmd (ModulePath, Module) Source #
Load the module contained in the given file.
loadModuleByName :: ModName -> ModuleCmd (ModulePath, Module) Source #
Load the given parsed module.
checkExpr :: Expr PName -> ModuleCmd (Expr Name, Expr, Schema) Source #
Check the type of an expression. Give back the renamed expression, the core expression, and its type schema.
checkDecls :: [TopDecl PName] -> ModuleCmd (NamingEnv, [DeclGroup]) Source #
Typecheck top-level declarations.
evalDecls :: [DeclGroup] -> ModuleCmd () Source #
Evaluate declarations and add them to the extended environment.
noPat :: RemovePatterns a => a -> ModuleCmd a Source #
focusedEnv :: ModuleEnv -> (IfaceParams, IfaceDecls, NamingEnv, NameDisp) Source #
Produce an ifaceDecls that represents the focused environment of the module
system, as well as a NameDisp
for pretty-printing names according to the
imports.
XXX This could really do with some better error handling, just returning mempty when one of the imports fails isn't really desirable.
XXX: This is not quite right. For example, it does not take into account *how* things were imported in a module (e.g., qualified). It would be simpler to simply store the naming environment that was actually used when we renamed the module.
Interfaces
The resulting interface generated by a module that has been typechecked.
Constructors
Iface | |
Fields
|
Instances
Show Iface Source # | |
Generic Iface Source # | |
NFData Iface Source # | |
Defined in Cryptol.ModuleSystem.Interface | |
type Rep Iface Source # | |
Defined in Cryptol.ModuleSystem.Interface type Rep Iface = D1 ('MetaData "Iface" "Cryptol.ModuleSystem.Interface" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "Iface" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ifModName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModName) :*: S1 ('MetaSel ('Just "ifPublic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IfaceDecls)) :*: (S1 ('MetaSel ('Just "ifPrivate") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IfaceDecls) :*: S1 ('MetaSel ('Just "ifParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IfaceParams)))) |
data IfaceParams Source #
Constructors
IfaceParams | |
Fields
|
Instances
Show IfaceParams Source # | |
Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceParams -> ShowS show :: IfaceParams -> String showList :: [IfaceParams] -> ShowS | |
Generic IfaceParams Source # | |
Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep IfaceParams :: Type -> Type | |
NFData IfaceParams Source # | |
Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceParams -> () | |
type Rep IfaceParams Source # | |
Defined in Cryptol.ModuleSystem.Interface type Rep IfaceParams = D1 ('MetaData "IfaceParams" "Cryptol.ModuleSystem.Interface" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "IfaceParams" 'PrefixI 'True) (S1 ('MetaSel ('Just "ifParamTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name ModTParam)) :*: (S1 ('MetaSel ('Just "ifParamConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located Prop]) :*: S1 ('MetaSel ('Just "ifParamFuns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name ModVParam))))) |
data IfaceDecls Source #
Constructors
IfaceDecls | |
Fields
|
Instances
Show IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceDecls -> ShowS show :: IfaceDecls -> String showList :: [IfaceDecls] -> ShowS | |
Generic IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep IfaceDecls :: Type -> Type | |
Semigroup IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface Methods (<>) :: IfaceDecls -> IfaceDecls -> IfaceDecls # sconcat :: NonEmpty IfaceDecls -> IfaceDecls # stimes :: Integral b => b -> IfaceDecls -> IfaceDecls # | |
Monoid IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface Methods mempty :: IfaceDecls # mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls # mconcat :: [IfaceDecls] -> IfaceDecls # | |
NFData IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceDecls -> () | |
type Rep IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface type Rep IfaceDecls |
type IfaceTySyn = TySyn Source #
Constructors
IfaceDecl | |
Fields
|
Instances
Show IfaceDecl Source # | |
Generic IfaceDecl Source # | |
NFData IfaceDecl Source # | |
Defined in Cryptol.ModuleSystem.Interface | |
type Rep IfaceDecl Source # | |
Defined in Cryptol.ModuleSystem.Interface type Rep IfaceDecl = D1 ('MetaData "IfaceDecl" "Cryptol.ModuleSystem.Interface" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "IfaceDecl" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ifDeclName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name) :*: (S1 ('MetaSel ('Just "ifDeclSig") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Schema) :*: S1 ('MetaSel ('Just "ifDeclPragmas") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Pragma]))) :*: (S1 ('MetaSel ('Just "ifDeclInfix") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "ifDeclFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity)) :*: S1 ('MetaSel ('Just "ifDeclDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))))) |