Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Nested modules #1048

Merged
merged 15 commits into from
Apr 6, 2021
Merged

Nested modules #1048

merged 15 commits into from
Apr 6, 2021

Commits on Mar 12, 2021

  1. Implementation of nested modules.

      * 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.
    yav committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    34b1d87 View commit details
    Browse the repository at this point in the history
  2. Fix missed test

    yav committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    dc1559f View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    fad47f5 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    c1914cc View commit details
    Browse the repository at this point in the history
  5. Add a test

    yav committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    fe17d24 View commit details
    Browse the repository at this point in the history
  6. Fix typo

    yav committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    e353c83 View commit details
    Browse the repository at this point in the history

Commits on Mar 13, 2021

  1. Configuration menu
    Copy the full SHA
    1ea8682 View commit details
    Browse the repository at this point in the history

Commits on Apr 1, 2021

  1. Fix dependency tracking with nested modules.

    See the example on the PR thread, which is captured in test T11
    yav committed Apr 1, 2021
    Configuration menu
    Copy the full SHA
    65cd467 View commit details
    Browse the repository at this point in the history
  2. Show the locations of the definitions when reporting invalid dependen…

    …cies
    
    We only show the file location as these will always be in the same file,
    I think.
    yav committed Apr 1, 2021
    Configuration menu
    Copy the full SHA
    cb21ab6 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    8b4778b View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    053c35c View commit details
    Browse the repository at this point in the history
  5. Add implicit imports for locally defined modules

    This also fixes the extra space in the "invlid dependency" error
    yav committed Apr 1, 2021
    Configuration menu
    Copy the full SHA
    f85b0e4 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    501f884 View commit details
    Browse the repository at this point in the history

Commits on Apr 2, 2021

  1. Redo the scoping on the command line and browsing.

    This fixes a bug where the scoping on the command line was incorrect
    for nested modules.
    
    It also changes the semantics of `:browse` (whose implementation is now
    in a separate module), to be more reasonable. See #689
    yav committed Apr 2, 2021
    Configuration menu
    Copy the full SHA
    1532223 View commit details
    Browse the repository at this point in the history

Commits on Apr 6, 2021

  1. Changes to make new command line scope and browsing work with the cur…

    …rent
    
    parameterzied modules.
    
    Some of this is a bit of a hack, but that code would change with the new
    parameterized modules, so the hack is temporary.
    yav committed Apr 6, 2021
    Configuration menu
    Copy the full SHA
    277a657 View commit details
    Browse the repository at this point in the history