jit: trivial isAvailable is now default impl fix #1277

aya-prover · Jan 5, 2025 · 44f548e · 44f548e
1 parent 353ce22
commit 44f548e
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 28 deletions.
diff --git a/jit-compiler/src/main/java/org/aya/compiler/serializers/ConSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/serializers/ConSerializer.java
@@ -42,25 +42,21 @@ public ConSerializer(ModuleSerializer.@NotNull MatchyRecorder recorder) {
     ));
   }
 
-  /// @see JitCon#isAvailable(Seq)
+  /// @param unit must be indexed, otherwise it should use the default impl.
+  /// @see JitCon#isAvailable
   private void buildIsAvailable(@NotNull FreeCodeBuilder builder, ConDef unit, @NotNull LocalVariable argsTerm) {
     FreeJavaExpr matchResult;
     var termSeq = builder.invoke(Constants.SEQ_TOIMMSEQ, argsTerm.ref(), ImmutableSeq.empty());
-    if (unit.pats.isEmpty()) {
-      // not indexed data type, this constructor is always available
-      matchResult = builder.invoke(Constants.RESULT_OK, ImmutableSeq.of(termSeq));
-    } else {
-      // It is too stupid to serialize pat meta solving, so we just call PatMatcher
-      var patsTerm = unit.pats.map(x -> new PatternExprializer(builder, true, recorder).serialize(x));
-      var patsSeq = AbstractExprializer.makeImmutableSeq(builder, Pat.class, patsTerm);
-      var id = builder.invoke(Constants.CLOSURE_ID, ImmutableSeq.empty());
-      var matcherTerm = builder.mkNew(PatMatcher.class, ImmutableSeq.of(
-        builder.iconst(true), id
-      ));
+    // It is too stupid to serialize pat meta solving, so we just call PatMatcher
+    var patsTerm = unit.pats.map(x -> new PatternExprializer(builder, true, recorder).serialize(x));
+    var patsSeq = AbstractExprializer.makeImmutableSeq(builder, Pat.class, patsTerm);
+    var id = builder.invoke(Constants.CLOSURE_ID, ImmutableSeq.empty());
+    var matcherTerm = builder.mkNew(PatMatcher.class, ImmutableSeq.of(
+      builder.iconst(true), id
+    ));
 
-      matchResult = builder.invoke(Constants.PATMATCHER_APPLY, matcherTerm,
-        ImmutableSeq.of(patsSeq, termSeq));
-    }
+    matchResult = builder.invoke(Constants.PATMATCHER_APPLY, matcherTerm,
+      ImmutableSeq.of(patsSeq, termSeq));
 
     builder.returnWith(matchResult);
   }
@@ -88,10 +84,10 @@ private void buildEquality(
 
   @Override public @NotNull ConSerializer serialize(@NotNull FreeClassBuilder builder0, ConDef unit) {
     buildFramework(builder0, unit, builder -> {
-      builder.buildMethod(
+      if (unit.pats.isNotEmpty()) builder.buildMethod(
         FreeUtil.fromClass(Result.class),
         "isAvailable",
-        ImmutableSeq.of(Constants.CD_Seq),
+        ImmutableSeq.of(Constants.CD_ImmutableSeq),
         (ap, builder1) ->
           buildIsAvailable(builder1, unit, ap.arg(0)));
 

diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitCon.java b/syntax/src/main/java/org/aya/syntax/compile/JitCon.java
@@ -1,23 +1,20 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.compile;
 
 import kala.collection.Seq;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableArrayList;
-import kala.collection.mutable.MutableList;
 import kala.control.Result;
 import org.aya.generic.State;
 import org.aya.syntax.core.def.ConDefLike;
 import org.aya.syntax.core.def.DataDefLike;
 import org.aya.syntax.core.term.FreeTerm;
 import org.aya.syntax.core.term.Param;
 import org.aya.syntax.core.term.Term;
-import org.aya.syntax.ref.GenerateKind;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.syntax.telescope.JitTele;
 import org.aya.util.error.Panic;
-import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.UnknownNullability;
 
@@ -37,13 +34,14 @@ protected JitCon(
     this.selfTeleSize = selfTeleSize;
   }
 
-  /**
-   * Whether this constructor is available of data type
-   *
-   * @param args the argument to the data type
-   * @return a match result, a sequence of substitution if success
-   */
-  public abstract @NotNull Result<ImmutableSeq<Term>, State> isAvailable(@NotNull Seq<Term> args);
+  /// Whether this constructor is available of data type.
+  /// The default impl is for non-indexed constructors, where it's always available.
+  ///
+  /// @param args the argument to the data type
+  /// @return a match result, a sequence of substitution if success
+  public @NotNull Result<ImmutableSeq<Term>, State> isAvailable(@NotNull ImmutableSeq<Term> args) {
+    return Result.ok(args);
+  }
 
   @Override public boolean hasEq() { return hasEq; }
   @Override public @NotNull Term equality(Seq<Term> args, boolean is0) { throw new Panic("Not an HIT"); }