suppress: clean after suppress, because scc tycker use the same `Stmt…

…Tycker`
aya-prover · Dec 21, 2024 · fbb6b46 · fbb6b46
1 parent 0982d59
commit fbb6b46
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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
@@ -21,4 +21,6 @@ public SuppressingReporter(@NotNull Reporter reporter) {
   public void suppress(@NotNull Class<? extends Problem> problem) {
     suppressed.add(problem);
   }
+
+  public void clearSuppress() { suppressed.clear(); }
 }