jit: primCall

base/src/main/java/org/aya/primitive/PrimFactory.java

@@ -195,7 +195,7 @@ public boolean have(@NotNull ID name) {
   }
 
   public @NotNull Term unfold(@NotNull PrimCall primCall, @NotNull TyckState state) {
-    var id = primCall.ref().core().id;
+    var id = primCall.ref().id();
     return seeds.get(id).unfold.apply(primCall, state);
   }
 

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

@@ -9,13 +9,9 @@
 import org.aya.compiler.util.SerializeUtils;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.TupTerm;
-import org.aya.syntax.core.term.call.ConCall;
-import org.aya.syntax.core.term.call.ConCallLike;
-import org.aya.syntax.core.term.call.DataCall;
-import org.aya.syntax.core.term.call.FnCall;
+import org.aya.syntax.core.term.call.*;
 import org.aya.util.error.Panic;
 import org.intellij.lang.annotations.Language;
-import org.jetbrains.annotations.NotNull;
 
 import static org.aya.compiler.AbstractSerializer.getJavaReference;
 
@@ -36,11 +32,12 @@ public interface AyaSerializer<T> {
   String PACKAGE_BASE = "AYA";
   String STATIC_FIELD_INSTANCE = "INSTANCE";
   String FIELD_INSTANCE = "ref";
-  String CLASS_JITCONCALL = getJavaReference(ConCall.class);
+  String CLASS_CONCALL = getJavaReference(ConCall.class);
   String CLASS_CONCALLLIKE = getJavaReference(ConCallLike.class);
   String CLASS_TUPLE = getJavaReference(TupTerm.class);
-  String CLASS_JITFNCALL = getJavaReference(FnCall.class);
-  String CLASS_JITDATACALL = getJavaReference(DataCall.class);
+  String CLASS_FNCALL = getJavaReference(FnCall.class);
+  String CLASS_DATACALL = getJavaReference(DataCall.class);
+  String CLASS_PRIMCALL = getJavaReference(PrimCall.class);
   String CLASS_IMMSEQ = getJavaReference(ImmutableSeq.class);
   String CLASS_MUTSEQ = getJavaReference(MutableSeq.class);
   String CLASS_SEQ = getJavaReference(Seq.class);

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

@@ -5,7 +5,6 @@
 import com.intellij.openapi.util.text.StringUtil;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableMap;
-import kala.text.StringUtils;
 import org.aya.generic.NameGenerator;
 import org.aya.generic.stmt.Shaped;
 import org.aya.generic.term.SortKind;
@@ -122,12 +121,12 @@ public TermExprializer(@NotNull NameGenerator nameGen, @NotNull ImmutableSeq<Str
       case AppTerm appTerm -> makeNew(CLASS_APPTERM, appTerm.fun(), appTerm.arg());
       case LocalTerm _ -> throw new Panic("LocalTerm");
       case LamTerm lamTerm -> makeNew(CLASS_LAMTERM, serializeClosure(lamTerm.body()));
-      case DataCall(var ref, var ulift, var args) -> makeNew(CLASS_JITDATACALL,
+      case DataCall(var ref, var ulift, var args) -> makeNew(CLASS_DATACALL,
         getInstance(getReference(ref)),
         Integer.toString(ulift),
         serializeToImmutableSeq(CLASS_TERM, args)
       );
-      case ConCall(var head, var args) -> makeNew(CLASS_JITCONCALL,
+      case ConCall(var head, var args) -> makeNew(CLASS_CONCALL,
         getInstance(getReference(head.ref())),
         serializeToImmutableSeq(CLASS_TERM, head.ownerArgs()),
         Integer.toString(head.ulift()),
@@ -141,7 +140,7 @@ case ConCall(var head, var args) -> makeNew(CLASS_JITCONCALL,
 
         var ulift = call.ulift();
         var args = call.args();
-        yield buildReducibleCall(ref, CLASS_JITFNCALL, ulift, ImmutableSeq.of(args), true);
+        yield buildReducibleCall(ref, CLASS_FNCALL, ulift, ImmutableSeq.of(args), true);
       }
       case RuleReducer.Con conRuler -> buildReducibleCall(
         serializeApplicable(conRuler.rule()),
@@ -184,7 +183,11 @@ case TupTerm(var items) -> makeNew(getJavaReference(TupTerm.class),
         serializeToImmutableSeq(CLASS_TERM, items)
       );
       case SigmaTerm sigmaTerm -> throw new UnsupportedOperationException("TODO");
-      case PrimCall primCall -> throw new UnsupportedOperationException("TODO");
+      case PrimCall(var ref, var ulift, var args) -> makeNew(CLASS_PRIMCALL,
+        getInstance(getReference(ref)),
+        Integer.toString(ulift),
+        serializeToImmutableSeq(CLASS_TERM, args)
+      );
       case IntegerTerm(var repr, var zero, var suc, var type) -> makeNew(CLASS_INTEGER,
         Integer.toString(repr),
         getInstance(getReference(zero)),

syntax/src/main/java/org/aya/syntax/compile/JitPrim.java

@@ -5,11 +5,13 @@
 import kala.collection.Seq;
 import org.aya.generic.stmt.Reducible;
 import org.aya.syntax.core.def.PrimDef;
+import org.aya.syntax.core.def.PrimDefLike;
 import org.aya.syntax.core.term.Term;
 import org.jetbrains.annotations.NotNull;
 
-public abstract non-sealed class JitPrim extends JitDef implements Reducible {
+public abstract non-sealed class JitPrim extends JitDef implements PrimDefLike, Reducible {
   public final PrimDef.ID id;
+  @Override public PrimDef.@NotNull ID id() { return id; }
   protected JitPrim(int telescopeSize, boolean[] telescopeLicit, String[] telescopeName, PrimDef.ID id) {
     super(telescopeSize, telescopeLicit, telescopeName);
     this.id = id;

syntax/src/main/java/org/aya/syntax/core/def/AnyDef.java

@@ -29,7 +29,7 @@
  * </ul>
  * Note that {@link ConDef.Delegate} <b>contains</b> a {@link ConDef} rather than a super class of.
  */
-public sealed interface AnyDef extends OpDecl permits JitDef, ConDefLike, DataDefLike, FnDefLike, TyckAnyDef {
+public sealed interface AnyDef extends OpDecl permits JitDef, ConDefLike, DataDefLike, FnDefLike, PrimDefLike, TyckAnyDef {
   /**
    * Returns which file level module this def lives in.
    */

syntax/src/main/java/org/aya/syntax/core/def/PrimDef.java

@@ -86,7 +86,8 @@ public enum ID {
 
   public @NotNull DefVar<@NotNull PrimDef, @NotNull PrimDecl> ref() { return ref; }
 
-  public static class Delegate extends TyckAnyDef<PrimDef> {
+  public static final class Delegate extends TyckAnyDef<PrimDef> implements PrimDefLike {
     public Delegate(@NotNull DefVar<PrimDef, ?> ref) { super(ref); }
+    @Override public @NotNull PrimDef.ID id() { return core().id; }
   }
 }

syntax/src/main/java/org/aya/syntax/core/def/PrimDefLike.java

@@ -0,0 +1,10 @@
+// Copyright (c) 2020-2024 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.core.def;
+
+import org.aya.syntax.compile.JitPrim;
+import org.jetbrains.annotations.NotNull;
+
+public sealed interface PrimDefLike extends AnyDef permits JitPrim, PrimDef.Delegate {
+  @NotNull PrimDef.ID id();
+}

syntax/src/main/java/org/aya/syntax/core/term/call/PrimCall.java

@@ -6,13 +6,13 @@
 import kala.function.IndexedFunction;
 import org.aya.syntax.concrete.stmt.decl.PrimDecl;
 import org.aya.syntax.core.def.PrimDef;
-import org.aya.syntax.core.def.TyckAnyDef;
+import org.aya.syntax.core.def.PrimDefLike;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.ref.DefVar;
 import org.jetbrains.annotations.NotNull;
 
 public record PrimCall(
-  @Override @NotNull TyckAnyDef<PrimDef> ref,
+  @Override @NotNull PrimDefLike ref,
   @Override int ulift,
   @Override @NotNull ImmutableSeq<@NotNull Term> args
 ) implements Callable.Tele {

syntax/src/main/java/org/aya/syntax/ref/ModulePath.java

@@ -7,7 +7,9 @@
 import org.aya.syntax.concrete.stmt.QualifiedID;
 import org.jetbrains.annotations.NotNull;
 
-public record ModulePath(@NotNull ImmutableSeq<String> module) {
+import java.io.Serializable;
+
+public record ModulePath(@NotNull ImmutableSeq<String> module) implements Serializable {
   public static @NotNull ModulePath of(@NotNull String... names) {
     return new ModulePath(ImmutableSeq.from(names));
   }

syntax/src/main/java/org/aya/syntax/ref/QName.java

@@ -5,9 +5,10 @@
 import kala.collection.immutable.ImmutableSeq;
 import org.jetbrains.annotations.NotNull;
 
+import java.io.Serializable;
 import java.util.Objects;
 
-public record QName(@NotNull QPath module, @NotNull String name) {
+public record QName(@NotNull QPath module, @NotNull String name) implements Serializable {
   public QName(@NotNull DefVar<?, ?> ref) {
     this(Objects.requireNonNull(ref.module), ref.name());
   }

syntax/src/main/java/org/aya/syntax/ref/QPath.java

@@ -4,7 +4,9 @@
 
 import org.jetbrains.annotations.NotNull;
 
-public record QPath(@NotNull ModulePath module, int fileModuleSize) {
+import java.io.Serializable;
+
+public record QPath(@NotNull ModulePath module, int fileModuleSize) implements Serializable {
   public QPath {
     assert 0 < fileModuleSize && fileModuleSize <= module.module().size();
   }