Nested modules

[yav]

• Limitations:
  Does not work in combination parameterized modules, as I am
  about to redo how that works.

  • General refeactorings:

    • Namespaces:

      • We have an explicit type for namespaces, see Cryptol.Util.Ident
      • Display environments should now be aware of the namespace of the
        name being displayed.

    • Renamer:

      • Factor out the renamer monad and error type into separate modules
      • All name resultion is done through a single function resolveName
      • The renamer now computes the dependencies between declarations,
        orders things in dependency order, and checks for bad recursion.

    • Typechecker: Redo checking of declarations (both top-level and local).
      Previously we used a sort of CPS to add things in scope. Now we use
      a state monad and add things to the state. We assume that the renamer
      has been run, which means that declarations are ordered in dependency
      order, and things have unique name, so we don't need to worry about
      scoping too much.

  • Change specific to nested modules:

    • We have a new namespace for module names
    • The interface file of a module contains the interfaces for nested modules
    • Most of the changes related to nested modules in the renamer are
      in ModuleSystem.NamingEnv and ModuleSystem.Rename
      • There is some trickiness when resolving module names when importing
        submodules (seed processOpen and openLoop)
    • There are some changes to the representation of modules in the typechecked
      syntax, in particular:
      • During type-checking we "flatten" nested module declarations into
        a single big declaration. Hopefully, this means that passes after
        the type checker don't need to worry about nested modules
      • There is a new field containing the interfaces of the nested modules,
        this is needed so that when we import the module we know we have the
        nested structure
      • Declarations in functor/parameterzied modules do not appear in the
        flattened list of declarations. Instead thouse modules are collected
        in a separate field, and the plan is that they would be used from
        there when we implmenet functor instantiation.

[robdockins]

Playing around with private submodules, I discovered that the following doesn't parse.

private submodule B where
  y : Integer
  y = 42

Basically, layout rules require the declarations in B to be further right than the beginning of the submodule keyword, or (or maybe right of the end of private). It might be nice if we could make this work somehow.

[robdockins]

This generates a panic:

module TopModule where

import submodule B

submodule A where
  propA = y > 5

submodule B where
  y : Integer
  y = 42

%< ---------------------------------------------------
  Revision:  76774d27f2c5a88e12529b78668304d0410d19ec
  Branch:    testing (uncommited files present)
  Location:  lookupVar
  Message:   Undefined vairable
             Name {nUnique = 4641, nInfo = Declared (Nested (TopModule (ModName "TopModule")) (Ident False "B")) UserName, nNamespace = NSValue, nIdent = Ident False "y", nFixity = Nothing, nLoc = Range {from = Position {line = 10, col = 3}, to = Position {line = 10, col = 4}, source = "tests/modsys/nested/TopModule.cry"}}
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.10.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/TypeCheck/Monad.hs:653:26 in cryptol-2.10.0.99-inplace:Cryptol.TypeCheck.Monad
%< ---------------------------------------------------

[robdockins]

It might be nice if we could treat all submodules as being in scope "qualified". Then, the following would work without the import A as A line. In fact, we could just directly refer to A::C::z in TopModule without any imports.

module TopModule where

import submodule A as A
import submodule A::C as C

submodule A where
  submodule C where
    z : [8]
    z = 109

[robdockins]

Right now, as I understand it, we have the following rules that control scoping with modules:

1. Declarations appearing in outer modules are in scope for their nested submodules.
   1a. Declarations that are imported into outer modules are in scope in their nested submodules.
2. Declarations in submodules (declared or imported from elsewhere) are not in scope unless the submodule is imported.
3. Declarations/submodules at the top level of a module (top or submodule) come into scope when that module is imported elsewhere.
   3b. However, private declarations/submodules do not come into scope when a module is imported.
4. Declarations that are imported into a module do not come into scope when that module is itself imported elsewhere.

I think point 1a is related to the panic above.

I think perhaps we should weaken point 2 so that submodules are automatically considered to be in scope qualified by their name, and import statements can be used to also import the declarations in a module unqualified, or qualified with a different name.

Finally, I think we should allow a mechanism to explicitly weaken point 4 via an export keyword that would allow you to add symbols to the exported interface of a module. An idea of how that might work:

export f
export type Asdf
export module SomeTopLevelModule
export submodule A

This would export the symbol f (presumably imported from elsewhere) and type Asdf from the current module. Also, exporting a module or submodule basically just adds the entire interface of that module to the interface of the module in which the export appears.

This makes it so the basic rule is that: declarations appearing in a module are exported unless they are explicitly made private. Declarations imported into a module are not exported unless they are explicitly re-exported. I think this gives a good default behavior, while still allowing sufficient control over the namespace to users that really want it.

[yav]

@robdockins thanks for the comments!

The layout issue is interesting, it totally makes sense that this is rejected with the current rules (there are 2 nested layout blocks and the inner one is closing the outer one), but I agree that it might be nice to make it work somehow...

On the issue about nested modules being in scope---my thinking is that this PR only implements the bare minimum "core" functionality (although clearly there is a bug, as the renamer should have caught that y is not in scope). To make your suggestion work, perhaps we can have a rule that's kind of like Haskell's implicit Prelude imports? So if a there are no explicit imports of a nested module, we implicitly add a qualified import, otherwise we don't. I like this because it seems easy to implement and specify, and gives the users flexibility to import things however they want.

For re-exporting things, I think we should deal with those as a separate feature. They might be nice, but also add some complexity, both to the implementation and the specification. In particular, a nice property of the current system is that you can tell what a module exports just by looking at the declarations in it (i.e., you don't need to know what's in scope). With re-exports that's not the case anymore, so some tricky dependencies can arise. I suspect it's doable, but we'd have to think carefully about it.

[robdockins]

Regarding the panic: I think y should be in scope because we imported B, so the renamer is doing the right thing on that front... but the naming environment doesn't include y, so that's wrong.

[yav]

@robdockins yep, I added the example as a test, and realized that what I said above is wrong, I am investigating what's happening. I suspect the declarations are not correctly ordered after the renamer.

[robdockins]

I agree the export issue can wait. I think you've addressed all the things I've found so far.

When this is merged, I suggest we make issues to track 1) exports and 2) documentation of nested modules (I imagine it makes sense to wait until we rework parameterized modules to write the new documentation).