merge: Implement prim serialization, do more experiments (#1044)

Fix #1030

cli-impl/src/main/java/org/aya/cli/library/incremental/DiskCompilerAdvisor.java

@@ -19,11 +19,13 @@
 import org.jetbrains.annotations.Nullable;
 
 import javax.tools.ToolProvider;
+import java.io.File;
 import java.io.IOException;
 import java.net.URL;
 import java.net.URLClassLoader;
 import java.nio.file.Files;
 import java.nio.file.Path;
+import java.util.List;
 
 public class DiskCompilerAdvisor implements CompilerAdvisor {
   @Override public boolean isSourceModified(@NotNull LibrarySource source) {
@@ -87,14 +89,18 @@ public class DiskCompilerAdvisor implements CompilerAdvisor {
       .serialize(new FileSerializer.FileResult(file.moduleName().dropLast(1), new ModuleSerializer.ModuleResult(
         name, defs.filterIsInstance(TopLevelDef.class), ImmutableSeq.empty())))
       .result();
-    var javaSrcPath = FileUtil.resolveFile(computeBaseDir(file.owner()).resolve(AyaSerializer.PACKAGE_BASE),
+    var baseDir = computeBaseDir(file.owner()).toAbsolutePath();
+    var javaSrcPath = FileUtil.resolveFile(baseDir.resolve(AyaSerializer.PACKAGE_BASE),
       file.moduleName().module(), ".java");
     FileUtil.writeString(javaSrcPath, javaCode);
     var compiler = ToolProvider.getSystemJavaCompiler();
     var fileManager = compiler.getStandardFileManager(null, null, null);
     var compilationUnits = fileManager.getJavaFileObjects(javaSrcPath);
-    var task = compiler.getTask(null, fileManager, null, null, null, compilationUnits);
+    var classpath = System.getProperty("java.class.path");
+    var options = List.of("-classpath", baseDir + File.pathSeparator + classpath);
+    var task = compiler.getTask(null, fileManager, null, options, null, compilationUnits);
     task.call();
+    Files.delete(javaSrcPath);
     var coreFile = file.compiledCorePath();
     CompilerUtil.saveCompiledCore(coreFile, resolveInfo);
   }

cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java

@@ -29,9 +29,9 @@ public class ReplCompilerTest {
 
   @Test public void library() throws IOException {
     compiler.loadToContext(Paths.get("../ide-lsp", "src", "test", "resources", "lsp-test-lib"));
-    assertNotNull(findContext("NatCore::zero"));
-    assertNotNull(findContext("Vec::vnil"));
-    assertNotNull(findContext("Vec:::>"));
+    assertNotNull(findContext("Nat::Core::zero"));
+    assertNotNull(findContext("VecCore::vnil"));
+    assertNotNull(findContext("VecCore:::>"));
   }
 
   @Test public void simpleExpr() { compile("Set"); }
@@ -51,15 +51,15 @@ public class ReplCompilerTest {
     assertNull(findContext("a"));
   }
 
-  // /** <a href="https://ice1000.jetbrains.space/im/group/4DLh053zIix6?message=2db0002db&channel=4DLh053zIix6">Bug report</a> */
-  // @Test public void reportedInSpace() {
-  //   // success cases, we can find the definition in the context
-  //   compile("data Unit | unit");
-  //   assertNotNull(findContext("Unit"));
-  //   compile("data What | what : Unit");
-  //   assertNotNull(findContext("What"));
-  //   assertNotNull(findContext("Unit"));
-  // }
+  /** <a href="https://ice1000.jetbrains.space/im/group/4DLh053zIix6?message=2db0002db&channel=4DLh053zIix6">Bug report</a> */
+  @Test public void reportedInSpace() {
+    // success cases, we can find the definition in the context
+    compile("data Unit | unit");
+    assertNotNull(findContext("Unit"));
+    compile("data What | what");
+    assertNotNull(findContext("What"));
+    assertNotNull(findContext("Unit"));
+  }
 
   private @Nullable AnyVar findContext(@NotNull String name) {
     try {

ide-lsp/src/test/java/org/aya/lsp/LspTest.java

@@ -52,7 +52,7 @@ public class LspTest {
   @Test public void test541() {
     launch(TEST_LIB).execute(compile((a, _) -> {
       var testOpt = a.lastCompiled()
-        .filter(x -> x.moduleName().module().getLast().equals("Vec"))
+        .filter(x -> x.moduleName().module().getLast().equals("VecCore"))
         .flatMap(x -> x.program().get())
         .filterIsInstance(FnDecl.class)
         .filter(x -> x.ref.name().equals("test"))
@@ -74,8 +74,8 @@ public class LspTest {
       compile((_, _) -> {}),
       mutate("HelloWorld"),
       compile((a, e) -> assertRemake(a, e, "HelloWorld")),
-      mutate("NatCore"),
-      compile((a, e) -> assertRemake(a, e, "NatCore", "Vec", "HelloWorld")),
+      mutate("Nat::Core"),
+      compile((a, e) -> assertRemake(a, e, "Nat::Core", "VecCore", "HelloWorld")),
       mutate("PathPrims"),
       compile((a, e) -> assertRemake(a, e, "PathPrims", "Path", "HelloWorld"))
     );
@@ -90,19 +90,19 @@ public class LspTest {
     client.execute(compile((_, _) -> {}));
 
     var param = new TextDocumentPositionParams(new TextDocumentIdentifier(
-      TEST_LIB.resolve("src").resolve("NatCore.aya").toUri()),
+      TEST_LIB.resolve("src/Nat/Core.aya").toUri()),
       new Position(0, 18)
     );
 
     var result0 = client.service.hover(param);
     assertTrue(result0.isPresent());
-    assertEquals("<a href=\"#NatCore-Nat\"><span style=\"color:#218c21;\">Nat</span></a>", result0.get().contents.getFirst().value);
+    assertEquals("<a href=\"#Nat-Core-Nat\"><span style=\"color:#218c21;\">Nat</span></a>", result0.get().contents.getFirst().value);
 
     client.service.updateServerOptions(new ServerOptions(new ServerRenderOptions("IntelliJ", null, RenderOptions.OutputTarget.HTML)));
 
     var result1 = client.service.hover(param);
     assertTrue(result1.isPresent());
-    assertEquals("<a href=\"#NatCore-Nat\"><span style=\"color:#000000;\">Nat</span></a>", result1.get().contents.getFirst().value);
+    assertEquals("<a href=\"#Nat-Core-Nat\"><span style=\"color:#000000;\">Nat</span></a>", result1.get().contents.getFirst().value);
   }
 
   private void logTime(long time) {

ide-lsp/src/test/resources/lsp-test-lib/src/HelloWorld.aya

@@ -1,4 +1,4 @@
-open import NatCore
+open import Nat::Core
 open import Path
 open import StringPrims using (
     String

ide-lsp/src/test/resources/lsp-test-lib/src/Vec.aya → ide-lsp/src/test/resources/lsp-test-lib/src/VecCore.aya

@@ -1,4 +1,4 @@
-open import NatCore
+open import Nat::Core
 
 open data Vec Type Nat : Type
 | A, 0 => vnil

jit-compiler/src/main/java/org/aya/compiler/JitTeleSerializer.java

@@ -123,7 +123,7 @@ protected void buildConstructor(@NotNull T def, @NotNull ImmutableSeq<String> ex
     buildSuperCall(ImmutableSeq.of(
       Integer.toString(size),
       makeArrayFrom("boolean", licit.toImmutableSeq()),
-      makeArrayFrom("String", names.toImmutableArray())
+      makeArrayFrom("java.lang.String", names.toImmutableArray())
     ).appendedAll(ext));
   }
 

jit-compiler/src/main/java/org/aya/compiler/PrimSerializer.java

@@ -12,7 +12,7 @@ public PrimSerializer(@NotNull AbstractSerializer<?> parent) {
     super(parent, JitPrim.class);
   }
   @Override protected void buildConstructor(PrimDef unit) {
-    super.buildConstructor(unit, ImmutableSeq.of("id"));
+    super.buildConstructor(unit, ImmutableSeq.of(STR."org.aya.syntax.core.def.PrimDef.ID.\{unit.id.name()}"));
   }
   @Override public AyaSerializer<PrimDef> serialize(PrimDef unit) {
     buildFramework(unit, () -> { });

syntax/src/main/java/org/aya/syntax/compile/JitPrim.java

@@ -7,6 +7,7 @@
 import org.aya.syntax.core.def.PrimDef;
 import org.aya.syntax.core.def.PrimDefLike;
 import org.aya.syntax.core.term.Term;
+import org.aya.util.error.Panic;
 import org.jetbrains.annotations.NotNull;
 
 public abstract non-sealed class JitPrim extends JitDef implements PrimDefLike, Reducible {
@@ -17,8 +18,7 @@ protected JitPrim(int telescopeSize, boolean[] telescopeLicit, String[] telescop
     this.id = id;
   }
 
-  /**
-   * Unfold this function
-   */
-  @Override public abstract Term invoke(Term stuck, @NotNull Seq<Term> args);
+  @Override public Term invoke(Term stuck, @NotNull Seq<Term> args) {
+    throw new Panic("Should not be called");
+  }
 }