merge: Post apocalypse fixes (#1043)

Author: ice1000

Diff for: .github/README.md

@@ -18,10 +18,7 @@ Aya is under active development, so please expect bugs, usability or performance
 
 + Dependent types, including pi-types, sigma types, indexed families, etc.
   You could write a [type-safe interpreter][gadt].
-+ Cartesian cubical type theory with generalized path types
-  similar to a "bounded" cubical subtype.
-  + Implementation prototype of De Morgan cubical: [Guest0x0].
-  + Demonstration of higher inductive types: [3-torus] (three-dimensional torus!!).
++ Set-level cubical type theory (XTT).
   + Demonstration of [higher-inductive-inductive-recursive types][hiir].
 + Pattern matching with first-match semantics.
   Checkout the [red-black tree][rbtree] (without deletion yet).
@@ -75,13 +72,11 @@ of IDE is IntelliJ IDEA, version 2023.3 or higher is required.
 [regularity]: ../base/src/test/resources/success/common/src/Paths.aya
 [funExt]: ../base/src/test/resources/success/common/src/Paths.aya
 [rbtree]: ../base/src/test/resources/success/common/src/Data/Tree/RedBlack/Direct.aya
-[3-torus]: ../base/src/test/resources/success/common/src/Spaces/Torus/T3.aya
 [hiir]: ../base/src/test/resources/success/common/src/TypeTheory/Thorsten.aya
 [assoc]: ../base/src/test/resources/success/src/Assoc.aya
 [foetus]: ../base/src/test/resources/success/src/FoetusLimitation.aya
 [mutual]: ../base/src/test/resources/success/src/Order.aya
 [maven-repo]: https://repo1.maven.org/maven2/org/aya-prover
-[Guest0x0]: https://github.com/ice1000/Guest0x0
 [stdlib-style]: ../base/src/test/resources/success/common
 
 ## Use as a library
@@ -105,7 +100,10 @@ implementation group: 'org.aya-prover', name: '[project name]', version: '[lates
 
 + `[project name]` specifies the subproject of Aya you want to use,
   and the options are `pretty`, `base`, `cli-impl`, `parser`, etc.
-  + The type checker lives in `base` and `parser`.
+  + The syntax definitions live in `syntax`.
+  + The parser lives in `parser` and `producer`.
+  + The type checker lives in `base`.
+  + The JIT compiler lives in `jit-compiler`.
   + The generalized pretty printing framework is in `pretty`.
   + The library system, literate mode, single-file type checker, and basic REPL are in `cli-impl`.
   + The generalized tree builder, generalized termination checker,

Diff for: base/src/main/java/org/aya/primitive/PrimFactory.java

@@ -195,7 +195,7 @@ public boolean have(@NotNull ID name) {
   }
 
   public @NotNull Term unfold(@NotNull PrimCall primCall, @NotNull TyckState state) {
-    var id = primCall.ref().core().id;
+    var id = primCall.ref().id();
     return seeds.get(id).unfold.apply(primCall, state);
   }
 

Diff for: cli-console/build.gradle.kts

@@ -2,6 +2,10 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 import org.aya.gradle.CommonTasks
 
+val mainClassQName = "org.aya.cli.console.Main"
+CommonTasks.fatJar(project, mainClassQName)
+application.mainClass.set(mainClassQName)
+
 dependencies {
   api(project(":tools-repl"))
   api(project(":cli-impl"))
@@ -13,3 +17,11 @@ dependencies {
   testImplementation(libs.junit.jupiter)
   testImplementation(libs.hamcrest)
 }
+
+plugins { application }
+
+tasks.withType<AbstractCopyTask>().configureEach {
+  duplicatesStrategy = DuplicatesStrategy.EXCLUDE
+}
+
+tasks.withType<JavaCompile>().configureEach { CommonTasks.picocli(this) }

Diff for: cli-impl/build.gradle.kts

@@ -6,7 +6,6 @@ dependencies {
   api(project(":base"))
   api(project(":parser"))
   api(libs.gson)
-  implementation(libs.sourcebuddy)
   implementation(project(":producer"))
   implementation(project(":jit-compiler"))
   implementation(libs.commonmark)

Diff for: cli-impl/src/main/java/module-info.java

@@ -9,6 +9,7 @@
   requires aya.compiler;
   requires org.jetbrains.annotations;
   requires org.commonmark;
+  requires java.compiler;
 
   exports org.aya.cli.interactive;
   exports org.aya.cli.library.incremental;

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

@@ -49,7 +49,6 @@
 import java.io.IOException;
 import java.nio.file.Files;
 import java.nio.file.Path;
-import java.util.function.Function;
 
 public class ReplCompiler {
   public final @NotNull CountingReporter reporter;

Diff for: cli-impl/src/main/java/org/aya/cli/library/LibraryModuleLoader.java

@@ -90,7 +90,7 @@ public boolean existsFileLevelModule(@NotNull ModulePath path) {
     @NotNull ModulePath mod, @Nullable Path sourcePath,
     @Nullable Path corePath, @NotNull ModuleLoader recurseLoader
   ) {
-    return advisor.loadCompiledCore(reporter, mod, sourcePath, corePath, recurseLoader);
+    return advisor.loadCompiledCore(reporter, owner, mod, sourcePath, corePath, recurseLoader);
   }
 
   private void saveCompiledCore(

Diff for: cli-impl/src/main/java/org/aya/cli/library/incremental/CompilerAdvisor.java

@@ -63,7 +63,7 @@ default void notifyIncrementalJob(
    */
   @Nullable ResolveInfo doLoadCompiledCore(
     @NotNull Reporter reporter,
-    @NotNull ModulePath mod,
+    @NotNull LibraryOwner owner, @NotNull ModulePath mod,
     @Nullable Path sourcePath,
     @Nullable Path corePath,
     @NotNull ModuleLoader recurseLoader
@@ -78,14 +78,14 @@ void doSaveCompiledCore(
   @ApiStatus.NonExtendable
   default @Nullable ResolveInfo loadCompiledCore(
     @NotNull Reporter reporter,
-    @NotNull ModulePath mod,
+    @NotNull LibraryOwner owner, @NotNull ModulePath mod,
     @Nullable Path sourcePath,
     @Nullable Path corePath,
     @NotNull ModuleLoader recurseLoader
   ) {
     assert recurseLoader instanceof CachedModuleLoader<?>;
     try {
-      return doLoadCompiledCore(reporter, mod, sourcePath, corePath, recurseLoader);
+      return doLoadCompiledCore(reporter, owner, mod, sourcePath, corePath, recurseLoader);
     } catch (IOException | ClassNotFoundException e) {
       throw new Panic("Compiled aya found but cannot be loaded", e);
     }

Diff for: cli-impl/src/main/java/org/aya/cli/library/incremental/DelegateCompilerAdvisor.java

@@ -52,8 +52,8 @@ public void notifyIncrementalJob(@NotNull ImmutableSeq<LibrarySource> modified,
   }
 
   @Override public @Nullable ResolveInfo
-  doLoadCompiledCore(@NotNull Reporter reporter, @NotNull ModulePath mod, @Nullable Path sourcePath, @Nullable Path corePath, @NotNull ModuleLoader recurseLoader) throws IOException, ClassNotFoundException {
-    return delegate.doLoadCompiledCore(reporter, mod, sourcePath, corePath, recurseLoader);
+  doLoadCompiledCore(@NotNull Reporter reporter, @NotNull LibraryOwner owner, @NotNull ModulePath mod, @Nullable Path sourcePath, @Nullable Path corePath, @NotNull ModuleLoader recurseLoader) throws IOException, ClassNotFoundException {
+    return delegate.doLoadCompiledCore(reporter, owner, mod, sourcePath, corePath, recurseLoader);
   }
 
   @Override public void

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

@@ -6,18 +6,22 @@
 import org.aya.cli.library.source.LibraryOwner;
 import org.aya.cli.library.source.LibrarySource;
 import org.aya.cli.utils.CompilerUtil;
-import org.aya.compiler.CompiledModule;
+import org.aya.compiler.*;
 import org.aya.resolve.ResolveInfo;
 import org.aya.resolve.context.EmptyContext;
 import org.aya.resolve.module.ModuleLoader;
+import org.aya.syntax.core.def.TopLevelDef;
 import org.aya.syntax.core.def.TyckDef;
 import org.aya.syntax.ref.ModulePath;
 import org.aya.util.FileUtil;
 import org.aya.util.reporter.Reporter;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
+import javax.tools.ToolProvider;
 import java.io.IOException;
+import java.net.URL;
+import java.net.URLClassLoader;
 import java.nio.file.Files;
 import java.nio.file.Path;
 
@@ -54,7 +58,7 @@ public class DiskCompilerAdvisor implements CompilerAdvisor {
   }
   @Override public @Nullable ResolveInfo doLoadCompiledCore(
     @NotNull Reporter reporter,
-    @NotNull ModulePath mod,
+    @NotNull LibraryOwner owner, @NotNull ModulePath mod,
     @Nullable Path sourcePath,
     @Nullable Path corePath,
     @NotNull ModuleLoader recurseLoader
@@ -63,10 +67,13 @@ public class DiskCompilerAdvisor implements CompilerAdvisor {
     if (!Files.exists(corePath)) return null;
 
     var context = new EmptyContext(reporter, sourcePath).derive(mod);
-    // TODO: load defs
     try (var inputStream = FileUtil.ois(corePath)) {
       var compiledAya = (CompiledModule) inputStream.readObject();
-      return compiledAya.toResolveInfo(recurseLoader, context);
+      var baseDir = computeBaseDir(owner);
+      try (var cl = new URLClassLoader(new URL[]{baseDir.toUri().toURL()})) {
+        cl.loadClass(AbstractSerializer.getModuleReference(mod));
+        return compiledAya.toResolveInfo(recurseLoader, context, cl);
+      }
     }
   }
 
@@ -75,8 +82,24 @@ public class DiskCompilerAdvisor implements CompilerAdvisor {
     @NotNull ResolveInfo resolveInfo,
     @NotNull ImmutableSeq<TyckDef> defs
   ) throws IOException {
-    // TODO: compile defs
+    var name = file.moduleName().last();
+    var javaCode = new FileSerializer(resolveInfo.shapeFactory())
+      .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),
+      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);
+    task.call();
     var coreFile = file.compiledCorePath();
     CompilerUtil.saveCompiledCore(coreFile, resolveInfo);
   }
+
+  private static @NotNull Path computeBaseDir(@NotNull LibraryOwner owner) {
+    return owner.outDir().resolve("compiled");
+  }
 }

Diff for: cli-impl/src/main/java/org/aya/cli/library/incremental/InMemoryCompilerAdvisor.java

@@ -63,7 +63,7 @@ public class InMemoryCompilerAdvisor implements CompilerAdvisor {
   @Override
   public @Nullable ResolveInfo doLoadCompiledCore(
     @NotNull Reporter reporter,
-    @NotNull ModulePath mod,
+    @NotNull LibraryOwner owner, @NotNull ModulePath mod,
     @Nullable Path sourcePath,
     @Nullable Path corePath,
     @NotNull ModuleLoader recurseLoader

Diff for: cli-impl/src/test/java/org/aya/test/cli/SimpleTest.java

@@ -2,7 +2,7 @@
 # The Version of this project, aka, The Aya Theorem Prover.
 # Remove "-SNAPSHOT" suffix and run gradle publish to release a new version.
 # After that, increase the version number and add "-SNAPSHOT" suffix back for next cycle.
-project = "0.30.0-SNAPSHOT"
+project = "0.31.0"
 
 # https://openjdk.org/
 java = "21"
@@ -28,8 +28,6 @@ jlink = "3.0.1"
 jacoco = "0.8.12"
 # https://github.com/manifold-systems/manifold/tree/master/manifold-deps-parent/manifold-delegation
 manifold = "2024.1.14"
-# https://github.com/sourcebuddy/sourcebuddy
-sourcebuddy = "2.5.0"
 
 [plugins]
 jlink = { id = "org.beryx.jlink", version.ref = "jlink" }
@@ -62,7 +60,6 @@ hamcrest = { group = "org.hamcrest", name = "hamcrest", version.ref = "hamcrest"
 
 gson = { group = "com.google.code.gson", name = "gson", version.ref = "gson" }
 commonmark = { group = "org.commonmark", name = "commonmark", version.ref = "commonmark" }
-sourcebuddy = { group = "com.javax0.sourcebuddy", name = "SourceBuddy", version.ref = "sourcebuddy" }
 
 manifold-delegate-runtime = { group = "systems.manifold", name = "manifold-delegation-rt", version.ref = "manifold" }
 manifold-delegate-codegen = { group = "systems.manifold", name = "manifold-delegation", version.ref = "manifold" }

Diff for: gradle/libs.versions.toml

@@ -127,7 +127,7 @@ supportedPlatforms.forEach { platform ->
       include("bin/aya")
       include("bin/aya-lsp")
       include("${Constants.jreDirName}/bin/**")
-      fileMode = "755".toInt(8)
+      filePermissions { unix("755") }
     }
     doLast {
       val bytes = MessageDigest.getInstance("SHA-256")

Diff for: ide-lsp/build.gradle.kts

@@ -1,29 +1,13 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
-// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
-import org.aya.gradle.GenerateVersionTask
-
 // Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 
 dependencies {
   api(project(":base"))
-  implementation(libs.sourcebuddy)
   testImplementation(libs.junit.jupiter)
   testImplementation(libs.hamcrest)
   testImplementation(project(":producer"))
 }
 
-val genTestDir = file("src/test/gen")
-idea.module.testSources.from(genTestDir)
-idea.module.generatedSourceDirs.add(genTestDir)
-sourceSets.test { java.srcDirs(genTestDir) }
-
-val cleanGenerated = tasks.register("cleanGenerated") {
-  group = "build"
-  genTestDir.deleteRecursively()
-}
-
-tasks.named("clean") { dependsOn(cleanGenerated) }
 tasks.withType<JavaExec>().configureEach {
   val vmArgs = jvmArgs ?: mutableListOf()
   vmArgs.add("-Xss32M")

Diff for: jit-compiler/build.gradle.kts

@@ -9,13 +9,9 @@
 import org.aya.compiler.util.SerializeUtils;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.TupTerm;
-import org.aya.syntax.core.term.call.ConCall;
-import org.aya.syntax.core.term.call.ConCallLike;
-import org.aya.syntax.core.term.call.DataCall;
-import org.aya.syntax.core.term.call.FnCall;
+import org.aya.syntax.core.term.call.*;
 import org.aya.util.error.Panic;
 import org.intellij.lang.annotations.Language;
-import org.jetbrains.annotations.NotNull;
 
 import static org.aya.compiler.AbstractSerializer.getJavaReference;
 
@@ -36,11 +32,12 @@ public interface AyaSerializer<T> {
   String PACKAGE_BASE = "AYA";
   String STATIC_FIELD_INSTANCE = "INSTANCE";
   String FIELD_INSTANCE = "ref";
-  String CLASS_JITCONCALL = getJavaReference(ConCall.class);
+  String CLASS_CONCALL = getJavaReference(ConCall.class);
   String CLASS_CONCALLLIKE = getJavaReference(ConCallLike.class);
   String CLASS_TUPLE = getJavaReference(TupTerm.class);
-  String CLASS_JITFNCALL = getJavaReference(FnCall.class);
-  String CLASS_JITDATACALL = getJavaReference(DataCall.class);
+  String CLASS_FNCALL = getJavaReference(FnCall.class);
+  String CLASS_DATACALL = getJavaReference(DataCall.class);
+  String CLASS_PRIMCALL = getJavaReference(PrimCall.class);
   String CLASS_IMMSEQ = getJavaReference(ImmutableSeq.class);
   String CLASS_MUTSEQ = getJavaReference(MutableSeq.class);
   String CLASS_SEQ = getJavaReference(Seq.class);

Diff for: jit-compiler/src/main/java/org/aya/compiler/AyaSerializer.java

@@ -166,9 +166,9 @@ private void serOp(@NotNull TyckDef def) {
   }
 
   public @NotNull ResolveInfo toResolveInfo(
-    @NotNull ModuleLoader loader, @NotNull PhysicalModuleContext context
+    @NotNull ModuleLoader loader, @NotNull PhysicalModuleContext context, ClassLoader classLoader
   ) {
-    var state = new DeState(getClass().getClassLoader());
+    var state = new DeState(classLoader);
     return toResolveInfo(loader, context, state, new PrimFactory(), new ShapeFactory());
   }
   public @NotNull ResolveInfo toResolveInfo(

Diff for: jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java

@@ -44,7 +44,8 @@ private void doSerialize(@NotNull TyckDef unit) {
         .serialize(dataDef);
       case ConDef conDef -> new ConSerializer(builder, indent, nameGen)
         .serialize(conDef);
-      case PrimDef primDef -> throw new UnsupportedOperationException("TODO");
+      case PrimDef primDef -> new PrimSerializer(this)
+        .serialize(primDef);
     }
   }