jit: allBinds

aya-prover · Jun 9, 2024 · a35c905 · a35c905
1 parent 884a2cb
commit a35c905
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 30 deletions.
diff --git a/jit-compiler/src/main/java/org/aya/compiler/FnSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/FnSerializer.java
@@ -57,7 +57,7 @@ private void buildInvoke(FnDef unit, @NotNull String onStuckTerm, @NotNull Immut
       case Either.Right(var clauses) -> {
         var ser = new PatternSerializer(this.sourceBuilder, argTerms, onStuckCon, onStuckCon);
         ser.serialize(clauses.map(matching -> new PatternSerializer.Matching(
-          matching.patterns(), (s, bindSize) ->
+          matching.bindCount(), matching.patterns(), (s, bindSize) ->
           s.buildReturn(serializeTermUnderTele(matching.body(), PatternSerializer.VARIABLE_RESULT, bindSize))
         )));
       }

diff --git a/jit-compiler/src/main/java/org/aya/compiler/PatternExprializer.java b/jit-compiler/src/main/java/org/aya/compiler/PatternExprializer.java
@@ -4,7 +4,6 @@
 
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.syntax.core.pat.Pat;
-import org.aya.syntax.core.term.ErrorTerm;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.call.ConCallLike;
 import org.aya.syntax.ref.LocalVar;
@@ -21,7 +20,6 @@ public class PatternExprializer extends AbstractExprializer<Pat> {
   public static final @NotNull String CLASS_PAT_INT = ExprializeUtils.makeSub(CLASS_PAT, ExprializeUtils.getJavaReference(Pat.ShapedInt.class));
   public static final @NotNull String CLASS_LOCALVAR = ExprializeUtils.getJavaReference(LocalVar.class);
   public static final @NotNull String CLASS_CONHEAD = ExprializeUtils.makeSub(ExprializeUtils.getJavaReference(ConCallLike.class), ExprializeUtils.getJavaReference(ConCallLike.Head.class));
-  public static final @NotNull String CLASS_ERROR = ExprializeUtils.getJavaReference(ErrorTerm.class);
   public static final @NotNull String CLASS_PAT_TUPLE = ExprializeUtils.makeSub(CLASS_PAT, ExprializeUtils.getJavaReference(Pat.Tuple.class));
 
   private final boolean allowLocalTerm;
@@ -67,8 +65,5 @@ protected PatternExprializer(@NotNull NameGenerator nameGen, boolean allowLocalT
     };
   }
 
-  @Override
-  public @NotNull String serialize(Pat unit) {
-    return doSerialize(unit);
-  }
+  @Override public @NotNull String serialize(Pat unit) { return doSerialize(unit); }
 }
diff --git a/jit-compiler/src/main/java/org/aya/compiler/PatternSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/PatternSerializer.java
@@ -6,7 +6,6 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.immutable.primitive.ImmutableIntSeq;
 import kala.range.primitive.IntRange;
-import kala.value.primitive.MutableIntValue;
 import org.aya.generic.AyaDocile;
 import org.aya.generic.State;
 import org.aya.syntax.core.pat.Pat;
@@ -27,28 +26,23 @@ public interface SuccessContinuation extends BiConsumer<PatternSerializer, Integ
   }
 
   public final static class Once implements Runnable {
-    public static @NotNull Once of(@NotNull Runnable run) {
-      return new Once(run);
-    }
-
+    public static @NotNull Once of(@NotNull Runnable run) { return new Once(run); }
     private final @NotNull Runnable run;
     private boolean dirty = false;
 
     public Once(@NotNull Runnable run) { this.run = run; }
 
-    @Override
-    public void run() {
-      if (dirty) {
-        throw new Panic("Once");
-      }
-
+    @Override public void run() {
+      if (dirty) throw new Panic("Once");
       dirty = true;
       this.run.run();
     }
   }
 
-  public record Matching(@NotNull ImmutableSeq<Pat> patterns, @NotNull SuccessContinuation onSucc) {
-  }
+  public record Matching(
+    int bindCount, @NotNull ImmutableSeq<Pat> patterns,
+    @NotNull SuccessContinuation onSucc
+  ) { }
 
   public static final @NotNull String VARIABLE_RESULT = "result";
   public static final @NotNull String VARIABLE_STATE = "matchState";
@@ -135,9 +129,7 @@ private void multiStage(
     buildLocalVar(CLASS_TERM, tmpName, term);
 
     for (var pre : preContinuation) {
-      buildIf(STR."! \{VARIABLE_SUBSTATE}", () -> {
-        pre.accept(tmpName);
-      });
+      buildIf(STR."! \{VARIABLE_SUBSTATE}", () -> pre.accept(tmpName));
     }
 
     buildIf(VARIABLE_SUBSTATE, continuation);
@@ -190,20 +182,14 @@ private void onMatchBind(@NotNull String term) {
     appendLine(STR."\{VARIABLE_RESULT}.set(\{bindCount++}, \{term});");
   }
 
-  private int bindAmount(@NotNull ImmutableSeq<Pat> pats) {
-    var acc = MutableIntValue.create();
-    pats.forEach(pat -> pat.consumeBindings((_, _) -> acc.increment()));
-    return acc.get();
-  }
-
   /// endregion Java Source Code Generate API
 
   @Override public PatternSerializer serialize(@NotNull ImmutableSeq<Matching> unit) {
     if (unit.isEmpty()) {
       onMismatch.accept(this);
       return this;
     }
-    var bindSize = unit.mapToInt(ImmutableIntSeq.factory(), x -> bindAmount(x.patterns));
+    var bindSize = unit.mapToInt(ImmutableIntSeq.factory(), Matching::bindCount);
     int maxBindSize = bindSize.max();
 
     buildLocalVar(STR."\{CLASS_MUTSEQ}<\{CLASS_TERM}>", VARIABLE_RESULT, STR."\{CLASS_MUTSEQ}.fill(\{maxBindSize}, (\{CLASS_TERM}) null)");