Parametric Sorts (#7)

* Added support for parametric sorts and correct conversion of identifiers with numeral arguments. Added shadowJar to gradle config to make fat JAR directly executable.

* Added readme note pointing to parser version.

Author: Shoooooon

README.md

@@ -67,4 +67,6 @@ problem, then dumps it to standard output:
 $ java -jar semgus-java.jar max2-exp.sem.json
 ```
 
+The current JSON format is in line with the 2-23-24 edition of Semgus-Parser which introduced support for parametric sorts.
+
 For more information, check out all the declarations and accompanying JavaDocs in the source code.

build.gradle.kts

@@ -1,6 +1,7 @@
 plugins {
     java
     `maven-publish`
+    id("com.github.johnrengelman.shadow") version "7.0.0"
 }
 
 group = "org.semgus"
@@ -38,6 +39,15 @@ tasks.getByName<Jar>("jar") {
     }
 }
 
+tasks.shadowJar {
+    configurations = listOf(project.configurations.getByName("runtimeClasspath")) // Include runtime dependencies in shadow JAR
+    manifest {
+        attributes(
+            "Main-Class" to "org.semgus.java.Main"
+        )
+    }
+}
+
 publishing {
     publications {
         create<MavenPublication>("maven") {

src/main/java/org/semgus/java/event/EventParser.java

@@ -164,13 +164,13 @@ private static DeclareFunctionEvent parseDeclareFunction(JSONObject eventDto) th
         String name = JsonUtils.getString(eventDto, "name");
         JSONObject rankDto = JsonUtils.getObject(eventDto, "rank");
 
-        Identifier returnType;
-        List<Identifier> argumentTypes;
+        Sort returnType;
+        List<Sort> argumentTypes;
         try {
-            returnType = Identifier.deserializeAt(rankDto, "returnSort");
+            returnType = Sort.deserializeAt(rankDto, "returnSort");
             JSONArray argumentTypesDto = JsonUtils.getArray(rankDto, "argumentSorts");
             try {
-                argumentTypes = Identifier.deserializeList(argumentTypesDto);
+                argumentTypes = Sort.deserializeList(argumentTypesDto);
             } catch (DeserializationException e) {
                 throw e.prepend("argumentSorts");
             }
@@ -246,9 +246,9 @@ private static DefineDatatypeEvent parseDefineDatatype(JSONObject eventDto) thro
                 String constructorName = JsonUtils.getString(constructorDto, "name");
                 JSONArray argumentTypesDto = JsonUtils.getArray(constructorDto, "children");
 
-                List<Identifier> argumentTypes;
+                List<Sort> argumentTypes;
                 try {
-                    argumentTypes = Identifier.deserializeList(argumentTypesDto);
+                    argumentTypes = Sort.deserializeList(argumentTypesDto);
                 } catch (DeserializationException e) {
                     throw e.prepend("children");
                 }
@@ -331,10 +331,10 @@ private static HornClauseEvent parseHornClause(JSONObject eventDto) throws Deser
                     "constructor");
         }
 
-        // parse constructor arg type identifiers
-        List<Identifier> constructorArgTypes;
+        // parse constructor arg type sorts
+        List<Sort> constructorArgTypes;
         try {
-            constructorArgTypes = Identifier.deserializeList(constructorArgTypesDto);
+            constructorArgTypes = Sort.deserializeList(constructorArgTypesDto);
         } catch (DeserializationException e) {
             throw e.prepend("constructor.argumentSorts");
         }

src/main/java/org/semgus/java/event/SmtSpecEvent.java

@@ -1,6 +1,6 @@
 package org.semgus.java.event;
 
-import org.semgus.java.object.Identifier;
+import org.semgus.java.object.Sort;
 import org.semgus.java.object.SmtTerm;
 import org.semgus.java.object.TypedVar;
 
@@ -21,8 +21,8 @@ public sealed interface SmtSpecEvent extends SpecEvent {
      */
     record DeclareFunctionEvent(
             String name,
-            Identifier returnType,
-            List<Identifier> argumentTypes
+            Sort returnType,
+            List<Sort> argumentTypes
     ) implements SmtSpecEvent {
         // NO-OP
     }
@@ -37,7 +37,7 @@ record DeclareFunctionEvent(
      */
     record DefineFunctionEvent(
             String name,
-            Identifier returnType,
+            Sort returnType,
             List<TypedVar> arguments,
             SmtTerm body
     ) implements SmtSpecEvent {
@@ -76,7 +76,7 @@ record DefineDatatypeEvent(String name, List<Constructor> constructors) implemen
          * @param name          The name of the constructor.
          * @param argumentTypes The types of the arguments to the constructor.
          */
-        public record Constructor(String name, List<Identifier> argumentTypes) {
+        public record Constructor(String name, List<Sort> argumentTypes) {
             // NO-OP
         }
 

src/main/java/org/semgus/java/object/Identifier.java

@@ -52,50 +52,14 @@ public static Identifier deserialize(Object idDtoRaw) throws DeserializationExce
         throw new DeserializationException("Identifier must either be a string or an array!");
     }
 
-    /**
-     * Deserializes an identifier from the SemGuS JSON format at a given key in a parent JSON object.
-     *
-     * @param parentDto The parent JSON object.
-     * @param key       The key whose value should be deserialized.
-     * @return The deserialized identifier.
-     * @throws DeserializationException If the value at {@code key} is not a valid representation of an identifier.
-     */
-    public static Identifier deserializeAt(JSONObject parentDto, String key) throws DeserializationException {
-        Object identifierDto = JsonUtils.get(parentDto, key);
-        try {
-            return deserialize(identifierDto);
-        } catch (DeserializationException e) {
-            throw e.prepend(key);
-        }
-    }
-
-    /**
-     * Deserializes a list of identifiers from a JSON array.
-     *
-     * @param idsDto The JSON array of identifiers.
-     * @return The list of the deserialized identifiers.
-     * @throws DeserializationException If {@code idsDto} is not an array of valid representations of identifiers.
-     */
-    public static List<Identifier> deserializeList(JSONArray idsDto) throws DeserializationException {
-        Identifier[] ids = new Identifier[idsDto.size()];
-        for (int i = 0; i < ids.length; i++) {
-            try {
-                ids[i] = deserialize(idsDto.get(i));
-            } catch (DeserializationException e) {
-                throw e.prepend(i);
-            }
-        }
-        return Arrays.asList(ids);
-    }
-
     @Override
     public String toString() {
         if (indices.length == 0) {
             return name;
         }
-        StringBuilder sb = new StringBuilder("(").append(name);
+        StringBuilder sb = new StringBuilder("(_ ").append(name);
         for (Index index : indices) {
-            sb.append(" ").append(index);
+            sb.append(" ").append(index.toString());
         }
         return sb.append(")").toString();
     }
@@ -113,26 +77,10 @@ public sealed interface Index {
          * @throws DeserializationException If {@code indexDtoRaw} is not a valid representation of an index value.
          */
         static Index deserialize(Object indexDtoRaw) throws DeserializationException {
-            if (indexDtoRaw instanceof String index) {
-                return new NString(index);
-            } else if (indexDtoRaw instanceof Long index) {
+            if (indexDtoRaw instanceof Long index) {
                 return new NInt(index.intValue());
             }
-            throw new DeserializationException("Identifier index must either be a string or integer constant!");
-        }
-
-        /**
-         * A string index value.
-         *
-         * @param value The string value.
-         */
-        record NString(String value) implements Index {
-
-            @Override
-            public String toString() {
-                return "\"" + value + "\"";
-            }
-
+            throw new DeserializationException("Identifier index must be an integer constant!");
         }
 
         /**

src/main/java/org/semgus/java/object/RelationApp.java

@@ -35,10 +35,10 @@ public static RelationApp deserialize(JSONObject relAppDto) throws Deserializati
                     sigDto.size(), args.size()));
         }
 
-        // deserialize type identifiers
-        List<Identifier> types;
+        // deserialize type sorts
+        List<Sort> types;
         try {
-            types = Identifier.deserializeList(sigDto);
+            types = Sort.deserializeList(sigDto);
         } catch (DeserializationException e) {
             throw e.prepend("signature");
         }

src/main/java/org/semgus/java/object/SmtContext.java

@@ -52,7 +52,7 @@ public String toString() {
          * @param name          The name of the constructor.
          * @param argumentTypes The types of the constructor's arguments.
          */
-        public record Constructor(String name, List<Identifier> argumentTypes) {
+        public record Constructor(String name, List<Sort> argumentTypes) {
 
             @Override
             public String toString() {
@@ -61,7 +61,7 @@ public String toString() {
                 }
 
                 StringBuilder sb = new StringBuilder("(").append(name);
-                for (Identifier argumentType : argumentTypes) {
+                for (Sort argumentType : argumentTypes) {
                     sb.append(" ").append(argumentType);
                 }
                 return sb.append(")").toString();

src/main/java/org/semgus/java/object/SmtTerm.java

@@ -69,9 +69,9 @@ static SmtTerm deserializeAt(JSONObject parentDto, String key) throws Deserializ
      * @throws DeserializationException If {@code termDto} is not a valid representation of a function application.
      */
     private static SmtTerm deserializeApplication(JSONObject termDto) throws DeserializationException {
-        // deserialize function and return type identifiers
-        Identifier id = Identifier.deserializeAt(termDto, "name");
-        Identifier returnType = Identifier.deserializeAt(termDto, "returnSort");
+        // deserialize function and return type sorts
+        Sort id = Sort.deserializeAt(termDto, "name");
+        Sort returnType = Sort.deserializeAt(termDto, "returnSort");
 
         // zip together argument terms and argument types
         JSONArray argTypes = JsonUtils.getArray(termDto, "argumentSorts");
@@ -84,9 +84,9 @@ private static SmtTerm deserializeApplication(JSONObject termDto) throws Deseria
         Application.TypedTerm[] argTerms = new Application.TypedTerm[argTypes.size()];
         for (int i = 0; i < argTerms.length; i++) {
             // deserialize type
-            Identifier type;
+            Sort type;
             try {
-                type = Identifier.deserialize(argTypes.get(i));
+                type = Sort.deserialize(argTypes.get(i));
             } catch (DeserializationException e) {
                 throw e.prepend("argumentSorts." + i);
             }
@@ -122,7 +122,7 @@ private static SmtTerm deserializeQuantifier(JSONObject termDto, Quantifier.Type
             JSONObject bindingDto = bindingsDto.get(i);
             try {
                 bindings[i] = new TypedVar(JsonUtils.getString(bindingDto, "name"),
-                        Identifier.deserializeAt(bindingDto, "sort"));
+                        Sort.deserializeAt(bindingDto, "sort"));
             } catch (DeserializationException e) {
                 throw e.prepend("bindings." + i);
             }
@@ -180,7 +180,7 @@ private static SmtTerm deserializeMatch(JSONObject termDto) throws Deserializati
      * @throws DeserializationException If {@code termDto} is not a valid representation of a variable.
      */
     private static SmtTerm deserializeVariable(JSONObject termDto) throws DeserializationException {
-        return new Variable(JsonUtils.getString(termDto, "name"), Identifier.deserializeAt(termDto, "sort"));
+        return new Variable(JsonUtils.getString(termDto, "name"), Sort.deserializeAt(termDto, "sort"));
     }
 
     /**
@@ -261,11 +261,11 @@ private static int readHexChar(char hexChar) throws DeserializationException {
     /**
      * Represents a function application in an SMT formula.
      *
-     * @param name       The identifier for the function.
+     * @param name       The Sort for the function.
      * @param returnType The function's return type.
      * @param arguments  The arguments to the function.
      */
-    record Application(Identifier name, Identifier returnType, List<TypedTerm> arguments) implements SmtTerm {
+    record Application(Sort name, Sort returnType, List<TypedTerm> arguments) implements SmtTerm {
 
         @Override
         public String toString() {
@@ -279,7 +279,7 @@ public String toString() {
          * @param type The argument type.
          * @param term The subterm being passed as an argument.
          */
-        public record TypedTerm(Identifier type, SmtTerm term) {
+        public record TypedTerm(Sort type, SmtTerm term) {
 
             @Override
             public String toString() {
@@ -398,9 +398,9 @@ public String toString() {
      * Represents a variable in an SMT formula.
      *
      * @param name The name of the variable.
-     * @param type The identifier for the type of the variable.
+     * @param type The Sort for the type of the variable.
      */
-    record Variable(String name, Identifier type) implements SmtTerm {
+    record Variable(String name, Sort type) implements SmtTerm {
 
         @Override
         public String toString() {