From 388f2a31fc2e62849a2d0bc55c613bd9c502d473 Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sun, 22 Dec 2024 04:01:09 +0800 Subject: [PATCH 1/6] pat: warning when unimported constructor name --- .../org/aya/tyck/error/PatternProblem.java | 14 +++++++ .../java/org/aya/tyck/pat/PatternTycker.java | 16 +++++++- .../org/aya/test/fixtures/PatTyckError.java | 8 ++++ .../test/resources/negative/PatTyckError.txt | 37 +++++++++++++++++++ 4 files changed, 74 insertions(+), 1 deletion(-) diff --git a/base/src/main/java/org/aya/tyck/error/PatternProblem.java b/base/src/main/java/org/aya/tyck/error/PatternProblem.java index 157c472cd..551c74cb8 100644 --- a/base/src/main/java/org/aya/tyck/error/PatternProblem.java +++ b/base/src/main/java/org/aya/tyck/error/PatternProblem.java @@ -126,6 +126,20 @@ record ImplicitDisallowed(@Override @NotNull WithPos pattern) implement } } + record UnimportedConName( + @Override @NotNull WithPos pattern + ) implements PatternProblem { + @Override + public @NotNull Doc describe(@NotNull PrettierOptions options) { + return Doc.vcat( + Doc.english("The binding name:"), + Doc.par(1, Doc.plain(pattern.data().bind().name())), + Doc.english("is equal to an un-imported constructor of:"), + Doc.par(1, pattern.data().type().get().toDoc(options)) + ); + } + } + record TooManyImplicitPattern( @Override @NotNull WithPos pattern, @NotNull Param param diff --git a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java index 831754996..2890f68c6 100644 --- a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java +++ b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java @@ -147,9 +147,23 @@ public record TyckResult( var typeRecog = state().shapeFactory.find(conCore.dataRef()).getOrNull(); yield new Pat.Con(conCore, patterns, realCon.conHead); } - case Pattern.Bind(var bind, var tyRef) -> { + case Pattern.Bind bindPat -> { + var bind = bindPat.bind(); + var tyRef = bindPat.type(); + exprTycker.localCtx().put(bind, type); tyRef.set(type); + + // report after tyRef.set, the error message requires it + if (whnf(type) instanceof DataCall call) { + var unimportedCon = call.ref().body() + .filter(con -> con.name().equals(bind.name())); + + if (unimportedCon.isNotEmpty()) { + fail(new PatternProblem.UnimportedConName(pattern.replace(bindPat))); + } + } + yield new Pat.Bind(bind, type); } case Pattern.CalmFace.INSTANCE -> diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java b/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java index 5bc555b90..4d6b800e7 100644 --- a/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java +++ b/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java @@ -106,4 +106,12 @@ open inductive Wrap (A B : Type) def foo (A : Type) A : A elim A | _, {a} => a """; + + @Language("Aya") String testUnimportedCon = """ + open import arith::bool using (Bool) + + def not (b : Bool) : Bool + | true => Bool::false + | false => Bool::true + """; } diff --git a/cli-impl/src/test/resources/negative/PatTyckError.txt b/cli-impl/src/test/resources/negative/PatTyckError.txt index 78e37b20d..17472a8e5 100644 --- a/cli-impl/src/test/resources/negative/PatTyckError.txt +++ b/cli-impl/src/test/resources/negative/PatTyckError.txt @@ -270,3 +270,40 @@ Error: Pattern matching with elim is not compatible with implicit patterns. 1 error(s), 0 warning(s). Let's learn from that. +UnimportedCon: +In file $FILE:4:2 -> + + 2 │ + 3 │ def not (b : Bool) : Bool + 4 │ | true => Bool::false + │ ╰──╯ + +Error: The binding name: + true + is equal to an un-imported constructor of: + Bool + +In file $FILE:5:2 -> + + 3 │ def not (b : Bool) : Bool + 4 │ | true => Bool::false + 5 │ | false => Bool::true + │ ╰───╯ + +Error: The binding name: + false + is equal to an un-imported constructor of: + Bool + +In file $FILE:5:2 -> + + 3 │ def not (b : Bool) : Bool + 4 │ | true => Bool::false + 5 │ | false => Bool::true + │ ╰─────────────────╯ + +Warning: The 2nd clause is dominated by the other clauses, hence unreachable + +2 error(s), 1 warning(s). +Let's learn from that. + From 19dfbfde7880e4e16a8b53d09a56b19a82538cd3 Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sun, 22 Dec 2024 04:26:03 +0800 Subject: [PATCH 2/6] pat: better impl in case of ind-ind --- .../org/aya/tyck/error/PatternProblem.java | 5 +++++ .../java/org/aya/tyck/pat/PatternTycker.java | 22 ++++++++++++++----- 2 files changed, 22 insertions(+), 5 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/error/PatternProblem.java b/base/src/main/java/org/aya/tyck/error/PatternProblem.java index 551c74cb8..05166fcc0 100644 --- a/base/src/main/java/org/aya/tyck/error/PatternProblem.java +++ b/base/src/main/java/org/aya/tyck/error/PatternProblem.java @@ -129,6 +129,11 @@ record ImplicitDisallowed(@Override @NotNull WithPos pattern) implement record UnimportedConName( @Override @NotNull WithPos pattern ) implements PatternProblem { + @Override + public @NotNull Severity level() { + return Severity.WARN; + } + @Override public @NotNull Doc describe(@NotNull PrettierOptions options) { return Doc.vcat( diff --git a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java index 2890f68c6..49082de58 100644 --- a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java +++ b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java @@ -13,11 +13,12 @@ import org.aya.generic.term.DTKind; import org.aya.normalize.Normalizer; import org.aya.syntax.compile.JitCon; +import org.aya.syntax.compile.JitData; import org.aya.syntax.concrete.Expr; import org.aya.syntax.concrete.Pattern; +import org.aya.syntax.concrete.stmt.decl.DataDecl; import org.aya.syntax.core.Jdg; -import org.aya.syntax.core.def.ConDef; -import org.aya.syntax.core.def.ConDefLike; +import org.aya.syntax.core.def.*; import org.aya.syntax.core.pat.Pat; import org.aya.syntax.core.pat.PatMatcher; import org.aya.syntax.core.pat.PatToTerm; @@ -156,10 +157,10 @@ public record TyckResult( // report after tyRef.set, the error message requires it if (whnf(type) instanceof DataCall call) { - var unimportedCon = call.ref().body() - .filter(con -> con.name().equals(bind.name())); + var unimportedCon = collectConNames(call.ref()) + .anyMatch(it -> it.equals(bind.name())); - if (unimportedCon.isNotEmpty()) { + if (unimportedCon) { fail(new PatternProblem.UnimportedConName(pattern.replace(bindPat))); } } @@ -479,6 +480,17 @@ private record Selection( }; } + private static @NotNull SeqView collectConNames(@NotNull DataDefLike call) { + return switch (call) { + case JitData jitData -> jitData.body().view().map(AnyDef::name); + case DataDef.Delegate delegate -> { + // the core may be unchecked! + var concrete = (DataDecl) delegate.ref.concrete; + yield concrete.body.view().map(it -> it.ref.name()); + } + }; + } + /** * Check whether {@param con} is available under {@param type} */ From 1365389b38d2248a5fe1a28d744b90c7753c9e21 Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sun, 22 Dec 2024 04:29:06 +0800 Subject: [PATCH 3/6] test: update fixture and add more cases --- .../org/aya/test/fixtures/PatTyckError.java | 3 ++ .../test/resources/negative/PatTyckError.txt | 31 +++++++++++++------ 2 files changed, 24 insertions(+), 10 deletions(-) diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java b/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java index 4d6b800e7..1a266692a 100644 --- a/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java +++ b/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java @@ -113,5 +113,8 @@ def foo (A : Type) A : A elim A def not (b : Bool) : Bool | true => Bool::false | false => Bool::true + + inductive RealCase (b : Bool) + | true => real_true """; } diff --git a/cli-impl/src/test/resources/negative/PatTyckError.txt b/cli-impl/src/test/resources/negative/PatTyckError.txt index 17472a8e5..3198e87cc 100644 --- a/cli-impl/src/test/resources/negative/PatTyckError.txt +++ b/cli-impl/src/test/resources/negative/PatTyckError.txt @@ -278,10 +278,10 @@ In file $FILE:4:2 -> 4 │ | true => Bool::false │ ╰──╯ -Error: The binding name: - true - is equal to an un-imported constructor of: - Bool +Warning: The binding name: + true + is equal to an un-imported constructor of: + Bool In file $FILE:5:2 -> @@ -290,10 +290,10 @@ In file $FILE:5:2 -> 5 │ | false => Bool::true │ ╰───╯ -Error: The binding name: - false - is equal to an un-imported constructor of: - Bool +Warning: The binding name: + false + is equal to an un-imported constructor of: + Bool In file $FILE:5:2 -> @@ -304,6 +304,17 @@ In file $FILE:5:2 -> Warning: The 2nd clause is dominated by the other clauses, hence unreachable -2 error(s), 1 warning(s). -Let's learn from that. +In file $FILE:8:2 -> + + 6 │ + 7 │ inductive RealCase (b : Bool) + 8 │ | true => real_true + │ ╰──╯ + +Warning: The binding name: + true + is equal to an un-imported constructor of: + Bool + +That looks right! From ff50258d6f33ae3dd0c4282f7bce7b220bfda0d8 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sat, 21 Dec 2024 17:00:45 -0500 Subject: [PATCH 4/6] error: write a longer error message --- .../org/aya/tyck/error/PatternProblem.java | 32 +++++++++++-------- .../java/org/aya/tyck/pat/PatternTycker.java | 5 ++- .../test/resources/negative/PatTyckError.txt | 18 +++++------ 3 files changed, 29 insertions(+), 26 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/error/PatternProblem.java b/base/src/main/java/org/aya/tyck/error/PatternProblem.java index 05166fcc0..8bc3114c7 100644 --- a/base/src/main/java/org/aya/tyck/error/PatternProblem.java +++ b/base/src/main/java/org/aya/tyck/error/PatternProblem.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.tyck.error; +import kala.collection.mutable.MutableList; import org.aya.prettier.BasePrettier; import org.aya.pretty.doc.Doc; import org.aya.syntax.concrete.Pattern; @@ -9,6 +10,7 @@ import org.aya.syntax.core.term.Term; import org.aya.syntax.core.term.call.ConCall; import org.aya.syntax.core.term.call.DataCall; +import org.aya.tyck.tycker.Stateful; import org.aya.util.error.SourcePos; import org.aya.util.error.WithPos; import org.aya.util.prettier.PrettierOptions; @@ -80,15 +82,21 @@ record UnknownCon(@Override @NotNull WithPos pattern) implements Patter record TupleNonSig( @Override @NotNull WithPos pattern, - @NotNull Term type + @NotNull Stateful stateful, @NotNull Term type ) implements PatternProblem { @Override public @NotNull Doc describe(@NotNull PrettierOptions options) { - return Doc.vcat( + var typeDoc = type.toDoc(options); + var lines = MutableList.of( Doc.english("The tuple pattern"), Doc.par(1, pattern.data().toDoc(options)), - Doc.english("splits only on sigma types, while the actual type"), - Doc.par(1, type.toDoc(options)), - Doc.english("does not look like one")); + Doc.english("splits only on sigma types, while the actual type is not:"), + Doc.par(1, typeDoc)); + var normalizedDoc = stateful.fullNormalize(type).toDoc(options); + if (!typeDoc.equals(normalizedDoc)) { + lines.append(Doc.english("Normalized:")); + lines.append(Doc.par(1, normalizedDoc)); + } + return Doc.vcat(lines); } } @@ -129,18 +137,14 @@ record ImplicitDisallowed(@Override @NotNull WithPos pattern) implement record UnimportedConName( @Override @NotNull WithPos pattern ) implements PatternProblem { - @Override - public @NotNull Severity level() { - return Severity.WARN; - } + @Override public @NotNull Severity level() { return Severity.WARN; } - @Override - public @NotNull Doc describe(@NotNull PrettierOptions options) { + @Override public @NotNull Doc describe(@NotNull PrettierOptions options) { return Doc.vcat( - Doc.english("The binding name:"), + Doc.english("You wrote the following pattern:"), Doc.par(1, Doc.plain(pattern.data().bind().name())), - Doc.english("is equal to an un-imported constructor of:"), - Doc.par(1, pattern.data().type().get().toDoc(options)) + Doc.english("It sounds like you are trying to match with a constructor that is not in scope," + + "so it will be treated as a variable pattern.") ); } } diff --git a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java index 49082de58..e21dda4c0 100644 --- a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java +++ b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java @@ -128,7 +128,7 @@ public record TyckResult( case Pattern.Tuple(var l, var r) -> { if (!(exprTycker.whnf(type) instanceof DepTypeTerm(var kind, var lT, var rT) && kind == DTKind.Sigma)) { var frozen = freezeHoles(type); - yield withError(new PatternProblem.TupleNonSig(pattern, frozen), frozen); + yield withError(new PatternProblem.TupleNonSig(pattern, this, frozen), frozen); } var lhs = doTyck(l, lT); yield new Pat.Tuple(lhs, doTyck(r, rT.apply(PatToTerm.visit(lhs)))); @@ -158,8 +158,7 @@ public record TyckResult( // report after tyRef.set, the error message requires it if (whnf(type) instanceof DataCall call) { var unimportedCon = collectConNames(call.ref()) - .anyMatch(it -> it.equals(bind.name())); - + .anyMatch(it -> it.equalsIgnoreCase(bind.name())); if (unimportedCon) { fail(new PatternProblem.UnimportedConName(pattern.replace(bindPat))); } diff --git a/cli-impl/src/test/resources/negative/PatTyckError.txt b/cli-impl/src/test/resources/negative/PatTyckError.txt index 3198e87cc..1a8231c54 100644 --- a/cli-impl/src/test/resources/negative/PatTyckError.txt +++ b/cli-impl/src/test/resources/negative/PatTyckError.txt @@ -278,10 +278,10 @@ In file $FILE:4:2 -> 4 │ | true => Bool::false │ ╰──╯ -Warning: The binding name: +Warning: You wrote the following pattern: true - is equal to an un-imported constructor of: - Bool + It sounds like you are trying to match with a constructor that is not + in scope,so it will be treated as a variable pattern. In file $FILE:5:2 -> @@ -290,10 +290,10 @@ In file $FILE:5:2 -> 5 │ | false => Bool::true │ ╰───╯ -Warning: The binding name: +Warning: You wrote the following pattern: false - is equal to an un-imported constructor of: - Bool + It sounds like you are trying to match with a constructor that is not + in scope,so it will be treated as a variable pattern. In file $FILE:5:2 -> @@ -311,10 +311,10 @@ In file $FILE:8:2 -> 8 │ | true => real_true │ ╰──╯ -Warning: The binding name: +Warning: You wrote the following pattern: true - is equal to an un-imported constructor of: - Bool + It sounds like you are trying to match with a constructor that is not + in scope,so it will be treated as a variable pattern. That looks right! From 0982d5901bc70ed0c5973d67f365441f44a8306c Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sat, 21 Dec 2024 17:12:07 -0500 Subject: [PATCH 5/6] error: extra space --- .../main/java/org/aya/tyck/StmtTycker.java | 5 +++ .../org/aya/tyck/error/PatternProblem.java | 2 +- .../org/aya/test/fixtures/PatTyckError.java | 9 +++++ .../test/resources/negative/PatTyckError.txt | 36 +++++++++++++++++-- .../main/java/org/aya/generic/Suppress.java | 2 ++ .../util/reporter/SuppressingReporter.java | 8 ++--- 6 files changed, 54 insertions(+), 8 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java index 0c0a13b7d..ddbe09e58 100644 --- a/base/src/main/java/org/aya/tyck/StmtTycker.java +++ b/base/src/main/java/org/aya/tyck/StmtTycker.java @@ -62,6 +62,11 @@ public void suppress(@NotNull Decl decl) { decl.suppresses.forEach(suppress -> { switch (suppress) { case MostGeneralSolution -> reporter.suppress(MetaVarError.DidSomethingBad.class); + case UnimportedCon -> reporter.suppress(PatternProblem.UnimportedConName.class); + case UnreachableClause -> { + reporter.suppress(ClausesProblem.FMDomination.class); + reporter.suppress(ClausesProblem.Domination.class); + } } }); } diff --git a/base/src/main/java/org/aya/tyck/error/PatternProblem.java b/base/src/main/java/org/aya/tyck/error/PatternProblem.java index 8bc3114c7..e45231d69 100644 --- a/base/src/main/java/org/aya/tyck/error/PatternProblem.java +++ b/base/src/main/java/org/aya/tyck/error/PatternProblem.java @@ -143,7 +143,7 @@ record UnimportedConName( return Doc.vcat( Doc.english("You wrote the following pattern:"), Doc.par(1, Doc.plain(pattern.data().bind().name())), - Doc.english("It sounds like you are trying to match with a constructor that is not in scope," + + Doc.english("It sounds like you are trying to match with a constructor that is not in scope, " + "so it will be treated as a variable pattern.") ); } diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java b/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java index 1a266692a..f70b650d6 100644 --- a/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java +++ b/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java @@ -36,6 +36,15 @@ def test (a : Type) : Type | unit y => a """; + @Language("Aya") String testTupleOnNonSigma = """ + def test (a' : Type) : Type + | (a, b) => a + + def Alias => Type + def test2 (a' : Alias) : Type + | (a, b) => a + """; + @Language("Aya") String testBadLiteral = """ open inductive Test | t def not-conf Test : Test diff --git a/cli-impl/src/test/resources/negative/PatTyckError.txt b/cli-impl/src/test/resources/negative/PatTyckError.txt index 1a8231c54..b662e1d22 100644 --- a/cli-impl/src/test/resources/negative/PatTyckError.txt +++ b/cli-impl/src/test/resources/negative/PatTyckError.txt @@ -71,6 +71,36 @@ Error: Cannot split on a non-inductive type 1 error(s), 0 warning(s). Let's learn from that. +TupleOnNonSigma: +In file $FILE:2:3 -> + + 1 │ def test (a' : Type) : Type + 2 │ | (a, b) => a + │ ╰────╯ + 3 │ + +Error: The tuple pattern + (a, b) + splits only on sigma types, while the actual type is not: + Type 0 + +In file $FILE:6:3 -> + + 4 │ def Alias => Type + 5 │ def test2 (a' : Alias) : Type + 6 │ | (a, b) => a + │ ╰────╯ + +Error: The tuple pattern + (a, b) + splits only on sigma types, while the actual type is not: + Alias + Normalized: + Type 0 + +2 error(s), 0 warning(s). +Let's learn from that. + BadLiteral: In file $FILE:3:2 -> @@ -281,7 +311,7 @@ In file $FILE:4:2 -> Warning: You wrote the following pattern: true It sounds like you are trying to match with a constructor that is not - in scope,so it will be treated as a variable pattern. + in scope, so it will be treated as a variable pattern. In file $FILE:5:2 -> @@ -293,7 +323,7 @@ In file $FILE:5:2 -> Warning: You wrote the following pattern: false It sounds like you are trying to match with a constructor that is not - in scope,so it will be treated as a variable pattern. + in scope, so it will be treated as a variable pattern. In file $FILE:5:2 -> @@ -314,7 +344,7 @@ In file $FILE:8:2 -> Warning: You wrote the following pattern: true It sounds like you are trying to match with a constructor that is not - in scope,so it will be treated as a variable pattern. + in scope, so it will be treated as a variable pattern. That looks right! diff --git a/syntax/src/main/java/org/aya/generic/Suppress.java b/syntax/src/main/java/org/aya/generic/Suppress.java index b413a98d6..211b0da98 100644 --- a/syntax/src/main/java/org/aya/generic/Suppress.java +++ b/syntax/src/main/java/org/aya/generic/Suppress.java @@ -4,5 +4,7 @@ public enum Suppress { Shadowing, + UnimportedCon, + UnreachableClause, MostGeneralSolution; } diff --git a/tools/src/main/java/org/aya/util/reporter/SuppressingReporter.java b/tools/src/main/java/org/aya/util/reporter/SuppressingReporter.java index b2045708a..361bebfa5 100644 --- a/tools/src/main/java/org/aya/util/reporter/SuppressingReporter.java +++ b/tools/src/main/java/org/aya/util/reporter/SuppressingReporter.java @@ -2,15 +2,15 @@ // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.util.reporter; -import kala.collection.mutable.MutableList; +import kala.collection.mutable.MutableSet; import org.jetbrains.annotations.NotNull; public record SuppressingReporter( @NotNull Reporter reporter, - @NotNull MutableList> suppressed + @NotNull MutableSet> suppressed ) implements Reporter { public SuppressingReporter(@NotNull Reporter reporter) { - this(reporter, MutableList.create()); + this(reporter, MutableSet.create()); } @Override public void report(@NotNull Problem problem) { @@ -19,6 +19,6 @@ public SuppressingReporter(@NotNull Reporter reporter) { } public void suppress(@NotNull Class problem) { - suppressed.append(problem); + suppressed.add(problem); } } From fbb6b46df6cad618302be833b5e1ef0c46cd4f00 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sat, 21 Dec 2024 17:20:44 -0500 Subject: [PATCH 6/6] suppress: clean after suppress, because scc tycker use the same `StmtTycker` --- base/src/main/java/org/aya/tyck/StmtTycker.java | 7 +++++-- .../test/java/org/aya/test/fixtures/PatTyckError.java | 5 +++++ cli-impl/src/test/resources/negative/PatTyckError.txt | 10 +++++----- .../org/aya/util/reporter/SuppressingReporter.java | 2 ++ 4 files changed, 17 insertions(+), 7 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java index ddbe09e58..6356e2eba 100644 --- a/base/src/main/java/org/aya/tyck/StmtTycker.java +++ b/base/src/main/java/org/aya/tyck/StmtTycker.java @@ -71,13 +71,13 @@ public void suppress(@NotNull Decl decl) { }); } public @Nullable TyckDef check(@NotNull Decl predecl) { - suppress(predecl); ExprTycker tycker = null; if (predecl instanceof TeleDecl decl) { if (decl.ref().signature == null) tycker = checkHeader(decl); } - return switch (predecl) { + suppress(predecl); + var core = switch (predecl) { case FnDecl fnDecl -> { var fnRef = fnDecl.ref; assert fnRef.signature != null; @@ -141,6 +141,8 @@ yield switch (fnDecl.body) { yield new DataDef(data.ref, data.body.map(kon -> kon.ref.core)); } }; + reporter.clearSuppress(); + return core; } public ExprTycker checkHeader(@NotNull TeleDecl decl) { @@ -181,6 +183,7 @@ else fail(BadTypeError.doNotLike(tycker.state, result, signature.result(), } } } + reporter.clearSuppress(); return tycker; } private void checkMember(@NotNull ClassMember member, @NotNull ExprTycker tycker) { diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java b/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java index f70b650d6..0155a937f 100644 --- a/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java +++ b/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java @@ -123,6 +123,11 @@ def not (b : Bool) : Bool | true => Bool::false | false => Bool::true + @suppress(UnimportedCon, UnreachableClause) + def don't-care (b : Bool) : Bool + | true => Bool::false + | false => Bool::true + inductive RealCase (b : Bool) | true => real_true """; diff --git a/cli-impl/src/test/resources/negative/PatTyckError.txt b/cli-impl/src/test/resources/negative/PatTyckError.txt index b662e1d22..6ca6296e1 100644 --- a/cli-impl/src/test/resources/negative/PatTyckError.txt +++ b/cli-impl/src/test/resources/negative/PatTyckError.txt @@ -334,12 +334,12 @@ In file $FILE:5:2 -> Warning: The 2nd clause is dominated by the other clauses, hence unreachable -In file $FILE:8:2 -> +In file $FILE:13:2 -> - 6 │ - 7 │ inductive RealCase (b : Bool) - 8 │ | true => real_true - │ ╰──╯ + 11 │ + 12 │ inductive RealCase (b : Bool) + 13 │ | true => real_true + │ ╰──╯ Warning: You wrote the following pattern: true diff --git a/tools/src/main/java/org/aya/util/reporter/SuppressingReporter.java b/tools/src/main/java/org/aya/util/reporter/SuppressingReporter.java index 361bebfa5..ce2dfc65a 100644 --- a/tools/src/main/java/org/aya/util/reporter/SuppressingReporter.java +++ b/tools/src/main/java/org/aya/util/reporter/SuppressingReporter.java @@ -21,4 +21,6 @@ public SuppressingReporter(@NotNull Reporter reporter) { public void suppress(@NotNull Class problem) { suppressed.add(problem); } + + public void clearSuppress() { suppressed.clear(); } }