Cryptol.ModuleSystem

Module System

data ModuleEnv

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

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

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: ModuleEnv -> ()

type Rep ModuleEnv

Defined in Cryptol.ModuleSystem.Env

type Rep ModuleEnv = D1 (MetaData "ModuleEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

data DynamicEnv

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

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

Defined in Cryptol.ModuleSystem.Env

Methods

(<>) :: DynamicEnv -> DynamicEnv -> DynamicEnv

sconcat :: NonEmpty DynamicEnv -> DynamicEnv

stimes :: Integral b => b -> DynamicEnv -> DynamicEnv

Monoid DynamicEnv

Defined in Cryptol.ModuleSystem.Env

Methods

mempty :: DynamicEnv

mappend :: DynamicEnv -> DynamicEnv -> DynamicEnv

mconcat :: [DynamicEnv] -> DynamicEnv

NFData DynamicEnv

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: DynamicEnv -> ()

type Rep DynamicEnv

Defined in Cryptol.ModuleSystem.Env

type Rep DynamicEnv = D1 (MetaData "DynamicEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

ModuleNotFound ModName [FilePath]

Unable to find the module given, tried looking in these paths

CantFindFile FilePath

Unable to open a file

BadUtf8 FilePath UnicodeException

Bad UTF-8 encoding in while decoding this 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

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

data ModuleWarning

Constructors

TypeCheckWarnings [(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.7.0-6VD9sMh08R1JPrYSq7DH8b" 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, ModuleEnv) -> IO (ModuleRes a)

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

findModule :: ModName -> ModuleCmd FilePath

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

loadModuleByPath :: FilePath -> ModuleCmd (FilePath, Module)

Load the module contained in the given file.

loadModuleByName :: ModName -> ModuleCmd (FilePath, Module)

Load the given parsed module.

checkExpr :: Expr PName -> ModuleCmd (Expr Name, Expr, Schema)

Check the type of an expression. Give back the renamed expression, the core expression, and its type schema.

evalExpr :: Expr -> ModuleCmd Value

Evaluate an expression.

checkDecls :: [TopDecl PName] -> ModuleCmd (NamingEnv, [DeclGroup])

Typecheck top-level declarations.

evalDecls :: [DeclGroup] -> ModuleCmd ()

Evaluate declarations and add them to the extended environment.

noPat :: RemovePatterns a => a -> ModuleCmd a

focusedEnv :: ModuleEnv -> (IfaceParams, IfaceDecls, NamingEnv, NameDisp)

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.

getPrimMap :: ModuleCmd PrimMap

renameVar :: NamingEnv -> PName -> ModuleCmd Name

renameType :: NamingEnv -> PName -> ModuleCmd Name

Interfaces

data Iface

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

Defined in Cryptol.ModuleSystem.Interface

Methods

showsPrec :: Int -> Iface -> ShowS

show :: Iface -> String

showList :: [Iface] -> ShowS

Generic Iface

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

Defined in Cryptol.ModuleSystem.Interface

Methods

rnf :: Iface -> ()

type Rep Iface

Defined in Cryptol.ModuleSystem.Interface

type Rep Iface = D1 (MetaData "Iface" "Cryptol.ModuleSystem.Interface" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

IfaceParams

Fields

• ifParamTypes :: Map Name ModTParam
• ifParamConstraints :: [Located Prop]

  Constraints on param. types

• ifParamFuns :: Map Name ModVParam

Instances

Show IfaceParams

Defined in Cryptol.ModuleSystem.Interface

Methods

showsPrec :: Int -> IfaceParams -> ShowS

show :: IfaceParams -> String

showList :: [IfaceParams] -> ShowS

Generic IfaceParams

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

Defined in Cryptol.ModuleSystem.Interface

Methods

rnf :: IfaceParams -> ()

type Rep IfaceParams

Defined in Cryptol.ModuleSystem.Interface

type Rep IfaceParams = D1 (MetaData "IfaceParams" "Cryptol.ModuleSystem.Interface" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

IfaceDecls

Fields

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

Instances

Show IfaceDecls

Defined in Cryptol.ModuleSystem.Interface

Methods

showsPrec :: Int -> IfaceDecls -> ShowS

show :: IfaceDecls -> String

showList :: [IfaceDecls] -> ShowS

Generic IfaceDecls

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

Defined in Cryptol.ModuleSystem.Interface

Methods

(<>) :: IfaceDecls -> IfaceDecls -> IfaceDecls

sconcat :: NonEmpty IfaceDecls -> IfaceDecls

stimes :: Integral b => b -> IfaceDecls -> IfaceDecls

Monoid IfaceDecls

Defined in Cryptol.ModuleSystem.Interface

Methods

mempty :: IfaceDecls

mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls

mconcat :: [IfaceDecls] -> IfaceDecls

NFData IfaceDecls

Defined in Cryptol.ModuleSystem.Interface

Methods

rnf :: IfaceDecls -> ()

type Rep IfaceDecls

Defined in Cryptol.ModuleSystem.Interface

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

genIface :: Module -> Iface

Generate an Iface from a typechecked module.

type IfaceTySyn = TySyn

data IfaceDecl

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

Defined in Cryptol.ModuleSystem.Interface

Methods

showsPrec :: Int -> IfaceDecl -> ShowS

show :: IfaceDecl -> String

showList :: [IfaceDecl] -> ShowS

Generic IfaceDecl

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

Defined in Cryptol.ModuleSystem.Interface

Methods

rnf :: IfaceDecl -> ()

type Rep IfaceDecl

Defined in Cryptol.ModuleSystem.Interface

type Rep IfaceDecl = D1 (MetaData "IfaceDecl" "Cryptol.ModuleSystem.Interface" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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))))))