merge: Free Java (#1197)

This PR proposes a `FreeJavaBuilder` interface that allows users to
construct the FreeJava in Java source code.

## Free Java

FreeJava is the AST of Java source code, which can be
compiled/interpreted to different targets, such as bytecode, source
code, or
 itself.

## FreeJavaBuilder

`FreeJavaBuilder` is an interface that allows users to construct a
FreeJava in builder form. Those methods are just like the constructor of
FreeJava, but they will be interpreted immediately.

## Goal

`FreeJavaBuilder` can be used to construct FreeJava, then we can perform
optimization, and translate to another target.

## TODO

- [x] Complete FreeJavaBuilder
- [x] Interpret to source code
- [ ] Interpret to bytecode
- [ ] Interpret to free java and optimization

## Note

This PR is supposed to run on JDK 24 which version with stable Classfile
API.

base/build.gradle.kts

@@ -8,6 +8,7 @@ dependencies {
   // implementation(libs.manifold.delegate.runtime)
   // annotationProcessor(libs.manifold.delegate.codegen)
   testImplementation(project(":producer"))
+  testImplementation(project(":jit-compiler"))
   testImplementation(libs.junit.params)
   testImplementation(libs.junit.jupiter)
   testImplementation(libs.hamcrest)

base/src/main/java/org/aya/normalize/Normalizer.java

@@ -6,7 +6,6 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.immutable.ImmutableSet;
 import kala.control.Either;
-import kala.control.Option;
 import kala.control.Result;
 import org.aya.generic.Modifier;
 import org.aya.syntax.compile.JitFn;
@@ -26,6 +25,7 @@
 import org.aya.tyck.tycker.Stateful;
 import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
 
 import java.util.function.UnaryOperator;
 
@@ -88,8 +88,8 @@ case FnCall(var fn, int ulift, var args) -> {
                   var result = tryUnfoldClauses(clauses.view().map(WithPos::data),
                     args, ulift, core.is(Modifier.Overlap));
                   // we may get stuck
-                  if (result.isEmpty()) return defaultValue;
-                  term = result.get();
+                  if (result == null) return defaultValue;
+                  term = result;
                   continue;
                 }
               }
@@ -156,10 +156,10 @@ case ConCall(var head, _) when !head.ref().hasEq() -> {
             }
           }
         }
-        case MatchTerm matchTerm -> {
-          var result = tryUnfoldClauses(matchTerm.clauses().view(), matchTerm.discriminant(), 0, false);
-          if (result.isEmpty()) return defaultValue;
-          term = result.get();
+        case MatchTerm(var discr, _, var clauses) -> {
+          var result = tryUnfoldClauses(clauses.view(), discr, 0, false);
+          if (result == null) return defaultValue;
+          term = result;
           continue;
         }
         default -> {
@@ -173,22 +173,22 @@ private boolean isOpaque(@NotNull FnDef fn) {
     return opaque.contains(fn.ref()) || fn.is(Modifier.Opaque) || fn.is(Modifier.Partial);
   }
 
-  public @NotNull Option<Term> tryUnfoldClauses(
+  public @Nullable Term tryUnfoldClauses(
     @NotNull SeqView<Term.Matching> clauses, @NotNull ImmutableSeq<Term> args,
     int ulift, boolean orderIndependent
   ) {
     for (var matchy : clauses) {
       var matcher = new PatMatcher(false, this);
       switch (matcher.apply(matchy.patterns(), args)) {
         case Result.Err(var st) -> {
-          if (!orderIndependent && st == Stuck) return Option.none();
+          if (!orderIndependent && st == Stuck) return null;
         }
         case Result.Ok(var subst) -> {
-          return Option.some(matchy.body().elevate(ulift).instantiateTele(subst.view()));
+          return matchy.body().elevate(ulift).instantiateTele(subst.view());
         }
       }
     }
-    return Option.none();
+    return null;
   }
 
   private class Full implements UnaryOperator<Term> {

base/src/main/java/org/aya/tyck/ExprTycker.java

@@ -367,7 +367,7 @@ case DepTypeTerm(var kind, var param, var body) when kind == DTKind.Sigma -> {
           yield fail(expr.data(), new NoRuleError(expr, null));
         }
         if (defs.sizeGreaterThan(1)) {
-          var type = freshMeta("_ty" + integer + "'", expr.sourcePos(), MetaVar.Misc.IsType, false);
+          var type = freshMeta(integer + "_ty", expr.sourcePos(), MetaVar.Misc.IsType, false);
           yield new Jdg.Default(new MetaLitTerm(expr.sourcePos(), integer, defs, type), type);
         }
         var match = defs.getFirst();

base/src/main/java/org/aya/tyck/tycker/Contextful.java

@@ -2,7 +2,6 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck.tycker;
 
-import org.aya.generic.Constants;
 import org.aya.generic.term.DTKind;
 import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.core.Closure;
@@ -18,8 +17,6 @@
 import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
 
-import java.util.function.Supplier;
-
 /**
  * Indicating something is {@link LocalCtx}ful.<br/>
  * Whenever you want to introduce some bind, make sure you are modifying
@@ -60,15 +57,15 @@ public interface Contextful {
     return new MetaCall(new MetaVar(name, pos, args.size(), req.bind(vars.view()), isUser), args);
   }
 
+  /** @see org.aya.syntax.ref.MetaVar#asDt */
   default @NotNull Term generatePi(Expr.@NotNull Lambda expr, SourcePos sourcePos) {
     var param = expr.param();
     return generatePi(sourcePos, param.ref().name());
   }
 
   private @NotNull Term generatePi(@NotNull SourcePos pos, @NotNull String name) {
-    var genName = name + Constants.GENERATED_POSTFIX;
-    var domain = freshMeta(genName + "ty", pos, MetaVar.Misc.IsType, false);
-    var codomain = freshMeta(genName + "ret", pos, MetaVar.Misc.IsType, false);
+    var domain = freshMeta(name + "ty", pos, MetaVar.Misc.IsType, false);
+    var codomain = freshMeta(name + "ret", pos, MetaVar.Misc.IsType, false);
     return new DepTypeTerm(DTKind.Pi, domain, Closure.mkConst(codomain));
   }
 }

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

@@ -8,9 +8,9 @@
 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.compiler.NameSerializer;
+import org.aya.compiler.free.morphism.SourceFreeJavaBuilder;
+import org.aya.compiler.serializers.ModuleSerializer;
+import org.aya.compiler.serializers.NameSerializer;
 import org.aya.primitive.PrimFactory;
 import org.aya.resolve.ResolveInfo;
 import org.aya.resolve.context.EmptyContext;
@@ -99,7 +99,7 @@ public void addURL(Path url) throws MalformedURLException {
     var context = new EmptyContext(reporter, sourcePath).derive(mod);
     var coreDir = computeBaseDir(libraryRoot);
     cl.addURL(coreDir);
-    cl.loadClass(NameSerializer.getModuleReference(QPath.fileLevel(mod)));
+    cl.loadClass(NameSerializer.getModuleClassName(QPath.fileLevel(mod)));
     return compiledAya.toResolveInfo(recurseLoader, context, cl, primFactory);
   }
 
@@ -128,11 +128,10 @@ public void addURL(Path url) throws MalformedURLException {
     @NotNull ImmutableSeq<TyckDef> defs,
     @NotNull ModuleLoader recurseLoader
   ) throws IOException, ClassNotFoundException {
-    var javaCode = new FileSerializer(resolveInfo.shapeFactory())
-      .serialize(new ModuleSerializer.ModuleResult(
+    var javaCode = new ModuleSerializer<String>(resolveInfo.shapeFactory())
+      .serialize(SourceFreeJavaBuilder.create(), new ModuleSerializer.ModuleResult(
         QPath.fileLevel(file.moduleName()),
-        defs.filterIsInstance(TopLevelDef.class)))
-      .result();
+        defs.filterIsInstance(TopLevelDef.class)));
     var libraryRoot = file.owner().outDir();
     var baseDir = computeBaseDir(libraryRoot).toAbsolutePath();
     var relativePath = NameSerializer.getReference(QPath.fileLevel(file.moduleName()), null,

jit-compiler/src/main/java/module-info.java

@@ -6,4 +6,8 @@
   requires static org.jetbrains.annotations;
 
   exports org.aya.compiler;
+  exports org.aya.compiler.free;
+  exports org.aya.compiler.free.data;
+  exports org.aya.compiler.free.morphism;
+  exports org.aya.compiler.serializers;
 }

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

@@ -7,6 +7,8 @@
 import kala.collection.immutable.ImmutableSet;
 import kala.collection.mutable.MutableMap;
 import kala.tuple.Tuple;
+import org.aya.compiler.serializers.AyaSerializer;
+import org.aya.compiler.serializers.NameSerializer;
 import org.aya.primitive.PrimFactory;
 import org.aya.primitive.ShapeFactory;
 import org.aya.resolve.ResolveInfo;
@@ -50,7 +52,7 @@ public record CompiledModule(
   public record DeState(@NotNull ClassLoader loader) {
     public @NotNull Class<?> topLevelClass(@NotNull ModulePath name) {
       try {
-        return loader.loadClass(NameSerializer.getModuleReference(QPath.fileLevel(name)));
+        return loader.loadClass(NameSerializer.getModuleClassName(QPath.fileLevel(name)));
       } catch (ClassNotFoundException e) {
         throw new Panic(e);
       }