From d31e8b3259c02e369ce4289df41074df1c0ad25c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=E6=BE=AA?= Date: Thu, 30 Jan 2025 14:51:30 -0500 Subject: [PATCH 01/14] generalize: port some code from #1226 Co-authored-by: ice1000 --- .../resolve/error/CyclicDependencyError.java | 27 ++++++ .../visitor/VariableDependencyCollector.java | 90 +++++++++++++++++++ .../org/aya/syntax/ref/GeneralizedVar.java | 5 +- 3 files changed, 121 insertions(+), 1 deletion(-) create mode 100644 base/src/main/java/org/aya/resolve/error/CyclicDependencyError.java create mode 100644 base/src/main/java/org/aya/resolve/visitor/VariableDependencyCollector.java diff --git a/base/src/main/java/org/aya/resolve/error/CyclicDependencyError.java b/base/src/main/java/org/aya/resolve/error/CyclicDependencyError.java new file mode 100644 index 0000000000..b0ce0efc4a --- /dev/null +++ b/base/src/main/java/org/aya/resolve/error/CyclicDependencyError.java @@ -0,0 +1,27 @@ +// 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.resolve.error; + +import org.aya.prettier.BasePrettier; +import org.aya.pretty.doc.Doc; +import org.aya.util.prettier.PrettierOptions; +import org.aya.util.reporter.Problem; +import org.aya.syntax.ref.GeneralizedVar; +import org.aya.util.error.SourcePos; +import org.jetbrains.annotations.NotNull; +import kala.collection.immutable.ImmutableSeq; + +public record CyclicDependencyError( + @NotNull SourcePos sourcePos, + @NotNull GeneralizedVar var, + @NotNull ImmutableSeq cyclePath +) implements Problem { + @Override public @NotNull Severity level() { return Severity.ERROR; } + @Override public @NotNull Stage stage() { return Stage.RESOLVE; } + @Override public @NotNull Doc describe(@NotNull PrettierOptions options) { + return Doc.vcat( + Doc.english("Cyclic dependency detected in variable declarations:"), + Doc.join(Doc.spaced(Doc.symbol("->")), cyclePath.map(BasePrettier::varDoc)) + ); + } +} diff --git a/base/src/main/java/org/aya/resolve/visitor/VariableDependencyCollector.java b/base/src/main/java/org/aya/resolve/visitor/VariableDependencyCollector.java new file mode 100644 index 0000000000..ec755a9ce7 --- /dev/null +++ b/base/src/main/java/org/aya/resolve/visitor/VariableDependencyCollector.java @@ -0,0 +1,90 @@ +// 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.resolve.visitor; + +import kala.collection.immutable.ImmutableSeq; +import kala.collection.mutable.MutableList; +import kala.collection.mutable.MutableSet; +import org.aya.syntax.ref.GenerateKind; +import org.aya.syntax.ref.LocalVar; +import org.aya.util.error.PosedUnaryOperator; +import org.aya.resolve.context.Context; +import org.aya.resolve.error.CyclicDependencyError; +import org.aya.syntax.concrete.Expr; +import org.aya.syntax.ref.GeneralizedVar; +import org.aya.util.error.SourcePos; +import org.aya.util.reporter.Reporter; +import org.jetbrains.annotations.NotNull; + +import java.util.HashMap; +import java.util.Map; + +/// Collects dependency information for generalized variables using DFS on their types. +/// +/// 1. A variable's type may reference other generalized variables; we record those as dependencies. +/// 2. If we revisit a variable already on the DFS stack ("visiting" set), that indicates +/// a cyclic dependency, and we report an error. +/// 3. Once a variable is fully processed, it goes into the "visited" set; future registrations +/// of the same variable skip repeated traversal. +/// +/// Pitfalls & Notes: +/// - A single variable (e.g. “A”) should be registered once, to avoid duplication. +/// - Attempting to re-scan or re-introduce “A” in another variable’s context can cause +/// confusion or potential cycles. So we do all dependency scans here, at declaration time. +/// - Any reference to a variable out of scope is handled as an error in the resolver +/// if it’s not in the allowedGeneralizes map. +public final class VariableDependencyCollector { + private final @NotNull Reporter reporter; + private final @NotNull MutableSet visiting = MutableSet.create(); + private final @NotNull MutableSet visited = MutableSet.create(); + private final @NotNull MutableList currentPath = MutableList.create(); + + public VariableDependencyCollector(@NotNull Reporter reporter) { + this.reporter = reporter; + } + + public void registerVariable(GeneralizedVar var) { + if (visited.contains(var)) return; + + // If var is already being visited in current DFS path, we found a cycle + if (!visiting.add(var)) { + // Find cycle start index + var cycleStart = currentPath.indexOf(var); + var cyclePath = currentPath.view().drop(cycleStart).appended(var); + reporter.report(new CyclicDependencyError(var.sourcePos(), var, cyclePath.toImmutableSeq())); + throw new Context.ResolvingInterruptedException(); + } + + currentPath.append(var); + var.dependencies = collectReferences(var); + + // Recursively register dependencies + for (var dep : var.dependencies) { + registerVariable(dep); + } + + currentPath.removeLast(); + visiting.remove(var); + visited.add(var); + } + + private @NotNull ImmutableSeq collectReferences(GeneralizedVar var) { + var type = var.owner.type; + var collector = new StaticGeneralizedVarCollector(); + type.descent(collector); + return collector.collected.toImmutableSeq(); + } + + private static class StaticGeneralizedVarCollector implements PosedUnaryOperator { + public final MutableList collected = MutableList.create(); + @Override public @NotNull Expr apply(@NotNull SourcePos pos, @NotNull Expr expr) { + if (expr instanceof Expr.Ref ref) { + var var = ref.var(); + if (var instanceof LocalVar local && local.generateKind() instanceof GenerateKind.Generalized(var origin)) { + collected.append(origin); + } + } + return expr.descent(this); + } + } +} diff --git a/syntax/src/main/java/org/aya/syntax/ref/GeneralizedVar.java b/syntax/src/main/java/org/aya/syntax/ref/GeneralizedVar.java index 9492a22b9d..b685a7455a 100644 --- a/syntax/src/main/java/org/aya/syntax/ref/GeneralizedVar.java +++ b/syntax/src/main/java/org/aya/syntax/ref/GeneralizedVar.java @@ -1,7 +1,8 @@ -// 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.ref; +import kala.collection.immutable.ImmutableSeq; import org.aya.syntax.concrete.stmt.Generalize; import org.aya.util.error.SourceNode; import org.aya.util.error.SourcePos; @@ -11,6 +12,8 @@ public final class GeneralizedVar implements AnyVar, SourceNode { public final @NotNull String name; public final @NotNull SourcePos sourcePos; public Generalize owner; + /// Late-initialized + public ImmutableSeq dependencies; public GeneralizedVar(@NotNull String name, @NotNull SourcePos sourcePos) { this.name = name; From 2e5342697b33521895dbe38aceea4ad8b9559a67 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 30 Jan 2025 15:02:30 -0500 Subject: [PATCH 02/14] generalize: store dependencies --- ...ndencyCollector.java => OverGeneralizer.java} | 16 ++++++---------- .../org/aya/resolve/visitor/StmtResolver.java | 5 +++-- .../org/aya/syntax/concrete/stmt/Generalize.java | 4 +++- .../java/org/aya/syntax/ref/GeneralizedVar.java | 2 -- 4 files changed, 12 insertions(+), 15 deletions(-) rename base/src/main/java/org/aya/resolve/visitor/{VariableDependencyCollector.java => OverGeneralizer.java} (90%) diff --git a/base/src/main/java/org/aya/resolve/visitor/VariableDependencyCollector.java b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java similarity index 90% rename from base/src/main/java/org/aya/resolve/visitor/VariableDependencyCollector.java rename to base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java index ec755a9ce7..d23a177f7a 100644 --- a/base/src/main/java/org/aya/resolve/visitor/VariableDependencyCollector.java +++ b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java @@ -16,9 +16,6 @@ import org.aya.util.reporter.Reporter; import org.jetbrains.annotations.NotNull; -import java.util.HashMap; -import java.util.Map; - /// Collects dependency information for generalized variables using DFS on their types. /// /// 1. A variable's type may reference other generalized variables; we record those as dependencies. @@ -33,17 +30,17 @@ /// confusion or potential cycles. So we do all dependency scans here, at declaration time. /// - Any reference to a variable out of scope is handled as an error in the resolver /// if it’s not in the allowedGeneralizes map. -public final class VariableDependencyCollector { +public final class OverGeneralizer { private final @NotNull Reporter reporter; private final @NotNull MutableSet visiting = MutableSet.create(); private final @NotNull MutableSet visited = MutableSet.create(); private final @NotNull MutableList currentPath = MutableList.create(); - public VariableDependencyCollector(@NotNull Reporter reporter) { + public OverGeneralizer(@NotNull Reporter reporter) { this.reporter = reporter; } - public void registerVariable(GeneralizedVar var) { + public void register(GeneralizedVar var) { if (visited.contains(var)) return; // If var is already being visited in current DFS path, we found a cycle @@ -56,12 +53,11 @@ public void registerVariable(GeneralizedVar var) { } currentPath.append(var); - var.dependencies = collectReferences(var); + var deps = collectReferences(var); + var.owner.dependencies = deps; // Recursively register dependencies - for (var dep : var.dependencies) { - registerVariable(dep); - } + for (var dep : deps) register(dep); currentPath.removeLast(); visiting.remove(var); diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java index 4c58dea905..74bc55bfbd 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java @@ -1,4 +1,4 @@ -// 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.resolve.visitor; @@ -37,9 +37,10 @@ static void resolveStmt(@NotNull ResolvingStmt stmt, @NotNull ResolveInfo info) case ResolvingStmt.ResolvingDecl decl -> resolveDecl(decl, info); case ResolvingStmt.ModStmt(var stmts) -> resolveStmt(stmts, info); case ResolvingStmt.GenStmt(var variables) -> { - var resolver = new ExprResolver(info.thisModule(), false); + var resolver = new ExprResolver(info.thisModule(), true); resolver.enter(Where.Head); variables.descentInPlace(resolver, (_, p) -> p); + variables.dependencies = resolver.allowedGeneralizes().keysView().toImmutableSeq(); addReferences(info, new TyckOrder.Head(variables), resolver); } } diff --git a/syntax/src/main/java/org/aya/syntax/concrete/stmt/Generalize.java b/syntax/src/main/java/org/aya/syntax/concrete/stmt/Generalize.java index b89cecb28d..c57c8811c5 100644 --- a/syntax/src/main/java/org/aya/syntax/concrete/stmt/Generalize.java +++ b/syntax/src/main/java/org/aya/syntax/concrete/stmt/Generalize.java @@ -1,4 +1,4 @@ -// 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.concrete.stmt; @@ -23,6 +23,8 @@ public final class Generalize implements Stmt { public final @NotNull SourcePos sourcePos; public final @NotNull ImmutableSeq variables; public @NotNull WithPos type; + /// Late-initialized + public ImmutableSeq dependencies; public Generalize( @NotNull SourcePos sourcePos, @NotNull ImmutableSeq variables, diff --git a/syntax/src/main/java/org/aya/syntax/ref/GeneralizedVar.java b/syntax/src/main/java/org/aya/syntax/ref/GeneralizedVar.java index b685a7455a..e5d29d262c 100644 --- a/syntax/src/main/java/org/aya/syntax/ref/GeneralizedVar.java +++ b/syntax/src/main/java/org/aya/syntax/ref/GeneralizedVar.java @@ -12,8 +12,6 @@ public final class GeneralizedVar implements AnyVar, SourceNode { public final @NotNull String name; public final @NotNull SourcePos sourcePos; public Generalize owner; - /// Late-initialized - public ImmutableSeq dependencies; public GeneralizedVar(@NotNull String name, @NotNull SourcePos sourcePos) { this.name = name; From bc75d24b859d1bda236b62f593739b0c7f31d0bf Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 30 Jan 2025 15:23:16 -0500 Subject: [PATCH 03/14] generalize: implement recursive generalize, fix loads of bugs --- .../org/aya/resolve/visitor/ExprResolver.java | 23 +++------ .../aya/resolve/visitor/OverGeneralizer.java | 47 ++++++++++++++----- .../org/aya/resolve/visitor/StmtResolver.java | 4 +- .../org/aya/syntax/ref/GeneralizedVar.java | 6 +++ 4 files changed, 49 insertions(+), 31 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java index d304a16ad3..78a92f967e 100644 --- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java @@ -3,9 +3,7 @@ package org.aya.resolve.visitor; import kala.collection.immutable.ImmutableSeq; -import kala.collection.mutable.MutableLinkedHashMap; import kala.collection.mutable.MutableList; -import kala.collection.mutable.MutableMap; import kala.collection.mutable.MutableStack; import kala.value.MutableValue; import org.aya.generic.stmt.TyckOrder; @@ -44,7 +42,7 @@ public record ExprResolver( @NotNull Context ctx, boolean allowGeneralizing, - @NotNull MutableMap allowedGeneralizes, + @NotNull OverGeneralizer allowedGeneralizes, @NotNull MutableList reference, @NotNull MutableStack where ) implements PosedUnaryOperator { @@ -65,12 +63,12 @@ public static LiterateResolved resolveLax(@NotNull ModuleContext context, @NotNu var resolver = new ExprResolver(context, true); resolver.enter(Where.FnBody); var inner = expr.descent(resolver); - var view = resolver.allowedGeneralizes().valuesView().toImmutableSeq(); + var view = resolver.allowedGeneralizes().allowedGeneralizeParams().toImmutableSeq(); return new LiterateResolved(view, inner); } public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) { - this(ctx, allowGeneralizing, MutableLinkedHashMap.of(), MutableList.create(), MutableStack.create()); + this(ctx, allowGeneralizing, new OverGeneralizer(ctx), MutableList.create(), MutableStack.create()); } public void resetRefs() { reference.clear(); } @@ -136,13 +134,7 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) { case GeneralizedVar generalized -> { // a "resolved" GeneralizedVar is not in [allowedGeneralizes] if (allowGeneralizing) { - // Ordered set semantics. Do not expect too many generalized vars. - var owner = generalized.owner; - assert owner != null : "Sanity check"; - var param = owner.toExpr(false, generalized.toLocal()); - allowedGeneralizes.put(generalized, param); - addReference(owner); - yield param.ref(); + yield allowedGeneralizes.register(generalized, this::addReference); } else { yield ctx.reportAndThrow(new GeneralizedNotAvailableError(pos, generalized)); } @@ -216,9 +208,8 @@ private void addReference(@NotNull TyckUnit unit) { } } - private void addReference(@NotNull DefVar defVar) { - addReference(defVar.concrete); - } + private void addReference(@NotNull GeneralizedVar defVar) { addReference(defVar.owner); } + private void addReference(@NotNull DefVar defVar) { addReference(defVar.concrete); } public @NotNull Pattern.Clause clause(@NotNull ImmutableSeq telescope, @NotNull Pattern.Clause clause) { var mCtx = MutableValue.create(ctx); @@ -261,7 +252,7 @@ private void addReference(@NotNull DefVar defVar) { public @NotNull AnyVar resolve(@NotNull QualifiedID name) { var result = ctx.get(name); if (result instanceof GeneralizedVar gvar) { - var gened = allowedGeneralizes.getOrNull(gvar); + var gened = allowedGeneralizes.getParam(gvar); if (gened != null) return gened.ref(); } diff --git a/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java index d23a177f7a..85f786c631 100644 --- a/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java +++ b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java @@ -2,19 +2,24 @@ // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.resolve.visitor; +import java.util.function.Consumer; + +import kala.collection.CollectionView; import kala.collection.immutable.ImmutableSeq; +import kala.collection.mutable.MutableLinkedHashMap; import kala.collection.mutable.MutableList; +import kala.collection.mutable.MutableMap; import kala.collection.mutable.MutableSet; -import org.aya.syntax.ref.GenerateKind; -import org.aya.syntax.ref.LocalVar; -import org.aya.util.error.PosedUnaryOperator; import org.aya.resolve.context.Context; import org.aya.resolve.error.CyclicDependencyError; import org.aya.syntax.concrete.Expr; import org.aya.syntax.ref.GeneralizedVar; +import org.aya.syntax.ref.GenerateKind; +import org.aya.syntax.ref.LocalVar; +import org.aya.util.error.PosedUnaryOperator; import org.aya.util.error.SourcePos; -import org.aya.util.reporter.Reporter; import org.jetbrains.annotations.NotNull; +import org.jetbrains.annotations.Nullable; /// Collects dependency information for generalized variables using DFS on their types. /// @@ -31,25 +36,25 @@ /// - Any reference to a variable out of scope is handled as an error in the resolver /// if it’s not in the allowedGeneralizes map. public final class OverGeneralizer { - private final @NotNull Reporter reporter; + private final @NotNull Context reporter; private final @NotNull MutableSet visiting = MutableSet.create(); - private final @NotNull MutableSet visited = MutableSet.create(); private final @NotNull MutableList currentPath = MutableList.create(); + private final @NotNull MutableMap allowedGeneralizes = MutableLinkedHashMap.of(); - public OverGeneralizer(@NotNull Reporter reporter) { + public OverGeneralizer(@NotNull Context reporter) { this.reporter = reporter; } - public void register(GeneralizedVar var) { - if (visited.contains(var)) return; + public @NotNull LocalVar register(GeneralizedVar var, @NotNull Consumer onGenVarVisited) { + if (allowedGeneralizes.containsKey(var)) return allowedGeneralizes.get(var).ref(); // If var is already being visited in current DFS path, we found a cycle if (!visiting.add(var)) { // Find cycle start index var cycleStart = currentPath.indexOf(var); var cyclePath = currentPath.view().drop(cycleStart).appended(var); - reporter.report(new CyclicDependencyError(var.sourcePos(), var, cyclePath.toImmutableSeq())); - throw new Context.ResolvingInterruptedException(); + visiting.clear(); + reporter.reportAndThrow(new CyclicDependencyError(var.sourcePos(), var, cyclePath.toImmutableSeq())); } currentPath.append(var); @@ -57,11 +62,26 @@ public void register(GeneralizedVar var) { var.owner.dependencies = deps; // Recursively register dependencies - for (var dep : deps) register(dep); + for (var dep : deps) register(dep, onGenVarVisited); currentPath.removeLast(); visiting.remove(var); - visited.add(var); + var param = var.toParam(false); + allowedGeneralizes.put(var, param); + onGenVarVisited.accept(var); + return param.ref(); + } + + public @NotNull CollectionView allowedGeneralizeParams() { + return allowedGeneralizes.valuesView(); + } + + public @NotNull CollectionView allowedGeneralizeVars() { + return allowedGeneralizes.keysView(); + } + + public @Nullable Expr.Param getParam(@NotNull GeneralizedVar var) { + return allowedGeneralizes.getOrNull(var); } private @NotNull ImmutableSeq collectReferences(GeneralizedVar var) { @@ -78,6 +98,7 @@ private static class StaticGeneralizedVarCollector implements PosedUnaryOperator var var = ref.var(); if (var instanceof LocalVar local && local.generateKind() instanceof GenerateKind.Generalized(var origin)) { collected.append(origin); + collected.appendAll(origin.owner.dependencies); } } return expr.descent(this); diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java index 74bc55bfbd..fb81550e0f 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java @@ -40,7 +40,7 @@ static void resolveStmt(@NotNull ResolvingStmt stmt, @NotNull ResolveInfo info) var resolver = new ExprResolver(info.thisModule(), true); resolver.enter(Where.Head); variables.descentInPlace(resolver, (_, p) -> p); - variables.dependencies = resolver.allowedGeneralizes().keysView().toImmutableSeq(); + variables.dependencies = resolver.allowedGeneralizes().allowedGeneralizeVars().toImmutableSeq(); addReferences(info, new TyckOrder.Head(variables), resolver); } } @@ -166,7 +166,7 @@ private static void addReferences(@NotNull ResolveInfo info, TyckOrder decl, Exp } private static void insertGeneralizedVars(@NotNull TeleDecl decl, @NotNull ExprResolver resolver) { - decl.telescope = decl.telescope.prependedAll(resolver.allowedGeneralizes().valuesView()); + decl.telescope = decl.telescope.prependedAll(resolver.allowedGeneralizes().allowedGeneralizeParams()); } private static void resolveElim(@NotNull ExprResolver resolver, @NotNull MatchBody body) { diff --git a/syntax/src/main/java/org/aya/syntax/ref/GeneralizedVar.java b/syntax/src/main/java/org/aya/syntax/ref/GeneralizedVar.java index e5d29d262c..9598d1d268 100644 --- a/syntax/src/main/java/org/aya/syntax/ref/GeneralizedVar.java +++ b/syntax/src/main/java/org/aya/syntax/ref/GeneralizedVar.java @@ -3,6 +3,7 @@ package org.aya.syntax.ref; import kala.collection.immutable.ImmutableSeq; +import org.aya.syntax.concrete.Expr; import org.aya.syntax.concrete.stmt.Generalize; import org.aya.util.error.SourceNode; import org.aya.util.error.SourcePos; @@ -22,6 +23,11 @@ public GeneralizedVar(@NotNull String name, @NotNull SourcePos sourcePos) { return new LocalVar(name, sourcePos, new GenerateKind.Generalized(this)); } + public @NotNull Expr.Param toParam(boolean explicit) { + assert owner != null : "Sanity check"; + return owner.toExpr(explicit, toLocal()); + } + public @NotNull String name() { return name; } @Override public @NotNull SourcePos sourcePos() { return sourcePos; } } From c5ad6cea7ee588dff239461095620509a6589b9d Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 30 Jan 2025 15:38:44 -0500 Subject: [PATCH 04/14] generalize: avoid adding repeated gvars to allowedGeneralizes --- .../java/org/aya/resolve/visitor/ExprResolver.java | 2 +- .../org/aya/resolve/visitor/OverGeneralizer.java | 13 ++++--------- .../java/org/aya/resolve/visitor/StmtResolver.java | 5 +++-- .../org/aya/syntax/concrete/stmt/Generalize.java | 3 ++- 4 files changed, 10 insertions(+), 13 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java index 78a92f967e..2b01f01734 100644 --- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java @@ -63,7 +63,7 @@ public static LiterateResolved resolveLax(@NotNull ModuleContext context, @NotNu var resolver = new ExprResolver(context, true); resolver.enter(Where.FnBody); var inner = expr.descent(resolver); - var view = resolver.allowedGeneralizes().allowedGeneralizeParams().toImmutableSeq(); + var view = resolver.allowedGeneralizes().allowedGeneralizes().valuesView().toImmutableSeq(); return new LiterateResolved(view, inner); } diff --git a/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java index 85f786c631..3cf4e8775c 100644 --- a/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java +++ b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java @@ -4,7 +4,8 @@ import java.util.function.Consumer; -import kala.collection.CollectionView; +import kala.collection.MapView; +import kala.collection.immutable.ImmutableMap; import kala.collection.immutable.ImmutableSeq; import kala.collection.mutable.MutableLinkedHashMap; import kala.collection.mutable.MutableList; @@ -59,7 +60,6 @@ public OverGeneralizer(@NotNull Context reporter) { currentPath.append(var); var deps = collectReferences(var); - var.owner.dependencies = deps; // Recursively register dependencies for (var dep : deps) register(dep, onGenVarVisited); @@ -72,12 +72,8 @@ public OverGeneralizer(@NotNull Context reporter) { return param.ref(); } - public @NotNull CollectionView allowedGeneralizeParams() { - return allowedGeneralizes.valuesView(); - } - - public @NotNull CollectionView allowedGeneralizeVars() { - return allowedGeneralizes.keysView(); + public @NotNull MapView allowedGeneralizes() { + return allowedGeneralizes.view(); } public @Nullable Expr.Param getParam(@NotNull GeneralizedVar var) { @@ -98,7 +94,6 @@ private static class StaticGeneralizedVarCollector implements PosedUnaryOperator var var = ref.var(); if (var instanceof LocalVar local && local.generateKind() instanceof GenerateKind.Generalized(var origin)) { collected.append(origin); - collected.appendAll(origin.owner.dependencies); } } return expr.descent(this); diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java index fb81550e0f..776d273a1d 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java @@ -3,6 +3,7 @@ package org.aya.resolve.visitor; import kala.collection.SeqView; +import kala.collection.immutable.ImmutableMap; import kala.collection.immutable.ImmutableSeq; import kala.value.MutableValue; import org.aya.generic.stmt.TyckOrder; @@ -40,7 +41,7 @@ static void resolveStmt(@NotNull ResolvingStmt stmt, @NotNull ResolveInfo info) var resolver = new ExprResolver(info.thisModule(), true); resolver.enter(Where.Head); variables.descentInPlace(resolver, (_, p) -> p); - variables.dependencies = resolver.allowedGeneralizes().allowedGeneralizeVars().toImmutableSeq(); + variables.dependencies = ImmutableMap.from(resolver.allowedGeneralizes().allowedGeneralizes()); addReferences(info, new TyckOrder.Head(variables), resolver); } } @@ -166,7 +167,7 @@ private static void addReferences(@NotNull ResolveInfo info, TyckOrder decl, Exp } private static void insertGeneralizedVars(@NotNull TeleDecl decl, @NotNull ExprResolver resolver) { - decl.telescope = decl.telescope.prependedAll(resolver.allowedGeneralizes().allowedGeneralizeParams()); + decl.telescope = decl.telescope.prependedAll(resolver.allowedGeneralizes().allowedGeneralizes().valuesView()); } private static void resolveElim(@NotNull ExprResolver resolver, @NotNull MatchBody body) { diff --git a/syntax/src/main/java/org/aya/syntax/concrete/stmt/Generalize.java b/syntax/src/main/java/org/aya/syntax/concrete/stmt/Generalize.java index c57c8811c5..2214e30ae2 100644 --- a/syntax/src/main/java/org/aya/syntax/concrete/stmt/Generalize.java +++ b/syntax/src/main/java/org/aya/syntax/concrete/stmt/Generalize.java @@ -2,6 +2,7 @@ // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.syntax.concrete.stmt; +import kala.collection.immutable.ImmutableMap; import kala.collection.immutable.ImmutableSeq; import org.aya.syntax.concrete.Expr; import org.aya.syntax.concrete.Pattern; @@ -24,7 +25,7 @@ public final class Generalize implements Stmt { public final @NotNull ImmutableSeq variables; public @NotNull WithPos type; /// Late-initialized - public ImmutableSeq dependencies; + public ImmutableMap dependencies; public Generalize( @NotNull SourcePos sourcePos, @NotNull ImmutableSeq variables, From 5bb9251402ad42bb9fa2f3873a42c9789230980a Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 30 Jan 2025 18:42:22 -0500 Subject: [PATCH 05/14] generalize: correctly implement MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: 澪 --- .../org/aya/resolve/visitor/ExprResolver.java | 45 +++++++++++++++---- .../aya/resolve/visitor/OverGeneralizer.java | 44 +++--------------- .../org/aya/resolve/visitor/StmtResolver.java | 4 +- 3 files changed, 43 insertions(+), 50 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java index 2b01f01734..d3829656be 100644 --- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java @@ -3,7 +3,9 @@ package org.aya.resolve.visitor; import kala.collection.immutable.ImmutableSeq; +import kala.collection.mutable.MutableLinkedHashMap; import kala.collection.mutable.MutableList; +import kala.collection.mutable.MutableMap; import kala.collection.mutable.MutableStack; import kala.value.MutableValue; import org.aya.generic.stmt.TyckOrder; @@ -17,10 +19,7 @@ import org.aya.syntax.concrete.stmt.QualifiedID; import org.aya.syntax.concrete.stmt.Stmt; import org.aya.syntax.concrete.stmt.decl.DataCon; -import org.aya.syntax.ref.AnyVar; -import org.aya.syntax.ref.DefVar; -import org.aya.syntax.ref.GeneralizedVar; -import org.aya.syntax.ref.LocalVar; +import org.aya.syntax.ref.*; import org.aya.tyck.error.ClassError; import org.aya.util.error.Panic; import org.aya.util.error.PosedUnaryOperator; @@ -42,7 +41,7 @@ public record ExprResolver( @NotNull Context ctx, boolean allowGeneralizing, - @NotNull OverGeneralizer allowedGeneralizes, + @NotNull MutableMap allowedGeneralizes, @NotNull MutableList reference, @NotNull MutableStack where ) implements PosedUnaryOperator { @@ -63,12 +62,12 @@ public static LiterateResolved resolveLax(@NotNull ModuleContext context, @NotNu var resolver = new ExprResolver(context, true); resolver.enter(Where.FnBody); var inner = expr.descent(resolver); - var view = resolver.allowedGeneralizes().allowedGeneralizes().valuesView().toImmutableSeq(); + var view = resolver.allowedGeneralizes().valuesView().toImmutableSeq(); return new LiterateResolved(view, inner); } public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) { - this(ctx, allowGeneralizing, new OverGeneralizer(ctx), MutableList.create(), MutableStack.create()); + this(ctx, allowGeneralizing, MutableLinkedHashMap.of(), MutableList.create(), MutableStack.create()); } public void resetRefs() { reference.clear(); } @@ -134,7 +133,9 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) { case GeneralizedVar generalized -> { // a "resolved" GeneralizedVar is not in [allowedGeneralizes] if (allowGeneralizing) { - yield allowedGeneralizes.register(generalized, this::addReference); + var param = generalized.toParam(false); + introduceDependencies(generalized, param); + yield param.ref(); } else { yield ctx.reportAndThrow(new GeneralizedNotAvailableError(pos, generalized)); } @@ -208,6 +209,19 @@ private void addReference(@NotNull TyckUnit unit) { } } + /// @param collected ordered set, implemented as a list + private record StaticGenVarCollector(MutableList collected) implements PosedUnaryOperator { + @Override public @NotNull Expr apply(@NotNull SourcePos pos, @NotNull Expr expr) { + if (expr instanceof Expr.Ref ref) { + var var = ref.var(); + if (var instanceof LocalVar local && local.generateKind() instanceof GenerateKind.Generalized(var origin)) { + if (!collected.contains(origin)) collected.append(origin); + } + } + return expr.descent(this); + } + } + private void addReference(@NotNull GeneralizedVar defVar) { addReference(defVar.owner); } private void addReference(@NotNull DefVar defVar) { addReference(defVar.concrete); } @@ -249,10 +263,23 @@ private void addReference(@NotNull TyckUnit unit) { }); } + private void introduceDependencies(@NotNull GeneralizedVar var, @NotNull Expr.Param param) { + if (allowedGeneralizes.containsKey(var)) return; + + // Introduce dependencies first + var.owner.dependencies.forEach(this::introduceDependencies); + + // Now introduce the variable itself + var owner = var.owner; + assert owner != null : "GeneralizedVar owner should not be null"; + allowedGeneralizes.put(var, param); + addReference(owner); + } + public @NotNull AnyVar resolve(@NotNull QualifiedID name) { var result = ctx.get(name); if (result instanceof GeneralizedVar gvar) { - var gened = allowedGeneralizes.getParam(gvar); + var gened = allowedGeneralizes.getOrNull(gvar); if (gened != null) return gened.ref(); } diff --git a/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java index 3cf4e8775c..133cf55249 100644 --- a/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java +++ b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java @@ -5,7 +5,6 @@ import java.util.function.Consumer; import kala.collection.MapView; -import kala.collection.immutable.ImmutableMap; import kala.collection.immutable.ImmutableSeq; import kala.collection.mutable.MutableLinkedHashMap; import kala.collection.mutable.MutableList; @@ -39,15 +38,15 @@ public final class OverGeneralizer { private final @NotNull Context reporter; private final @NotNull MutableSet visiting = MutableSet.create(); + private final @NotNull MutableSet visited = MutableSet.create(); private final @NotNull MutableList currentPath = MutableList.create(); - private final @NotNull MutableMap allowedGeneralizes = MutableLinkedHashMap.of(); public OverGeneralizer(@NotNull Context reporter) { this.reporter = reporter; } - public @NotNull LocalVar register(GeneralizedVar var, @NotNull Consumer onGenVarVisited) { - if (allowedGeneralizes.containsKey(var)) return allowedGeneralizes.get(var).ref(); + public void register(GeneralizedVar var) { + if (visited.contains(var)) return; // If var is already being visited in current DFS path, we found a cycle if (!visiting.add(var)) { @@ -59,44 +58,11 @@ public OverGeneralizer(@NotNull Context reporter) { } currentPath.append(var); - var deps = collectReferences(var); - // Recursively register dependencies - for (var dep : deps) register(dep, onGenVarVisited); + var.owner.dependencies.keysView().forEach(this::register); currentPath.removeLast(); visiting.remove(var); - var param = var.toParam(false); - allowedGeneralizes.put(var, param); - onGenVarVisited.accept(var); - return param.ref(); - } - - public @NotNull MapView allowedGeneralizes() { - return allowedGeneralizes.view(); - } - - public @Nullable Expr.Param getParam(@NotNull GeneralizedVar var) { - return allowedGeneralizes.getOrNull(var); - } - - private @NotNull ImmutableSeq collectReferences(GeneralizedVar var) { - var type = var.owner.type; - var collector = new StaticGeneralizedVarCollector(); - type.descent(collector); - return collector.collected.toImmutableSeq(); - } - - private static class StaticGeneralizedVarCollector implements PosedUnaryOperator { - public final MutableList collected = MutableList.create(); - @Override public @NotNull Expr apply(@NotNull SourcePos pos, @NotNull Expr expr) { - if (expr instanceof Expr.Ref ref) { - var var = ref.var(); - if (var instanceof LocalVar local && local.generateKind() instanceof GenerateKind.Generalized(var origin)) { - collected.append(origin); - } - } - return expr.descent(this); - } + visited.add(var); } } diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java index 776d273a1d..07bfa849f5 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java @@ -41,7 +41,7 @@ static void resolveStmt(@NotNull ResolvingStmt stmt, @NotNull ResolveInfo info) var resolver = new ExprResolver(info.thisModule(), true); resolver.enter(Where.Head); variables.descentInPlace(resolver, (_, p) -> p); - variables.dependencies = ImmutableMap.from(resolver.allowedGeneralizes().allowedGeneralizes()); + variables.dependencies = ImmutableMap.from(resolver.allowedGeneralizes().view()); addReferences(info, new TyckOrder.Head(variables), resolver); } } @@ -167,7 +167,7 @@ private static void addReferences(@NotNull ResolveInfo info, TyckOrder decl, Exp } private static void insertGeneralizedVars(@NotNull TeleDecl decl, @NotNull ExprResolver resolver) { - decl.telescope = decl.telescope.prependedAll(resolver.allowedGeneralizes().allowedGeneralizes().valuesView()); + decl.telescope = decl.telescope.prependedAll(resolver.allowedGeneralizes().valuesView()); } private static void resolveElim(@NotNull ExprResolver resolver, @NotNull MatchBody body) { From 02b24ca62a54384fa7e7942e55249579684c80b3 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 30 Jan 2025 18:52:27 -0500 Subject: [PATCH 06/14] generalize: cleanup --- .../java/org/aya/resolve/visitor/ExprResolver.java | 14 -------------- .../java/org/aya/resolve/visitor/StmtResolver.java | 3 ++- .../src/main/java/org/aya/util/error/WithPos.java | 4 +--- 3 files changed, 3 insertions(+), 18 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java index d3829656be..28eeea77f1 100644 --- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java @@ -209,20 +209,6 @@ private void addReference(@NotNull TyckUnit unit) { } } - /// @param collected ordered set, implemented as a list - private record StaticGenVarCollector(MutableList collected) implements PosedUnaryOperator { - @Override public @NotNull Expr apply(@NotNull SourcePos pos, @NotNull Expr expr) { - if (expr instanceof Expr.Ref ref) { - var var = ref.var(); - if (var instanceof LocalVar local && local.generateKind() instanceof GenerateKind.Generalized(var origin)) { - if (!collected.contains(origin)) collected.append(origin); - } - } - return expr.descent(this); - } - } - - private void addReference(@NotNull GeneralizedVar defVar) { addReference(defVar.owner); } private void addReference(@NotNull DefVar defVar) { addReference(defVar.concrete); } public @NotNull Pattern.Clause clause(@NotNull ImmutableSeq telescope, @NotNull Pattern.Clause clause) { diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java index 07bfa849f5..0570cfddfc 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java @@ -18,6 +18,7 @@ import org.aya.syntax.ref.LocalVar; import org.aya.tyck.error.TyckOrderError; import org.aya.util.error.Panic; +import org.aya.util.error.PosedUnaryOperator; import org.jetbrains.annotations.NotNull; /** @@ -40,7 +41,7 @@ static void resolveStmt(@NotNull ResolvingStmt stmt, @NotNull ResolveInfo info) case ResolvingStmt.GenStmt(var variables) -> { var resolver = new ExprResolver(info.thisModule(), true); resolver.enter(Where.Head); - variables.descentInPlace(resolver, (_, p) -> p); + variables.descentInPlace(resolver, PosedUnaryOperator.identity()); variables.dependencies = ImmutableMap.from(resolver.allowedGeneralizes().view()); addReferences(info, new TyckOrder.Head(variables), resolver); } diff --git a/tools/src/main/java/org/aya/util/error/WithPos.java b/tools/src/main/java/org/aya/util/error/WithPos.java index b4107851b7..c1498e2818 100644 --- a/tools/src/main/java/org/aya/util/error/WithPos.java +++ b/tools/src/main/java/org/aya/util/error/WithPos.java @@ -1,4 +1,4 @@ -// 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.util.error; @@ -8,8 +8,6 @@ import java.util.function.Function; public record WithPos(@NotNull SourcePos sourcePos, T data) implements SourceNode { - public static WithPos narrow(@NotNull WithPos value) { return value; } - public static @NotNull WithPos dummy(@NotNull T data) { return new WithPos<>(SourcePos.NONE, data); } From 4e22e3e99117df2099c23df937eadd654b247745 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 30 Jan 2025 19:13:38 -0500 Subject: [PATCH 07/14] generalize: integrate `OverGeneralizer` --- .../org/aya/resolve/visitor/ExprResolver.java | 23 +++++++------ .../aya/resolve/visitor/OverGeneralizer.java | 32 ++++++------------- .../org/aya/resolve/visitor/StmtResolver.java | 24 ++++++-------- 3 files changed, 31 insertions(+), 48 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java index 28eeea77f1..2bdf032067 100644 --- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java @@ -134,7 +134,8 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) { // a "resolved" GeneralizedVar is not in [allowedGeneralizes] if (allowGeneralizing) { var param = generalized.toParam(false); - introduceDependencies(generalized, param); + var generalizer = new OvergrownGeneralizer(); + generalizer.introduceDependencies(generalized, param); yield param.ref(); } else { yield ctx.reportAndThrow(new GeneralizedNotAvailableError(pos, generalized)); @@ -249,17 +250,15 @@ private void addReference(@NotNull TyckUnit unit) { }); } - private void introduceDependencies(@NotNull GeneralizedVar var, @NotNull Expr.Param param) { - if (allowedGeneralizes.containsKey(var)) return; - - // Introduce dependencies first - var.owner.dependencies.forEach(this::introduceDependencies); - - // Now introduce the variable itself - var owner = var.owner; - assert owner != null : "GeneralizedVar owner should not be null"; - allowedGeneralizes.put(var, param); - addReference(owner); + private class OvergrownGeneralizer extends OverGeneralizer { + public OvergrownGeneralizer() { super(ctx); } + @Override protected boolean contains(@NotNull GeneralizedVar var) { return allowedGeneralizes.containsKey(var); } + @Override protected void introduceDependency(@NotNull GeneralizedVar var, Expr.@NotNull Param param) { + var owner = var.owner; + assert owner != null : "GeneralizedVar owner should not be null"; + allowedGeneralizes.put(var, param); + addReference(owner); + } } public @NotNull AnyVar resolve(@NotNull QualifiedID name) { diff --git a/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java index 133cf55249..0cd9e57a99 100644 --- a/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java +++ b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java @@ -2,24 +2,13 @@ // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.resolve.visitor; -import java.util.function.Consumer; - -import kala.collection.MapView; -import kala.collection.immutable.ImmutableSeq; -import kala.collection.mutable.MutableLinkedHashMap; import kala.collection.mutable.MutableList; -import kala.collection.mutable.MutableMap; import kala.collection.mutable.MutableSet; import org.aya.resolve.context.Context; import org.aya.resolve.error.CyclicDependencyError; import org.aya.syntax.concrete.Expr; import org.aya.syntax.ref.GeneralizedVar; -import org.aya.syntax.ref.GenerateKind; -import org.aya.syntax.ref.LocalVar; -import org.aya.util.error.PosedUnaryOperator; -import org.aya.util.error.SourcePos; import org.jetbrains.annotations.NotNull; -import org.jetbrains.annotations.Nullable; /// Collects dependency information for generalized variables using DFS on their types. /// @@ -35,34 +24,33 @@ /// confusion or potential cycles. So we do all dependency scans here, at declaration time. /// - Any reference to a variable out of scope is handled as an error in the resolver /// if it’s not in the allowedGeneralizes map. -public final class OverGeneralizer { +public abstract class OverGeneralizer { private final @NotNull Context reporter; private final @NotNull MutableSet visiting = MutableSet.create(); - private final @NotNull MutableSet visited = MutableSet.create(); private final @NotNull MutableList currentPath = MutableList.create(); - public OverGeneralizer(@NotNull Context reporter) { - this.reporter = reporter; - } + public OverGeneralizer(@NotNull Context reporter) { this.reporter = reporter; } + protected abstract boolean contains(@NotNull GeneralizedVar var); + protected abstract void introduceDependency(@NotNull GeneralizedVar var, @NotNull Expr.Param param); - public void register(GeneralizedVar var) { - if (visited.contains(var)) return; + public final void introduceDependencies(@NotNull GeneralizedVar var, @NotNull Expr.Param param) { + if (contains(var)) return; // If var is already being visited in current DFS path, we found a cycle if (!visiting.add(var)) { // Find cycle start index var cycleStart = currentPath.indexOf(var); var cyclePath = currentPath.view().drop(cycleStart).appended(var); - visiting.clear(); reporter.reportAndThrow(new CyclicDependencyError(var.sourcePos(), var, cyclePath.toImmutableSeq())); } currentPath.append(var); - // Recursively register dependencies - var.owner.dependencies.keysView().forEach(this::register); + // Introduce dependencies first + var.owner.dependencies.forEach(this::introduceDependencies); + // Now introduce the variable itself + introduceDependency(var, param); currentPath.removeLast(); visiting.remove(var); - visited.add(var); } } diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java index 0570cfddfc..9f52c4e3f7 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java @@ -21,19 +21,17 @@ import org.aya.util.error.PosedUnaryOperator; import org.jetbrains.annotations.NotNull; -/** - * Resolves expressions inside stmts, after {@link StmtPreResolver} - * - * @author re-xyr, ice1000, kiva - * @see StmtPreResolver - * @see ExprResolver - */ +/// Resolves expressions inside stmts, after [StmtPreResolver] +/// +/// @author re-xyr, ice1000, kiva +/// @see StmtPreResolver +/// @see ExprResolver public interface StmtResolver { static void resolveStmt(@NotNull ImmutableSeq stmt, @NotNull ResolveInfo info) { stmt.forEach(s -> resolveStmt(s, info)); } - /** @apiNote Note that this function MUTATES the stmt if it's a Decl. */ + /// @apiNote Note that this function MUTATES the stmt if it's a Decl. static void resolveStmt(@NotNull ResolvingStmt stmt, @NotNull ResolveInfo info) { switch (stmt) { case ResolvingStmt.ResolvingDecl decl -> resolveDecl(decl, info); @@ -48,11 +46,9 @@ static void resolveStmt(@NotNull ResolvingStmt stmt, @NotNull ResolveInfo info) } } - /** - * Resolve {@param predecl}, where {@code predecl.ctx()} is the context of the body of {@param predecl} - * - * @apiNote Note that this function MUTATES the decl - */ + /// Resolve {@param predecl}, where `predecl.ctx()` is the context of the body of {@param predecl} + /// + /// @apiNote Note that this function MUTATES the decl private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @NotNull ResolveInfo info) { switch (predecl) { case ResolvingStmt.TopDecl(FnDecl decl, var ctx) -> { @@ -146,7 +142,7 @@ private static void addReferences(@NotNull ResolveInfo info, TyckOrder decl, Seq .filter(unit -> TyckUnit.needTyck(unit, info.modulePath()))); } - /** @param decl is unmodified */ + /// @param decl is unmodified private static void addReferences(@NotNull ResolveInfo info, TyckOrder decl, ExprResolver resolver) { addReferences(info, decl, resolver.reference().view()); } From b5170ce2a5b6980288db804dabd82aa272dd8786 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 30 Jan 2025 19:15:29 -0500 Subject: [PATCH 08/14] generalize: do not use a set --- .../main/java/org/aya/resolve/visitor/OverGeneralizer.java | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java index 0cd9e57a99..615a608f4c 100644 --- a/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java +++ b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java @@ -3,7 +3,6 @@ package org.aya.resolve.visitor; import kala.collection.mutable.MutableList; -import kala.collection.mutable.MutableSet; import org.aya.resolve.context.Context; import org.aya.resolve.error.CyclicDependencyError; import org.aya.syntax.concrete.Expr; @@ -26,7 +25,6 @@ /// if it’s not in the allowedGeneralizes map. public abstract class OverGeneralizer { private final @NotNull Context reporter; - private final @NotNull MutableSet visiting = MutableSet.create(); private final @NotNull MutableList currentPath = MutableList.create(); public OverGeneralizer(@NotNull Context reporter) { this.reporter = reporter; } @@ -37,7 +35,7 @@ public final void introduceDependencies(@NotNull GeneralizedVar var, @NotNull Ex if (contains(var)) return; // If var is already being visited in current DFS path, we found a cycle - if (!visiting.add(var)) { + if (currentPath.contains(var)) { // Find cycle start index var cycleStart = currentPath.indexOf(var); var cyclePath = currentPath.view().drop(cycleStart).appended(var); @@ -51,6 +49,5 @@ public final void introduceDependencies(@NotNull GeneralizedVar var, @NotNull Ex // Now introduce the variable itself introduceDependency(var, param); currentPath.removeLast(); - visiting.remove(var); } } From a4aaed1ad8067e9d6452c2440a1b26d65ae19833 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 30 Jan 2025 19:24:21 -0500 Subject: [PATCH 09/14] test: remove duplicated test, port test to integration tests --- base/src/test/java/org/aya/tyck/TyckTest.java | 62 ------------------- .../success/src/TestNoExtraLists.aya | 30 +++++++++ 2 files changed, 30 insertions(+), 62 deletions(-) diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java index 35ba04944f..63d508c868 100644 --- a/base/src/test/java/org/aya/tyck/TyckTest.java +++ b/base/src/test/java/org/aya/tyck/TyckTest.java @@ -74,24 +74,6 @@ def coeFill0 (A : I -> Type) (u : A 0) : Path A u (transp A u) => \\i => coe 0 i assertTrue(result.isNotEmpty()); } - @Test public void path1() { - var result = tyck(""" - inductive Nat | O | S Nat - prim I : ISet - prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type - prim coe - variable A : Type - def infix = (a b : A) => Path (\\i => A) a b - def refl {a : A} : a = a => \\i => a - open inductive Int - | pos Nat | neg Nat - | zro : pos 0 = neg 0 - example def testZro0 : zro 0 = pos 0 => refl - example def testZro1 : zro 1 = neg 0 => refl - """).defs; - assertTrue(result.isNotEmpty()); - } - /// Need pruning /*@Test*/ public void issue768() { @@ -107,42 +89,6 @@ public void issue768() { assertTrue(result.isNotEmpty()); } - @Test public void test2() { - var result = tyck(""" - open inductive Nat | O | S Nat - open inductive Bool | true | false - def not Bool : Bool | true => false | false => true - def even Nat : Bool - | 0 => true - | S n => odd n - def odd Nat : Bool - | 0 => false - | S n => even n - """).defs; - assertTrue(result.isNotEmpty()); - } - - @Test public void test3() { - assertTrue(tyck(""" - open inductive Nat | O | S Nat - open inductive Natt | OO | SS Nat - def infix = {A : Type} (a b : A) => Type - // Disambiguate by type checking - def test (a : Nat) => a = 114514 - """).defs.isNotEmpty()); - } - - @Test public void elimResolve() { - assertTrue(tyck(""" - open inductive Nat | O | S Nat - open inductive Phantom Nat Nat (A : Type) | mk A - variable a b : Nat - def plus : Phantom a b Nat elim a - | O => mk b - | S a => mk b - """).defs.isNotEmpty()); - } - @Test public void classTyck() { // 🦀 assertTrue(tyck(""" @@ -159,14 +105,6 @@ class Monoid """).defs.isNotEmpty()); } - @Test public void what() { - assertTrue(tyck(""" - class Kontainer - | Taipe : Type - | walue : Taipe - """).defs.isNotEmpty()); - } - @SuppressWarnings("unchecked") private static T getDef(@NotNull ImmutableSeq defs, @NotNull String name) { return (T) TyckAnyDef.make(defs.find(x -> x.ref().name().equals(name)).get()); diff --git a/cli-impl/src/test/resources/success/src/TestNoExtraLists.aya b/cli-impl/src/test/resources/success/src/TestNoExtraLists.aya index cabd8c847c..cdffdbeef8 100644 --- a/cli-impl/src/test/resources/success/src/TestNoExtraLists.aya +++ b/cli-impl/src/test/resources/success/src/TestNoExtraLists.aya @@ -1,3 +1,33 @@ open import prelude def canonicalList => [ 114514 ] + +// Below are ported from TyckTest + +def even Nat : Bool +| 0 => true +| suc n => odd n +def odd Nat : Bool +| 0 => false +| suc n => even n + +open inductive Nat2 +| zero2 +| suc2 Nat2 + +// Disambiguate by type checking +def test (a : Nat) => a = 114514 + + open inductive Int +| pos Nat | neg Nat +| zro : pos 0 = neg 0 +example def testZro0 : zro 0 = pos 0 => refl +example def testZro1 : zro 1 = neg 0 => refl + +module ElimResolve { + open inductive Phantom Nat Nat (A : Type) | mk A + variable a b : Nat + def plus : Phantom a b Nat elim a + | 0 => mk b + | suc a => mk b +} From 6df35e3e524445ff0259feb74dc21267157730f2 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 30 Jan 2025 19:33:37 -0500 Subject: [PATCH 10/14] revert: "generalize: integrate `OverGeneralizer`" This reverts commit 10ac7a64 --- .../org/aya/resolve/visitor/ExprResolver.java | 21 +++++++------------ 1 file changed, 7 insertions(+), 14 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java index 2bdf032067..066f1c9136 100644 --- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java @@ -19,7 +19,10 @@ import org.aya.syntax.concrete.stmt.QualifiedID; import org.aya.syntax.concrete.stmt.Stmt; import org.aya.syntax.concrete.stmt.decl.DataCon; -import org.aya.syntax.ref.*; +import org.aya.syntax.ref.AnyVar; +import org.aya.syntax.ref.DefVar; +import org.aya.syntax.ref.GeneralizedVar; +import org.aya.syntax.ref.LocalVar; import org.aya.tyck.error.ClassError; import org.aya.util.error.Panic; import org.aya.util.error.PosedUnaryOperator; @@ -134,8 +137,9 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) { // a "resolved" GeneralizedVar is not in [allowedGeneralizes] if (allowGeneralizing) { var param = generalized.toParam(false); - var generalizer = new OvergrownGeneralizer(); - generalizer.introduceDependencies(generalized, param); + // Now introduce the variable itself + allowedGeneralizes.put(generalized, param); + addReference(generalized.owner); yield param.ref(); } else { yield ctx.reportAndThrow(new GeneralizedNotAvailableError(pos, generalized)); @@ -250,17 +254,6 @@ private void addReference(@NotNull TyckUnit unit) { }); } - private class OvergrownGeneralizer extends OverGeneralizer { - public OvergrownGeneralizer() { super(ctx); } - @Override protected boolean contains(@NotNull GeneralizedVar var) { return allowedGeneralizes.containsKey(var); } - @Override protected void introduceDependency(@NotNull GeneralizedVar var, Expr.@NotNull Param param) { - var owner = var.owner; - assert owner != null : "GeneralizedVar owner should not be null"; - allowedGeneralizes.put(var, param); - addReference(owner); - } - } - public @NotNull AnyVar resolve(@NotNull QualifiedID name) { var result = ctx.get(name); if (result instanceof GeneralizedVar gvar) { From c40307ce88e96b2cbba56bc4065e4594a50ff6db Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 30 Jan 2025 20:20:17 -0500 Subject: [PATCH 11/14] generalize: basic error report --- .../aya/resolve/visitor/OverGeneralizer.java | 4 +- .../org/aya/resolve/visitor/StmtResolver.java | 82 ++++++++++++++++--- .../src/test/resources/success/src/Test.aya | 6 ++ 3 files changed, 79 insertions(+), 13 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java index 615a608f4c..bda40752ea 100644 --- a/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java +++ b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java @@ -29,15 +29,17 @@ public abstract class OverGeneralizer { public OverGeneralizer(@NotNull Context reporter) { this.reporter = reporter; } protected abstract boolean contains(@NotNull GeneralizedVar var); + protected abstract boolean isSelf(@NotNull GeneralizedVar var); protected abstract void introduceDependency(@NotNull GeneralizedVar var, @NotNull Expr.Param param); public final void introduceDependencies(@NotNull GeneralizedVar var, @NotNull Expr.Param param) { if (contains(var)) return; // If var is already being visited in current DFS path, we found a cycle - if (currentPath.contains(var)) { + if (currentPath.contains(var) || isSelf(var)) { // Find cycle start index var cycleStart = currentPath.indexOf(var); + if (cycleStart < 0) cycleStart = 0; var cyclePath = currentPath.view().drop(cycleStart).appended(var); reporter.reportAndThrow(new CyclicDependencyError(var.sourcePos(), var, cyclePath.toImmutableSeq())); } diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java index 9f52c4e3f7..da32049053 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java @@ -5,6 +5,9 @@ import kala.collection.SeqView; import kala.collection.immutable.ImmutableMap; import kala.collection.immutable.ImmutableSeq; +import kala.collection.mutable.MutableLinkedHashMap; +import kala.collection.mutable.MutableMap; +import kala.control.Option; import kala.value.MutableValue; import org.aya.generic.stmt.TyckOrder; import org.aya.generic.stmt.TyckUnit; @@ -13,8 +16,12 @@ import org.aya.resolve.context.Context; import org.aya.resolve.error.NameProblem; import org.aya.resolve.visitor.ExprResolver.Where; +import org.aya.syntax.concrete.Expr; +import org.aya.syntax.concrete.stmt.Generalize; import org.aya.syntax.concrete.stmt.QualifiedID; +import org.aya.syntax.concrete.stmt.Stmt; import org.aya.syntax.concrete.stmt.decl.*; +import org.aya.syntax.ref.GeneralizedVar; import org.aya.syntax.ref.LocalVar; import org.aya.tyck.error.TyckOrderError; import org.aya.util.error.Panic; @@ -28,28 +35,77 @@ /// @see ExprResolver public interface StmtResolver { static void resolveStmt(@NotNull ImmutableSeq stmt, @NotNull ResolveInfo info) { - stmt.forEach(s -> resolveStmt(s, info)); + var todos = stmt.flatMap(s -> resolveStmt(s, info)); + abstract class OvergrownGeneralizer extends OverGeneralizer { + final MutableMap dependencyGeneralizes = MutableLinkedHashMap.of(); + final ResolveStmt task; + // MutableList deps = MutableList.create(); + public OvergrownGeneralizer(@NotNull ResolveStmt task) { + super(info.thisModule()); + this.task = task; + } + @Override protected boolean contains(@NotNull GeneralizedVar var) { + return dependencyGeneralizes.containsKey(var) || task.generalizes.containsKey(var); + } + @Override protected void introduceDependency(@NotNull GeneralizedVar var, Expr.@NotNull Param param) { + var owner = var.owner; + assert owner != null : "GeneralizedVar owner should not be null"; + dependencyGeneralizes.put(var, param); + // deps.append(owner); + } + } + + todos.forEach(task -> { + if (task.stmt instanceof Generalize gen) { + var generalizer = new OvergrownGeneralizer(task) { + @Override protected boolean isSelf(@NotNull GeneralizedVar var) { return gen.variables.contains(var); } + }; + task.generalizes.forEach((depGen, _) -> depGen.owner.dependencies.forEach(generalizer::introduceDependencies)); + generalizer.dependencyGeneralizes.putAll(task.generalizes); + gen.dependencies = ImmutableMap.from(generalizer.dependencyGeneralizes); + } + }); + todos.forEach(task -> { + if (task.stmt instanceof TeleDecl decl) { + var generalizer = new OvergrownGeneralizer(task) { + @Override protected boolean isSelf(@NotNull GeneralizedVar var) { return false; } + }; + task.generalizes.forEach((gen, _) -> gen.owner.dependencies.forEach(generalizer::introduceDependencies)); + insertGeneralizedVars(decl, task.generalizes); + insertGeneralizedVars(decl, generalizer.dependencyGeneralizes); + // addReferences(info, new TyckOrder.Head(gen), generalizer.deps.view().map(TyckOrder.Head::new)); + } + }); } + /// @param generalizes the directly referred generalized variables + record ResolveStmt(Stmt stmt, MutableMap generalizes) { } + + /// @return the "TO-DO" for the rest of the resolving, see [ResolveStmt] /// @apiNote Note that this function MUTATES the stmt if it's a Decl. - static void resolveStmt(@NotNull ResolvingStmt stmt, @NotNull ResolveInfo info) { - switch (stmt) { + static Option resolveStmt(@NotNull ResolvingStmt stmt, @NotNull ResolveInfo info) { + return switch (stmt) { case ResolvingStmt.ResolvingDecl decl -> resolveDecl(decl, info); - case ResolvingStmt.ModStmt(var stmts) -> resolveStmt(stmts, info); + case ResolvingStmt.ModStmt(var stmts) -> { + resolveStmt(stmts, info); + yield Option.none(); + } case ResolvingStmt.GenStmt(var variables) -> { var resolver = new ExprResolver(info.thisModule(), true); resolver.enter(Where.Head); variables.descentInPlace(resolver, PosedUnaryOperator.identity()); variables.dependencies = ImmutableMap.from(resolver.allowedGeneralizes().view()); addReferences(info, new TyckOrder.Head(variables), resolver); + yield Option.some(new ResolveStmt(variables, resolver.allowedGeneralizes())); } - } + }; } /// Resolve {@param predecl}, where `predecl.ctx()` is the context of the body of {@param predecl} /// /// @apiNote Note that this function MUTATES the decl - private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @NotNull ResolveInfo info) { + private static Option + resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @NotNull ResolveInfo info) { switch (predecl) { case ResolvingStmt.TopDecl(FnDecl decl, var ctx) -> { var where = decl.body instanceof FnBody.BlockBody ? Where.Head : Where.FnSimple; @@ -58,8 +114,7 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N switch (decl.body) { case FnBody.BlockBody body -> { assert body.elims() == null; - // introducing generalized variable is not allowed in clauses, hence we insert them before body resolving - insertGeneralizedVars(decl, resolver); + // insertGeneralizedVars(decl, resolver); resolveElim(resolver, body.inner()); var clausesResolver = resolver.deriveRestrictive(); clausesResolver.reference().append(new TyckOrder.Head(decl)); @@ -68,15 +123,16 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N } case FnBody.ExprBody(var expr) -> { var body = expr.descent(resolver); - insertGeneralizedVars(decl, resolver); + // insertGeneralizedVars(decl, resolver); decl.body = new FnBody.ExprBody(body); addReferences(info, new TyckOrder.Head(decl), resolver); } } + return Option.some(new ResolveStmt(decl, resolver.allowedGeneralizes())); } case ResolvingStmt.TopDecl(DataDecl data, var ctx) -> { var resolver = resolveDeclSignature(info, new ExprResolver(ctx, true), data, Where.Head); - insertGeneralizedVars(data, resolver); + // insertGeneralizedVars(data, resolver); resolveElim(resolver, data.body); data.body.forEach(con -> { var bodyResolver = resolver.deriveRestrictive(); @@ -94,6 +150,7 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N addReferences(info, new TyckOrder.Body(data), resolver.reference().view() .concat(data.body.clauses.map(TyckOrder.Body::new))); + return Option.some(new ResolveStmt(data, resolver.allowedGeneralizes())); } case ResolvingStmt.TopDecl(ClassDecl decl, var ctx) -> { var resolver = new ExprResolver(ctx, false); @@ -120,6 +177,7 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N // handled in DataDecl and ClassDecl case ResolvingStmt.MiscDecl _ -> Panic.unreachable(); } + return Option.none(); } private static void resolveMemberSignature(TeleDecl con, ExprResolver bodyResolver, MutableValue<@NotNull Context> mCtx) { @@ -163,8 +221,8 @@ private static void addReferences(@NotNull ResolveInfo info, TyckOrder decl, Exp return newResolver; } - private static void insertGeneralizedVars(@NotNull TeleDecl decl, @NotNull ExprResolver resolver) { - decl.telescope = decl.telescope.prependedAll(resolver.allowedGeneralizes().valuesView()); + private static void insertGeneralizedVars(@NotNull TeleDecl decl, MutableMap generalizes) { + decl.telescope = decl.telescope.prependedAll(generalizes.valuesView()); } private static void resolveElim(@NotNull ExprResolver resolver, @NotNull MatchBody body) { diff --git a/cli-impl/src/test/resources/success/src/Test.aya b/cli-impl/src/test/resources/success/src/Test.aya index 13d4353007..2b90ebc3c9 100644 --- a/cli-impl/src/test/resources/success/src/Test.aya +++ b/cli-impl/src/test/resources/success/src/Test.aya @@ -135,3 +135,9 @@ module Issue243 { | nothing => refl | _ => 233 } + +module PullRequest1226 { + variable A : Type + variable a b : A + def basic (a = a) => a +} From 27f3a86ff6a5826ccab43aadd8c23dcd747b0e03 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 30 Jan 2025 20:30:35 -0500 Subject: [PATCH 12/14] generalize: test on error report --- .../aya/resolve/visitor/OverGeneralizer.java | 18 +++++------------- .../org/aya/resolve/visitor/StmtResolver.java | 17 +++++++++-------- .../java/org/aya/test/fixtures/ScopeError.java | 6 +++++- .../src/test/resources/negative/ScopeError.txt | 14 ++++++++++++++ 4 files changed, 33 insertions(+), 22 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java index bda40752ea..a9181e311d 100644 --- a/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java +++ b/base/src/main/java/org/aya/resolve/visitor/OverGeneralizer.java @@ -12,31 +12,23 @@ /// Collects dependency information for generalized variables using DFS on their types. /// /// 1. A variable's type may reference other generalized variables; we record those as dependencies. -/// 2. If we revisit a variable already on the DFS stack ("visiting" set), that indicates +/// 2. If we revisit a variable already on the DFS stack [#currentPath], that indicates /// a cyclic dependency, and we report an error. -/// 3. Once a variable is fully processed, it goes into the "visited" set; future registrations -/// of the same variable skip repeated traversal. -/// -/// Pitfalls & Notes: -/// - A single variable (e.g. “A”) should be registered once, to avoid duplication. -/// - Attempting to re-scan or re-introduce “A” in another variable’s context can cause -/// confusion or potential cycles. So we do all dependency scans here, at declaration time. -/// - Any reference to a variable out of scope is handled as an error in the resolver -/// if it’s not in the allowedGeneralizes map. +/// 3. Once a variable is fully processed, it goes into the [#introduceDependency] method; future registrations +/// of the same variable skip repeated traversal using [#contains]. public abstract class OverGeneralizer { private final @NotNull Context reporter; - private final @NotNull MutableList currentPath = MutableList.create(); + public final @NotNull MutableList currentPath = MutableList.create(); public OverGeneralizer(@NotNull Context reporter) { this.reporter = reporter; } protected abstract boolean contains(@NotNull GeneralizedVar var); - protected abstract boolean isSelf(@NotNull GeneralizedVar var); protected abstract void introduceDependency(@NotNull GeneralizedVar var, @NotNull Expr.Param param); public final void introduceDependencies(@NotNull GeneralizedVar var, @NotNull Expr.Param param) { if (contains(var)) return; // If var is already being visited in current DFS path, we found a cycle - if (currentPath.contains(var) || isSelf(var)) { + if (currentPath.contains(var)) { // Find cycle start index var cycleStart = currentPath.indexOf(var); if (cycleStart < 0) cycleStart = 0; diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java index da32049053..46a09753e5 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java @@ -36,7 +36,7 @@ public interface StmtResolver { static void resolveStmt(@NotNull ImmutableSeq stmt, @NotNull ResolveInfo info) { var todos = stmt.flatMap(s -> resolveStmt(s, info)); - abstract class OvergrownGeneralizer extends OverGeneralizer { + class OvergrownGeneralizer extends OverGeneralizer { final MutableMap dependencyGeneralizes = MutableLinkedHashMap.of(); final ResolveStmt task; // MutableList deps = MutableList.create(); @@ -57,19 +57,20 @@ public OvergrownGeneralizer(@NotNull ResolveStmt task) { todos.forEach(task -> { if (task.stmt instanceof Generalize gen) { - var generalizer = new OvergrownGeneralizer(task) { - @Override protected boolean isSelf(@NotNull GeneralizedVar var) { return gen.variables.contains(var); } - }; - task.generalizes.forEach((depGen, _) -> depGen.owner.dependencies.forEach(generalizer::introduceDependencies)); + var generalizer = new OvergrownGeneralizer(task); + generalizer.currentPath.appendAll(gen.variables); + task.generalizes.forEach((depGen, _) -> { + generalizer.currentPath.append(depGen); + depGen.owner.dependencies.forEach(generalizer::introduceDependencies); + generalizer.currentPath.removeLast(); + }); generalizer.dependencyGeneralizes.putAll(task.generalizes); gen.dependencies = ImmutableMap.from(generalizer.dependencyGeneralizes); } }); todos.forEach(task -> { if (task.stmt instanceof TeleDecl decl) { - var generalizer = new OvergrownGeneralizer(task) { - @Override protected boolean isSelf(@NotNull GeneralizedVar var) { return false; } - }; + var generalizer = new OvergrownGeneralizer(task); task.generalizes.forEach((gen, _) -> gen.owner.dependencies.forEach(generalizer::introduceDependencies)); insertGeneralizedVars(decl, task.generalizes); insertGeneralizedVars(decl, generalizer.dependencyGeneralizes); diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/ScopeError.java b/cli-impl/src/test/java/org/aya/test/fixtures/ScopeError.java index 5a52e9b0db..645ac26d6e 100644 --- a/cli-impl/src/test/java/org/aya/test/fixtures/ScopeError.java +++ b/cli-impl/src/test/java/org/aya/test/fixtures/ScopeError.java @@ -1,4 +1,4 @@ -// 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.test.fixtures; @@ -103,4 +103,8 @@ def test (A : Type) (a : A) : A => | x : A := a in x """; + @Language("Aya") String testCyclicDependency = """ + variable A : B + variable B : A + """; } diff --git a/cli-impl/src/test/resources/negative/ScopeError.txt b/cli-impl/src/test/resources/negative/ScopeError.txt index 58bec7ba96..49bc19ef13 100644 --- a/cli-impl/src/test/resources/negative/ScopeError.txt +++ b/cli-impl/src/test/resources/negative/ScopeError.txt @@ -318,3 +318,17 @@ That looks right! LocalShadowSuppress: That looks right! +CyclicDependency: +In file $FILE:1:11 -> + + 1 │ variable A : B + │ ╰╯ + 2 │ variable B : A + +Error: Cyclic dependency detected in variable declarations: + A → B → A + +Resolving interrupted due to: +1 error(s), 0 warning(s). +Let's learn from that. + From e4b963e1ea1748c4d67ebd84845108a395edc9a1 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 30 Jan 2025 20:40:36 -0500 Subject: [PATCH 13/14] generalize: more intensive test, fix a long-standing undiscovered bug on generalize & contexts --- .../java/org/aya/resolve/ResolvingStmt.java | 5 +++-- .../aya/resolve/visitor/StmtPreResolver.java | 2 +- .../org/aya/resolve/visitor/StmtResolver.java | 4 ++-- .../src/test/resources/success/src/Test.aya | 19 +++++++++++++++++-- 4 files changed, 23 insertions(+), 7 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/ResolvingStmt.java b/base/src/main/java/org/aya/resolve/ResolvingStmt.java index ee273a1d88..3218d85a0c 100644 --- a/base/src/main/java/org/aya/resolve/ResolvingStmt.java +++ b/base/src/main/java/org/aya/resolve/ResolvingStmt.java @@ -1,9 +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.resolve; import kala.collection.immutable.ImmutableSeq; import org.aya.resolve.context.Context; +import org.aya.resolve.context.ModuleContext; import org.aya.syntax.concrete.stmt.Generalize; import org.aya.syntax.concrete.stmt.Stmt; import org.aya.syntax.concrete.stmt.decl.Decl; @@ -38,6 +39,6 @@ sealed interface ResolvingDecl extends ResolvingStmt { } record TopDecl(@NotNull Decl stmt, @NotNull Context context) implements ResolvingDecl { } record MiscDecl(@NotNull Decl stmt) implements ResolvingDecl { } - record GenStmt(@NotNull Generalize stmt) implements ResolvingStmt { } + record GenStmt(@NotNull Generalize stmt, @NotNull ModuleContext context) implements ResolvingStmt { } record ModStmt(@NotNull ImmutableSeq<@NotNull ResolvingStmt> resolved) implements ResolvingStmt { } } diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java index c3b2121656..ee5aaddca2 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java @@ -99,7 +99,7 @@ public ImmutableSeq resolveStmt(@NotNull ImmutableSeq stmts case Generalize variables -> { for (var variable : variables.variables) context.defineSymbol(variable, Stmt.Accessibility.Private, variable.sourcePos); - yield new ResolvingStmt.GenStmt(variables); + yield new ResolvingStmt.GenStmt(variables, context); } }; } diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java index 46a09753e5..ffbc058421 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java @@ -91,8 +91,8 @@ static Option resolveStmt(@NotNull ResolvingStmt stmt, @NotNull Res resolveStmt(stmts, info); yield Option.none(); } - case ResolvingStmt.GenStmt(var variables) -> { - var resolver = new ExprResolver(info.thisModule(), true); + case ResolvingStmt.GenStmt(var variables, var context) -> { + var resolver = new ExprResolver(context, true); resolver.enter(Where.Head); variables.descentInPlace(resolver, PosedUnaryOperator.identity()); variables.dependencies = ImmutableMap.from(resolver.allowedGeneralizes().view()); diff --git a/cli-impl/src/test/resources/success/src/Test.aya b/cli-impl/src/test/resources/success/src/Test.aya index 2b90ebc3c9..c59a8212f0 100644 --- a/cli-impl/src/test/resources/success/src/Test.aya +++ b/cli-impl/src/test/resources/success/src/Test.aya @@ -136,8 +136,23 @@ module Issue243 { | _ => 233 } -module PullRequest1226 { +module PullRequest1226Basic { variable A : Type variable a b : A - def basic (a = a) => a + def test (a = a) => a +} + +module PullRequest1226Hard { + variable A : Type + variable a : A + open inductive K | kk + open inductive G (k : K) | gg + open inductive F (A : Type) (k : K) (n : G k) | ff + open inductive N (b : A) (c : A) | nn + variable k : K + variable n : G k + variable xs : F A k n + variable b c : A + variable d : N b c + def test : d = d => refl } From 9dbce46989c2ddd8ea405bee7a2c594d399ba3fb Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 30 Jan 2025 21:00:01 -0500 Subject: [PATCH 14/14] generalize: erm I can't get this to work --- .../main/java/org/aya/resolve/visitor/StmtResolver.java | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java index ffbc058421..4200e62e96 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java @@ -59,13 +59,12 @@ public OvergrownGeneralizer(@NotNull ResolveStmt task) { if (task.stmt instanceof Generalize gen) { var generalizer = new OvergrownGeneralizer(task); generalizer.currentPath.appendAll(gen.variables); + // Check loops task.generalizes.forEach((depGen, _) -> { generalizer.currentPath.append(depGen); depGen.owner.dependencies.forEach(generalizer::introduceDependencies); generalizer.currentPath.removeLast(); }); - generalizer.dependencyGeneralizes.putAll(task.generalizes); - gen.dependencies = ImmutableMap.from(generalizer.dependencyGeneralizes); } }); todos.forEach(task -> { @@ -129,7 +128,8 @@ static Option resolveStmt(@NotNull ResolvingStmt stmt, @NotNull Res addReferences(info, new TyckOrder.Head(decl), resolver); } } - return Option.some(new ResolveStmt(decl, resolver.allowedGeneralizes())); + if (resolver.allowedGeneralizes().isNotEmpty()) + return Option.some(new ResolveStmt(decl, resolver.allowedGeneralizes())); } case ResolvingStmt.TopDecl(DataDecl data, var ctx) -> { var resolver = resolveDeclSignature(info, new ExprResolver(ctx, true), data, Where.Head); @@ -151,7 +151,8 @@ static Option resolveStmt(@NotNull ResolvingStmt stmt, @NotNull Res addReferences(info, new TyckOrder.Body(data), resolver.reference().view() .concat(data.body.clauses.map(TyckOrder.Body::new))); - return Option.some(new ResolveStmt(data, resolver.allowedGeneralizes())); + if (resolver.allowedGeneralizes().isNotEmpty()) + return Option.some(new ResolveStmt(data, resolver.allowedGeneralizes())); } case ResolvingStmt.TopDecl(ClassDecl decl, var ctx) -> { var resolver = new ExprResolver(ctx, false);