build: add missing build, initialize java code

aya-prover · May 27, 2024 · 4b1f643 · 4b1f643
1 parent ad1c97c
commit 4b1f643
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 3 deletions.
diff --git a/cli-console/build.gradle.kts b/cli-console/build.gradle.kts
@@ -17,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 --git a/cli-impl/src/main/java/org/aya/cli/library/incremental/DiskCompilerAdvisor.java b/cli-impl/src/main/java/org/aya/cli/library/incremental/DiskCompilerAdvisor.java
@@ -7,9 +7,13 @@
 import org.aya.cli.library.source.LibrarySource;
 import org.aya.cli.utils.CompilerUtil;
 import org.aya.compiler.CompiledModule;
+import org.aya.compiler.FileSerializer;
+import org.aya.compiler.ModuleSerializer;
 import org.aya.resolve.ResolveInfo;
 import org.aya.resolve.context.EmptyContext;
+import org.aya.resolve.module.DumbModuleLoader;
 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;
@@ -75,6 +79,10 @@ public class DiskCompilerAdvisor implements CompilerAdvisor {
     @NotNull ResolveInfo resolveInfo,
     @NotNull ImmutableSeq<TyckDef> defs
   ) throws IOException {
+    var javaCode = new FileSerializer(resolveInfo.shapeFactory())
+      .serialize(new FileSerializer.FileResult(file.moduleName().dropLast(1), new ModuleSerializer.ModuleResult(
+        file.moduleName().last(), defs.filterIsInstance(TopLevelDef.class), ImmutableSeq.empty())))
+      .result();
     // TODO: compile defs
     var coreFile = file.compiledCorePath();
     CompilerUtil.saveCompiledCore(coreFile, resolveInfo);

diff --git a/jit-compiler/src/test/java/CompileTest.java b/jit-compiler/src/test/java/CompileTest.java
@@ -97,9 +97,7 @@ def plus (a b : Nat) : Nat elim a
     System.out.println(out);
   }
 
-  public record TyckResult(@NotNull ImmutableSeq<TyckDef> defs, @NotNull ResolveInfo info) {
-
-  }
+  public record TyckResult(@NotNull ImmutableSeq<TyckDef> defs, @NotNull ResolveInfo info) { }
 
   private static final @NotNull Path FILE = Path.of("/home/senpai/1919810.aya");
   public static final ThrowingReporter REPORTER = new ThrowingReporter(AyaPrettierOptions.pretty());

diff --git a/syntax/src/main/java/org/aya/syntax/ref/ModulePath.java b/syntax/src/main/java/org/aya/syntax/ref/ModulePath.java
@@ -41,4 +41,5 @@ public boolean sameElements(ModulePath other) {
   @Override public String toString() { return QualifiedID.join(module); }
   public boolean isEmpty() { return module.isEmpty(); }
   public int size() { return module.size(); }
+  public @NotNull String last() { return module.getLast(); }
 }