merge: Refactor CompiledModule/ResolveInfo (#1449)

This PR slightly refactors CompiledModule and ResolveInfo, by
serializing/deserializing the `ResolveInfo.thisModule.export` directly
instead of serializing/deserializing the context-related commands (such
as Command.Import).

Q: Why don't serialize context-related commands?
A: Commands are imperative, thus the order is important, furthermore,
some definitions act like a command, such as `inductive`, which
introduces a sub-module, and it is very stupid to store the order
information...

Although serializing `ModuleExport` directly may increase the size of
`,ayac`, especially `prelude.aya`.

Author: ice1000

base/src/main/java/org/aya/resolve/ResolveInfo.java

@@ -41,8 +41,6 @@
  * @param imports      importing information, it only contains the modules that is explicitly imported,
  *                     should not be confused with the {@code import} in {@link ModuleContext#importModuleContext}
  *                     the prim factory will be copied to the current one
- * @param reExports    re-exporting module, it is {@link ModuleName.Qualified} rather than {@link String}
- *                     because we can re-export a module inside another module without import it.
  */
 @Debug.Renderer(text = "modulePath().toString()")
 public record ResolveInfo(
@@ -53,7 +51,6 @@ public record ResolveInfo(
   @NotNull AyaBinOpSet opSet,
   @NotNull MutableMap<AnyDef, OpRenameInfo> opRename,
   @NotNull MutableMap<ModuleName.Qualified, ImportInfo> imports,
-  @NotNull MutableMap<ModuleName.Qualified, UseHide> reExports,
   @NotNull MutableGraph<TyckOrder> depGraph
 ) {
   public ResolveInfo(
@@ -63,7 +60,7 @@ public ResolveInfo(
     @NotNull AyaBinOpSet opSet
   ) {
     this(thisModule, primFactory, shapeFactory, new GlobalInstanceSet(), opSet,
-      MutableMap.create(), MutableMap.create(), MutableMap.create(), MutableGraph.create());
+      MutableMap.create(), MutableMap.create(), MutableGraph.create());
   }
   public @NotNull TyckState makeTyckState() {
     return new TyckState(shapeFactory, primFactory);
@@ -76,7 +73,13 @@ public ExprTycker newTycker(@NotNull Reporter reporter) {
     return new ExprTycker(makeTyckState(), new InstanceSet(instancesSet), reporter, modulePath());
   }
 
-  public record ImportInfo(@NotNull ResolveInfo resolveInfo, boolean reExport) { }
+  /// @param open only used by serialization, not null if it should be [ResolveInfo#open]
+  public record ImportInfo(
+    @NotNull ResolveInfo resolveInfo,
+    boolean reExport,
+    @Nullable Stmt.Accessibility open
+  ) { }
+
   public record OpRenameInfo(
     @NotNull Context bindCtx, @NotNull RenamedOpDecl renamed,
     @NotNull BindBlock bind, boolean reExport
@@ -107,6 +110,8 @@ public void renameOp(
     opRename.put(defVar, new OpRenameInfo(bindCtx, renamed, bind, reExport));
   }
 
+  /// Called when a module opens another imported module, note that [#opSet] and [#shapeFactory] are not affected by
+  /// {@param acc}
   public void open(@NotNull ResolveInfo other, @NotNull SourcePos sourcePos, @NotNull Stmt.Accessibility acc) {
     // open defined operator and their bindings
     opSet.importBind(other.opSet, sourcePos);

base/src/main/java/org/aya/resolve/context/Context.java

@@ -8,10 +8,7 @@
 import org.aya.syntax.concrete.stmt.ModuleName;
 import org.aya.syntax.context.Candidate;
 import org.aya.syntax.context.ContextView;
-import org.aya.syntax.ref.AnyVar;
-import org.aya.syntax.ref.GenerateKind;
-import org.aya.syntax.ref.LocalVar;
-import org.aya.syntax.ref.ModulePath;
+import org.aya.syntax.ref.*;
 import org.aya.util.position.SourcePos;
 import org.aya.util.reporter.Reporter;
 import org.jetbrains.annotations.NotNull;
@@ -103,7 +100,8 @@ default Context bind(@NotNull LocalVar ref, @NotNull Predicate<@Nullable Candida
     return derive(new ModulePath(ImmutableSeq.of(extraName)));
   }
 
+  /// Note that this won't increase [QPath#fileLevelSize]
   default @NotNull ModuleContext derive(@NotNull ModulePath extraName) {
-    return new PhysicalModuleContext(this, modulePath().derive(extraName));
+    return new PhysicalModuleContext(this, qualifiedPath().derive(extraName));
   }
 }

base/src/main/java/org/aya/resolve/context/EmptyContext.java

@@ -8,6 +8,7 @@
 import org.aya.syntax.context.ModuleExport;
 import org.aya.syntax.ref.AnyVar;
 import org.aya.syntax.ref.ModulePath;
+import org.aya.syntax.ref.QPath;
 import org.aya.util.position.SourcePos;
 import org.aya.util.reporter.Reporter;
 import org.jetbrains.annotations.NotNull;
@@ -29,10 +30,10 @@ public record EmptyContext(@NotNull Path underlyingFile) implements Context {
   ) { return null; }
 
   @Override public @NotNull PhysicalModuleContext derive(@NotNull ModulePath extraName) {
-    return new PhysicalModuleContext(this, extraName);
+    return new PhysicalModuleContext(this, QPath.fileLevel(extraName));
   }
 
-  @Override public @NotNull ModulePath modulePath() {
+  @Override public @NotNull QPath qualifiedPath() {
     throw new UnsupportedOperationException();
   }
 

base/src/main/java/org/aya/resolve/context/NoExportContext.java

@@ -9,6 +9,7 @@
 import org.aya.syntax.context.ModuleSymbol;
 import org.aya.syntax.ref.AnyVar;
 import org.aya.syntax.ref.ModulePath;
+import org.aya.syntax.ref.QPath;
 import org.jetbrains.annotations.NotNull;
 
 import java.nio.file.Path;
@@ -18,20 +19,20 @@ public record NoExportContext(
   @NotNull Context parent,
   @NotNull ModuleSymbol<AnyVar> symbols,
   @NotNull MutableMap<ModuleName.Qualified, ModuleExport> modules,
-  @Override @NotNull ModulePath modulePath
+  @Override @NotNull QPath qualifiedPath
 ) implements ModuleContext {
   public NoExportContext(
     @NotNull Context parent,
     @NotNull ModuleSymbol<AnyVar> symbols,
     @NotNull MutableMap<ModuleName.Qualified, ModuleExport> modules
   ) {
-    this(parent, symbols, modules, parent.modulePath().derive(":NoExport"));
+    this(parent, symbols, modules, parent.qualifiedPath().derive(":NoExport"));
   }
 
   public NoExportContext(@NotNull Context parent) {
     this(parent, new ModuleSymbol<>(), MutableHashMap.create());
   }
 
   @Override public @NotNull Path underlyingFile() { return parent.underlyingFile(); }
-  @Override public @NotNull ModuleExport exports() { return new ModuleExport(); }
+  @Override public @NotNull ModuleExport exports() { return new ModuleExport(qualifiedPath); }
 }

base/src/main/java/org/aya/resolve/context/PhysicalModuleContext.java

@@ -10,7 +10,7 @@
 import org.aya.syntax.context.ModuleSymbol;
 import org.aya.syntax.ref.AnyDefVar;
 import org.aya.syntax.ref.AnyVar;
-import org.aya.syntax.ref.ModulePath;
+import org.aya.syntax.ref.QPath;
 import org.aya.util.position.SourcePos;
 import org.aya.util.reporter.Reporter;
 import org.jetbrains.annotations.NotNull;
@@ -23,17 +23,18 @@
  */
 public class PhysicalModuleContext implements ModuleContext {
   public final @NotNull Context parent;
-  public final @NotNull ModuleExport exports = new ModuleExport();
+  public final @NotNull ModuleExport exports;
   public final @NotNull ModuleSymbol<AnyVar> symbols = new ModuleSymbol<>();
   public final @NotNull MutableMap<ModuleName.Qualified, ModuleExport> modules = MutableHashMap.create();
-  private final @NotNull ModulePath modulePath;
-  @Override public @NotNull ModulePath modulePath() { return modulePath; }
+  private final @NotNull QPath qualifiedPath;
+  @Override public @NotNull QPath qualifiedPath() { return qualifiedPath; }
 
   private @Nullable NoExportContext exampleContext;
 
-  public PhysicalModuleContext(@NotNull Context parent, @NotNull ModulePath modulePath) {
+  public PhysicalModuleContext(@NotNull Context parent, @NotNull QPath qualifiedPath) {
     this.parent = parent;
-    this.modulePath = modulePath;
+    this.qualifiedPath = qualifiedPath;
+    this.exports = new ModuleExport(qualifiedPath);
   }
 
   @Override public boolean importModule(

base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java

@@ -90,7 +90,7 @@ public ImmutableSeq<ResolvingStmt> resolveStmt(@NotNull ImmutableSeq<Stmt> stmts
         context.importModuleContext(importedName, mod, cmd.accessibility(), cmd.sourcePos(), thisReporter);
         resolveInfo.primFactory().importFrom(success.primFactory());
 
-        var importInfo = new ResolveInfo.ImportInfo(success, cmd.accessibility() == Stmt.Accessibility.Public);
+        var importInfo = new ResolveInfo.ImportInfo(success, cmd.accessibility() == Stmt.Accessibility.Public, null);
         resolveInfo.imports().put(importedName, importInfo);
         yield null;
       }
@@ -103,15 +103,13 @@ public ImmutableSeq<ResolvingStmt> resolveStmt(@NotNull ImmutableSeq<Stmt> stmts
         var success = ctx.openModule(mod, acc, cmd.sourcePos(), useHide, thisReporter);
         if (!success) yield null;
 
-        // store top-level re-exports
-        // FIXME: this is not enough, because submodule export definitions are not stored
-        if (ctx == resolveInfo.thisModule()) {
-          if (acc == Stmt.Accessibility.Public) resolveInfo.reExports().put(mod, useHide);
-        }
         // open necessities from imported modules (not submodules)
         // because the module itself and its submodules share the same ResolveInfo
-        resolveInfo.imports().getOption(mod).ifDefined(modResolveInfo ->
-          resolveInfo.open(modResolveInfo.resolveInfo(), cmd.sourcePos(), acc));
+        resolveInfo.imports().getOption(mod).ifDefined(modResolveInfo -> {
+          // TODO: open regardless the strategy(use / hide)? the user may be able to refer hidden data by `shapeFactory`
+          resolveInfo.open(modResolveInfo.resolveInfo(), cmd.sourcePos(), acc);
+          resolveInfo.imports().put(mod, new ResolveInfo.ImportInfo(modResolveInfo.resolveInfo(), modResolveInfo.reExport(), acc));
+        });
 
         // renaming as infix
         if (useHide.strategy() == UseHide.Strategy.Using) useHide.list().forEach(use -> {

cli-impl/src/main/java/org/aya/cli/interactive/ReplCompiler.java

@@ -182,7 +182,7 @@ private void loadFile(@NotNull Path file) {
   private @NotNull ResolveInfo makeResolveInfo(@NotNull ModuleContext ctx) {
     var resolveInfo = new ResolveInfo(ctx, tcState.primFactory, tcState.shapeFactory, opSet);
     imports.forEach(ii -> resolveInfo.imports().put(
-      ii.modulePath().asName(), new ResolveInfo.ImportInfo(ii, false)));
+      ii.modulePath().asName(), new ResolveInfo.ImportInfo(ii, false, null)));
     return resolveInfo;
   }
 

cli-impl/src/main/java/org/aya/cli/interactive/ReplContext.java

@@ -16,10 +16,7 @@
 import org.aya.syntax.concrete.stmt.Stmt;
 import org.aya.syntax.context.ModuleExport;
 import org.aya.syntax.context.ModuleSymbol;
-import org.aya.syntax.ref.AnyDefVar;
-import org.aya.syntax.ref.AnyVar;
-import org.aya.syntax.ref.DefVar;
-import org.aya.syntax.ref.ModulePath;
+import org.aya.syntax.ref.*;
 import org.aya.util.RepoLike;
 import org.aya.util.position.SourcePos;
 import org.aya.util.reporter.Reporter;
@@ -34,7 +31,8 @@ public final class ReplContext extends PhysicalModuleContext implements RepoLike
   private @Nullable ImmutableMap<String, ModuleTrie> moduleTree = null;
 
   public ReplContext(@NotNull Context parent, @NotNull ModulePath name) {
-    super(parent, name);
+    // QPath is used for serialization only
+    super(parent, QPath.fileLevel(name));
   }
 
   @Override public boolean importSymbol(