Handle sort parameters correctly in JSON Kast format

k-distribution/tests/regression-new/json-input/json-in1.json.kast

@@ -1 +1 @@
-{"format":"KAST","version":3,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K"},{"node":"KSort","name":"K"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"4"}]}}
+{"format":"KAST","version":4,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K","params":[]},{"node":"KSort","name":"K","params":[]}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"4"}]}}

k-distribution/tests/regression-new/json-input/json-in2.json.kast

@@ -1 +1 @@
-{"format":"KAST","version":3,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K"},{"node":"KSort","name":"K"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3"}]}}
+{"format":"KAST","version":4,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K","params":[]},{"node":"KSort","name":"K","params":[]}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"3"}]}}

k-distribution/tests/regression-new/json-input/json-in3.json.kast

@@ -1 +1 @@
-{"format":"KAST","version":3,"term":{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"K"}]},"variable":false,"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<k>","params":[]},"variable":false,"arity":1,"args":[{"node":"KVariable","name":"N"}]},{"node":"KApply","label":{"node":"KLabel","name":"_>=Int_","params":[]},"variable":false,"arity":2,"args":[{"node":"KVariable","name":"N"},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0"}]}]}}
+{"format":"KAST","version":4,"term":{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"K","params":[]}]},"variable":false,"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<k>","params":[]},"variable":false,"arity":1,"args":[{"node":"KVariable","name":"N"}]},{"node":"KApply","label":{"node":"KLabel","name":"_>=Int_","params":[]},"variable":false,"arity":2,"args":[{"node":"KVariable","name":"N"},{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"0"}]}]}}

k-frontend/src/main/java/org/kframework/parser/json/JsonParser.java

@@ -42,7 +42,6 @@
 import org.kframework.kore.KLabel;
 import org.kframework.kore.KORE;
 import org.kframework.kore.Sort;
-import org.kframework.parser.outer.Outer;
 import org.kframework.parser.outer.ParseRegex;
 import org.kframework.unparser.ToJson;
 import org.kframework.utils.errorsystem.KEMException;
@@ -288,7 +287,12 @@ private static Sort toSort(JsonObject data) {
     if (!data.getString("node").equals(KSORT))
       throw KEMException.criticalError(
           "Unexpected node found in KAST Json term: " + data.getString("node"));
-    return Outer.parseSort(data.getString("name"));
+    String name = data.getString("name");
+    List<Sort> params = new ArrayList<>();
+    for (JsonValue p : data.getJsonArray("params")) {
+      params.add(toSort((JsonObject) p));
+    }
+    return Sort(name, params);
   }
 
   private static ProductionItem toProductionItem(JsonObject data) {

k-frontend/src/main/java/org/kframework/unparser/ToJson.java

@@ -53,7 +53,7 @@
 /** Writes a KAST term to the KAST Json format. */
 public class ToJson {
 
-  public static final int version = 3;
+  public static final int version = 4;
 
   ///////////////////////////////
   // ToJson Definition Objects //
@@ -381,11 +381,11 @@ public static JsonObject toJson(ProductionItem prod) {
 
   public static JsonStructure toJson(Sort sort) {
     JsonObjectBuilder jsort = factory.createObjectBuilder();
-
     jsort.add("node", JsonParser.KSORT);
-    // store sort and its parameters as a flat string
-    jsort.add("name", sort.toString());
-
+    jsort.add("name", sort.name());
+    JsonArrayBuilder jparams = factory.createArrayBuilder();
+    JavaConverters.seqAsJavaList(sort.params()).forEach(p -> jparams.add(toJson(p)));
+    jsort.add("params", jparams.build());
     return jsort.build();
   }
 

pyk/regression-new/json-input/json-in1.json.kast

@@ -1 +1 @@
-{"format":"KAST","version":3,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K"},{"node":"KSort","name":"K"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"4"}]}}
+{"format":"KAST","version":4,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K","params":[]},{"node":"KSort","name":"K","params":[]}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"4"}]}}

pyk/regression-new/json-input/json-in2.json.kast

@@ -1 +1 @@
-{"format":"KAST","version":3,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K"},{"node":"KSort","name":"K"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3"}]}}
+{"format":"KAST","version":4,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K","params":[]},{"node":"KSort","name":"K","params":[]}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"3"}]}}

pyk/regression-new/json-input/json-in3.json.kast

@@ -1 +1 @@
-{"format":"KAST","version":3,"term":{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"K"}]},"variable":false,"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<k>","params":[]},"variable":false,"arity":1,"args":[{"node":"KVariable","name":"N"}]},{"node":"KApply","label":{"node":"KLabel","name":"_>=Int_","params":[]},"variable":false,"arity":2,"args":[{"node":"KVariable","name":"N"},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0"}]}]}}
+{"format":"KAST","version":4,"term":{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"K","params":[]}]},"variable":false,"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<k>","params":[]},"variable":false,"arity":1,"args":[{"node":"KVariable","name":"N"}]},{"node":"KApply","label":{"node":"KLabel","name":"_>=Int_","params":[]},"variable":false,"arity":2,"args":[{"node":"KVariable","name":"N"},{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"0"}]}]}}

pyk/src/pyk/kast/inner.py

@@ -27,25 +27,29 @@
 @final
 @dataclass(frozen=True)
 class KSort(KAst):
-    """Store a simple sort name."""
+    """Represent a K sort, optionally applied to sort parameters."""
 
     name: str
+    params: tuple[KSort, ...]
 
-    def __init__(self, name: str):
-        """Construct a new sort given the name."""
+    def __init__(self, name: str, params: Iterable[KSort] = ()):
         object.__setattr__(self, 'name', name)
+        object.__setattr__(self, 'params', tuple(params))
 
     @staticmethod
     def from_dict(d: Mapping[str, Any]) -> KSort:
-        return KSort(name=d['name'])
+        return KSort(
+            name=d['name'],
+            params=(KSort.from_dict(p) for p in d.get('params', ())),
+        )
 
     def to_dict(self) -> dict[str, Any]:
-        return {'node': 'KSort', 'name': self.name}
+        return {'node': 'KSort', 'name': self.name, 'params': [p.to_dict() for p in self.params]}
 
-    def let(self, *, name: str | None = None) -> KSort:
-        """Return a new `KSort` with the name potentially updated."""
+    def let(self, *, name: str | None = None, params: Iterable[KSort] | None = None) -> KSort:
         name = name if name is not None else self.name
-        return KSort(name=name)
+        params = params if params is not None else self.params
+        return KSort(name=name, params=params)
 
 
 @final

pyk/src/pyk/kast/kast.py

@@ -20,7 +20,7 @@
 class KAst(ABC):
     @staticmethod
     def version() -> int:
-        return 3
+        return 4
 
     @abstractmethod
     def to_dict(self) -> dict[str, Any]: ...

pyk/src/pyk/konvert/_module_to_kore.py

@@ -212,19 +212,22 @@ def _parse_special_att_value(key: AttKey, value: Any) -> tuple[tuple[Sort, ...],
 
 def sort_decl_to_kore(syntax_sort: KSyntaxSort) -> SortDecl:
     name = _sort_name(syntax_sort.sort.name)
+    # Kore sort declarations use canonical indexed sort variable names (SortS0, SortS1, ...)
+    sort_vars = tuple(SortVar(f'SortS{i}') for i in range(len(syntax_sort.sort.params)))
     attrs = atts_to_kore(syntax_sort.att)
     hooked = Atts.HOOK in syntax_sort.att
-    return SortDecl(name, (), attrs=attrs, hooked=hooked)
+    return SortDecl(name, sort_vars, attrs=attrs, hooked=hooked)
 
 
 def sort_to_kore(sort: KSort, production: KProduction | None = None) -> Sort:
     if production and sort in production.params:
         return _sort_var(sort)
-    return _sort_app(sort)
+    return _sort_app(sort, production)
 
 
-def _sort_app(sort: KSort) -> SortApp:
-    return SortApp(_sort_name(sort.name))
+def _sort_app(sort: KSort, production: KProduction | None = None) -> SortApp:
+    sort_args = tuple(sort_to_kore(p, production) for p in sort.params)
+    return SortApp(_sort_name(sort.name), sort_args)
 
 
 def _sort_var(sort: KSort) -> SortVar:
@@ -638,6 +641,10 @@ def prods_by_sort() -> dict[KSort, list[KProduction]]:
     res: list[Axiom] = []
     prods = prods_by_sort()
     for syntax_sort in module.syntax_sorts:
+        # Parameterized sorts (e.g. MInt{Width}) have sort-variable parameters;
+        # Java does not generate no-junk axioms for them.
+        if syntax_sort.sort.params:
+            continue
         no_junk = no_junk_for(syntax_sort, prods.get(syntax_sort.sort, []))
         axiom = no_junk.axiom()
         if axiom:

pyk/src/tests/integration/konvert/test_module_to_kore.py

@@ -56,7 +56,6 @@ def kore_module(definition_dir: Path, definition_info: DefinitionInfo) -> Module
 IGNORED_SYMBOL_ATTRS: Final = {"symbol'Kywd'"}
 
 
-@pytest.mark.skip('TODO: https://github.com/runtimeverification/k/issues/4653')
 def test_module_to_kore(kast_defn: KDefinition, kore_module: Module) -> None:
     # Given
     expected = kore_module