diff --git a/base/src/main/java/org/aya/normalize/Normalizer.java b/base/src/main/java/org/aya/normalize/Normalizer.java index fc1229538..1f4793809 100644 --- 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 index 4c5df43b3..08b10da7b 100644 --- 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 index ec2f01087..88ee70b4b 100644 --- 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 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 index 84fd69a57..a5550c690 100644 --- 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 index 2d6aed76b..ec0ef7469 100644 --- 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 { 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 index f80ee53a2..b3d4b8166 100644 --- 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 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 index 14910d847..f60c11e4d 100644 --- 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> clauses; public ImmutableSeq>> classes; public FnClauseBody(ImmutableSeq> clauses) { this.clauses = clauses; } + public @NotNull SeqView matchingsView() { + return clauses.view().map(WithPos::data); + } }