diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
index 2c60639d3b7..2e52e5e7c73 100644
--- a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
+++ b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
@@ -2013,7 +2013,10 @@ private void convert(
for (Tuple2<Tuple2<Att.Key, String>, ?> attribute :
// Sort to stabilize error messages
- stream(att.att()).sorted(Comparator.comparing(Tuple2::toString)).toList()) {
+ stream(att.att())
+ .filter(e -> e._1._1.shouldEmit())
+ .sorted(Comparator.comparing(Tuple2::toString))
+ .toList()) {
Att.Key key = attribute._1._1;
String strKey = key.key();
String clsName = attribute._1._2;
diff --git a/kore/src/main/java/org/kframework/attributes/Attribute.java b/kore/src/main/java/org/kframework/attributes/Attribute.java
new file mode 100644
index 00000000000..7bc222fbe1d
--- /dev/null
+++ b/kore/src/main/java/org/kframework/attributes/Attribute.java
@@ -0,0 +1,45 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+package org.kframework.attributes;
+
+import com.google.common.collect.Sets;
+import java.util.Arrays;
+import java.util.EnumSet;
+
+public abstract class Attribute {
+
+ public enum Syntax {
+ CELL,
+ CLAIM,
+ CONTEXT,
+ CONTEXT_ALIAS,
+ MODULE,
+ PRODUCTION,
+ RULE,
+ SENTENCE,
+ SYNTAX_SORT,
+ UNCHECKED
+ }
+
+ public sealed interface Visibility {
+ record User(EnumSet<Syntax> allowedSyntax) implements Visibility {
+ User(Syntax... allowed) {
+ this(Sets.newEnumSet(Arrays.asList(allowed), Syntax.class));
+ }
+ }
+
+ record Internal() implements Visibility {}
+ }
+
+ public enum EmitToKORE {
+ YES,
+ NO
+ }
+
+ public final Visibility visibility;
+ public final EmitToKORE emit;
+
+ protected Attribute(Visibility visibility, EmitToKORE emit) {
+ this.visibility = visibility;
+ this.emit = emit;
+ }
+}
diff --git a/kore/src/main/java/org/kframework/attributes/ClassSet.java b/kore/src/main/java/org/kframework/attributes/ClassSet.java
new file mode 100644
index 00000000000..4b9454d4854
--- /dev/null
+++ b/kore/src/main/java/org/kframework/attributes/ClassSet.java
@@ -0,0 +1,34 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+package org.kframework.attributes;
+
+import java.util.Objects;
+import java.util.Optional;
+import org.pcollections.HashPMap;
+
+public class ClassSet<U> {
+
+ public final HashPMap<Class<? extends U>, Object> data;
+
+ private ClassSet(HashPMap<Class<? extends U>, Object> data) {
+ this.data = data;
+ }
+
+ public <T extends U> ClassSet<U> add(Class<T> elemClass, T elem) {
+ return new ClassSet<>(data.plus(elemClass, elem));
+ }
+
+ public <T extends U> Optional<T> get(Class<T> elemClass) {
+ if (!data.containsKey(elemClass)) {
+ return Optional.empty();
+ }
+ return Optional.of(Objects.requireNonNull(elemClass.cast(data.get(elemClass))));
+ }
+
+ public <T extends U> boolean contains(Class<T> elemClass) {
+ return data.containsKey(elemClass);
+ }
+
+ public <T extends U> ClassSet<U> remove(Class<T> elemClass) {
+ return new ClassSet<>(data.minus(elemClass));
+ }
+}
diff --git a/kore/src/main/java/org/kframework/attributes/JavaAtt.java b/kore/src/main/java/org/kframework/attributes/JavaAtt.java
new file mode 100644
index 00000000000..b6d8027be11
--- /dev/null
+++ b/kore/src/main/java/org/kframework/attributes/JavaAtt.java
@@ -0,0 +1,834 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+package org.kframework.attributes;
+
+import com.google.common.collect.ImmutableSet;
+import java.util.Arrays;
+import java.util.Optional;
+import java.util.Set;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+import org.kframework.utils.errorsystem.KEMException;
+import scala.util.Either;
+import scala.util.Left;
+
+public class JavaAtt {
+ public record Key<T>(
+ Class<T> type,
+ String key,
+ Function<Optional<String>, Either<ParseError, Attribute>> parser) {}
+
+ public class MyAtt {}
+ ;
+
+ public static class Whitelist {
+ public static final Key<MyAtt> FOO_1 = new Key<>(MyAtt.class, "foo", s -> null);
+ public static final Key<MyAtt> FOO_2 = new Key<>(MyAtt.class, "foo", s -> null);
+ }
+
+ public static final ImmutableSet<Key<?>> whitelist =
+ Arrays.stream(JavaAtt.Whitelist.class.getDeclaredFields())
+ .map(
+ f -> {
+ try {
+ return (Key<?>) f.get(null);
+ } catch (IllegalAccessException e) {
+ throw KEMException.internalError(
+ "Malformed Att.Whitelist field: "
+ + f.getName()
+ + "\nExpected `public static final Key<MyAtt> MY_ATT = new Key<>(...)`");
+ }
+ })
+ .collect(ImmutableSet.toImmutableSet());
+
+ static {
+ String dupKeysErr =
+ whitelist.stream().collect(Collectors.groupingBy(Key::key)).entrySet().stream()
+ .filter(e -> e.getValue().size() > 1)
+ .map(
+ e ->
+ "\""
+ + e.getKey()
+ + "\": "
+ + e.getValue().stream().map(k -> k.type.getSimpleName()).toList())
+ .collect(Collectors.joining("\n"));
+ if (!dupKeysErr.isEmpty()) {
+ throw KEMException.internalError("Found duplicate keys in Att.Whitelist!\n" + dupKeysErr);
+ }
+ }
+
+ public sealed interface ParseError {
+ record UnrecognizedKey(String key) implements ParseError {}
+
+ record BadValue(KEMException e) implements ParseError {}
+ }
+
+ public static Either<ParseError, Attribute> parse(String key, Optional<String> value) {
+ Set<Key<?>> keys =
+ whitelist.stream().filter(k -> k.key.equals(key)).collect(Collectors.toSet());
+ if (keys.size() > 1) {
+ throw new AssertionError(
+ "Attribute "
+ + key
+ + value.map(v -> "(" + v + ")").orElse("")
+ + " parsed by multiple Att.Whitelist keys: "
+ + keys.stream().map(p -> p.type.getSimpleName()).toList());
+ }
+ if (keys.isEmpty()) {
+ return Left.apply(new ParseError.UnrecognizedKey(key));
+ }
+ return null;
+ }
+
+ // public static Either<AttParsingError, Attribute<?>> parse(String key, String value) {
+ // Attribute<?> foo =
+ // switch (key) {
+ // case "alias" -> TaggedData.ALIAS;
+ // case "alias-rec" -> TaggedData.ALIAS_REC;
+ // case "all-path" -> TaggedData.ALL_PATH;
+ // case "anywhere" -> TaggedData.ANYWHERE;
+ // case "applyPriority" -> new ApplyPriority();
+ // case "assoc" -> TaggedData.ASSOC;
+ // case "avoid" -> TaggedData.AVOID;
+ // case "bag" -> TaggedData.BAG;
+ // case "binder" -> TaggedData.BINDER;
+ // case "bracket" -> TaggedData.BRACKET;
+ // case "cell" -> TaggedData.CELL;
+ // case "cellCollection" -> TaggedData.CELL_COLLECTION;
+ // case "cellName" -> new CellName();
+ // case "circularity" -> TaggedData.CIRCULARITY;
+ // case "color" -> new Color();
+ // case "colors" -> new Colors();
+ // case "comm" -> TaggedData.COMM;
+ // case "concrete" -> new Concrete();
+ // case "constructor" -> TaggedData.CONSTRUCTOR;
+ // case "context" -> new Context();
+ // case "cool" -> TaggedData.COOL;
+ // case "depends" -> new Depends();
+ // case "deprecated" -> TaggedData.DEPRECATED;
+ // case "element" -> new Element();
+ // case "exit" -> TaggedData.EXIT;
+ // case "format" -> new Format();
+ // case "freshGenerator" -> TaggedData.FRESH_GENERATOR;
+ // case "function" -> TaggedData.FUNCTION;
+ // case "functional" -> TaggedData.FUNCTIONAL;
+ // case "group" -> new Group();
+ // case "haskell" -> TaggedData.HASKELL;
+ // case "heat" -> TaggedData.HEAT;
+ // case "hook" -> new Hook();
+ // case "hybrid" -> new Hybrid();
+ // case "idem" -> TaggedData.IDEM;
+ // case "impure" -> TaggedData.IMPURE;
+ // case "index" -> new Index();
+ // case "initial" -> TaggedData.INITIAL;
+ // case "initializer" -> TaggedData.INITIALIZER;
+ // case "injective" -> TaggedData.INJECTIVE;
+ // case "internal" -> TaggedData.INTERNAL;
+ // case "klabel" -> new Klabel();
+ // case "terminator-klabel" -> new TerminatorKlabel();
+ // case "label" -> new Label();
+ // case "latex" -> new Latex();
+ // case "left" -> TaggedData.LEFT;
+ // case "locations" -> TaggedData.LOCATIONS;
+ // case "macro" -> TaggedData.MACRO;
+ // case "macro-rec" -> TaggedData.MACRO_REC;
+ // case "maincell" -> TaggedData.MAINCELL;
+ // case "memo" -> TaggedData.MEMO;
+ // case "mlBinder" -> TaggedData.ML_BINDER;
+ // case "mlOp" -> TaggedData.ML_OP;
+ // case "multiplicity" -> new Multiplicity();
+ // case "non-assoc" -> TaggedData.NON_ASSOC;
+ // case "non-executable" -> TaggedData.NON_EXECUTABLE;
+ // case "not-lr1" -> TaggedData.NOT_LR1;
+ // case "no-evaluators" -> TaggedData.NO_EVALUATORS;
+ // case "one-path" -> TaggedData.ONE_PATH;
+ // case "owise" -> TaggedData.OWISE;
+ // case "parser" -> new Parser();
+ // case "prec" -> new Prec();
+ // case "prefer" -> TaggedData.PREFER;
+ // case "preserves-definedness" -> TaggedData.PRESERVES_DEFINEDNESS;
+ // case "priority" -> new Priority();
+ // case "private" -> TaggedData.PRIVATE;
+ // case "public" -> TaggedData.PUBLIC;
+ // case "result" -> new Result();
+ // case "returnsUnit" -> TaggedData.RETURNS_UNIT;
+ // case "right" -> TaggedData.RIGHT;
+ // case "seqstrict" -> new Seqstrict();
+ // case "simplification" -> new Simplification();
+ // case "smtlib" -> new SMTlib();
+ // case "smt-hook" -> new SMTHook();
+ // case "smt-lemma" -> TaggedData.SMT_LEMMA;
+ // case "stream" -> new Stream();
+ // case "strict" -> new Strict();
+ // case "symbol" -> new Symbol();
+ // case "symbolic" -> new Symbolic();
+ // case "tag" -> new Tag();
+ // case "token" -> TaggedData.TOKEN;
+ // case "total" -> TaggedData.TOTAL;
+ // case "trusted" -> TaggedData.TRUSTED;
+ // case "type" -> new Type();
+ // case "unboundVariables" -> new UnboundVariables();
+ // case "unit" -> new Unit();
+ // case "unparseAvoid" -> TaggedData.UNPARSE_AVOID;
+ // case "unused" -> TaggedData.UNUSED;
+ // case "wrapElement" -> new WrapElement();
+ // case "anonymous" -> new Anonymous();
+ // case "bracketLabel" -> new BracketLabel();
+ // case "cellFragment" -> new CellFragment();
+ // case "cellOptAbsent" -> new CellOptAbsent();
+ // case "cellSort" -> new CellSort();
+ // case "concat" -> new Concat();
+ // case "contentStartColumn" -> new ContentStartColumn();
+ // case "contentStartLine" -> new ContentStartLine();
+ // case "cool-like" -> new CoolLike();
+ // case "denormal" -> new Denormal();
+ // case "digest" -> new Digest();
+ // case "dummy_cell" -> new DummyCell();
+ // case "filterElement" -> new FilterElement();
+ // case "fresh" -> new Fresh();
+ // case "hasDomainValues" -> new HasDomainValues();
+ // case "left" -> new LeftInternal();
+ // case "nat" -> new Nat();
+ // case "notInjection" -> new NotInjection();
+ // case "not-lr1-modules" -> new NotLr1Modules();
+ // case "originalPrd" -> new OriginalPrd();
+ // case "overload" -> new Overload();
+ // case "predicate" -> new Predicate();
+ // case "prettyPrintWithSortAnnotation" -> new PrettyPrintWithSortAnnotation();
+ // case "priorities" -> new Priorities();
+ // case "projection" -> new Projection();
+ // case "recordPrd" -> new RecordPrd();
+ // case "recordPrd-zero" -> new RecordPrdZero();
+ // case "recordPrd-one" -> new RecordPrdOne();
+ // case "recordPrd-main" -> new RecordPrdMain();
+ // case "recordPrd-empty" -> new RecordPrdEmpty();
+ // case "recordPrd-subsort" -> new RecordPrdSubsort();
+ // case "recordPrd-repeat" -> new RecordPrdRepeat();
+ // case "recordPrd-item" -> new RecordPrdItem();
+ // case "refreshed" -> new Refreshed();
+ // case "right" -> new RightInternal();
+ // case "smt-prelude" -> new SMTPrelude();
+ // case "sortParams" -> new SortParams();
+ // case "symbol-overload" -> new SymbolOverload();
+ // case "syntaxModule" -> new SyntaxModule();
+ // case "temporary-cell-sort-decl" -> new TemporaryCellSortDecl();
+ // case "terminals" -> new Terminals();
+ // case "UNIQUE_ID" -> new UniqueId();
+ // case "userList" -> new UserList();
+ // case "userListTerminator" -> new UserListTerminator();
+ // case "withConfig" -> new WithConfig();
+ // default -> null;
+ // };
+ // }
+
+ // public static final class Alias extends MarkerAttribute<Alias> {
+ // private Alias() {
+ // super(new Key<>(Alias.class), "alias", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class AliasRec extends MarkerAttribute<AliasRec> {
+ // private AliasRec() {
+ // super(new Key<>(AliasRec.class), "alias-rec", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class AllPath extends MarkerAttribute<AllPath> {
+ // private AllPath() {
+ // super(new Key<>(AllPath.class), "all-path", new Visibility.User(Syntax.CLAIM,
+ // Syntax.MODULE));
+ // }
+ // }
+ //
+ // public static final class Anywhere extends MarkerAttribute<Anywhere> {
+ // private Anywhere() {
+ // super(new Key<>(Anywhere.class), "anywhere", new Visibility.User(Syntax.RULE));
+ // }
+ // }
+ //
+ // public static final class Assoc extends MarkerAttribute<Assoc> {
+ // private Assoc() {
+ // super(new Key<>(Assoc.class), "assoc", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Avoid extends MarkerAttribute<Avoid> {
+ // private Avoid() {
+ // super(new Key<>(Avoid.class), "avoid", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Bag extends MarkerAttribute<Bag> {
+ // private Bag() {
+ // super(new Key<>(Bag.class), "bag", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Binder extends MarkerAttribute<Binder> {
+ // private Binder() {
+ // super(new Key<>(Binder.class), "binder", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Bracket extends MarkerAttribute<Bracket> {
+ // private Bracket() {
+ // super(new Key<>(Bracket.class), "bracket", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Cell extends MarkerAttribute<Cell> {
+ // private Cell() {
+ // super(new Key<>(Cell.class), "cell", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class CellCollection extends MarkerAttribute<CellCollection> {
+ // private CellCollection() {
+ // super(
+ // new Key<>(CellCollection.class),
+ // "cellCollection",
+ // new Visibility.User(Syntax.PRODUCTION, Syntax.SYNTAX_SORT));
+ // }
+ // }
+ //
+ // public static final class Circularity extends MarkerAttribute<Circularity> {
+ // private Circularity() {
+ // super(new Key<>(Circularity.class), "circularity", new Visibility.User(Syntax.CLAIM));
+ // }
+ // }
+ //
+ // public static final class Comm extends MarkerAttribute<Comm> {
+ // private Comm() {
+ // super(new Key<>(Comm.class), "comm", new Visibility.User(Syntax.PRODUCTION, Syntax.RULE));
+ // }
+ // }
+ //
+ // public static final class Constructor extends MarkerAttribute<Constructor> {
+ // private Constructor() {
+ // super(new Key<>(Constructor.class), "constructor", new
+ // Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Cool extends MarkerAttribute<Cool> {
+ // private Cool() {
+ // super(new Key<>(Cool.class), "cool", new Visibility.User(Syntax.RULE));
+ // }
+ // }
+ //
+ // public static final class Deprecated extends MarkerAttribute<Deprecated> {
+ // private Deprecated() {
+ // super(new Key<>(Deprecated.class), "deprecated", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Exit extends MarkerAttribute<Exit> {
+ // private Exit() {
+ // super(new Key<>(Exit.class), "exit", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class FreshGenerator extends MarkerAttribute<FreshGenerator> {
+ // private FreshGenerator() {
+ // super(
+ // new Key<>(FreshGenerator.class),
+ // "freshGenerator",
+ // new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Function extends MarkerAttribute<Function> {
+ // private Function() {
+ // super(new Key<>(Function.class), "function", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Functional extends MarkerAttribute<Functional> {
+ // private Functional() {
+ // super(new Key<>(Functional.class), "functional", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Haskell extends MarkerAttribute<Haskell> {
+ // private Haskell() {
+ // super(new Key<>(Haskell.class), "haskell", new Visibility.User(Syntax.MODULE));
+ // }
+ // }
+ //
+ // public static final class Heat extends MarkerAttribute<Heat> {
+ // private Heat() {
+ // super(new Key<>(Heat.class), "heat", new Visibility.User(Syntax.RULE));
+ // }
+ // }
+ //
+ // public static final class Idem extends MarkerAttribute<Idem> {
+ // private Idem() {
+ // super(new Key<>(Idem.class), "idem", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Impure extends MarkerAttribute<Impure> {
+ // private Impure() {
+ // super(new Key<>(Impure.class), "impure", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Initial extends MarkerAttribute<Initial> {
+ // private Initial() {
+ // super(new Key<>(Initial.class), "initial", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Initializer extends MarkerAttribute<Initializer> {
+ // private Initializer() {
+ // super(
+ // new Key<>(Initializer.class),
+ // "initializer",
+ // new Visibility.User(Syntax.PRODUCTION, Syntax.RULE));
+ // }
+ // }
+ //
+ // public static final class Injective extends MarkerAttribute<Injective> {
+ // private Injective() {
+ // super(new Key<>(Injective.class), "injective", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Internal extends MarkerAttribute<Internal> {
+ // private Internal() {
+ // super(new Key<>(Internal.class), "internal", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Left extends MarkerAttribute<Left> {
+ // private Left() {
+ // super(new Key<>(Left.class), "left", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Locations extends MarkerAttribute<Locations> {
+ // private Locations() {
+ // super(new Key<>(Locations.class), "locations", new Visibility.User(Syntax.SYNTAX_SORT));
+ // }
+ // }
+ //
+ // public static final class Macro extends MarkerAttribute<Macro> {
+ // private Macro() {
+ // super(new Key<>(Macro.class), "macro", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class MacroRec extends MarkerAttribute<MacroRec> {
+ // private MacroRec() {
+ // super(new Key<>(MacroRec.class), "macro-rec", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Maincell extends MarkerAttribute<Maincell> {
+ // private Maincell() {
+ // super(new Key<>(Maincell.class), "maincell", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Memo extends MarkerAttribute<Memo> {
+ // private Memo() {
+ // super(new Key<>(Memo.class), "memo", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class MLBinder extends MarkerAttribute<MLBinder> {
+ // private MLBinder() {
+ // super(new Key<>(MLBinder.class), "mlBinder", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class MLOp extends MarkerAttribute<MLOp> {
+ // private MLOp() {
+ // super(new Key<>(MLOp.class), "mlOp", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class NonAssoc extends MarkerAttribute<NonAssoc> {
+ // private NonAssoc() {
+ // super(new Key<>(NonAssoc.class), "non-assoc", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class NonExecutable extends MarkerAttribute<NonExecutable> {
+ // private NonExecutable() {
+ // super(new Key<>(NonExecutable.class), "non-executable", new Visibility.User(Syntax.RULE));
+ // }
+ // }
+ //
+ // public static final class NotLR1 extends MarkerAttribute<NotLR1> {
+ // private NotLR1() {
+ // super(new Key<>(NotLR1.class), "not-lr1", new Visibility.User(Syntax.MODULE));
+ // }
+ // }
+ //
+ // public static final class NoEvaluators extends MarkerAttribute<NoEvaluators> {
+ // private NoEvaluators() {
+ // super(new Key<>(NoEvaluators.class), "no-evaluators", new
+ // Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class OnePath extends MarkerAttribute<OnePath> {
+ // private OnePath() {
+ // super(new Key<>(OnePath.class), "one-path", new Visibility.User(Syntax.CLAIM,
+ // Syntax.MODULE));
+ // }
+ // }
+ //
+ // public static final class Owise extends MarkerAttribute<Owise> {
+ // private Owise() {
+ // super(new Key<>(Owise.class), "owise", new Visibility.User(Syntax.RULE));
+ // }
+ // }
+ //
+ // public static final class Prefer extends MarkerAttribute<Prefer> {
+ // private Prefer() {
+ // super(new Key<>(Prefer.class), "prefer", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class PreservesDefinedness extends MarkerAttribute<PreservesDefinedness> {
+ // private PreservesDefinedness() {
+ // super(
+ // new Key<>(PreservesDefinedness.class),
+ // "preserves-definedness",
+ // new Visibility.User(Syntax.RULE));
+ // }
+ // }
+ //
+ // public static final class Private extends MarkerAttribute<Private> {
+ // private Private() {
+ // super(
+ // new Key<>(Private.class),
+ // "private",
+ // new Visibility.User(Syntax.MODULE, Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Public extends MarkerAttribute<Public> {
+ // private Public() {
+ // super(
+ // new Key<>(Public.class), "public", new Visibility.User(Syntax.MODULE,
+ // Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class ReturnsUnit extends MarkerAttribute<ReturnsUnit> {
+ // private ReturnsUnit() {
+ // super(new Key<>(ReturnsUnit.class), "returnsUnit", new
+ // Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Right extends MarkerAttribute<Right> {
+ // private Right() {
+ // super(new Key<>(Right.class), "right", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class SMTLemma extends MarkerAttribute<SMTLemma> {
+ // private SMTLemma() {
+ // super(new Key<>(SMTLemma.class), "smt-lemma", new Visibility.User(Syntax.RULE));
+ // }
+ // }
+ //
+ // public static final class Token extends MarkerAttribute<Token> {
+ // private Token() {
+ // super(
+ // new Key<>(Token.class),
+ // "token",
+ // new Visibility.User(Syntax.SYNTAX_SORT, Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Total extends MarkerAttribute<Total> {
+ // private Total() {
+ // super(new Key<>(Total.class), "total", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Trusted extends MarkerAttribute<Trusted> {
+ // private Trusted() {
+ // super(new Key<>(Trusted.class), "trusted", new Visibility.User(Syntax.CLAIM));
+ // }
+ // }
+ //
+ // public static final class UnparseAvoid extends MarkerAttribute<UnparseAvoid> {
+ // private UnparseAvoid() {
+ // super(new Key<>(UnparseAvoid.class), "unparseAvoid", new
+ // Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Unused extends MarkerAttribute<Unused> {
+ // private Unused() {
+ // super(new Key<>(Unused.class), "unused", new Visibility.User(Syntax.PRODUCTION));
+ // }
+ // }
+ //
+ // public static final class Anonymous extends MarkerAttribute<Anonymous> {
+ // private Anonymous() {
+ // super(new Key<>(Anonymous.class), "anonymous", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class BracketLabel extends MarkerAttribute<BracketLabel> {
+ // private BracketLabel() {
+ // super(new Key<>(BracketLabel.class), "bracketLabel", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class CellFragment extends MarkerAttribute<CellFragment> {
+ // private CellFragment() {
+ // super(new Key<>(CellFragment.class), "cellFragment", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class CellOptAbsent extends MarkerAttribute<CellOptAbsent> {
+ // private CellOptAbsent() {
+ // super(new Key<>(CellOptAbsent.class), "cellOptAbsent", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class CellSort extends MarkerAttribute<CellSort> {
+ // private CellSort() {
+ // super(new Key<>(CellSort.class), "cellSort", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class Concat extends MarkerAttribute<Concat> {
+ // private Concat() {
+ // super(new Key<>(Concat.class), "concat", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class ContentStartColumn extends MarkerAttribute<ContentStartColumn> {
+ // private ContentStartColumn() {
+ // super(new Key<>(ContentStartColumn.class), "contentStartColumn", new
+ // Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class ContentStartLine extends MarkerAttribute<ContentStartLine> {
+ // private ContentStartLine() {
+ // super(new Key<>(ContentStartLine.class), "contentStartLine", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class CoolLike extends MarkerAttribute<CoolLike> {
+ // private CoolLike() {
+ // super(new Key<>(CoolLike.class), "cool-like", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class Denormal extends MarkerAttribute<Denormal> {
+ // private Denormal() {
+ // super(new Key<>(Denormal.class), "denormal", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class Digest extends MarkerAttribute<Digest> {
+ // private Digest() {
+ // super(new Key<>(Digest.class), "digest", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class DummyCell extends MarkerAttribute<DummyCell> {
+ // private DummyCell() {
+ // super(new Key<>(DummyCell.class), "dummy_cell", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class FilterElement extends MarkerAttribute<FilterElement> {
+ // private FilterElement() {
+ // super(new Key<>(FilterElement.class), "filterElement", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class Fresh extends MarkerAttribute<Fresh> {
+ // private Fresh() {
+ // super(new Key<>(Fresh.class), "fresh", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class HasDomainValues extends MarkerAttribute<HasDomainValues> {
+ // private HasDomainValues() {
+ // super(new Key<>(HasDomainValues.class), "hasDomainValues", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class LeftInternal extends MarkerAttribute<LeftInternal> {
+ // private LeftInternal() {
+ // super(new Key<>(LeftInternal.class), "left", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class Nat extends MarkerAttribute<Nat> {
+ // private Nat() {
+ // super(new Key<>(Nat.class), "nat", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class NotInjection extends MarkerAttribute<NotInjection> {
+ // private NotInjection() {
+ // super(new Key<>(NotInjection.class), "notInjection", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class NotLR1Modules extends MarkerAttribute<NotLR1Modules> {
+ // private NotLR1Modules() {
+ // super(new Key<>(NotLR1Modules.class), "not-lr1-modules", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class OriginalPrd extends MarkerAttribute<OriginalPrd> {
+ // private OriginalPrd() {
+ // super(new Key<>(OriginalPrd.class), "originalPrd", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class Overload extends MarkerAttribute<Overload> {
+ // private Overload() {
+ // super(new Key<>(Overload.class), "overload", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class Predicate extends MarkerAttribute<Predicate> {
+ // private Predicate() {
+ // super(new Key<>(Predicate.class), "predicate", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class PrettyPrintWithSortAnnotation
+ // extends MarkerAttribute<PrettyPrintWithSortAnnotation> {
+ // private PrettyPrintWithSortAnnotation() {
+ // super(
+ // new Key<>(PrettyPrintWithSortAnnotation.class),
+ // "prettyPrintWithSortAnnotation",
+ // new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class Priorities extends MarkerAttribute<Priorities> {
+ // private Priorities() {
+ // super(new Key<>(Priorities.class), "priorities", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class Projection extends MarkerAttribute<Projection> {
+ // private Projection() {
+ // super(new Key<>(Projection.class), "projection", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class RecordPrd extends MarkerAttribute<RecordPrd> {
+ // private RecordPrd() {
+ // super(new Key<>(RecordPrd.class), "recordPrd", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class RecordPrdZero extends MarkerAttribute<RecordPrdZero> {
+ // private RecordPrdZero() {
+ // super(new Key<>(RecordPrdZero.class), "recordPrd-zero", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class RecordPrdOne extends MarkerAttribute<RecordPrdOne> {
+ // private RecordPrdOne() {
+ // super(new Key<>(RecordPrdOne.class), "recordPrd-one", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class RecordPrdMain extends MarkerAttribute<RecordPrdMain> {
+ // private RecordPrdMain() {
+ // super(new Key<>(RecordPrdMain.class), "recordPrd-main", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class RecordPrdEmpty extends MarkerAttribute<RecordPrdEmpty> {
+ // private RecordPrdEmpty() {
+ // super(new Key<>(RecordPrdEmpty.class), "recordPrd-empty", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class RecordPrdSubsort extends MarkerAttribute<RecordPrdSubsort> {
+ // private RecordPrdSubsort() {
+ // super(new Key<>(RecordPrdSubsort.class), "recordPrd-subsort", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class RecordPrdRepeat extends MarkerAttribute<RecordPrdRepeat> {
+ // private RecordPrdRepeat() {
+ // super(new Key<>(RecordPrdRepeat.class), "recordPrd-repeat", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class RecordPrdItem extends MarkerAttribute<RecordPrdItem> {
+ // private RecordPrdItem() {
+ // super(new Key<>(RecordPrdItem.class), "recordPrd-item", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class Refreshed extends MarkerAttribute<Refreshed> {
+ // private Refreshed() {
+ // super(new Key<>(Refreshed.class), "refreshed", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class RightInternal extends MarkerAttribute<RightInternal> {
+ // private RightInternal() {
+ // super(new Key<>(RightInternal.class), "right", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class SMTPrelude extends MarkerAttribute<SMTPrelude> {
+ // private SMTPrelude() {
+ // super(new Key<>(SMTPrelude.class), "smt-prelude", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class SortParams extends MarkerAttribute<SortParams> {
+ // private SortParams() {
+ // super(new Key<>(SortParams.class), "sortParams", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class SyntaxModule extends MarkerAttribute<SyntaxModule> {
+ // private SyntaxModule() {
+ // super(new Key<>(SyntaxModule.class), "syntaxModule", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class TemporaryCellSortDecl extends MarkerAttribute<TemporaryCellSortDecl>
+ // {
+ // private TemporaryCellSortDecl() {
+ // super(
+ // new Key<>(TemporaryCellSortDecl.class),
+ // "temporary-cell-sort-decl",
+ // new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class UserList extends MarkerAttribute<UserList> {
+ // private UserList() {
+ // super(new Key<>(UserList.class), "userList", new Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class UserListTerminator extends MarkerAttribute<UserListTerminator> {
+ // private UserListTerminator() {
+ // super(new Key<>(UserListTerminator.class), "userListTerminator", new
+ // Visibility.Internal());
+ // }
+ // }
+ //
+ // public static final class WithConfig extends MarkerAttribute<WithConfig> {
+ // private WithConfig() {
+ // super(new Key<>(WithConfig.class), "withConfig", new Visibility.Internal());
+ // }
+ // }
+}
diff --git a/kore/src/main/scala/org/kframework/attributes/Att.scala b/kore/src/main/scala/org/kframework/attributes/Att.scala
index 7c2f6f00a5f..c5b7e940b2c 100644
--- a/kore/src/main/scala/org/kframework/attributes/Att.scala
+++ b/kore/src/main/scala/org/kframework/attributes/Att.scala
@@ -140,6 +140,14 @@ object Att {
case object Forbidden extends KeyParameter
}
+ sealed trait KeyRange
+ private object KeyRange extends Serializable {
+ // Attributes that are only used by the frontend, and will not be emitted to the backends
+ case object FrontendOnly extends KeyRange
+ // Attributes used by both the frontend and at least one backend
+ case object WholePipeline extends KeyRange
+ }
+
/* The Key class can only be constructed within Att. To enforce this, we must
* - Make the constructor private
* - Manually declare apply() and make it private, lest a public one is generated
@@ -149,8 +157,10 @@ object Att {
key: String,
keyType: KeyType,
keyParam: KeyParameter,
- allowedSentences: Set[Class[_]]
+ allowedSentences: Set[Class[_]],
+ keyRange: KeyRange
) extends Serializable {
+ val shouldEmit: Boolean = keyRange.equals(KeyRange.WholePipeline)
override def toString: String = key
private[Key] def copy(): Unit = ()
}
@@ -158,12 +168,14 @@ object Att {
private[Att] def builtin(
key: String,
keyParam: KeyParameter,
- allowedSentences: Set[Class[_]]
- ): Key = Key(key, KeyType.BuiltIn, keyParam, allowedSentences)
+ allowedSentences: Set[Class[_]],
+ KeyRange: KeyRange
+ ): Key = Key(key, KeyType.BuiltIn, keyParam, allowedSentences, KeyRange)
private[Att] def internal(
- key: String
+ key: String,
+ KeyRange: KeyRange
): Key =
- Key(key, KeyType.Internal, KeyParameter.Optional, onlyon[AnyRef])
+ Key(key, KeyType.Internal, KeyParameter.Optional, onlyon[AnyRef], KeyRange)
}
def unrecognizedKey(key: String): Att.Key =
@@ -171,7 +183,8 @@ object Att {
key,
KeyType.Unrecognized,
KeyParameter.Optional,
- onlyon[AnyRef]
+ onlyon[AnyRef],
+ KeyRange.FrontendOnly
)
val empty: Att = Att(Map.empty)
@@ -186,160 +199,301 @@ object Att {
onlyon3[T1, T2, T3] ++ onlyon[T4]
/* Built-in attribute keys which can appear in user source code */
- final val ALIAS = Key.builtin("alias", KeyParameter.Forbidden, onlyon[Production])
- final val ALIAS_REC = Key.builtin("alias-rec", KeyParameter.Forbidden, onlyon[Production])
- final val ALL_PATH = Key.builtin("all-path", KeyParameter.Forbidden, onlyon2[Claim, Module])
- final val ANYWHERE = Key.builtin("anywhere", KeyParameter.Forbidden, onlyon[Rule])
- final val APPLY_PRIORITY = Key.builtin("applyPriority", KeyParameter.Required, onlyon[Production])
- final val ASSOC = Key.builtin("assoc", KeyParameter.Forbidden, onlyon[Production])
- final val AVOID = Key.builtin("avoid", KeyParameter.Forbidden, onlyon[Production])
- final val BAG = Key.builtin("bag", KeyParameter.Forbidden, onlyon[Production])
- final val BINDER = Key.builtin("binder", KeyParameter.Forbidden, onlyon[Production])
- final val BRACKET = Key.builtin("bracket", KeyParameter.Forbidden, onlyon[Production])
- final val CELL = Key.builtin("cell", KeyParameter.Forbidden, onlyon[Production])
+ final val ALIAS =
+ Key.builtin("alias", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val ALIAS_REC =
+ Key.builtin("alias-rec", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val ALL_PATH =
+ Key.builtin("all-path", KeyParameter.Forbidden, onlyon2[Claim, Module], KeyRange.FrontendOnly)
+ final val ANYWHERE =
+ Key.builtin("anywhere", KeyParameter.Forbidden, onlyon[Rule], KeyRange.WholePipeline)
+ final val APPLY_PRIORITY =
+ Key.builtin("applyPriority", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly)
+ final val ASSOC =
+ Key.builtin("assoc", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val AVOID =
+ Key.builtin("avoid", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+ final val BAG =
+ Key.builtin("bag", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+ final val BINDER =
+ Key.builtin("binder", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val BRACKET =
+ Key.builtin("bracket", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val CELL =
+ Key.builtin("cell", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
final val CELL_COLLECTION =
- Key.builtin("cellCollection", KeyParameter.Forbidden, onlyon2[Production, SyntaxSort])
- final val CELL_NAME = Key.builtin("cellName", KeyParameter.Required, onlyon[Production])
- final val CIRCULARITY = Key.builtin("circularity", KeyParameter.Forbidden, onlyon[Claim])
- final val COLOR = Key.builtin("color", KeyParameter.Required, onlyon[Production])
- final val COLORS = Key.builtin("colors", KeyParameter.Required, onlyon[Production])
- final val COMM = Key.builtin("comm", KeyParameter.Forbidden, onlyon2[Production, Rule])
+ Key.builtin(
+ "cellCollection",
+ KeyParameter.Forbidden,
+ onlyon2[Production, SyntaxSort],
+ KeyRange.FrontendOnly
+ )
+ final val CELL_NAME =
+ Key.builtin("cellName", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly)
+ final val CIRCULARITY =
+ Key.builtin("circularity", KeyParameter.Forbidden, onlyon[Claim], KeyRange.WholePipeline)
+ final val COLOR =
+ Key.builtin("color", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly)
+ final val COLORS =
+ Key.builtin("colors", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline)
+ final val COMM =
+ Key.builtin("comm", KeyParameter.Forbidden, onlyon2[Production, Rule], KeyRange.WholePipeline)
final val CONCRETE =
- Key.builtin("concrete", KeyParameter.Optional, onlyon3[Module, Production, Rule])
- final val CONSTRUCTOR = Key.builtin("constructor", KeyParameter.Forbidden, onlyon[Production])
- final val CONTEXT = Key.builtin("context", KeyParameter.Required, onlyon[ContextAlias])
- final val COOL = Key.builtin("cool", KeyParameter.Forbidden, onlyon[Rule])
- final val DEPENDS = Key.builtin("depends", KeyParameter.Required, onlyon[Claim])
- final val DEPRECATED = Key.builtin("deprecated", KeyParameter.Forbidden, onlyon[Production])
- final val ELEMENT = Key.builtin("element", KeyParameter.Required, onlyon[Production])
- final val EXIT = Key.builtin("exit", KeyParameter.Forbidden, onlyon[Production])
- final val FORMAT = Key.builtin("format", KeyParameter.Required, onlyon[Production])
+ Key.builtin(
+ "concrete",
+ KeyParameter.Optional,
+ onlyon3[Module, Production, Rule],
+ KeyRange.WholePipeline
+ )
+ final val CONSTRUCTOR =
+ Key.builtin("constructor", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val CONTEXT =
+ Key.builtin("context", KeyParameter.Required, onlyon[ContextAlias], KeyRange.FrontendOnly)
+ final val COOL = Key.builtin("cool", KeyParameter.Forbidden, onlyon[Rule], KeyRange.WholePipeline)
+ final val DEPENDS =
+ Key.builtin("depends", KeyParameter.Required, onlyon[Claim], KeyRange.WholePipeline)
+ final val DEPRECATED =
+ Key.builtin("deprecated", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val ELEMENT =
+ Key.builtin("element", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline)
+ final val EXIT =
+ Key.builtin("exit", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+ final val FORMAT =
+ Key.builtin("format", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline)
final val FRESH_GENERATOR =
- Key.builtin("freshGenerator", KeyParameter.Forbidden, onlyon[Production])
- final val FUNCTION = Key.builtin("function", KeyParameter.Forbidden, onlyon[Production])
- final val FUNCTIONAL = Key.builtin("functional", KeyParameter.Forbidden, onlyon[Production])
- final val GROUP = Key.builtin("group", KeyParameter.Required, onlyon[Sentence])
- final val HASKELL = Key.builtin("haskell", KeyParameter.Forbidden, onlyon[Module])
- final val HEAT = Key.builtin("heat", KeyParameter.Forbidden, onlyon[Rule])
- final val HOOK = Key.builtin("hook", KeyParameter.Required, onlyon2[Production, SyntaxSort])
- final val HYBRID = Key.builtin("hybrid", KeyParameter.Optional, onlyon[Production])
- final val IDEM = Key.builtin("idem", KeyParameter.Forbidden, onlyon[Production])
- final val IMPURE = Key.builtin("impure", KeyParameter.Forbidden, onlyon[Production])
- final val INDEX = Key.builtin("index", KeyParameter.Required, onlyon[Production])
- final val INITIAL = Key.builtin("initial", KeyParameter.Forbidden, onlyon[Production])
+ Key.builtin(
+ "freshGenerator",
+ KeyParameter.Forbidden,
+ onlyon[Production],
+ KeyRange.WholePipeline
+ )
+ final val FUNCTION =
+ Key.builtin("function", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val FUNCTIONAL =
+ Key.builtin("functional", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val GROUP =
+ Key.builtin("group", KeyParameter.Required, onlyon[Sentence], KeyRange.FrontendOnly)
+ final val HASKELL =
+ Key.builtin("haskell", KeyParameter.Forbidden, onlyon[Module], KeyRange.FrontendOnly)
+ final val HEAT = Key.builtin("heat", KeyParameter.Forbidden, onlyon[Rule], KeyRange.FrontendOnly)
+ final val HOOK =
+ Key.builtin(
+ "hook",
+ KeyParameter.Required,
+ onlyon2[Production, SyntaxSort],
+ KeyRange.WholePipeline
+ )
+ final val HYBRID =
+ Key.builtin("hybrid", KeyParameter.Optional, onlyon[Production], KeyRange.FrontendOnly)
+ final val IDEM =
+ Key.builtin("idem", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val IMPURE =
+ Key.builtin("impure", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+ final val INDEX =
+ Key.builtin("index", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly)
+ final val INITIAL =
+ Key.builtin("initial", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
final val INITIALIZER =
- Key.builtin("initializer", KeyParameter.Forbidden, onlyon2[Production, Rule])
- final val INJECTIVE = Key.builtin("injective", KeyParameter.Forbidden, onlyon[Production])
- final val INTERNAL = Key.builtin("internal", KeyParameter.Forbidden, onlyon[Production])
- final val KLABEL = Key.builtin("klabel", KeyParameter.Required, onlyon[Production])
+ Key.builtin(
+ "initializer",
+ KeyParameter.Forbidden,
+ onlyon2[Production, Rule],
+ KeyRange.FrontendOnly
+ )
+ final val INJECTIVE =
+ Key.builtin("injective", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val INTERNAL =
+ Key.builtin("internal", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+ final val KLABEL =
+ Key.builtin("klabel", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline)
final val TERMINATOR_KLABEL =
- Key.builtin("terminator-klabel", KeyParameter.Required, onlyon[Production])
- final val LABEL = Key.builtin("label", KeyParameter.Required, onlyon[Sentence])
- final val LATEX = Key.builtin("latex", KeyParameter.Required, onlyon[Production])
- final val LEFT = Key.builtin("left", KeyParameter.Forbidden, onlyon[Production])
- final val LOCATIONS = Key.builtin("locations", KeyParameter.Forbidden, onlyon[SyntaxSort])
- final val MACRO = Key.builtin("macro", KeyParameter.Forbidden, onlyon[Production])
- final val MACRO_REC = Key.builtin("macro-rec", KeyParameter.Forbidden, onlyon[Production])
- final val MAINCELL = Key.builtin("maincell", KeyParameter.Forbidden, onlyon[Production])
- final val MEMO = Key.builtin("memo", KeyParameter.Forbidden, onlyon[Production])
- final val ML_BINDER = Key.builtin("mlBinder", KeyParameter.Forbidden, onlyon[Production])
- final val ML_OP = Key.builtin("mlOp", KeyParameter.Forbidden, onlyon[Production])
- final val MULTIPLICITY = Key.builtin("multiplicity", KeyParameter.Required, onlyon[Production])
- final val NON_ASSOC = Key.builtin("non-assoc", KeyParameter.Forbidden, onlyon[Production])
- final val NON_EXECUTABLE = Key.builtin("non-executable", KeyParameter.Forbidden, onlyon[Rule])
- final val NOT_LR1 = Key.builtin("not-lr1", KeyParameter.Forbidden, onlyon[Module])
- final val NO_EVALUATORS = Key.builtin("no-evaluators", KeyParameter.Forbidden, onlyon[Production])
- final val ONE_PATH = Key.builtin("one-path", KeyParameter.Forbidden, onlyon2[Claim, Module])
- final val OWISE = Key.builtin("owise", KeyParameter.Forbidden, onlyon[Rule])
- final val OVERLOAD = Key.builtin("overload", KeyParameter.Required, onlyon[Production])
- final val PARSER = Key.builtin("parser", KeyParameter.Required, onlyon[Production])
- final val PREC = Key.builtin("prec", KeyParameter.Required, onlyon[Production])
- final val PREFER = Key.builtin("prefer", KeyParameter.Forbidden, onlyon[Production])
+ Key.builtin(
+ "terminator-klabel",
+ KeyParameter.Required,
+ onlyon[Production],
+ KeyRange.WholePipeline
+ )
+ final val LABEL =
+ Key.builtin("label", KeyParameter.Required, onlyon[Sentence], KeyRange.WholePipeline)
+ final val LATEX =
+ Key.builtin("latex", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly)
+ final val LEFT =
+ Key.builtin("left", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+ final val LOCATIONS =
+ Key.builtin("locations", KeyParameter.Forbidden, onlyon[SyntaxSort], KeyRange.FrontendOnly)
+ final val MACRO =
+ Key.builtin("macro", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val MACRO_REC =
+ Key.builtin("macro-rec", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val MAINCELL =
+ Key.builtin("maincell", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+ final val MEMO =
+ Key.builtin("memo", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val ML_BINDER =
+ Key.builtin("mlBinder", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+ final val ML_OP =
+ Key.builtin("mlOp", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+ final val MULTIPLICITY =
+ Key.builtin("multiplicity", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly)
+ final val NON_ASSOC =
+ Key.builtin("non-assoc", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+ final val NON_EXECUTABLE =
+ Key.builtin("non-executable", KeyParameter.Forbidden, onlyon[Rule], KeyRange.WholePipeline)
+ final val NOT_LR1 =
+ Key.builtin("not-lr1", KeyParameter.Forbidden, onlyon[Module], KeyRange.FrontendOnly)
+ final val NO_EVALUATORS =
+ Key.builtin("no-evaluators", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val ONE_PATH =
+ Key.builtin("one-path", KeyParameter.Forbidden, onlyon2[Claim, Module], KeyRange.FrontendOnly)
+ final val OVERLOAD =
+ Key.builtin("overload", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly)
+ final val OWISE =
+ Key.builtin("owise", KeyParameter.Forbidden, onlyon[Rule], KeyRange.WholePipeline)
+ final val PARSER =
+ Key.builtin("parser", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly)
+ final val PREC =
+ Key.builtin("prec", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly)
+ final val PREFER =
+ Key.builtin("prefer", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
final val PRESERVES_DEFINEDNESS =
- Key.builtin("preserves-definedness", KeyParameter.Forbidden, onlyon[Rule])
+ Key.builtin(
+ "preserves-definedness",
+ KeyParameter.Forbidden,
+ onlyon[Rule],
+ KeyRange.WholePipeline
+ )
final val PRIORITY =
- Key.builtin("priority", KeyParameter.Required, onlyon4[Context, ContextAlias, Production, Rule])
- final val PRIVATE = Key.builtin("private", KeyParameter.Forbidden, onlyon2[Module, Production])
- final val PUBLIC = Key.builtin("public", KeyParameter.Forbidden, onlyon2[Module, Production])
+ Key.builtin(
+ "priority",
+ KeyParameter.Required,
+ onlyon4[Context, ContextAlias, Production, Rule],
+ KeyRange.WholePipeline
+ )
+ final val PRIVATE = Key.builtin(
+ "private",
+ KeyParameter.Forbidden,
+ onlyon2[Module, Production],
+ KeyRange.FrontendOnly
+ )
+ final val PUBLIC = Key.builtin(
+ "public",
+ KeyParameter.Forbidden,
+ onlyon2[Module, Production],
+ KeyRange.FrontendOnly
+ )
final val RESULT =
- Key.builtin("result", KeyParameter.Required, onlyon4[Context, ContextAlias, Production, Rule])
- final val RETURNS_UNIT = Key.builtin("returnsUnit", KeyParameter.Forbidden, onlyon[Production])
- final val RIGHT = Key.builtin("right", KeyParameter.Forbidden, onlyon[Production])
- final val SEQSTRICT = Key.builtin("seqstrict", KeyParameter.Optional, onlyon[Production])
- final val SIMPLIFICATION = Key.builtin("simplification", KeyParameter.Optional, onlyon[Rule])
- final val SMTLIB = Key.builtin("smtlib", KeyParameter.Required, onlyon[Production])
- final val SMT_HOOK = Key.builtin("smt-hook", KeyParameter.Required, onlyon[Production])
- final val SMT_LEMMA = Key.builtin("smt-lemma", KeyParameter.Forbidden, onlyon[Rule])
- final val STREAM = Key.builtin("stream", KeyParameter.Optional, onlyon2[Production, Rule])
- final val STRICT = Key.builtin("strict", KeyParameter.Optional, onlyon[Production])
- final val SYMBOL = Key.builtin("symbol", KeyParameter.Optional, onlyon[Production])
+ Key.builtin(
+ "result",
+ KeyParameter.Required,
+ onlyon4[Context, ContextAlias, Production, Rule],
+ KeyRange.FrontendOnly
+ )
+ final val RETURNS_UNIT =
+ Key.builtin("returnsUnit", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+ final val RIGHT =
+ Key.builtin("right", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+ final val SEQSTRICT =
+ Key.builtin("seqstrict", KeyParameter.Optional, onlyon[Production], KeyRange.FrontendOnly)
+ final val SIMPLIFICATION =
+ Key.builtin("simplification", KeyParameter.Optional, onlyon[Rule], KeyRange.WholePipeline)
+ final val SMTLIB =
+ Key.builtin("smtlib", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline)
+ final val SMT_HOOK =
+ Key.builtin("smt-hook", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline)
+ final val SMT_LEMMA =
+ Key.builtin("smt-lemma", KeyParameter.Forbidden, onlyon[Rule], KeyRange.WholePipeline)
+ final val STREAM =
+ Key.builtin("stream", KeyParameter.Optional, onlyon2[Production, Rule], KeyRange.FrontendOnly)
+ final val STRICT =
+ Key.builtin("strict", KeyParameter.Optional, onlyon[Production], KeyRange.FrontendOnly)
+ final val SYMBOL =
+ Key.builtin("symbol", KeyParameter.Optional, onlyon[Production], KeyRange.WholePipeline)
final val SYMBOLIC =
- Key.builtin("symbolic", KeyParameter.Optional, onlyon3[Module, Production, Rule])
- final val TAG = Key.builtin("tag", KeyParameter.Required, onlyon[Rule])
- final val TOKEN = Key.builtin("token", KeyParameter.Forbidden, onlyon2[SyntaxSort, Production])
- final val TOTAL = Key.builtin("total", KeyParameter.Forbidden, onlyon[Production])
- final val TRUSTED = Key.builtin("trusted", KeyParameter.Forbidden, onlyon[Claim])
- final val TYPE = Key.builtin("type", KeyParameter.Required, onlyon[Production])
+ Key.builtin(
+ "symbolic",
+ KeyParameter.Optional,
+ onlyon3[Module, Production, Rule],
+ KeyRange.WholePipeline
+ )
+ final val TAG = Key.builtin("tag", KeyParameter.Required, onlyon[Rule], KeyRange.FrontendOnly)
+ final val TOKEN = Key.builtin(
+ "token",
+ KeyParameter.Forbidden,
+ onlyon2[SyntaxSort, Production],
+ KeyRange.WholePipeline
+ )
+ final val TOTAL =
+ Key.builtin("total", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
+ final val TRUSTED =
+ Key.builtin("trusted", KeyParameter.Forbidden, onlyon[Claim], KeyRange.WholePipeline)
+ final val TYPE =
+ Key.builtin("type", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly)
final val UNBOUND_VARIABLES = Key.builtin(
"unboundVariables",
KeyParameter.Required,
- onlyon4[Context, ContextAlias, Production, RuleOrClaim]
+ onlyon4[Context, ContextAlias, Production, RuleOrClaim],
+ KeyRange.FrontendOnly
)
- final val UNIT = Key.builtin("unit", KeyParameter.Required, onlyon[Production])
- final val UNPARSE_AVOID = Key.builtin("unparseAvoid", KeyParameter.Forbidden, onlyon[Production])
- final val UNUSED = Key.builtin("unused", KeyParameter.Forbidden, onlyon[Production])
- final val WRAP_ELEMENT = Key.builtin("wrapElement", KeyParameter.Required, onlyon[Production])
+ final val UNIT =
+ Key.builtin("unit", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline)
+ final val UNPARSE_AVOID =
+ Key.builtin("unparseAvoid", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+ final val UNUSED =
+ Key.builtin("unused", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+ final val WRAP_ELEMENT =
+ Key.builtin("wrapElement", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly)
/* Internal attribute keys which cannot appear in user source code */
- final val ANONYMOUS = Key.internal("anonymous")
- final val BRACKET_LABEL = Key.internal("bracketLabel")
- final val CELL_FRAGMENT = Key.internal("cellFragment")
- final val CELL_OPT_ABSENT = Key.internal("cellOptAbsent")
- final val CELL_SORT = Key.internal("cellSort")
- final val CONCAT = Key.internal("concat")
- final val CONTENT_START_COLUMN = Key.internal("contentStartColumn")
- final val CONTENT_START_LINE = Key.internal("contentStartLine")
- final val COOL_LIKE = Key.internal("cool-like")
- final val DENORMAL = Key.internal("denormal")
- final val DIGEST = Key.internal("digest")
- final val DUMMY_CELL = Key.internal("dummy_cell")
- final val FILTER_ELEMENT = Key.internal("filterElement")
- final val FRESH = Key.internal("fresh")
- final val HAS_DOMAIN_VALUES = Key.internal("hasDomainValues")
- final val LEFT_INTERNAL = Key.internal("left")
- final val LOCATION = Key.internal(classOf[Location].getName)
- final val NAT = Key.internal("nat")
- final val NOT_INJECTION = Key.internal("notInjection")
- final val NOT_LR1_MODULES = Key.internal("not-lr1-modules")
- final val ORIGINAL_PRD = Key.internal("originalPrd")
- final val PREDICATE = Key.internal("predicate")
+ final val ANONYMOUS = Key.internal("anonymous", KeyRange.FrontendOnly)
+ final val BRACKET_LABEL = Key.internal("bracketLabel", KeyRange.FrontendOnly)
+ final val CELL_FRAGMENT = Key.internal("cellFragment", KeyRange.FrontendOnly)
+ final val CELL_OPT_ABSENT = Key.internal("cellOptAbsent", KeyRange.FrontendOnly)
+ final val CELL_SORT = Key.internal("cellSort", KeyRange.FrontendOnly)
+ final val CONCAT = Key.internal("concat", KeyRange.WholePipeline)
+ final val CONTENT_START_COLUMN = Key.internal("contentStartColumn", KeyRange.FrontendOnly)
+ final val CONTENT_START_LINE = Key.internal("contentStartLine", KeyRange.FrontendOnly)
+ final val COOL_LIKE = Key.internal("cool-like", KeyRange.WholePipeline)
+ final val DENORMAL = Key.internal("denormal", KeyRange.FrontendOnly)
+ final val DIGEST = Key.internal("digest", KeyRange.FrontendOnly)
+ final val DUMMY_CELL = Key.internal("dummy_cell", KeyRange.FrontendOnly)
+ final val FILTER_ELEMENT = Key.internal("filterElement", KeyRange.FrontendOnly)
+ final val FRESH = Key.internal("fresh", KeyRange.FrontendOnly)
+ final val HAS_DOMAIN_VALUES = Key.internal("hasDomainValues", KeyRange.WholePipeline)
+ final val LEFT_INTERNAL = Key.internal("left", KeyRange.WholePipeline)
+ final val LOCATION = Key.internal(classOf[Location].getName, KeyRange.WholePipeline)
+ final val NAT = Key.internal("nat", KeyRange.WholePipeline)
+ final val NOT_INJECTION = Key.internal("notInjection", KeyRange.FrontendOnly)
+ final val NOT_LR1_MODULES = Key.internal("not-lr1-modules", KeyRange.FrontendOnly)
+ final val ORIGINAL_PRD = Key.internal("originalPrd", KeyRange.FrontendOnly)
+ final val PREDICATE = Key.internal("predicate", KeyRange.FrontendOnly)
final val PRETTY_PRINT_WITH_SORT_ANNOTATION =
- Key.internal("prettyPrintWithSortAnnotation")
- final val PRIORITIES = Key.internal("priorities")
- final val PRODUCTION = Key.internal(classOf[Production].getName)
- final val PROJECTION = Key.internal("projection")
- final val RECORD_PRD = Key.internal("recordPrd")
- final val RECORD_PRD_ZERO = Key.internal("recordPrd-zero")
- final val RECORD_PRD_ONE = Key.internal("recordPrd-one")
- final val RECORD_PRD_MAIN = Key.internal("recordPrd-main")
- final val RECORD_PRD_EMPTY = Key.internal("recordPrd-empty")
- final val RECORD_PRD_SUBSORT = Key.internal("recordPrd-subsort")
- final val RECORD_PRD_REPEAT = Key.internal("recordPrd-repeat")
- final val RECORD_PRD_ITEM = Key.internal("recordPrd-item")
- final val REFRESHED = Key.internal("refreshed")
- final val RIGHT_INTERNAL = Key.internal("right")
- final val SMT_PRELUDE = Key.internal("smt-prelude")
- final val SORT = Key.internal(classOf[Sort].getName)
- final val SORT_PARAMS = Key.internal("sortParams")
- final val SOURCE = Key.internal(classOf[Source].getName)
- final val SYMBOL_OVERLOAD = Key.internal("symbol-overload")
- final val SYNTAX_MODULE = Key.internal("syntaxModule")
- final val TEMPORARY_CELL_SORT_DECL = Key.internal("temporary-cell-sort-decl")
- final val TERMINALS = Key.internal("terminals")
- final val UNIQUE_ID = Key.internal("UNIQUE_ID")
- final val USER_LIST = Key.internal("userList")
- final val USER_LIST_TERMINATOR = Key.internal("userListTerminator")
- final val WITH_CONFIG = Key.internal("withConfig")
+ Key.internal("prettyPrintWithSortAnnotation", KeyRange.FrontendOnly)
+ final val PRIORITIES = Key.internal("priorities", KeyRange.WholePipeline)
+ final val PRODUCTION = Key.internal(classOf[Production].getName, KeyRange.FrontendOnly)
+ final val PROJECTION = Key.internal("projection", KeyRange.FrontendOnly)
+ final val RECORD_PRD = Key.internal("recordPrd", KeyRange.FrontendOnly)
+ final val RECORD_PRD_ZERO = Key.internal("recordPrd-zero", KeyRange.FrontendOnly)
+ final val RECORD_PRD_ONE = Key.internal("recordPrd-one", KeyRange.FrontendOnly)
+ final val RECORD_PRD_MAIN = Key.internal("recordPrd-main", KeyRange.FrontendOnly)
+ final val RECORD_PRD_EMPTY = Key.internal("recordPrd-empty", KeyRange.FrontendOnly)
+ final val RECORD_PRD_SUBSORT = Key.internal("recordPrd-subsort", KeyRange.FrontendOnly)
+ final val RECORD_PRD_REPEAT = Key.internal("recordPrd-repeat", KeyRange.FrontendOnly)
+ final val RECORD_PRD_ITEM = Key.internal("recordPrd-item", KeyRange.FrontendOnly)
+ final val REFRESHED = Key.internal("refreshed", KeyRange.FrontendOnly)
+ final val RIGHT_INTERNAL = Key.internal("right", KeyRange.WholePipeline)
+ final val SMT_PRELUDE = Key.internal("smt-prelude", KeyRange.FrontendOnly)
+ final val SORT = Key.internal(classOf[Sort].getName, KeyRange.FrontendOnly)
+ final val SORT_PARAMS = Key.internal("sortParams", KeyRange.FrontendOnly)
+ final val SOURCE = Key.internal(classOf[Source].getName, KeyRange.WholePipeline)
+ final val SYMBOL_OVERLOAD = Key.internal("symbol-overload", KeyRange.WholePipeline)
+ final val SYNTAX_MODULE = Key.internal("syntaxModule", KeyRange.FrontendOnly)
+ final val TEMPORARY_CELL_SORT_DECL =
+ Key.internal("temporary-cell-sort-decl", KeyRange.FrontendOnly)
+ final val TERMINALS = Key.internal("terminals", KeyRange.WholePipeline)
+ final val UNIQUE_ID = Key.internal("UNIQUE_ID", KeyRange.WholePipeline)
+ final val USER_LIST = Key.internal("userList", KeyRange.FrontendOnly)
+ final val USER_LIST_TERMINATOR = Key.internal("userListTerminator", KeyRange.FrontendOnly)
+ final val WITH_CONFIG = Key.internal("withConfig", KeyRange.FrontendOnly)
private val stringClassName = classOf[String].getName
private val intClassName = classOf[java.lang.Integer].getName