WIP

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;
+  }
+}

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));
+  }
+}