serde: fix compile

aya-prover · Jan 25, 2025 · ea1ca98 · ea1ca98
1 parent ad5cce9
commit ea1ca98
Show file tree

Hide file tree

Showing 7 changed files with 29 additions and 32 deletions.
diff --git a/base/src/main/java/org/aya/normalize/Normalizer.java b/base/src/main/java/org/aya/normalize/Normalizer.java
@@ -30,7 +30,6 @@
 import org.aya.syntax.ref.LocalVar;
 import org.aya.tyck.TyckState;
 import org.aya.tyck.tycker.Stateful;
-import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
@@ -93,7 +92,7 @@ case FnCall(FnDef.Delegate delegate, int ulift, var args) -> {
               continue;
             }
             case Either.Right(var body): {
-              var result = tryUnfoldClauses(body.clauses.view().map(WithPos::data),
+              var result = tryUnfoldClauses(body.matchingsView(),
                 args, core.is(Modifier.Overlap), ulift);
               // we may get stuck
               if (result == null) return defaultValue;

diff --git a/base/src/main/java/org/aya/primitive/ShapeMatcher.java b/base/src/main/java/org/aya/primitive/ShapeMatcher.java
@@ -29,7 +29,6 @@
 import org.aya.util.Pair;
 import org.aya.util.RepoLike;
 import org.aya.util.error.Panic;
-import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
@@ -126,7 +125,7 @@ case Pair(Either.Left(var termShape), Either.Left(var term)) ->
       case Pair(Either.Right(var clauseShapes), Either.Right(var body)) -> {
         var mode = def.is(Modifier.Overlap) ? MatchMode.Sub : MatchMode.Eq;
         yield matchInside(() -> captures.put(shape.name(), def.ref()), () ->
-          matchMany(mode, clauseShapes, body.clauses.view().map(WithPos::data), this::matchClause));
+          matchMany(mode, clauseShapes, body.matchingsView(), this::matchClause));
       }
       default -> false;
     };

diff --git a/base/src/main/java/org/aya/terck/CallResolver.java b/base/src/main/java/org/aya/terck/CallResolver.java
@@ -24,7 +24,6 @@
 import org.aya.syntax.core.term.xtt.PAppTerm;
 import org.aya.tyck.TyckState;
 import org.aya.tyck.tycker.Stateful;
-import org.aya.util.error.WithPos;
 import org.aya.util.terck.CallGraph;
 import org.aya.util.terck.CallMatrix;
 import org.aya.util.terck.Relation;
@@ -139,8 +138,8 @@ private Relation compareConArgs(@NotNull ImmutableSeq<Term> conArgs, @NotNull Pa
   }
 
   public void check() {
-    var clauses = caller.body().getRightValue().clauses;
-    clauses.view().map(WithPos::data).forEach(this);
+    var clauses = caller.body().getRightValue().matchingsView();
+    clauses.forEach(this);
   }
 
   @Override public void accept(@NotNull Term.Matching matching) {

diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -191,8 +191,7 @@ && whnf(type) instanceof DataCall dataCall
       ImmutableSeq.fill(discriminant.size(), i ->
         new LocalVar("match" + i, discriminant.get(i).sourcePos(), GenerateKind.Basic.Tyck)),
       ImmutableSeq.empty(), clauses);
-    var wellClauses = clauseTycker.check(exprPos)
-      .wellTyped().clauses.map(WithPos::data);
+    var wellClauses = clauseTycker.check(exprPos).wellTyped().matchingsView();
 
     // Find free occurrences
     var usages = new FreeCollector();

diff --git a/jit-compiler/src/main/java/org/aya/compiler/serializers/FnSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/serializers/FnSerializer.java
@@ -1,29 +1,28 @@
-// 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.compiler.serializers;
 
+import java.lang.constant.ClassDesc;
+import java.lang.constant.ConstantDescs;
+import java.util.EnumSet;
+import java.util.function.Consumer;
+
 import kala.collection.immutable.ImmutableSeq;
 import kala.control.Either;
 import org.aya.compiler.free.Constants;
 import org.aya.compiler.free.FreeClassBuilder;
 import org.aya.compiler.free.FreeCodeBuilder;
 import org.aya.compiler.free.FreeJavaExpr;
-import org.aya.compiler.free.data.MethodRef;
 import org.aya.compiler.free.data.LocalVariable;
+import org.aya.compiler.free.data.MethodRef;
 import org.aya.generic.Modifier;
 import org.aya.primitive.ShapeFactory;
 import org.aya.syntax.compile.JitFn;
 import org.aya.syntax.core.def.FnDef;
 import org.aya.syntax.core.def.TyckAnyDef;
 import org.aya.syntax.core.term.call.FnCall;
-import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
 
-import java.lang.constant.ClassDesc;
-import java.lang.constant.ConstantDescs;
-import java.util.EnumSet;
-import java.util.function.Consumer;
-
 public final class FnSerializer extends JitTeleSerializer<FnDef> {
   private final @NotNull ShapeFactory shapeFactory;
 
@@ -83,19 +82,17 @@ private void buildInvoke(
       }
       case Either.Right(var clauses) -> {
         var ser = new PatternSerializer(argExprs, onStuckCon, unit.is(Modifier.Overlap));
-        ser.serialize(builder, clauses.view()
-          .map(WithPos::data)
-          .map(matching -> new PatternSerializer.Matching(
-              matching.bindCount(), matching.patterns(), (patSer, builder0, bindSize) -> {
-              var result = serializeTermUnderTele(
-                builder0,
-                matching.body(),
-                patSer.result.ref(),
-                bindSize
-              );
-              builder0.returnWith(result);
-            })
-          ).toImmutableSeq());
+        ser.serialize(builder, clauses.matchingsView().map(matching -> new PatternSerializer.Matching(
+            matching.bindCount(), matching.patterns(), (patSer, builder0, bindSize) -> {
+            var result = serializeTermUnderTele(
+              builder0,
+              matching.body(),
+              patSer.result.ref(),
+              bindSize
+            );
+            builder0.returnWith(result);
+          })
+        ).toImmutableSeq());
       }
     }
   }

diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -36,7 +36,6 @@
 import org.aya.syntax.ref.LocalVar;
 import org.aya.util.Arg;
 import org.aya.util.error.SourcePos;
-import org.aya.util.error.WithPos;
 import org.aya.util.prettier.PrettierOptions;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
@@ -286,7 +285,7 @@ private ImmutableSeq<Term> visibleArgsOf(Callable call) {
         yield switch (def.body()) {
           case Either.Left(var term) -> Doc.sep(line1sep, FN_DEFINED_AS, term(Outer.Free, term.instTele(subst)));
           case Either.Right(var body) -> Doc.vcat(line1sep,
-            Doc.nest(2, visitClauses(body.clauses.view().map(WithPos::data), tele.view().map(ParamLike::explicit))));
+            Doc.nest(2, visitClauses(body.matchingsView(), tele.view().map(ParamLike::explicit))));
         };
       }
       case MemberDef field -> Doc.sepNonEmpty(Doc.symbol("|"),

diff --git a/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java b/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java
@@ -2,13 +2,18 @@
 // 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 kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.syntax.core.term.Term;
 import org.aya.util.error.WithPos;
 import org.aya.util.tyck.pat.PatClass;
+import org.jetbrains.annotations.NotNull;
 
 public final class FnClauseBody {
   public final ImmutableSeq<WithPos<Term.Matching>> clauses;
   public ImmutableSeq<PatClass<ImmutableSeq<Term>>> classes;
   public FnClauseBody(ImmutableSeq<WithPos<Term.Matching>> clauses) { this.clauses = clauses; }
+  public @NotNull SeqView<Term.Matching> matchingsView() {
+    return clauses.view().map(WithPos::data);
+  }
 }