Cryptol.ModuleSystem.Renamer.Imports

This module deals with imports of nested modules (import submodule). This is more complex than it might seem at first because to resolve a declaration like import submodule X we need to resolve what X referes to before we know what it will import.

Even triciker is the case for functor instantiations:

module M = F { X } import M

In this case, even if we know what M referes to, we first need to resolve F, so that we can generate the instantiation and generate fresh names for names defined by M.

If we want to support applicative semantics, then before instantiation M we also need to resolve X so that we know if this instantiation has already been generated.

An overall guiding principle of the design is that we assume that declarations can be ordered in dependency order, and submodules can be processed one at a time. In particular, this does not allow recursion across modules, or functor instantiations depending on their arguments.

Thus, the following is OK:

module A where x = 0x2

submodule B where y = x

z = B::y

However, this is not OK:

submodule A = F X submodule F where import A

Documentation

resolveImports :: (ImpName Name -> Mod ()) -> TopDef -> Supply -> (Map (ImpName Name) ResolvedLocal, Supply)

data ResolvedModule imps

This represents a resolved module or signaure. The type parameter helps us distinguish between two types of resolved modules:

1. Resolved modules that are *inputs* to the algorithm (i.e., they are defined outside the current module). For such modules the type parameter is imps is ()
2. Resolved modules that are *outputs* of the algorithm (i.e., they are defined within the current module). For such modules the type parameter imps contains the naming environment for things that came in through the import.

Note that signaures are never "imported", however we do need to keep them here so that signatures in a functor are properly instantiated when the functor is instantiated.

Constructors

ResolvedModule

Fields

• rmodDefines :: NamingEnv

  Things defined by the module/signature.

• rmodPublic :: !(Set Name)

  Exported names

• rmodKind :: ModKind

  What sort of thing are we

• rmodNested :: Set Name

  Modules and signatures nested in this one

• rmodImports :: imps

  Resolved imports. External modules need not specify this field, it is just part of the thing we compute for local modules.

data ModKind

Constructors

AFunctor

ASignature

AModule

Instances

Generic ModKind

Defined in Cryptol.ModuleSystem.Renamer.Error

Associated Types

type Rep ModKind :: Type -> Type

Methods

from :: ModKind -> Rep ModKind x

to :: Rep ModKind x -> ModKind

Show ModKind

Defined in Cryptol.ModuleSystem.Renamer.Error

Methods

showsPrec :: Int -> ModKind -> ShowS

show :: ModKind -> String

showList :: [ModKind] -> ShowS

PP ModKind

Defined in Cryptol.ModuleSystem.Renamer.Error

Methods

ppPrec :: Int -> ModKind -> Doc

NFData ModKind

Defined in Cryptol.ModuleSystem.Renamer.Error

Methods

rnf :: ModKind -> ()

Eq ModKind

Defined in Cryptol.ModuleSystem.Renamer.Error

Methods

(==) :: ModKind -> ModKind -> Bool

(/=) :: ModKind -> ModKind -> Bool

Ord ModKind

Defined in Cryptol.ModuleSystem.Renamer.Error

Methods

compare :: ModKind -> ModKind -> Ordering

(<) :: ModKind -> ModKind -> Bool

(<=) :: ModKind -> ModKind -> Bool

(>) :: ModKind -> ModKind -> Bool

(>=) :: ModKind -> ModKind -> Bool

max :: ModKind -> ModKind -> ModKind

min :: ModKind -> ModKind -> ModKind

type Rep ModKind

Defined in Cryptol.ModuleSystem.Renamer.Error

type Rep ModKind = D1 ('MetaData "ModKind" "Cryptol.ModuleSystem.Renamer.Error" "cryptol-3.2.0-35bDsq0QUVdvBXha47jji" 'False) (C1 ('MetaCons "AFunctor" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ASignature" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AModule" 'PrefixI 'False) (U1 :: Type -> Type)))

type ResolvedLocal = ResolvedModule NamingEnv

A resolved module that's defined in (or is) the current top-level module

type ResolvedExt = ResolvedModule ()

A resolved module that's not defined in the current top-level module