New module system

[yav]

Cryptol's new module system rebased on top of master

TODO

• Importing instantiated submodule doesn't introduce members into scope. #1366
• [New module system] Instantiate functor while importing #1368
• [New module system] Fixity rebalancing broken #1371
• [New module system] Type/constraint synonyms always warn as unused #1372
• [New module system] "Inheriting" and "distributing" interfaces/parameters of imports #1373
• Rewrite the AES parameterized example to show off the new module system #1375
• Make sure browsing modules on the REPL still works
• Make sure the cryptol-specs repo still builds

[rybla]

Why does this give me a dependency error?

module A

interface submodule I where 
  type a : *
  
import interface submodule I

Causes this error:

[error] Invalid recursive dependency:
    • module A
    • submodule A::I, defined at 3:21--3:22

[robdockins]

That would make the submodule I into a dependency of A (as it defines the parameters of A), but I is defined in A. @yav and I talked about this situation, and in general it seems very difficult to support.

[rybla]

That would make the submodule I into a dependency of A (as it defines the parameters of A), but I is defined in A. @yav and I talked about this situation, and in general it seems very difficult to support.

It's interesting because this is how I imagine anonymous interfaces working implicitly i.e.

parameter 
  a : *

But I guess not quite

[robdockins]

That would make the submodule I into a dependency of A (as it defines the parameters of A), but I is defined in A. @yav and I talked about this situation, and in general it seems very difficult to support.

It's interesting because this is how I imagine anonymous interfaces working implicitly i.e.

parameter 
  a : *

But I guess not quite

Indeed, the desugaring has to play some tricks to make sure that the anonymous interface module is defined "outside" the module that uses it.

[rybla]

Why does this give me a Module not in scope: Lib1_Inst error while loading Lib2

module Lib1 where

parameter
  type a : *


module Lib2 where

parameter 
  type b : *

submodule Lib1_Inst = Lib1
  where 
  type a = b

import submodule Lib1_Inst

Whereas this does not give any errors?

module Lib1 where

parameter
  type a : *


module Lib2 where

submodule Lib1_Inst = Lib1
  where 
  type a = [8]

import submodule Lib1_Inst

Is it for a similar reason as we just discussed with the previous example of importing a local interface?

[yav]

@Riib11 I think this is due to the bug discussed yesterday on the channel---currently the desugaring for parameter blocks makes an interface to be placed outside the functor. At the moment it also adds all imports from the module to the new interface. This however is wrong, because some of the imports might refer to names defined in the module, and so they don't make sense outside.

It is hard to know what's a good solution here, but the current idea is that we'll only move top-level imports to the new signature. @m-yac is working on implementing this I believe.

Concretely, in your example, the new interface incorrectly gets the import submodule Lib1_Inst which leads to the error you are seeing.

[rybla]

@Riib11 I think this is due to the bug discussed yesterday on the channel---currently the desugaring for parameter blocks makes an interface to be placed outside the functor. At the moment it also adds all imports from the module to the new interface. This however is wrong, because some of the imports might refer to names defined in the module, and so they don't make sense outside.

It is hard to know what's a good solution here, but the current idea is that we'll only move top-level imports to the new signature. @m-yac is working on implementing this I believe.

Concretely, in your example, the new interface incorrectly gets the import submodule Lib1_Inst which leads to the error you are seeing.

That all makes sense.

Basically what I'm trying to accomplish is "functor eta-expansion" in order to allow a parametrized module B to be imported by another module A that is parametrized by the same (of perhaps some subset of) parameters. And even when this bug is fixed, it's still a little clunky to do this.

[rybla]

Another way this could be thought of is as providing an interface as a module argument. For example

interface module I where
type a : *
/// ... a variety of other parameters

module A1 where
import interface I as I1

module A2 where
import interface I as I2

module A3 where
import interface I as I3
submodule A1_Inst = A1 { I1 = I3 }
submodule A2_Inst = A2 { I2 = I3 }

Here, the idea is that modules A1, A2, A3 are a collection of modules that all share some parameters specified by interface I. Module A3 imports modules A2, A3, but needs to provide an I instance in order to use them since they are functors. So, module A3 itself just imports I and then gives its abstracted instance as the functor arguments to module A1, A2.

A much more convenient syntax for doing this would be the following, where the instantiated functor imports are currently in the works (as mentioned by @yav).

interface module I where
type a : *
/// ... a variety of other parameters

module A1 where
import interface I as I1

module A2 where
import interface I as I2

module A3 where
import interface I as I3
import A1 { I1 = I3 }
import A2 { I2 = I3 }

[m-yac]

Why does this give me a Module not in scope: Lib1_Inst error while loading Lib2

module Lib1 where

parameter
  type a : *


module Lib2 where

parameter 
  type b : *

submodule Lib1_Inst = Lib1
  where 
  type a = b

import submodule Lib1_Inst

@Riib11 I just pushed the change @yav suggested - this example should work now.

I also got a bunch more of the tests working. I think the only one that's still failing is tests/regression/repl-decls.icry because for some reason:

let x -<- y = x - y; infixl 5 -<-; let (-<-) : Integer -> Integer -> Integer
let x ->- y = x - y; infixr 5 ->-; let (->-) : Integer -> Integer -> Integer

42 -<- 10 -<- 100
42 ->- 10 ->- 100
42 ->- 10 -<- 100

outputs

-68
-68
-68

instead of what is used to, which was:

-68
132

[error] at repl-decls.icry:6:4--6:7 and repl-decls.icry:6:11--6:14
    The fixities of
      • (->-) (precedence 5, right-associative)
      • (-<-) (precedence 5, left-associative)
    are not compatible.
    You may use explicit parentheses to disambiguate.

Any idea why this PR changes precedence behavior? There aren't even any modules or imports in this file.

[rybla]

Unfortunately I'm having a different problem now. When I run Lib2, I'm told Value not in scope: x. But it should be available from import submodule Lib1_Inst right?

module Lib1 where
parameter
  type a : *
  x : a


module Lib2 where
parameter
  type b : *
  y : b

submodule Lib1_Inst = Lib1
  where
  type a = b
  x = y

import submodule Lib1_Inst
z : b
z = x

[yav]

Can you make tickets if you find issues, so we can keep track of the various things that need fixing. Let's try to keep the PR comments for specific issues related to the code.