| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Cryptol.ModuleSystem
Description
Synopsis
- data ModuleEnv = ModuleEnv {}
- initialModuleEnv :: IO ModuleEnv
- data DynamicEnv = DEnv {}
- data ModuleError
- = ModuleNotFound ImportSource 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
- data ModuleWarning
- type ModuleCmd a = ModuleInput IO -> IO (ModuleRes a)
- type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning])
- data ModuleInput (m :: Type -> Type) = ModuleInput {}
- findModule :: ModName -> ModuleCmd ModulePath
- loadModuleByPath :: FilePath -> ModuleCmd (ModulePath, TCTopEntity)
- loadModuleByName :: ModName -> ModuleCmd (ModulePath, TCTopEntity)
- checkModuleByPath :: FilePath -> ModuleCmd (ModulePath, TCTopEntity)
- checkExpr :: Expr PName -> ModuleCmd (Expr Name, Expr, Schema)
- evalExpr :: Expr -> ModuleCmd Value
- benchmarkExpr :: Double -> Expr -> ModuleCmd BenchmarkStats
- checkDecls :: [TopDecl PName] -> ModuleCmd (NamingEnv, [DeclGroup], Map Name TySyn)
- evalDecls :: [DeclGroup] -> ModuleCmd ()
- noPat :: RemovePatterns a => a -> ModuleCmd a
- focusedEnv :: ModuleEnv -> ModContext
- getPrimMap :: ModuleCmd PrimMap
- renameVar :: NamingEnv -> PName -> ModuleCmd Name
- renameType :: NamingEnv -> PName -> ModuleCmd Name
- setFocusedModule :: ImpName Name -> ModuleM ()
- renameImpNameInCurrentEnv :: ImpName PName -> ModuleM (ImpName Name)
- impNameTopModule :: ImpName Name -> ModName
- type Iface = IfaceG ModName
- data IfaceG name = Iface {
- ifNames :: IfaceNames name
- ifParams :: FunctorParams
- ifDefines :: IfaceDecls
- data IfaceDecls = IfaceDecls {
- ifTySyns :: Map Name TySyn
- ifNominalTypes :: Map Name NominalType
- ifDecls :: Map Name IfaceDecl
- ifModules :: !(Map Name (IfaceNames Name))
- ifSignatures :: !(Map Name ModParamNames)
- ifFunctors :: !(Map Name (IfaceG Name))
- genIface :: ModuleG name -> IfaceG name
- data IfaceDecl = IfaceDecl {
- ifDeclName :: !Name
- ifDeclSig :: Schema
- ifDeclIsPrim :: !Bool
- ifDeclPragmas :: [Pragma]
- ifDeclInfix :: Bool
- ifDeclFixity :: Maybe Fixity
- ifDeclDoc :: Maybe Text
- getFileDependencies :: FilePath -> ModuleCmd (ModulePath, FileInfo)
- getModuleDependencies :: ModName -> ModuleCmd (ModulePath, FileInfo)
Module System
This is the current state of the interpreter.
Constructors
| ModuleEnv | |
Fields
| |
Instances
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.
Constructors
| DEnv | |
Instances
| Monoid DynamicEnv Source # | |||||
Defined in Cryptol.ModuleSystem.Env Methods mempty :: DynamicEnv # mappend :: DynamicEnv -> DynamicEnv -> DynamicEnv # mconcat :: [DynamicEnv] -> DynamicEnv # | |||||
| Semigroup DynamicEnv Source # | |||||
Defined in Cryptol.ModuleSystem.Env Methods (<>) :: DynamicEnv -> DynamicEnv -> DynamicEnv # sconcat :: NonEmpty DynamicEnv -> DynamicEnv # stimes :: Integral b => b -> DynamicEnv -> DynamicEnv # | |||||
| Generic DynamicEnv Source # | |||||
Defined in Cryptol.ModuleSystem.Env Associated Types
| |||||
| type Rep DynamicEnv Source # | |||||
Defined in Cryptol.ModuleSystem.Env type Rep DynamicEnv = D1 ('MetaData "DynamicEnv" "Cryptol.ModuleSystem.Env" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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 "deTySyns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name TySyn)) :*: S1 ('MetaSel ('Just "deEnv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 EvalEnv)))) | |||||
data ModuleError Source #
Constructors
| ModuleNotFound ImportSource 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
| Show ModuleError Source # | |
Defined in Cryptol.ModuleSystem.Monad Methods showsPrec :: Int -> ModuleError -> ShowS # show :: ModuleError -> String # showList :: [ModuleError] -> ShowS # | |
| PP ModuleError Source # | |
Defined in Cryptol.ModuleSystem.Monad Methods ppPrec :: Int -> ModuleError -> Doc Source # ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> ModuleError -> Doc Source # | |
| NFData ModuleError Source # | |
Defined in Cryptol.ModuleSystem.Monad Methods rnf :: ModuleError -> () # | |
data ModuleWarning Source #
Constructors
| TypeCheckWarnings NameMap [(Range, Warning)] | |
| RenamerWarnings [RenamerWarning] |
Instances
| Generic ModuleWarning Source # | |||||
Defined in Cryptol.ModuleSystem.Monad Associated Types
| |||||
| Show ModuleWarning Source # | |||||
Defined in Cryptol.ModuleSystem.Monad Methods showsPrec :: Int -> ModuleWarning -> ShowS # show :: ModuleWarning -> String # showList :: [ModuleWarning] -> ShowS # | |||||
| PP ModuleWarning Source # | |||||
Defined in Cryptol.ModuleSystem.Monad Methods ppPrec :: Int -> ModuleWarning -> Doc Source # ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> ModuleWarning -> Doc Source # | |||||
| NFData ModuleWarning Source # | |||||
Defined in Cryptol.ModuleSystem.Monad Methods rnf :: ModuleWarning -> () # | |||||
| type Rep ModuleWarning Source # | |||||
Defined in Cryptol.ModuleSystem.Monad type Rep ModuleWarning = D1 ('MetaData "ModuleWarning" "Cryptol.ModuleSystem.Monad" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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]))) | |||||
type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning]) Source #
data ModuleInput (m :: Type -> Type) Source #
Constructors
| ModuleInput | |
Fields
| |
findModule :: ModName -> ModuleCmd ModulePath Source #
Find the file associated with a module name in the module search path.
loadModuleByPath :: FilePath -> ModuleCmd (ModulePath, TCTopEntity) Source #
Load the module contained in the given file.
loadModuleByName :: ModName -> ModuleCmd (ModulePath, TCTopEntity) Source #
Load the given parsed module.
checkModuleByPath :: FilePath -> ModuleCmd (ModulePath, TCTopEntity) Source #
Parse and typecheck a module, but don't evaluate or change the environment.
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.
benchmarkExpr :: Double -> Expr -> ModuleCmd BenchmarkStats Source #
Benchmark an expression.
checkDecls :: [TopDecl PName] -> ModuleCmd (NamingEnv, [DeclGroup], Map Name TySyn) 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 -> ModContext Source #
focusedEnv me - Given me, the state of the environment, compute
information about what's in scope on the REPL. This includes
what's in the focused module (`meFocusedModule me`), plus any
additional definitions from the REPL (e.g., let bound names, and
it).
renameVar :: NamingEnv -> PName -> ModuleCmd Name Source #
Rename a *use* of a value name. The distinction between uses and binding is used to keep track of dependencies.
renameType :: NamingEnv -> PName -> ModuleCmd Name Source #
Rename a *use* of a type name. The distinction between uses and binding is used to keep track of dependencies.
Interfaces
The interface representing a typechecked top-level module.
Constructors
| Iface | |
Fields
| |
Instances
| Functor IfaceG Source # | |||||
| Generic (IfaceG name) Source # | |||||
Defined in Cryptol.ModuleSystem.Interface Associated Types
| |||||
| Show name => Show (IfaceG name) Source # | |||||
| NFData name => NFData (IfaceG name) Source # | |||||
Defined in Cryptol.ModuleSystem.Interface | |||||
| type Rep (IfaceG name) Source # | |||||
Defined in Cryptol.ModuleSystem.Interface type Rep (IfaceG name) = D1 ('MetaData "IfaceG" "Cryptol.ModuleSystem.Interface" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "Iface" 'PrefixI 'True) (S1 ('MetaSel ('Just "ifNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (IfaceNames name)) :*: (S1 ('MetaSel ('Just "ifParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FunctorParams) :*: S1 ('MetaSel ('Just "ifDefines") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IfaceDecls)))) | |||||
data IfaceDecls Source #
Declarations in a module. Note that this includes things from nested
modules, but not things from nested functors, which are in ifFunctors.
Constructors
| IfaceDecls | |
Fields
| |
Instances
| Monoid IfaceDecls Source # | |||||
Defined in Cryptol.ModuleSystem.Interface Methods mempty :: IfaceDecls # mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls # mconcat :: [IfaceDecls] -> IfaceDecls # | |||||
| Semigroup IfaceDecls Source # | |||||
Defined in Cryptol.ModuleSystem.Interface Methods (<>) :: IfaceDecls -> IfaceDecls -> IfaceDecls # sconcat :: NonEmpty IfaceDecls -> IfaceDecls # stimes :: Integral b => b -> IfaceDecls -> IfaceDecls # | |||||
| Generic IfaceDecls Source # | |||||
Defined in Cryptol.ModuleSystem.Interface Associated Types
| |||||
| Show IfaceDecls Source # | |||||
Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceDecls -> ShowS # show :: IfaceDecls -> String # showList :: [IfaceDecls] -> ShowS # | |||||
| NFData IfaceDecls Source # | |||||
Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceDecls -> () # | |||||
| type Rep IfaceDecls Source # | |||||
Defined in Cryptol.ModuleSystem.Interface type Rep IfaceDecls = D1 ('MetaData "IfaceDecls" "Cryptol.ModuleSystem.Interface" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "IfaceDecls" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ifTySyns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name TySyn)) :*: (S1 ('MetaSel ('Just "ifNominalTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name NominalType)) :*: S1 ('MetaSel ('Just "ifDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name IfaceDecl)))) :*: (S1 ('MetaSel ('Just "ifModules") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map Name (IfaceNames Name))) :*: (S1 ('MetaSel ('Just "ifSignatures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map Name ModParamNames)) :*: S1 ('MetaSel ('Just "ifFunctors") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map Name (IfaceG Name))))))) | |||||
Constructors
| IfaceDecl | |
Fields
| |
Instances
| Generic IfaceDecl Source # | |||||
Defined in Cryptol.ModuleSystem.Interface Associated Types
| |||||
| Show 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-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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 "ifDeclIsPrim") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool))) :*: ((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 Text)))))) | |||||
Dependencies
getFileDependencies :: FilePath -> ModuleCmd (ModulePath, FileInfo) Source #
Get information about the dependencies of a file.
getModuleDependencies :: ModName -> ModuleCmd (ModulePath, FileInfo) Source #
Get information about the dependencies of a module.