From 300148e29f25e1c5db03336cbe6128aa8362a311 Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sun, 29 Dec 2024 23:48:15 +0800 Subject: [PATCH 1/4] elim-shadow: intro --- .../org/aya/resolve/visitor/ExprResolver.java | 13 ++++++++----- .../aya/resolve/visitor/PatternResolver.java | 18 +++++++++++------- .../org/aya/resolve/visitor/StmtResolver.java | 6 ++++-- 3 files changed, 23 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 2157d16211..7cb0f378ae 100644 --- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java @@ -22,6 +22,7 @@ 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; @@ -29,6 +30,7 @@ import org.aya.util.error.WithPos; import org.jetbrains.annotations.Contract; import org.jetbrains.annotations.NotNull; +import org.jetbrains.annotations.Nullable; /** * Resolves bindings. @@ -194,7 +196,7 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) { // Requires exhaustiveness check, therefore must need the full data body enter(Where.FnPattern); - var clauses = match.clauses().map(this::clause); + var clauses = match.clauses().map(x -> clause(ImmutableSeq.empty(), x)); exit(); yield match.update(discriminant, clauses, returns); @@ -221,10 +223,11 @@ private void addReference(@NotNull DefVar defVar) { addReference(defVar.concrete); } - public @NotNull Pattern.Clause clause(@NotNull Pattern.Clause clause) { + public @NotNull Pattern.Clause clause(@NotNull ImmutableSeq telescope, @NotNull Pattern.Clause clause) { var mCtx = MutableValue.create(ctx); enter(Where.FnPattern); - var pats = clause.patterns.map(pa -> pa.descent(pat -> resolvePattern(pat, mCtx))); + var pats = clause.patterns.map(pa -> + pa.descent(pat -> resolvePattern(pat, telescope, mCtx))); exit(); enter(Where.FnBody); var body = clause.expr.map(x -> x.descent(enter(mCtx.get()))); @@ -232,8 +235,8 @@ private void addReference(@NotNull DefVar defVar) { return clause.update(pats, body); } - public @NotNull WithPos resolvePattern(@NotNull WithPos pattern, MutableValue ctx) { - var resolver = new PatternResolver(ctx.get(), this::addReference); + public @NotNull WithPos resolvePattern(@NotNull WithPos pattern, @NotNull ImmutableSeq telescope, MutableValue ctx) { + var resolver = new PatternResolver(ctx.get(), telescope, this::addReference); var result = pattern.descent(resolver); ctx.set(resolver.context()); return result; diff --git a/base/src/main/java/org/aya/resolve/visitor/PatternResolver.java b/base/src/main/java/org/aya/resolve/visitor/PatternResolver.java index a8cc94e215..5fd929bf1c 100644 --- a/base/src/main/java/org/aya/resolve/visitor/PatternResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/PatternResolver.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.resolve.visitor; +import kala.collection.immutable.ImmutableSeq; import org.aya.generic.stmt.TyckUnit; import org.aya.resolve.context.Context; import org.aya.resolve.error.NameProblem; @@ -10,10 +11,7 @@ import org.aya.syntax.concrete.stmt.ModuleName; import org.aya.syntax.concrete.stmt.decl.DataCon; import org.aya.syntax.core.def.ConDefLike; -import org.aya.syntax.ref.AnyDefVar; -import org.aya.syntax.ref.AnyVar; -import org.aya.syntax.ref.CompiledVar; -import org.aya.syntax.ref.DefVar; +import org.aya.syntax.ref.*; import org.aya.util.error.Panic; import org.aya.util.error.PosedUnaryOperator; import org.aya.util.error.SourcePos; @@ -25,10 +23,12 @@ public class PatternResolver implements PosedUnaryOperator { // DIRTY!! private @NotNull Context context; + private final @NotNull ImmutableSeq mercy; private final @NotNull Consumer parentAdd; - public PatternResolver(@NotNull Context context, @NotNull Consumer parentAdd) { + public PatternResolver(@NotNull Context context, @NotNull ImmutableSeq mercy, @NotNull Consumer parentAdd) { this.context = context; + this.mercy = mercy; this.parentAdd = parentAdd; } @@ -47,7 +47,7 @@ public PatternResolver(@NotNull Context context, @NotNull Consumer par } // It is not a constructor, it is a bind - context = context.bind(bind.bind()); + context = context.bind(bind.bind(), this::toWarn); yield bind; } case Pattern.QualifiedRef qref -> { @@ -64,13 +64,17 @@ public PatternResolver(@NotNull Context context, @NotNull Consumer par yield context.reportAndThrow(new NameProblem.QualifiedNameNotFoundError(qid.component(), qid.name(), pos)); } case Pattern.As as -> { - context = context.bind(as.as()); + context = context.bind(as.as(), this::toWarn); yield as; } default -> pat; }; } + private boolean toWarn(@Nullable AnyVar var) { + return var instanceof LocalVar && !mercy.contains(var); + } + private void addReference(@NotNull AnyDefVar defVar) { if (defVar instanceof DefVar fr) parentAdd.accept(fr.concrete); } 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 d9741b22ce..4c58dea905 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java @@ -64,7 +64,7 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N resolveElim(resolver, body.inner()); var clausesResolver = resolver.deriveRestrictive(); clausesResolver.reference().append(new TyckOrder.Head(decl)); - decl.body = body.map(clausesResolver::clause); + decl.body = body.map(x -> clausesResolver.clause(decl.teleVars().toImmutableSeq(), x)); addReferences(info, new TyckOrder.Body(decl), clausesResolver); } case FnBody.ExprBody(var expr) -> { @@ -84,7 +84,9 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N var mCtx = MutableValue.create(resolver.ctx()); bodyResolver.reference().append(new TyckOrder.Head(data)); bodyResolver.enter(Where.ConPattern); - con.patterns = con.patterns.map(pat -> pat.descent(pattern -> bodyResolver.resolvePattern(pattern, mCtx))); + con.patterns = con.patterns.map(pat -> + pat.descent(pattern -> + bodyResolver.resolvePattern(pattern, data.teleVars().toImmutableSeq(), mCtx))); bodyResolver.exit(); resolveMemberSignature(con, bodyResolver, mCtx); addReferences(info, new TyckOrder.Head(con), bodyResolver); From d1a69115d6e94b896c078d1bfa37e6c11d08420e Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Mon, 30 Dec 2024 21:38:56 +0800 Subject: [PATCH 2/4] stdlib: remove unnecessary suppressing --- cli-impl/src/test/resources/shared/src/data/list/base.aya | 4 ++-- .../test/resources/shared/src/data/list/properties.aya | 8 ++++---- cli-impl/src/test/resources/shared/src/data/vec/base.aya | 2 +- .../src/test/resources/shared/src/data/vec/properties.aya | 2 +- .../test/resources/shared/src/relation/binary/nat_cmp.aya | 4 ++-- 5 files changed, 10 insertions(+), 10 deletions(-) diff --git a/cli-impl/src/test/resources/shared/src/data/list/base.aya b/cli-impl/src/test/resources/shared/src/data/list/base.aya index 110de8aa03..88166f869b 100644 --- a/cli-impl/src/test/resources/shared/src/data/list/base.aya +++ b/cli-impl/src/test/resources/shared/src/data/list/base.aya @@ -28,13 +28,13 @@ def rev' (buf xs : List A) : List A elim xs def rev (xs : List A) : List A => rev' [ ] xs -@suppress(Shadowing) + overlap def take (n : Nat) (xs : List A) : List A | _, [ ] => [ ] | 0, _ => [ ] | suc n, x :< xs => x :< (take n xs) -@suppress(Shadowing) + overlap def drop (n : Nat) (xs : List A) : List A | _, [ ] => [ ] | 0, _ => xs diff --git a/cli-impl/src/test/resources/shared/src/data/list/properties.aya b/cli-impl/src/test/resources/shared/src/data/list/properties.aya index de9a6f900f..b1b174349b 100644 --- a/cli-impl/src/test/resources/shared/src/data/list/properties.aya +++ b/cli-impl/src/test/resources/shared/src/data/list/properties.aya @@ -29,19 +29,19 @@ def head-def (x : A) (xs : List A) : A elim xs | [ ] => x | a :< _ => a -@suppress(Shadowing) + def ++-assoc (xs ys zs : List A) : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) elim xs | [ ] => refl | x :< xs => pmap (x :<) (++-assoc xs ys zs) -@suppress(Shadowing) + private def rev'-map (f : A -> B) (buf xs : List A) : map f (rev' buf xs) = rev' (map f buf) (map f xs) elim xs | [ ] => refl | x :< xs => rev'-map f (x :< buf) xs def rev-map (f : A -> B) (xs : List A) : map f (rev xs) = rev (map f xs) => rev'-map f [ ] xs -@suppress(Shadowing) + private def rev'-++ (buf xs : List A) : rev' buf xs = rev xs ++ buf elim xs | [ ] => refl | x :< xs => @@ -51,7 +51,7 @@ private def rev'-++ (buf xs : List A) : rev' buf xs = rev xs ++ buf elim xs | step2 : (rev xs ++ [ x ]) ++ buf = rev xs ++ (x :< buf) := ++-assoc (rev xs) [ x ] buf in step0 <=> pinv step2 <=> pinv step1 -@suppress(Shadowing) + def rev-distrib-++ (xs ys : List A) : rev (xs ++ ys) = (rev ys ++ rev xs) elim xs | [ ] => refl | x :< xs => diff --git a/cli-impl/src/test/resources/shared/src/data/vec/base.aya b/cli-impl/src/test/resources/shared/src/data/vec/base.aya index 74d37c30b2..52959e9532 100644 --- a/cli-impl/src/test/resources/shared/src/data/vec/base.aya +++ b/cli-impl/src/test/resources/shared/src/data/vec/base.aya @@ -1,6 +1,6 @@ open import prelude hiding (++) -@suppress(Shadowing) + open inductive Vec (n : Nat) (A : Type) elim n | 0 => [] | suc n => infixr :> A (Vec n A) diff --git a/cli-impl/src/test/resources/shared/src/data/vec/properties.aya b/cli-impl/src/test/resources/shared/src/data/vec/properties.aya index 9b553db32e..8c134ab294 100644 --- a/cli-impl/src/test/resources/shared/src/data/vec/properties.aya +++ b/cli-impl/src/test/resources/shared/src/data/vec/properties.aya @@ -13,7 +13,7 @@ def ++-assoc (xs : Vec n A) (ys : Vec m A) (zs : Vec o A) | [] => refl | x :> xs' => pmapd _ (\i => x :>) (++-assoc xs' ys zs) -@suppress(Shadowing) + def vmap-distrib-++ (f : A -> B) (xs : Vec n A) (ys : Vec m A) : vmap f (xs ++ ys) = vmap f xs ++ vmap f ys elim xs | [] => refl | x :> xs => pmap (f x :>) (vmap-distrib-++ f xs ys) diff --git a/cli-impl/src/test/resources/shared/src/relation/binary/nat_cmp.aya b/cli-impl/src/test/resources/shared/src/relation/binary/nat_cmp.aya index 2034203ffa..edb158c750 100644 --- a/cli-impl/src/test/resources/shared/src/relation/binary/nat_cmp.aya +++ b/cli-impl/src/test/resources/shared/src/relation/binary/nat_cmp.aya @@ -47,14 +47,14 @@ private def some-lemma {a b : Nat} (p : subTrunc a b = 0) (np : neg (subTrunc (s | suc a, 0 => exfalso (z≠s (pinv p)) | suc a, suc b => pmap suc (some-lemma p np) -@suppress(Shadowing) + def <=-case {a b : Nat} (p : a <= b) : Sum (a < b) (a = b) => match a inl p | _ because reflect_false np => inr (some-lemma p np) } -@suppress(Shadowing) + def ¬<→>= {a b : Nat} (np : neg (a < b)) : a >= b | {_}, {0}, np => refl | {0}, {suc b}, np => exfalso (np refl) From a924a992f5d55c9952ef1cb3d05f4c9006394d9c Mon Sep 17 00:00:00 2001 From: ice1000 Date: Mon, 30 Dec 2024 21:20:14 -0500 Subject: [PATCH 3/4] shadow: add test --- .../org/aya/resolve/visitor/StmtPreResolver.java | 2 +- .../java/org/aya/test/fixtures/ScopeError.java | 13 +++++++++++++ .../src/test/resources/negative/ScopeError.txt | 15 +++++++++++++++ .../test/resources/shared/src/data/list/base.aya | 2 -- .../resources/shared/src/data/list/properties.aya | 4 ---- .../test/resources/shared/src/data/vec/base.aya | 1 - .../resources/shared/src/data/vec/properties.aya | 1 - .../shared/src/relation/binary/nat_cmp.aya | 1 - .../src/main/java/org/aya/generic/Suppress.java | 2 +- 9 files changed, 30 insertions(+), 11 deletions(-) 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 60ea166118..ba0171e54e 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java @@ -151,7 +151,7 @@ private static Reporter suppress(@NotNull Reporter reporter, @NotNull Decl decl) var r = new SuppressingReporter(reporter); decl.suppresses.forEach(suppress -> { switch (suppress) { - case Shadowing -> r.suppress(NameProblem.ShadowingWarn.class); + case LocalShadow -> r.suppress(NameProblem.ShadowingWarn.class); } }); return r; 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 32d82478f3..5a52e9b0db 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 @@ -90,4 +90,17 @@ def p (a : Bool) : Bool elim b open class Cls | A : Type def test (c : Cls) => c.B """; + @Language("Aya") String testLocalShadow = """ + def test (A : Type) (a : A) : A => + let | x : A := a + | x : A := a + in x + """; + @Language("Aya") String testLocalShadowSuppress = """ + @suppress(LocalShadow) + def test (A : Type) (a : A) : A => + let | x : A := a + | x : A := a + in x + """; } diff --git a/cli-impl/src/test/resources/negative/ScopeError.txt b/cli-impl/src/test/resources/negative/ScopeError.txt index 49ba204eb1..58bec7ba96 100644 --- a/cli-impl/src/test/resources/negative/ScopeError.txt +++ b/cli-impl/src/test/resources/negative/ScopeError.txt @@ -303,3 +303,18 @@ Resolving interrupted due to: 1 error(s), 0 warning(s). Let's learn from that. +LocalShadow: +In file $FILE:3:8 -> + + 1 │ def test (A : Type) (a : A) : A => + 2 │ let | x : A := a + 3 │ | x : A := a + │ ╰╯ + +Warning: The name `x` shadows a previous local definition from outer scope + +That looks right! + +LocalShadowSuppress: +That looks right! + diff --git a/cli-impl/src/test/resources/shared/src/data/list/base.aya b/cli-impl/src/test/resources/shared/src/data/list/base.aya index 88166f869b..76bb32a8ef 100644 --- a/cli-impl/src/test/resources/shared/src/data/list/base.aya +++ b/cli-impl/src/test/resources/shared/src/data/list/base.aya @@ -28,13 +28,11 @@ def rev' (buf xs : List A) : List A elim xs def rev (xs : List A) : List A => rev' [ ] xs - overlap def take (n : Nat) (xs : List A) : List A | _, [ ] => [ ] | 0, _ => [ ] | suc n, x :< xs => x :< (take n xs) - overlap def drop (n : Nat) (xs : List A) : List A | _, [ ] => [ ] | 0, _ => xs diff --git a/cli-impl/src/test/resources/shared/src/data/list/properties.aya b/cli-impl/src/test/resources/shared/src/data/list/properties.aya index b1b174349b..ffe504befb 100644 --- a/cli-impl/src/test/resources/shared/src/data/list/properties.aya +++ b/cli-impl/src/test/resources/shared/src/data/list/properties.aya @@ -29,19 +29,16 @@ def head-def (x : A) (xs : List A) : A elim xs | [ ] => x | a :< _ => a - def ++-assoc (xs ys zs : List A) : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) elim xs | [ ] => refl | x :< xs => pmap (x :<) (++-assoc xs ys zs) - private def rev'-map (f : A -> B) (buf xs : List A) : map f (rev' buf xs) = rev' (map f buf) (map f xs) elim xs | [ ] => refl | x :< xs => rev'-map f (x :< buf) xs def rev-map (f : A -> B) (xs : List A) : map f (rev xs) = rev (map f xs) => rev'-map f [ ] xs - private def rev'-++ (buf xs : List A) : rev' buf xs = rev xs ++ buf elim xs | [ ] => refl | x :< xs => @@ -51,7 +48,6 @@ private def rev'-++ (buf xs : List A) : rev' buf xs = rev xs ++ buf elim xs | step2 : (rev xs ++ [ x ]) ++ buf = rev xs ++ (x :< buf) := ++-assoc (rev xs) [ x ] buf in step0 <=> pinv step2 <=> pinv step1 - def rev-distrib-++ (xs ys : List A) : rev (xs ++ ys) = (rev ys ++ rev xs) elim xs | [ ] => refl | x :< xs => diff --git a/cli-impl/src/test/resources/shared/src/data/vec/base.aya b/cli-impl/src/test/resources/shared/src/data/vec/base.aya index 52959e9532..50de0a1397 100644 --- a/cli-impl/src/test/resources/shared/src/data/vec/base.aya +++ b/cli-impl/src/test/resources/shared/src/data/vec/base.aya @@ -1,6 +1,5 @@ open import prelude hiding (++) - open inductive Vec (n : Nat) (A : Type) elim n | 0 => [] | suc n => infixr :> A (Vec n A) diff --git a/cli-impl/src/test/resources/shared/src/data/vec/properties.aya b/cli-impl/src/test/resources/shared/src/data/vec/properties.aya index 8c134ab294..2c878a2e91 100644 --- a/cli-impl/src/test/resources/shared/src/data/vec/properties.aya +++ b/cli-impl/src/test/resources/shared/src/data/vec/properties.aya @@ -13,7 +13,6 @@ def ++-assoc (xs : Vec n A) (ys : Vec m A) (zs : Vec o A) | [] => refl | x :> xs' => pmapd _ (\i => x :>) (++-assoc xs' ys zs) - def vmap-distrib-++ (f : A -> B) (xs : Vec n A) (ys : Vec m A) : vmap f (xs ++ ys) = vmap f xs ++ vmap f ys elim xs | [] => refl | x :> xs => pmap (f x :>) (vmap-distrib-++ f xs ys) diff --git a/cli-impl/src/test/resources/shared/src/relation/binary/nat_cmp.aya b/cli-impl/src/test/resources/shared/src/relation/binary/nat_cmp.aya index edb158c750..2f04d2910f 100644 --- a/cli-impl/src/test/resources/shared/src/relation/binary/nat_cmp.aya +++ b/cli-impl/src/test/resources/shared/src/relation/binary/nat_cmp.aya @@ -54,7 +54,6 @@ def <=-case {a b : Nat} (p : a <= b) : Sum (a < b) (a = b) => | _ because reflect_false np => inr (some-lemma p np) } - def ¬<→>= {a b : Nat} (np : neg (a < b)) : a >= b | {_}, {0}, np => refl | {0}, {suc b}, np => exfalso (np refl) diff --git a/syntax/src/main/java/org/aya/generic/Suppress.java b/syntax/src/main/java/org/aya/generic/Suppress.java index 211b0da985..03aa0273f5 100644 --- a/syntax/src/main/java/org/aya/generic/Suppress.java +++ b/syntax/src/main/java/org/aya/generic/Suppress.java @@ -3,7 +3,7 @@ package org.aya.generic; public enum Suppress { - Shadowing, + LocalShadow, UnimportedCon, UnreachableClause, MostGeneralSolution; From c6d88260c0eeb099e8ac320bc8344785dbb6f270 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Mon, 30 Dec 2024 21:45:30 -0500 Subject: [PATCH 4/4] doc: javadoc --- .../main/java/org/aya/resolve/context/NoExportContext.java | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/context/NoExportContext.java b/base/src/main/java/org/aya/resolve/context/NoExportContext.java index c86d6f9001..0ba87c0af3 100644 --- a/base/src/main/java/org/aya/resolve/context/NoExportContext.java +++ b/base/src/main/java/org/aya/resolve/context/NoExportContext.java @@ -11,9 +11,7 @@ import java.nio.file.Path; -/** - * Used for `let open` - */ +/// Used for `let open` and `example` public record NoExportContext( @NotNull Context parent, @NotNull ModuleSymbol symbols,