From 884a2cb29378abba2ef4290205a8ffc6f3623c92 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sun, 9 Jun 2024 02:45:45 -0400 Subject: [PATCH 1/2] pat: `allBinds` --- .../org/aya/resolve/context/ModuleSymbol.java | 24 +++++++------------ .../java/org/aya/tyck/pat/ClauseTycker.java | 24 ++++++++++++------- .../test/java/org/aya/test/TestRunner.java | 3 ++- .../org/aya/test/fixtures/ParseError.java | 8 ++----- .../test/resources/negative/ParseError.txt | 2 +- .../java/org/aya/syntax/core/pat/Pat.java | 8 +++---- .../java/org/aya/syntax/core/term/Term.java | 4 ++-- 7 files changed, 35 insertions(+), 38 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/context/ModuleSymbol.java b/base/src/main/java/org/aya/resolve/context/ModuleSymbol.java index d805189b7f..38f879ba4d 100644 --- a/base/src/main/java/org/aya/resolve/context/ModuleSymbol.java +++ b/base/src/main/java/org/aya/resolve/context/ModuleSymbol.java @@ -23,12 +23,8 @@ * It says a `Symbol` can be referred by `{Component}::{Unqualified}` * @apiNote the methods that end with `Definitely` will get/remove only one symbol or fail if ambiguous. */ -public record ModuleSymbol( - @NotNull MutableMap> table -) { - public ModuleSymbol() { - this(MutableMap.create()); - } +public record ModuleSymbol(@NotNull MutableMap> table) { + public ModuleSymbol() { this(MutableMap.create()); } public ModuleSymbol(@NotNull ModuleSymbol other) { this(other.table.toImmutableSeq().collect(MutableMap.collector( @@ -38,8 +34,10 @@ public ModuleSymbol(@NotNull ModuleSymbol other) { } /** @apiNote should not use this after {@link #asMut} is called. */ - public record UnqualifiedResolve(@NotNull MapView map, - @NotNull LazyValue> asMut) { + public record UnqualifiedResolve( + @NotNull MapView map, + @NotNull LazyValue> asMut + ) { public @NotNull ImmutableSeq uniqueCandidates() { return map.valuesView().distinct().toImmutableSeq(); } @@ -95,8 +93,8 @@ public record UnqualifiedResolve(@NotNull MapView map, */ public @NotNull Result getMaybe(@NotNull ModuleName component, @NotNull String unqualifiedName) { return switch (component) { - case ModuleName.Qualified qualified -> getQualifiedMaybe(component, unqualifiedName).toResult(Error.NotFound); - case ModuleName.ThisRef aThis -> getUnqualifiedMaybe(unqualifiedName); + case ModuleName.Qualified qualified -> getQualifiedMaybe(qualified, unqualifiedName).toResult(Error.NotFound); + case ModuleName.ThisRef _ -> getUnqualifiedMaybe(unqualifiedName); }; } @@ -118,11 +116,7 @@ public enum Error { * * @implNote This method always overwrites the symbol that is added in the past. */ - public Option add( - @NotNull ModuleName componentName, - @NotNull String name, - @NotNull T ref - ) { + public Option add(@NotNull ModuleName componentName, @NotNull String name, @NotNull T ref) { var candidates = resolveUnqualified(name).asMut.get(); return candidates.put(componentName, ref); } diff --git a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java b/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java index 10e82acf9b..25d8609128 100644 --- a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java +++ b/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java @@ -114,10 +114,11 @@ public record Worker( exprTycker.solveMetas(); // inline terms in rhsResult - rhsResult = rhsResult.map(x -> new Pat.Preclause<>( - x.sourcePos(), - x.pats().map(p -> p.descent(UnaryOperator.identity(), exprTycker::zonk)), - x.expr() == null ? null : x.expr().descent((_, t) -> exprTycker.zonk(t)) + rhsResult = rhsResult.map(preclause -> new Pat.Preclause<>( + preclause.sourcePos(), + preclause.pats().map(p -> p.descent(UnaryOperator.identity(), exprTycker::zonk)), + preclause.bindCount(), + preclause.expr() == null ? null : preclause.expr().descent((_, t) -> exprTycker.zonk(t)) )); return new TyckResult( @@ -170,8 +171,10 @@ public record Worker( ctx = ctx.map(TermInline::apply); var patWithTypeBound = Pat.collectVariables(patResult.wellTyped().view()); - var newClause = new Pat.Preclause<>(clause.sourcePos, patWithTypeBound.component2(), patResult.newBody()); - return new LhsResult(ctx, resultTerm, patWithTypeBound.component1().toImmutableSeq(), + var allBinds = patWithTypeBound.component1().toImmutableSeq(); + var newClause = new Pat.Preclause<>(clause.sourcePos, patWithTypeBound.component2(), + allBinds.size(), patResult.newBody()); + return new LhsResult(ctx, resultTerm, allBinds, patResult.wellTyped(), patResult.paramSubst(), patResult.asSubst(), newClause, patResult.hasError()); }); } @@ -189,6 +192,7 @@ public record Worker( var clause = result.clause; var bodyExpr = clause.expr(); Term wellBody; + var bindCount = 0; if (bodyExpr == null) wellBody = null; else if (result.hasError) { // In case the patterns are malformed, do not check the body @@ -204,11 +208,13 @@ else if (result.hasError) { wellBody = exprTycker.inherit(bodyExpr, result.type).wellTyped(); // bind all pat bindings - var patBindTele = Pat.collectVariables(result.clause.pats().view()).component1().view(); - wellBody = wellBody.bindTele(patBindTele); + var patBindTele = Pat.collectVariables(result.clause.pats().view()).component1(); + bindCount = patBindTele.size(); + wellBody = wellBody.bindTele(patBindTele.view()); } - return new Pat.Preclause<>(clause.sourcePos(), clause.pats(), wellBody == null ? null : WithPos.dummy(wellBody)); + return new Pat.Preclause<>(clause.sourcePos(), clause.pats(), bindCount, + wellBody == null ? null : WithPos.dummy(wellBody)); }); } diff --git a/cli-impl/src/test/java/org/aya/test/TestRunner.java b/cli-impl/src/test/java/org/aya/test/TestRunner.java index 7ea609c8d5..7c2cbb9f96 100644 --- a/cli-impl/src/test/java/org/aya/test/TestRunner.java +++ b/cli-impl/src/test/java/org/aya/test/TestRunner.java @@ -140,6 +140,7 @@ private static void runSingleCase(String code, SingleFileCompiler compiler) thro public static @NotNull CompilerFlags flags() { var modulePaths = ImmutableSeq.of(DEFAULT_TEST_DIR.resolve("shared/src")); - return new CompilerFlags(CompilerFlags.Message.ASCII, false, false, null, modulePaths, null); + return new CompilerFlags(CompilerFlags.Message.ASCII, + false, false, null, modulePaths, null); } } diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/ParseError.java b/cli-impl/src/test/java/org/aya/test/fixtures/ParseError.java index 14d1c1892c..991587da6c 100644 --- a/cli-impl/src/test/java/org/aya/test/fixtures/ParseError.java +++ b/cli-impl/src/test/java/org/aya/test/fixtures/ParseError.java @@ -6,12 +6,8 @@ @SuppressWarnings("unused") public interface ParseError { - String testTrivial = """ - def - """; - @Language("Aya") String testModifier = """ - overlap inductive Empty - """; + String testTrivial = "def"; + @Language("Aya") String testModifier = "overlap inductive E"; @Language("Aya") String testIgnoredModifier = """ inline def id {A : Type} A : A | a => a diff --git a/cli-impl/src/test/resources/negative/ParseError.txt b/cli-impl/src/test/resources/negative/ParseError.txt index 8a86324422..b3db6d9cb4 100644 --- a/cli-impl/src/test/resources/negative/ParseError.txt +++ b/cli-impl/src/test/resources/negative/ParseError.txt @@ -12,7 +12,7 @@ What are you doing? Modifier: In file $FILE:1:0 -> - 1 │ overlap inductive Empty + 1 │ overlap inductive E │ ╰─────╯ Error: The modifier overlap is not suitable here. diff --git a/syntax/src/main/java/org/aya/syntax/core/pat/Pat.java b/syntax/src/main/java/org/aya/syntax/core/pat/Pat.java index e20440de65..b28f4d2cc6 100644 --- a/syntax/src/main/java/org/aya/syntax/core/pat/Pat.java +++ b/syntax/src/main/java/org/aya/syntax/core/pat/Pat.java @@ -49,7 +49,6 @@ public sealed interface Pat extends AyaDocile { */ void consumeBindings(@NotNull BiConsumer consumer); - /** * Bind the types in {@link Pat}s * @@ -263,7 +262,7 @@ public ShapedInt update(DataCall type) { record Preclause( @NotNull SourcePos sourcePos, @NotNull ImmutableSeq pats, - @Nullable WithPos expr + int bindCount, @Nullable WithPos expr ) implements AyaDocile { @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) { var prettier = new CorePrettier(options); @@ -273,13 +272,14 @@ record Preclause( } public static @NotNull Preclause weaken(@NotNull Term.Matching clause) { - return new Preclause<>(clause.sourcePos(), clause.patterns(), WithPos.dummy(clause.body())); + return new Preclause<>(clause.sourcePos(), clause.patterns(), clause.bindCount(), + WithPos.dummy(clause.body())); } public static @NotNull Option lift(@NotNull Preclause clause) { if (clause.expr == null) return Option.none(); - var match = new Term.Matching(clause.sourcePos, clause.pats, clause.expr.data()); + var match = new Term.Matching(clause.sourcePos, clause.pats, clause.bindCount, clause.expr.data()); return Option.some(match); } } diff --git a/syntax/src/main/java/org/aya/syntax/core/term/Term.java b/syntax/src/main/java/org/aya/syntax/core/term/Term.java index 999bbf9118..0b703235e9 100644 --- a/syntax/src/main/java/org/aya/syntax/core/term/Term.java +++ b/syntax/src/main/java/org/aya/syntax/core/term/Term.java @@ -181,7 +181,7 @@ public sealed interface Term extends Serializable, AyaDocile record Matching( @NotNull SourcePos sourcePos, @NotNull ImmutableSeq patterns, - @NotNull Term body + int bindCount, @NotNull Term body ) implements AyaDocile { @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) { return Pat.Preclause.weaken(this).toDoc(options); @@ -189,7 +189,7 @@ record Matching( public @NotNull Matching update(@NotNull ImmutableSeq patterns, @NotNull Term body) { return body == body() && patterns.sameElements(patterns(), true) ? this - : new Matching(sourcePos, patterns, body); + : new Matching(sourcePos, patterns, bindCount, body); } public @NotNull Matching descent(@NotNull UnaryOperator f, @NotNull UnaryOperator g) { From a35c905ba63892be4dfb771b9552759d189d841c Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sun, 9 Jun 2024 02:51:24 -0400 Subject: [PATCH 2/2] jit: `allBinds` --- .../java/org/aya/compiler/FnSerializer.java | 2 +- .../org/aya/compiler/PatternExprializer.java | 7 +--- .../org/aya/compiler/PatternSerializer.java | 32 ++++++------------- 3 files changed, 11 insertions(+), 30 deletions(-) diff --git a/jit-compiler/src/main/java/org/aya/compiler/FnSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/FnSerializer.java index 389d557a3a..03792377f6 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/FnSerializer.java +++ b/jit-compiler/src/main/java/org/aya/compiler/FnSerializer.java @@ -57,7 +57,7 @@ private void buildInvoke(FnDef unit, @NotNull String onStuckTerm, @NotNull Immut case Either.Right(var clauses) -> { var ser = new PatternSerializer(this.sourceBuilder, argTerms, onStuckCon, onStuckCon); ser.serialize(clauses.map(matching -> new PatternSerializer.Matching( - matching.patterns(), (s, bindSize) -> + matching.bindCount(), matching.patterns(), (s, bindSize) -> s.buildReturn(serializeTermUnderTele(matching.body(), PatternSerializer.VARIABLE_RESULT, bindSize)) ))); } diff --git a/jit-compiler/src/main/java/org/aya/compiler/PatternExprializer.java b/jit-compiler/src/main/java/org/aya/compiler/PatternExprializer.java index 66b6b79f00..46e4421e27 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/PatternExprializer.java +++ b/jit-compiler/src/main/java/org/aya/compiler/PatternExprializer.java @@ -4,7 +4,6 @@ import kala.collection.immutable.ImmutableSeq; import org.aya.syntax.core.pat.Pat; -import org.aya.syntax.core.term.ErrorTerm; import org.aya.syntax.core.term.Term; import org.aya.syntax.core.term.call.ConCallLike; import org.aya.syntax.ref.LocalVar; @@ -21,7 +20,6 @@ public class PatternExprializer extends AbstractExprializer { public static final @NotNull String CLASS_PAT_INT = ExprializeUtils.makeSub(CLASS_PAT, ExprializeUtils.getJavaReference(Pat.ShapedInt.class)); public static final @NotNull String CLASS_LOCALVAR = ExprializeUtils.getJavaReference(LocalVar.class); public static final @NotNull String CLASS_CONHEAD = ExprializeUtils.makeSub(ExprializeUtils.getJavaReference(ConCallLike.class), ExprializeUtils.getJavaReference(ConCallLike.Head.class)); - public static final @NotNull String CLASS_ERROR = ExprializeUtils.getJavaReference(ErrorTerm.class); public static final @NotNull String CLASS_PAT_TUPLE = ExprializeUtils.makeSub(CLASS_PAT, ExprializeUtils.getJavaReference(Pat.Tuple.class)); private final boolean allowLocalTerm; @@ -67,8 +65,5 @@ protected PatternExprializer(@NotNull NameGenerator nameGen, boolean allowLocalT }; } - @Override - public @NotNull String serialize(Pat unit) { - return doSerialize(unit); - } + @Override public @NotNull String serialize(Pat unit) { return doSerialize(unit); } } diff --git a/jit-compiler/src/main/java/org/aya/compiler/PatternSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/PatternSerializer.java index 303dc067ee..d623721ef0 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/PatternSerializer.java +++ b/jit-compiler/src/main/java/org/aya/compiler/PatternSerializer.java @@ -6,7 +6,6 @@ import kala.collection.immutable.ImmutableSeq; import kala.collection.immutable.primitive.ImmutableIntSeq; import kala.range.primitive.IntRange; -import kala.value.primitive.MutableIntValue; import org.aya.generic.AyaDocile; import org.aya.generic.State; import org.aya.syntax.core.pat.Pat; @@ -27,28 +26,23 @@ public interface SuccessContinuation extends BiConsumer patterns, @NotNull SuccessContinuation onSucc) { - } + public record Matching( + int bindCount, @NotNull ImmutableSeq patterns, + @NotNull SuccessContinuation onSucc + ) { } public static final @NotNull String VARIABLE_RESULT = "result"; public static final @NotNull String VARIABLE_STATE = "matchState"; @@ -135,9 +129,7 @@ private void multiStage( buildLocalVar(CLASS_TERM, tmpName, term); for (var pre : preContinuation) { - buildIf(STR."! \{VARIABLE_SUBSTATE}", () -> { - pre.accept(tmpName); - }); + buildIf(STR."! \{VARIABLE_SUBSTATE}", () -> pre.accept(tmpName)); } buildIf(VARIABLE_SUBSTATE, continuation); @@ -190,12 +182,6 @@ private void onMatchBind(@NotNull String term) { appendLine(STR."\{VARIABLE_RESULT}.set(\{bindCount++}, \{term});"); } - private int bindAmount(@NotNull ImmutableSeq pats) { - var acc = MutableIntValue.create(); - pats.forEach(pat -> pat.consumeBindings((_, _) -> acc.increment())); - return acc.get(); - } - /// endregion Java Source Code Generate API @Override public PatternSerializer serialize(@NotNull ImmutableSeq unit) { @@ -203,7 +189,7 @@ private int bindAmount(@NotNull ImmutableSeq pats) { onMismatch.accept(this); return this; } - var bindSize = unit.mapToInt(ImmutableIntSeq.factory(), x -> bindAmount(x.patterns)); + var bindSize = unit.mapToInt(ImmutableIntSeq.factory(), Matching::bindCount); int maxBindSize = bindSize.max(); buildLocalVar(STR."\{CLASS_MUTSEQ}<\{CLASS_TERM}>", VARIABLE_RESULT, STR."\{CLASS_MUTSEQ}.fill(\{maxBindSize}, (\{CLASS_TERM}) null)");