cryptol-3.0.0: Cryptol: The Language of Cryptography

Safe Haskell | Safe-Inferred
Language | Haskell2010

Cryptol.ModuleSystem.Renamer.Imports

Description

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

Synopsis

- resolveImports :: (ImpName Name -> Mod ()) -> TopDef -> Supply -> (Map (ImpName Name) ResolvedLocal, Supply)
- data ResolvedModule imps = ResolvedModule {
  - rmodDefines :: NamingEnv
  - rmodPublic :: !(Set Name)
  - rmodKind :: ModKind
  - rmodNested :: Set Name
  - rmodImports :: imps
  }
- data ModKind
  - = AFunctor
  - | ASignature
  - | AModule
- type ResolvedLocal = ResolvedModule NamingEnv
- type ResolvedExt = ResolvedModule ()

# Documentation

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

data ResolvedModule imps Source #

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

Constructors

AFunctor |
ASignature |
AModule |

#### Instances

Instances details

Generic ModKind Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer.Error Associated Types type Rep ModKind :: Type -> Type Source # Methods from :: ModKind -> Rep ModKind x Source # to :: Rep ModKind x -> ModKind Source #
Show ModKind Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer.Error Methods showsPrec :: Int -> ModKind -> ShowS Source # show :: ModKind -> String Source # showList :: [ModKind] -> ShowS Source #
PP ModKind Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer.Error Methods ppPrec :: Int -> ModKind -> Doc Source #
NFData ModKind Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer.Error Methods rnf :: ModKind -> () Source #
Eq ModKind Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer.Error Methods (==) :: ModKind -> ModKind -> Bool Source # (/=) :: ModKind -> ModKind -> Bool Source #
Ord ModKind Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer.Error Methods compare :: ModKind -> ModKind -> Ordering Source # (<) :: ModKind -> ModKind -> Bool Source # (<=) :: ModKind -> ModKind -> Bool Source # (>) :: ModKind -> ModKind -> Bool Source # (>=) :: ModKind -> ModKind -> Bool Source # max :: ModKind -> ModKind -> ModKind Source # min :: ModKind -> ModKind -> ModKind Source #
type Rep ModKind Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer.Error type Rep ModKind = D1 ('MetaData "ModKind" "Cryptol.ModuleSystem.Renamer.Error" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 Source #

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

type ResolvedExt = ResolvedModule () Source #

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