cryptol-2.4.0: Cryptol: The Language of Cryptography

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

Cryptol.ModuleSystem

Contents

- Module System
- Interfaces

Description

Synopsis

- data ModuleEnv = ModuleEnv {
  - meLoadedModules :: LoadedModules
  - meNameSeeds :: NameSeeds
  - meEvalEnv :: EvalEnv
  - meFocusedModule :: Maybe ModName
  - meSearchPath :: [FilePath]
  - meDynEnv :: DynamicEnv
  - meMonoBinds :: !Bool
  - meSolverConfig :: SolverConfig
  - meCoreLint :: CoreLint
  - meSupply :: !Supply
  }
- initialModuleEnv :: IO ModuleEnv
- data DynamicEnv = DEnv {
  - deNames :: NamingEnv
  - deDecls :: [DeclGroup]
  - deEnv :: EvalEnv
  }
- data ModuleError
  - = ModuleNotFound ModName [FilePath]
  - | CantFindFile FilePath
  - | OtherIOError FilePath IOException
  - | ModuleParseError FilePath 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
- data ModuleWarning
  - = TypeCheckWarnings [(Range, Warning)]
  - | RenamerWarnings [RenamerWarning]
- type ModuleCmd a = ModuleEnv -> IO (ModuleRes a)
- type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning])
- findModule :: ModName -> ModuleCmd FilePath
- loadModuleByPath :: FilePath -> ModuleCmd Module
- loadModule :: FilePath -> Module PName -> ModuleCmd 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 -> (IfaceDecls, NamingEnv, NameDisp)
- getPrimMap :: ModuleCmd PrimMap
- renameVar :: NamingEnv -> PName -> ModuleCmd Name
- renameType :: NamingEnv -> PName -> ModuleCmd Name
- data Iface = Iface {
  - ifModName :: !ModName
  - ifPublic :: IfaceDecls
  - ifPrivate :: IfaceDecls
  }
- data IfaceDecls = IfaceDecls {
  - ifTySyns :: Map Name IfaceTySyn
  - ifNewtypes :: Map Name IfaceNewtype
  - 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 #

Constructors

ModuleEnv |

Fields

- meLoadedModules :: LoadedModules
- meNameSeeds :: NameSeeds
- meEvalEnv :: EvalEnv
- meFocusedModule :: Maybe ModName
- meSearchPath :: [FilePath]
- meDynEnv :: DynamicEnv
- meMonoBinds :: !Bool
- meSolverConfig :: SolverConfig
- meCoreLint :: CoreLint
- meSupply :: !Supply

Instances

Generic ModuleEnv Source # |
Associated Types type Rep ModuleEnv :: * -> * # Methods from :: ModuleEnv -> Rep ModuleEnv x # to :: Rep ModuleEnv x -> ModuleEnv #
NFData ModuleEnv Source # |
Methods rnf :: ModuleEnv -> () #
type Rep ModuleEnv Source # |

type Rep ModuleEnv = D1 (MetaData "ModuleEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "ModuleEnv" PrefixI True) ((:*:) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "meLoadedModules") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 LoadedModules)) (S1 (MetaSel (Just Symbol "meNameSeeds") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameSeeds))) ((:*:) (S1 (MetaSel (Just Symbol "meEvalEnv") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 EvalEnv)) ((:*:) (S1 (MetaSel (Just Symbol "meFocusedModule") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe ModName))) (S1 (MetaSel (Just Symbol "meSearchPath") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [FilePath]))))) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "meDynEnv") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 DynamicEnv)) (S1 (MetaSel (Just Symbol "meMonoBinds") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Bool))) ((:*:) (S1 (MetaSel (Just Symbol "meSolverConfig") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 SolverConfig)) ((:*:) (S1 (MetaSel (Just Symbol "meCoreLint") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 CoreLint)) (S1 (MetaSel (Just Symbol "meSupply") NoSourceUnpackedness SourceStrict DecidedUnpack) (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 # |
Associated Types type Rep DynamicEnv :: * -> * # Methods from :: DynamicEnv -> Rep DynamicEnv x # to :: Rep DynamicEnv x -> DynamicEnv #
Monoid DynamicEnv Source # |
Methods mempty :: DynamicEnv # mappend :: DynamicEnv -> DynamicEnv -> DynamicEnv # mconcat :: [DynamicEnv] -> DynamicEnv #
NFData DynamicEnv Source # |
Methods rnf :: DynamicEnv -> () #
type Rep DynamicEnv Source # |

type Rep DynamicEnv = D1 (MetaData "DynamicEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "DEnv" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "deNames") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NamingEnv)) ((:*:) (S1 (MetaSel (Just Symbol "deDecls") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [DeclGroup])) (S1 (MetaSel (Just Symbol "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
OtherIOError FilePath IOException | Some other IO error occurred while reading this file
ModuleParseError FilePath 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

Instances

Show ModuleError Source # |
Methods showsPrec :: Int -> ModuleError -> ShowS # show :: ModuleError -> String # showList :: [ModuleError] -> ShowS #
NFData ModuleError Source # |
Methods rnf :: ModuleError -> () #
PP ModuleError Source # |
Methods ppPrec :: Int -> ModuleError -> Doc Source #

data ModuleWarning Source #

Constructors

TypeCheckWarnings [(Range, Warning)] |
RenamerWarnings [RenamerWarning] |

Instances

Show ModuleWarning Source # |
Methods showsPrec :: Int -> ModuleWarning -> ShowS # show :: ModuleWarning -> String # showList :: [ModuleWarning] -> ShowS #
Generic ModuleWarning Source # |
Associated Types type Rep ModuleWarning :: * -> * # Methods from :: ModuleWarning -> Rep ModuleWarning x # to :: Rep ModuleWarning x -> ModuleWarning #
NFData ModuleWarning Source # |
Methods rnf :: ModuleWarning -> () #
PP ModuleWarning Source # |
Methods ppPrec :: Int -> ModuleWarning -> Doc Source #
type Rep ModuleWarning Source # |

type Rep ModuleWarning = D1 (MetaData "ModuleWarning" "Cryptol.ModuleSystem.Monad" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "TypeCheckWarnings" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Range, Warning)]))) (C1 (MetaCons "RenamerWarnings" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [RenamerWarning]))))

type ModuleCmd a = ModuleEnv -> IO (ModuleRes a) Source #

type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning]) Source #

findModule :: ModName -> ModuleCmd FilePath Source #

Find the file associated with a module name in the module search path.

loadModuleByPath :: FilePath -> ModuleCmd Module Source #

Load the module contained in the given file.

loadModule :: FilePath -> Module PName -> ModuleCmd 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 -> (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.

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
- ifPublic :: IfaceDecls
- ifPrivate :: IfaceDecls

Instances

Show Iface Source # |
Methods showsPrec :: Int -> Iface -> ShowS # show :: Iface -> String # showList :: [Iface] -> ShowS #
Generic Iface Source # |
Associated Types type Rep Iface :: * -> * # Methods from :: Iface -> Rep Iface x # to :: Rep Iface x -> Iface #
NFData Iface Source # |
Methods rnf :: Iface -> () #
type Rep Iface Source # |

type Rep Iface = D1 (MetaData "Iface" "Cryptol.ModuleSystem.Interface" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "Iface" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "ifModName") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 ModName)) ((:*:) (S1 (MetaSel (Just Symbol "ifPublic") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IfaceDecls)) (S1 (MetaSel (Just Symbol "ifPrivate") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IfaceDecls)))))

data IfaceDecls Source #

Constructors

IfaceDecls |

Fields

- ifTySyns :: Map Name IfaceTySyn
- ifNewtypes :: Map Name IfaceNewtype
- ifDecls :: Map Name IfaceDecl

Instances

Show IfaceDecls Source # |
Methods showsPrec :: Int -> IfaceDecls -> ShowS # show :: IfaceDecls -> String # showList :: [IfaceDecls] -> ShowS #
Generic IfaceDecls Source # |
Associated Types type Rep IfaceDecls :: * -> * # Methods from :: IfaceDecls -> Rep IfaceDecls x # to :: Rep IfaceDecls x -> IfaceDecls #
Monoid IfaceDecls Source # |
Methods mempty :: IfaceDecls # mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls # mconcat :: [IfaceDecls] -> IfaceDecls #
NFData IfaceDecls Source # |
Methods rnf :: IfaceDecls -> () #
type Rep IfaceDecls Source # |

type Rep IfaceDecls = D1 (MetaData "IfaceDecls" "Cryptol.ModuleSystem.Interface" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "IfaceDecls" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "ifTySyns") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map Name IfaceTySyn))) ((:*:) (S1 (MetaSel (Just Symbol "ifNewtypes") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map Name IfaceNewtype))) (S1 (MetaSel (Just Symbol "ifDecls") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map Name IfaceDecl))))))

genIface :: Module -> Iface Source #

Generate an Iface from a typechecked module.

type IfaceTySyn = TySyn Source #

data IfaceDecl Source #

Constructors

IfaceDecl |

Fields

- ifDeclName :: !Name
- ifDeclSig :: Schema
- ifDeclPragmas :: [Pragma]
- ifDeclInfix :: Bool
- ifDeclFixity :: Maybe Fixity
- ifDeclDoc :: Maybe String

Instances

Show IfaceDecl Source # |
Methods showsPrec :: Int -> IfaceDecl -> ShowS # show :: IfaceDecl -> String # showList :: [IfaceDecl] -> ShowS #
Generic IfaceDecl Source # |
Associated Types type Rep IfaceDecl :: * -> * # Methods from :: IfaceDecl -> Rep IfaceDecl x # to :: Rep IfaceDecl x -> IfaceDecl #
NFData IfaceDecl Source # |
Methods rnf :: IfaceDecl -> () #
type Rep IfaceDecl Source # |

type Rep IfaceDecl = D1 (MetaData "IfaceDecl" "Cryptol.ModuleSystem.Interface" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "IfaceDecl" PrefixI True) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "ifDeclName") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Name)) ((:*:) (S1 (MetaSel (Just Symbol "ifDeclSig") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Schema)) (S1 (MetaSel (Just Symbol "ifDeclPragmas") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Pragma])))) ((:*:) (S1 (MetaSel (Just Symbol "ifDeclInfix") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) ((:*:) (S1 (MetaSel (Just Symbol "ifDeclFixity") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Fixity))) (S1 (MetaSel (Just Symbol "ifDeclDoc") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe String)))))))