Remove Att methods based on Class rather than Att.Key (#4008)

This PR removes all methods from `Att` which refer to attributes by their value type (e.g. `Source.class`, `Location.class`, etc.) rather than by their `Att.Key`. As a result, we maintain the nice property that usages of an attribute exactly correspond with usages of the whitelisted `Att.Key`.
runtimeverification · Feb 19, 2024 · 845bca1 · 845bca1
1 parent f9d00d9
commit 845bca1
Show file tree

Hide file tree

Showing 47 changed files with 242 additions and 174 deletions.
diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java
@@ -151,7 +151,8 @@ public K search(
         if (patternTerm instanceof KVariable) {
           patternTerm =
               KORE.KVariable(
-                  ((KVariable) patternTerm).name(), Att.empty().add(Sort.class, initializerSort));
+                  ((KVariable) patternTerm).name(),
+                  Att.empty().add(Att.SORT(), Sort.class, initializerSort));
         }
         K patternCondition = pattern.requires();
         String patternTermKore =

diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
@@ -161,7 +161,7 @@ public void convert(
     // insert the location of the main module so the backend can provide better error location
     convert(
         considerSource,
-        Att.empty().add(Source.class, module.att().get(Source.class)),
+        Att.empty().add(Att.SOURCE(), Source.class, module.att().get(Att.SOURCE(), Source.class)),
         sb,
         null,
         null);
@@ -671,7 +671,7 @@ private void genMapCeilAxioms(Production prod, Collection<Rule> rules) {
     // #Ceil(@K1) and #Ceil(@Rest).
     // [simplification]
 
-    K restMapSet = KVariable("@Rest", Att.empty().add(Sort.class, mapSort));
+    K restMapSet = KVariable("@Rest", Att.empty().add(Att.SORT(), Sort.class, mapSort));
     KLabel ceilMapLabel = KLabel(KLabels.ML_CEIL.name(), mapSort, sortParam);
     KLabel andLabel = KLabel(KLabels.ML_AND.name(), sortParam);
 
@@ -680,7 +680,7 @@ private void genMapCeilAxioms(Production prod, Collection<Rule> rules) {
     K setArgsCeil = KApply(KLabel(KLabels.ML_TRUE.name(), sortParam));
     for (int i = 0; i < nonterminals.length(); i++) {
       Sort sort = nonterminals.apply(i).sort();
-      KVariable setVar = KVariable("@K" + i, Att.empty().add(Sort.class, sort));
+      KVariable setVar = KVariable("@K" + i, Att.empty().add(Att.SORT(), Sort.class, sort));
       setArgs.add(setVar);
       if (i > 0) {
         KLabel ceil = KLabel(KLabels.ML_CEIL.name(), sort, sortParam);
@@ -959,7 +959,7 @@ public String convertSpecificationModule(
     considerSource.put(Att.SOURCE(), true);
     convert(
         considerSource,
-        Att.empty().add(Source.class, spec.att().get(Source.class)),
+        Att.empty().add(Att.SOURCE(), Source.class, spec.att().get(Att.SOURCE(), Source.class)),
         sb,
         null,
         null);
@@ -1454,7 +1454,7 @@ private void genAliasForSemanticsRuleLHS(
     String conn = "";
     for (KVariable var : freeVars) {
       sb.append(conn);
-      convert(var.att().getOptional(Sort.class).orElse(Sorts.K()), sb);
+      convert(var.att().getOptional(Att.SORT(), Sort.class).orElse(Sorts.K()), sb);
       conn = ",";
     }
     sb.append(") : ");
@@ -2218,7 +2218,7 @@ public void apply(KToken k) {
       public void apply(KSequence k) {
         for (int i = 0; i < k.items().size(); i++) {
           K item = k.items().get(i);
-          boolean isList = item.att().get(Sort.class).equals(Sorts.K());
+          boolean isList = item.att().get(Att.SORT(), Sort.class).equals(Sorts.K());
           if (i == k.items().size() - 1) {
             if (isList) {
               apply(item);
@@ -2228,7 +2228,7 @@ public void apply(KSequence k) {
               sb.append(",dotk{}())");
             }
           } else {
-            if (item.att().get(Sort.class).equals(Sorts.K())) {
+            if (item.att().get(Att.SORT(), Sort.class).equals(Sorts.K())) {
               sb.append("append{}(");
             } else {
               sb.append("kseq{}(");
@@ -2255,13 +2255,13 @@ public void apply(KVariable k) {
         String name = setVar ? k.name().substring(1) : k.name();
         convert(name, sb);
         sb.append(":");
-        convert(k.att().getOptional(Sort.class).orElse(Sorts.K()), sb);
+        convert(k.att().getOptional(Att.SORT(), Sort.class).orElse(Sorts.K()), sb);
       }
 
       @Override
       public void apply(KRewrite k) {
         sb.append("\\rewrites{");
-        convert(k.att().get(Sort.class), sb);
+        convert(k.att().get(Att.SORT(), Sort.class), sb);
         sb.append("}(");
         apply(k.left());
         sb.append(",");
@@ -2271,7 +2271,7 @@ public void apply(KRewrite k) {
 
       @Override
       public void apply(KAs k) {
-        Sort sort = k.att().get(Sort.class);
+        Sort sort = k.att().get(Att.SORT(), Sort.class);
         sb.append("\\and{");
         convert(sort, sb);
         sb.append("}(");

diff --git a/kernel/src/main/java/org/kframework/compile/AddParentCells.java b/kernel/src/main/java/org/kframework/compile/AddParentCells.java
@@ -19,6 +19,7 @@
 import java.util.function.Function;
 import java.util.stream.Collectors;
 import java.util.stream.Stream;
+import org.kframework.attributes.Att;
 import org.kframework.builtin.KLabels;
 import org.kframework.definition.Context;
 import org.kframework.definition.RuleOrClaim;
@@ -183,8 +184,8 @@ Optional<Integer> getLevel(K k) {
     if (k instanceof KApply) {
       return getLevel((KApply) k);
     } else if (k instanceof KVariable) {
-      if (k.att().contains(Sort.class)) {
-        Sort sort = k.att().get(Sort.class);
+      if (k.att().contains(Att.SORT(), Sort.class)) {
+        Sort sort = k.att().get(Att.SORT(), Sort.class);
         int level = cfg.cfg().getLevel(sort);
         if (level >= 0) {
           return Optional.of(level);
@@ -239,7 +240,7 @@ Optional<KLabel> getParent(K k) {
         return Optional.empty();
       }
     } else if (k instanceof KVariable) {
-      Sort sort = k.att().get(Sort.class);
+      Sort sort = k.att().get(Att.SORT(), Sort.class);
       return Optional.of(cfg.getParent(sort));
     } else {
       Optional<KLabel> leftParent = getParent(((KRewrite) k).left());

diff --git a/kernel/src/main/java/org/kframework/compile/AddSortInjections.java b/kernel/src/main/java/org/kframework/compile/AddSortInjections.java
@@ -135,7 +135,7 @@ private K internalAddSortInjections(K term, Sort expectedSort) {
             KApply(
                 KLabel("inj", actualSort, Sorts.KItem()),
                 KList(visitChildren(term, actualSort, expectedSort)),
-                Att.empty().add(Sort.class, Sorts.KItem())));
+                Att.empty().add(Att.SORT(), Sort.class, Sorts.KItem())));
       }
     } else {
       String hookAtt =
@@ -167,8 +167,8 @@ private K internalAddSortInjections(K term, Sort expectedSort) {
                           KList(visitChildren(k, actualSort, expectedSort)));
                 }
                 Sort adjustedExpectedSort = expectedSort;
-                if (k.att().contains(Sort.class)) {
-                  adjustedExpectedSort = k.att().get(Sort.class);
+                if (k.att().contains(Att.SORT(), Sort.class)) {
+                  adjustedExpectedSort = k.att().get(Att.SORT(), Sort.class);
                 }
                 Production prod = production(k);
                 Production substituted =
@@ -184,12 +184,12 @@ private K internalAddSortInjections(K term, Sort expectedSort) {
                     KList(
                         visitChildren(key, actualKeySort, expectedKeySort),
                         visitChildren(k, actualSort, expectedSort)),
-                    Att.empty().add(Sort.class, expectedSort));
+                    Att.empty().add(Att.SORT(), Sort.class, expectedSort));
               } else {
                 return KApply(
                     elementLabel,
                     KList(visitChildren(k, actualSort, expectedSort)),
-                    Att.empty().add(Sort.class, expectedSort));
+                    Att.empty().add(Att.SORT(), Sort.class, expectedSort));
               }
             }
           }
@@ -198,7 +198,7 @@ private K internalAddSortInjections(K term, Sort expectedSort) {
       return KApply(
           KLabel("inj", actualSort, expectedSort),
           KList(visitChildren(term, actualSort, expectedSort)),
-          Att.empty().add(Sort.class, expectedSort));
+          Att.empty().add(Att.SORT(), Sort.class, expectedSort));
     }
   }
 
@@ -208,16 +208,16 @@ private void initSortParams() {
   }
 
   private K visitChildren(K term, Sort actualSort, Sort expectedSort) {
-    Att att = term.att().add(Sort.class, actualSort);
+    Att att = term.att().add(Att.SORT(), Sort.class, actualSort);
     if (actualSort.name().equals(SORTPARAM_NAME)) {
       sortParams.add(actualSort.params().head().name());
     }
     if (term instanceof KApply kapp) {
       if (kapp.klabel().name().equals("inj")) {
         return term;
       }
-      if (kapp.att().contains(Sort.class)) {
-        expectedSort = kapp.att().get(Sort.class);
+      if (kapp.att().contains(Att.SORT(), Sort.class)) {
+        expectedSort = kapp.att().get(Att.SORT(), Sort.class);
       }
       Production prod = production(kapp);
       List<K> children = new ArrayList<>();
@@ -376,8 +376,8 @@ public Sort sort(K term, Sort expectedSort) {
       if (kapp.klabel().name().equals("_:/=K_")) {
         return Sorts.Bool();
       }
-      if (kapp.att().contains(Sort.class)) {
-        expectedSort = kapp.att().get(Sort.class);
+      if (kapp.att().contains(Att.SORT(), Sort.class)) {
+        expectedSort = kapp.att().get(Att.SORT(), Sort.class);
       }
       Production prod = production(kapp);
       Production substituted = prod;
@@ -418,7 +418,7 @@ public Sort sort(K term, Sort expectedSort) {
     } else if (term instanceof KToken) {
       return ((KToken) term).sort();
     } else if (term instanceof KVariable) {
-      return term.att().getOptional(Sort.class).orElse(Sorts.K());
+      return term.att().getOptional(Att.SORT(), Sort.class).orElse(Sorts.K());
     } else if (term instanceof KSequence) {
       return Sorts.K();
     } else if (term instanceof InjectedKLabel) {

diff --git a/kernel/src/main/java/org/kframework/compile/CloseCells.java b/kernel/src/main/java/org/kframework/compile/CloseCells.java
@@ -86,7 +86,8 @@ KVariable newDotVariable(Sort s) {
         newLabel = KVariable("_DotVar" + (counter++), Att().add(Att.ANONYMOUS()));
       } else {
         newLabel =
-            KVariable("_DotVar" + (counter++), Att().add(Att.ANONYMOUS()).add(Sort.class, s));
+            KVariable(
+                "_DotVar" + (counter++), Att().add(Att.ANONYMOUS()).add(Att.SORT(), Sort.class, s));
       }
     } while (vars.contains(newLabel));
     vars.add(newLabel);
@@ -290,8 +291,8 @@ private void filterRequired(Set<Sort> required, K item) {
     if (item instanceof KApply) {
       required.remove(labelInfo.getCodomain(((KApply) item).klabel()));
     } else if (item instanceof KVariable) {
-      if (item.att().contains(Sort.class)) {
-        Sort sort = item.att().get(Sort.class);
+      if (item.att().contains(Att.SORT(), Sort.class)) {
+        Sort sort = item.att().get(Att.SORT(), Sort.class);
         if (cfg.cfg().isCell(sort)) {
           required.remove(sort);
         } else {

diff --git a/kernel/src/main/java/org/kframework/compile/ConcretizationInfo.java b/kernel/src/main/java/org/kframework/compile/ConcretizationInfo.java
@@ -4,6 +4,7 @@
 import static org.kframework.kore.KORE.*;
 
 import java.util.List;
+import org.kframework.attributes.Att;
 import org.kframework.kore.K;
 import org.kframework.kore.KApply;
 import org.kframework.kore.KLabel;
@@ -18,7 +19,7 @@ public Sort getCellSort(K k) {
     if (k instanceof KApply) {
       return labels.getCodomain(((KApply) k).klabel());
     } else if (k instanceof KVariable) {
-      return k.att().get(Sort.class);
+      return k.att().get(Att.SORT(), Sort.class);
     } else {
       throw new AssertionError(
           "expected KApply or KVariable, found " + k.getClass().getSimpleName());

diff --git a/kernel/src/main/java/org/kframework/compile/ConcretizeCells.java b/kernel/src/main/java/org/kframework/compile/ConcretizeCells.java
@@ -69,7 +69,8 @@ public Sentence concretize(Module m, Sentence s) {
 
   public static boolean hasCells(K item) {
     if (IncompleteCellUtils.flattenCells(item).stream()
-        .anyMatch(k -> k.att().get(Production.class).att().contains(Att.CELL()))) {
+        .anyMatch(
+            k -> k.att().get(Att.PRODUCTION(), Production.class).att().contains(Att.CELL()))) {
       return true;
     }
 

diff --git a/kernel/src/main/java/org/kframework/compile/ExpandMacros.java b/kernel/src/main/java/org/kframework/compile/ExpandMacros.java
@@ -345,7 +345,7 @@ private boolean hasPolyAtt(Production prod, int idx) {
 
   private Set<Sort> sort(K k, RuleOrClaim r) {
     if (k instanceof KVariable) {
-      return Collections.singleton(k.att().getOptional(Sort.class).orElse(null));
+      return Collections.singleton(k.att().getOptional(Att.SORT(), Sort.class).orElse(null));
     } else if (k instanceof KToken) {
       return Collections.singleton(((KToken) k).sort());
     } else if (k instanceof KApply kapp) {
@@ -389,8 +389,8 @@ private boolean match(Map<KVariable, K> subst, K pattern, K subject, RuleOrClaim
       if (subst.containsKey(pattern)) {
         return subst.get(pattern).equals(subject);
       } else {
-        if (pattern.att().contains(Sort.class)) {
-          Sort patternSort = pattern.att().get(Sort.class);
+        if (pattern.att().contains(Att.SORT(), Sort.class)) {
+          Sort patternSort = pattern.att().get(Att.SORT(), Sort.class);
           if (sort(subject, r).stream()
               .anyMatch(s -> s == null || mod.subsorts().lessThanEq(s, patternSort))) {
             subst.put((KVariable) pattern, subject);

diff --git a/kernel/src/main/java/org/kframework/compile/GenerateCoverage.java b/kernel/src/main/java/org/kframework/compile/GenerateCoverage.java
@@ -16,7 +16,7 @@
 public record GenerateCoverage(boolean cover, FileUtil files) {
 
   public K gen(RuleOrClaim r, K body, Module mod) {
-    if (!cover || r.att().getOptional(Source.class).isEmpty()) {
+    if (!cover || r.att().getOptional(Att.SOURCE(), Source.class).isEmpty()) {
       return body;
     }
     K left = RewriteToTop.toLeft(body);

diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java b/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java
@@ -105,8 +105,12 @@ private static Tuple4<Set<Sentence>, List<Sort>, K, Boolean> genInternal(
 
                 K cellContents = kapp.klist().items().get(2);
                 Att att = cfgAtt;
-                if (kapp.att().contains(Location.class))
-                  att = cfgAtt.add(Location.class, kapp.att().get(Location.class));
+                if (kapp.att().contains(Att.LOCATION(), Location.class))
+                  att =
+                      cfgAtt.add(
+                          Att.LOCATION(),
+                          Location.class,
+                          kapp.att().get(Att.LOCATION(), Location.class));
                 Tuple4<Set<Sentence>, List<Sort>, K, Boolean> childResult =
                     genInternal(cellContents, null, att, m);
 
@@ -201,7 +205,7 @@ private static Tuple4<Set<Sentence>, List<Sort>, K, Boolean> genInternal(
       // child of a leaf cell. Generate no productions, but inform parent that it has a child of a
       // particular sort.
       // A leaf cell initializes to the value specified in the configuration declaration.
-      Sort sort = kapp.att().get(Production.class).sort();
+      Sort sort = kapp.att().get(Att.PRODUCTION(), Production.class).sort();
       Tuple2<K, Set<Sentence>> res = getLeafInitializer(term);
       return Tuple4.apply(res._2(), Lists.newArrayList(sort), res._1(), true);
     } else if (term instanceof KToken ktoken) {
@@ -311,7 +315,7 @@ class Holder {
           @Override
           public K apply(KApply k) {
             if (k.klabel().name().startsWith("#SemanticCastTo")) {
-              sort = k.att().get(Production.class).sort();
+              sort = k.att().get(Att.PRODUCTION(), Production.class).sort();
             }
             return super.apply(k);
           }
@@ -335,7 +339,8 @@ public K apply(KToken k) {
         h.sentences);
   }
 
-  private static final KVariable INIT = KVariable("Init", Att.empty().add(Sort.class, Sorts.Map()));
+  private static final KVariable INIT =
+      KVariable("Init", Att.empty().add(Att.SORT(), Sort.class, Sorts.Map()));
 
   /**
    * Generates the sentences associated with a particular cell.
@@ -659,7 +664,8 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
                     NonTerminal(sort),
                     Terminal(")")),
                 Att().add(Att.FUNCTION()).add(Att.TOTAL()));
-        KVariable key = KVariable("Key", Att.empty().add(Sort.class, childSorts.get(0)));
+        KVariable key =
+            KVariable("Key", Att.empty().add(Att.SORT(), Sort.class, childSorts.get(0)));
         Rule cellMapKeyRule =
             Rule(
                 KRewrite(
@@ -721,7 +727,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
                   Terminal(")")),
               Att.empty().add(Att.FUNCTION()));
       sentences.add(getExitCode);
-      KVariable var = KVariable("Exit", Att.empty().add(Sort.class, Sorts.Int()));
+      KVariable var = KVariable("Exit", Att.empty().add(Att.SORT(), Sort.class, Sorts.Int()));
       Rule getExitCodeRule =
           Rule(
               KRewrite(

diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateRules.java b/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateRules.java
@@ -59,7 +59,9 @@ private Stream<? extends Sentence> gen(Sort sort) {
       res.add(
           Rule(
               KRewrite(
-                  KApply(KLabel("is" + sort), KVariable(sort.name(), Att().add(Sort.class, sort))),
+                  KApply(
+                      KLabel("is" + sort),
+                      KVariable(sort.name(), Att().add(Att.SORT(), Sort.class, sort))),
                   BooleanUtils.TRUE),
               BooleanUtils.TRUE,
               BooleanUtils.TRUE));

diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java b/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java
@@ -71,7 +71,7 @@ public Stream<? extends Sentence> gen(Sort sort) {
       return Stream.empty();
     }
     KLabel lbl = getProjectLbl(sort);
-    KVariable var = KVariable("K", Att.empty().add(Sort.class, sort));
+    KVariable var = KVariable("K", Att.empty().add(Att.SORT(), Sort.class, sort));
     Rule r =
         Rule(
             KRewrite(KApply(lbl, var), var),
@@ -105,7 +105,9 @@ public Stream<? extends Sentence> gen(Sort sort) {
           Rule(
               KRewrite(
                   KApply(
-                      sideEffectLbl, KVariable("K2", Att.empty().add(Sort.class, Sorts.K())), var),
+                      sideEffectLbl,
+                      KVariable("K2", Att.empty().add(Att.SORT(), Sort.class, Sorts.K())),
+                      var),
                   var),
               BooleanUtils.TRUE,
               BooleanUtils.TRUE);
@@ -125,7 +127,7 @@ public Stream<? extends Sentence> gen(Production prod) {
     int i = 0;
     boolean hasName = false;
     for (NonTerminal nt : iterable(prod.nonterminals())) {
-      vars.add(KVariable("K" + i++, Att.empty().add(Sort.class, nt.sort())));
+      vars.add(KVariable("K" + i++, Att.empty().add(Att.SORT(), Sort.class, nt.sort())));
       hasName = hasName || nt.name().isDefined();
     }
     if (!hasName) {

diff --git a/kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java b/kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java
@@ -93,7 +93,9 @@ KVariable newDotVariable(Sort s) {
     }
     KVariable newLabel;
     do {
-      newLabel = KVariable("_Gen" + (counter++), Att().add(Att.ANONYMOUS()).add(Sort.class, s));
+      newLabel =
+          KVariable(
+              "_Gen" + (counter++), Att().add(Att.ANONYMOUS()).add(Att.SORT(), Sort.class, s));
     } while (vars.contains(newLabel));
     vars.add(newLabel);
     return newLabel;