From 44f548e2b696425def39c1c869448ed7abd5b8cd Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sun, 5 Jan 2025 06:13:33 -0500
Subject: [PATCH] jit: trivial `isAvailable` is now default impl fix #1277

---
 .../compiler/serializers/ConSerializer.java   | 30 ++++++++-----------
 .../java/org/aya/syntax/compile/JitCon.java   | 20 ++++++-------
 2 files changed, 22 insertions(+), 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
index d9f9783ade..b4c77779ed 100644
--- 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
index 29f7e39909..6f7b177c2e 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitCon.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitCon.java
@@ -1,11 +1,10 @@
-// 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;
@@ -13,11 +12,9 @@
 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"); }