Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	None
Language	Haskell2010

Cryptol.ModuleSystem

Contents

Module System
Interfaces

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 {
- deNames :: NamingEnv
- deDecls :: [DeclGroup]
- deEnv :: EvalEnv
}
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
- = TypeCheckWarnings [(Range, Warning)]
- | RenamerWarnings [RenamerWarning]
type ModuleCmd a = (EvalOpts, FilePath -> IO ByteString, 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 -> ModContext
getPrimMap :: ModuleCmd PrimMap
renameVar :: NamingEnv -> PName -> ModuleCmd Name
renameType :: NamingEnv -> PName -> ModuleCmd Name
data Iface = Iface {
- ifModName :: !ModName
- ifPublic :: IfaceDecls
- ifPrivate :: IfaceDecls
- ifParams :: IfaceParams
}
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

data ModuleEnv Source #

This is the current state of the interpreter.

Constructors

ModuleEnv

Fields

meLoadedModules :: LoadedModules
Information about all loaded modules. See LoadedModule. Contains information such as the file where the module was loaded from, as well as the module's interface, used for type checking.
meNameSeeds :: NameSeeds
A source of new names for the type checker.
meSolverConfig :: SolverConfig
Configuration settings for the SMT solver used for type-checking.
meEvalEnv :: EvalEnv
The evaluation environment. Contains the values for all loaded modules, both public and private.
meCoreLint :: CoreLint
Should we run the linter to ensure sanity.
meMonoBinds :: !Bool
Are we assuming that local bindings are monomorphic. XXX: We should probably remove this flag, and set it to True.
meFocusedModule :: Maybe ModName
The "current" module. Used to decide how to print names, for example.
meSearchPath :: [FilePath]
Where we look for things.
meDynEnv :: DynamicEnv
This contains additional definitions that were made at the command line, and so they don't reside in any module.
meSupply :: !Supply
Name source for the renamer

Instances

Generic ModuleEnv Source #
Instance details Defined in Cryptol.ModuleSystem.Env Associated Types type Rep ModuleEnv :: Type -> Type # Methods from :: ModuleEnv -> Rep ModuleEnv x # to :: Rep ModuleEnv x -> ModuleEnv #
NFData ModuleEnv Source #
Instance details Defined in Cryptol.ModuleSystem.Env Methods rnf :: ModuleEnv -> () #
type Rep ModuleEnv Source #
Instance details Defined in Cryptol.ModuleSystem.Env type Rep ModuleEnv = D1 (MetaData "ModuleEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.9.0-4aSi1YZNBynFQwh9aOpllR" 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.

Constructors

DEnv
Fields deNames :: NamingEnv deDecls :: [DeclGroup] deEnv :: EvalEnv

Instances

Generic DynamicEnv Source #
Instance details Defined in Cryptol.ModuleSystem.Env Associated Types type Rep DynamicEnv :: Type -> Type # Methods from :: DynamicEnv -> Rep DynamicEnv x # to :: Rep DynamicEnv x -> DynamicEnv #
Semigroup DynamicEnv Source #
Instance details Defined in Cryptol.ModuleSystem.Env Methods (<>) :: DynamicEnv -> DynamicEnv -> DynamicEnv # sconcat :: NonEmpty DynamicEnv -> DynamicEnv # stimes :: Integral b => b -> DynamicEnv -> DynamicEnv #
Monoid DynamicEnv Source #
Instance details Defined in Cryptol.ModuleSystem.Env Methods mempty :: DynamicEnv # mappend :: DynamicEnv -> DynamicEnv -> DynamicEnv # mconcat :: [DynamicEnv] -> DynamicEnv #
type Rep DynamicEnv Source #
Instance details Defined in Cryptol.ModuleSystem.Env type Rep DynamicEnv = D1 (MetaData "DynamicEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.9.0-4aSi1YZNBynFQwh9aOpllR" 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 #
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 #

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.9.0-4aSi1YZNBynFQwh9aOpllR" 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 ModuleCmd a = (EvalOpts, FilePath -> IO ByteString, ModuleEnv) -> IO (ModuleRes a) Source #

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.

evalExpr :: Expr -> ModuleCmd Value Source #

Evaluate an expression.

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 -> ModContext Source #

Given the state of the environment, compute information about what's in scope on the REPL. This includes what's in the focused module, plus any additional definitions from the REPL (e.g., let bound names, and it).

getPrimMap :: ModuleCmd PrimMap Source #

renameVar :: NamingEnv -> PName -> ModuleCmd Name Source #

renameType :: NamingEnv -> PName -> ModuleCmd Name Source #

Interfaces

data Iface Source #

The resulting interface generated by a module that has been typechecked.

Constructors

Iface
Fields ifModName :: !ModName Module name ifPublic :: IfaceDecls Exported definitions ifPrivate :: IfaceDecls Private defintiions ifParams :: IfaceParams Uninterpreted constants (aka module params)

Instances

Show Iface Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> Iface -> ShowS # show :: Iface -> String # showList :: [Iface] -> ShowS #
Generic Iface Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep Iface :: Type -> Type # Methods from :: Iface -> Rep Iface x # to :: Rep Iface x -> Iface #
NFData Iface Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: Iface -> () #
type Rep Iface Source #
Instance details Defined in Cryptol.ModuleSystem.Interface type Rep Iface = D1 (MetaData "Iface" "Cryptol.ModuleSystem.Interface" "cryptol-2.9.0-4aSi1YZNBynFQwh9aOpllR" 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 ifParamTypes :: Map Name ModTParam ifParamConstraints :: [Located Prop] Constraints on param. types ifParamFuns :: Map Name ModVParam

Instances

Show IfaceParams Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceParams -> ShowS # show :: IfaceParams -> String # showList :: [IfaceParams] -> ShowS #
Generic IfaceParams Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep IfaceParams :: Type -> Type # Methods from :: IfaceParams -> Rep IfaceParams x # to :: Rep IfaceParams x -> IfaceParams #
NFData IfaceParams Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceParams -> () #
type Rep IfaceParams Source #
Instance details Defined in Cryptol.ModuleSystem.Interface type Rep IfaceParams = D1 (MetaData "IfaceParams" "Cryptol.ModuleSystem.Interface" "cryptol-2.9.0-4aSi1YZNBynFQwh9aOpllR" 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 ifTySyns :: Map Name IfaceTySyn ifNewtypes :: Map Name IfaceNewtype ifAbstractTypes :: Map Name IfaceAbstractType ifDecls :: Map Name IfaceDecl

Instances

Show IfaceDecls Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceDecls -> ShowS # show :: IfaceDecls -> String # showList :: [IfaceDecls] -> ShowS #
Generic IfaceDecls Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep IfaceDecls :: Type -> Type # Methods from :: IfaceDecls -> Rep IfaceDecls x # to :: Rep IfaceDecls x -> IfaceDecls #
Semigroup IfaceDecls Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods (<>) :: IfaceDecls -> IfaceDecls -> IfaceDecls # sconcat :: NonEmpty IfaceDecls -> IfaceDecls # stimes :: Integral b => b -> IfaceDecls -> IfaceDecls #
Monoid IfaceDecls Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods mempty :: IfaceDecls # mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls # mconcat :: [IfaceDecls] -> IfaceDecls #
NFData IfaceDecls Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceDecls -> () #
type Rep IfaceDecls Source #
Instance details Defined in Cryptol.ModuleSystem.Interface type Rep IfaceDecls

genIface :: Module -> Iface Source #

Generate an Iface from a typechecked module.

type IfaceTySyn = TySyn Source #

data IfaceDecl Source #

Constructors

IfaceDecl
Fields ifDeclName :: !Name Name of thing ifDeclSig :: Schema Type ifDeclPragmas :: [Pragma] Pragmas ifDeclInfix :: Bool Is this an infix thing ifDeclFixity :: Maybe Fixity Fixity information ifDeclDoc :: Maybe String Documentation

Instances

Show IfaceDecl Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceDecl -> ShowS # show :: IfaceDecl -> String # showList :: [IfaceDecl] -> ShowS #
Generic IfaceDecl Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep IfaceDecl :: Type -> Type # Methods from :: IfaceDecl -> Rep IfaceDecl x # to :: Rep IfaceDecl x -> IfaceDecl #
NFData IfaceDecl Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceDecl -> () #
type Rep IfaceDecl Source #
Instance details Defined in Cryptol.ModuleSystem.Interface type Rep IfaceDecl = D1 (MetaData "IfaceDecl" "Cryptol.ModuleSystem.Interface" "cryptol-2.9.0-4aSi1YZNBynFQwh9aOpllR" 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))))))