merge: Pretty Print and Highlight for Pragma (#1281)

base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java

@@ -147,21 +147,26 @@ else if (factory.isForbiddenRedefinition(primID, false))
   }
 
   private static Reporter suppress(@NotNull Reporter reporter, @NotNull Decl decl) {
-    if (decl.suppresses.isEmpty()) return reporter;
+    var suppressInfo = decl.pragmaInfo.suppressWarn;
+    if (suppressInfo == null) return reporter;
+
+    var suppresses = suppressInfo.args();
+    if (suppresses.isEmpty()) return reporter;
     var r = new SuppressingReporter(reporter);
-    decl.suppresses.forEach(suppress -> {
-      switch (suppress) {
+    suppresses.forEach(suppress -> {
+      switch (suppress.data()) {
         case LocalShadow -> r.suppress(NameProblem.ShadowingWarn.class);
       }
     });
+
     return r;
   }
 
   /**
    * pre-resolve children of {@param decl}
    *
    * @param decl          the top-level decl
-   * @param context       the context where {@paran decl} lives in
+   * @param context       the context where {@param decl} lives in
    * @param childrenGet   the children of {@param decl}
    * @param childResolver perform resolve on the child of {@param decl}
    * @return the module context of {@param decl}, it should be a sub-module of {@param context}

base/src/main/java/org/aya/tyck/StmtTycker.java

@@ -60,8 +60,11 @@ public StmtTycker(
     this(new SuppressingReporter(reporter), fileModule, shapeFactory, primFactory);
   }
   public void suppress(@NotNull Decl decl) {
-    decl.suppresses.forEach(suppress -> {
-      switch (suppress) {
+    var suppressInfo = decl.pragmaInfo.suppressWarn;
+    if (suppressInfo == null) return;
+
+    suppressInfo.args().forEach(suppress -> {
+      switch (suppress.data()) {
         case MostGeneralSolution -> reporter.suppress(MetaVarError.DidSomethingBad.class);
         case UnimportedCon -> reporter.suppress(PatternProblem.UnimportedConName.class);
         case UnreachableClause -> {

base/src/test/java/org/aya/syntax/concrete/SyntaxTest.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;
 
@@ -21,6 +21,7 @@ def foo (f : Type -> Type 0) (a : Type 0) =>
         [ f a ]
       def foo2 => ↑↑ foo
       def bar (A : Type 0) : A -> A => fn x => {? x ?}
+      @suppress(LocalShadow)
       open inductive Nat | O | S Nat
       open inductive Fin Nat
       | S n => FZ

cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.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.cli.literate;
 
@@ -137,6 +137,18 @@ else if (SPECIAL_SYMBOL.contains(tokenType))
     return kindOf(var).toRef(sourcePos, BasePrettier.linkIdOf(currentFileModule, var), type);
   }
 
+  private void visitPragma(@NotNull PragmaInfo pInfo) {
+    if (pInfo.suppressWarn != null) {
+      info.append(new Lit(pInfo.suppressWarn.sourcePos(), LitKind.Keyword));
+    }
+  }
+
+  @Override
+  public void accept(@NotNull Stmt stmt) {
+    if (stmt instanceof Decl decl) visitPragma(decl.pragmaInfo);
+    StmtVisitor.super.accept(stmt);
+  }
+
   public static @NotNull DefKind kindOf(@NotNull AnyVar var) {
     return switch (var) {
       case GeneralizedVar _ -> DefKind.Generalized;

cli-impl/src/test/resources/literate/hoshino-said.aya.md

@@ -7,6 +7,7 @@ variable Hoshino : Type
 So, `Hoshino -> Hoshino`() is a thing.
 
 ```aya
+@suppress(LocalShadow)
 inductive Nat | O | S Nat
 prim I : ISet
 prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type

producer/src/main/java/org/aya/producer/AyaProducer.java

@@ -9,8 +9,7 @@
 import com.intellij.psi.tree.TokenSet;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
-import kala.collection.mutable.MutableList;
-import kala.collection.mutable.MutableSinglyLinkedList;
+import kala.collection.mutable.*;
 import kala.control.Either;
 import kala.control.Option;
 import kala.function.BooleanObjBiFunction;
@@ -46,6 +45,8 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
+import java.util.Arrays;
+import java.util.Objects;
 import java.util.stream.Collectors;
 
 import static org.aya.parser.AyaPsiElementTypes.*;
@@ -293,19 +294,31 @@ private void pragma(GenericNode<?> node, Decl decl) {
     node.childrenOfType(PRAGMA).forEach(pragma -> {
       var nameToken = pragma.child(ID);
       var name = nameToken.tokenText().toString();
+      var namePos = sourcePosOf(nameToken);
       var argsNode = pragma.peekChild(COMMA_SEP);
       var args = argsNode != null ? argsNode.childrenOfType(ID) : SeqView.<GenericNode<?>>empty();
+
       switch (name) {
-        case "suppress" -> args.forEach(arg -> {
-          for (var suppress : Suppress.values()) {
-            if (arg.tokenText().contentEquals(suppress.name())) {
-              decl.suppresses.add(suppress);
-              return;
+        case Constants.PRAGMA_SUPPRESS -> {
+          // TODO: use MutableEnumSet
+          MutableList<WithPos<Suppress>> sups = FreezableMutableList.create();
+
+          for (var arg : args) {
+            var resolved = Arrays.stream(Suppress.values())
+              .filter(x -> arg.tokenText().contentEquals(x.name()))
+              .findFirst()
+              .orElse(null);
+
+            if (resolved == null) {
+              reporter.report(new BadXWarn.BadWarnWarn(sourcePosOf(arg), arg.tokenText().toString()));
+            } else {
+              sups.append(new WithPos<>(sourcePosOf(arg), resolved));
             }
           }
-          reporter.report(new BadXWarn.BadWarnWarn(sourcePosOf(arg), arg.tokenText().toString()));
-        });
-        default -> reporter.report(new BadXWarn.BadPragmaWarn(sourcePosOf(nameToken), name));
+
+          decl.pragmaInfo.suppressWarn = new PragmaInfo.SuppressWarn(namePos, sups.toImmutableSeq());
+        }
+        default -> reporter.report(new BadXWarn.BadPragmaWarn(namePos, name));
       }
     });
   }

syntax/src/main/java/org/aya/generic/Constants.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.generic;
 
@@ -23,6 +23,8 @@ public interface Constants {
   @NotNull @NonNls String AYAC_POSTFIX = ".ayac";
   @NotNull @NonNls String AYA_JSON = "aya.json";
 
+  @NotNull @NonNls String PRAGMA_SUPPRESS = "suppress";
+
   @NotNull @NonNls String ALTERNATIVE_EMPTY = "empty";
   @NotNull @NonNls String ALTERNATIVE_OR = "<|>";
   @NotNull @NonNls String APPLICATIVE_APP = "<*>";

syntax/src/main/java/org/aya/prettier/ConcretePrettier.java

@@ -7,6 +7,7 @@
 import kala.collection.SeqLike;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
+import kala.collection.mutable.MutableEnumSet;
 import kala.collection.mutable.MutableList;
 import kala.range.primitive.IntRange;
 import org.aya.generic.Constants;
@@ -24,6 +25,7 @@
 import org.aya.syntax.ref.DefVar;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.util.Arg;
+import org.aya.util.IterableUtil;
 import org.aya.util.binop.Assoc;
 import org.aya.util.error.WithPos;
 import org.aya.util.prettier.PrettierOptions;
@@ -320,8 +322,26 @@ private Doc visitAccess(@NotNull Accessibility acc, @Nullable Accessibility theD
     };
   }
 
+  private @NotNull Doc doPragma(@NotNull Doc name, @NotNull Doc args) {
+    return Doc.cat(AT, name, Doc.parened(args));
+  }
+
+  public @NotNull Doc pragma(@NotNull PragmaInfo info) {
+    var lines = MutableList.<Doc>create();
+
+    if (info.suppressWarn != null) {
+      var args = info.suppressWarn.args().view()
+        .map(x -> Doc.plain(x.data().name()));
+
+      lines.append(doPragma(Doc.styled(KEYWORD, Constants.PRAGMA_SUPPRESS), Doc.commaList(args)));
+    }
+
+    return Doc.vcat(lines);
+  }
+
   public @NotNull Doc decl(@NotNull Decl predecl) {
-    return switch (predecl) {
+    var pragma = pragma(predecl.pragmaInfo);
+    var declDoc = switch (predecl) {
       case ClassDecl decl -> {
         var prelude = MutableList.of(KW_CLASS);
         prelude.append(defVar(decl.ref));
@@ -377,6 +397,8 @@ private Doc visitAccess(@NotNull Accessibility acc, @Nullable Accessibility theD
       }
       case PrimDecl primDecl -> primDoc(primDecl.ref);
     };
+
+    return Doc.vcatNonEmpty(pragma, declDoc);
   }
 
   private @NotNull MutableList<Doc> declPrelude(@NotNull Decl decl) {

syntax/src/main/java/org/aya/prettier/Tokens.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.prettier;
 
@@ -29,6 +29,7 @@ private Tokens() {
   public static final Doc LIST_LEFT = Doc.symbol("[");
   public static final Doc LIST_RIGHT = Doc.symbol("]");
   public static final Doc EQ = Doc.symbol("=");
+  public static final Doc AT = Doc.symbol("@");
 
   public static final Doc KW_DO = Doc.styled(KEYWORD, "do");
   public static final Doc KW_AS = Doc.styled(KEYWORD, "as");

syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/Decl.java

@@ -1,7 +1,9 @@
-// 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.decl;
 
+import kala.collection.mutable.MutableEnumSet;
+import kala.collection.mutable.MutableSet;
 import org.aya.generic.Suppress;
 import org.aya.generic.stmt.TyckUnit;
 import org.aya.syntax.concrete.stmt.BindBlock;
@@ -27,7 +29,8 @@ public sealed abstract class Decl implements SourceNode, Stmt, TyckUnit, OpDecl
   permits ClassDecl, TeleDecl {
   public @NotNull DeclInfo info;
   public boolean isExample;
-  public EnumSet<Suppress> suppresses = EnumSet.noneOf(Suppress.class);
+  public @NotNull PragmaInfo pragmaInfo = new PragmaInfo();
+  public @NotNull Object suppresses = null;
 
   public final @NotNull BindBlock bindBlock() { return info.bindBlock(); }
   public final @NotNull SourcePos entireSourcePos() { return info.entireSourcePos(); }

syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/PragmaInfo.java

@@ -0,0 +1,22 @@
+// 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.decl;
+
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.generic.Suppress;
+import org.aya.util.error.SourcePos;
+import org.aya.util.error.WithPos;
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+
+public class PragmaInfo {
+  /// @param sourcePos the name, not the whole pragma
+  public record SuppressWarn(@NotNull SourcePos sourcePos, @NotNull ImmutableSeq<WithPos<Suppress>> args) {
+  }
+
+  public @Nullable SuppressWarn suppressWarn = null;
+
+  public PragmaInfo() {
+  }
+}