Add support for annotations in DefineFunctionEvent

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

@@ -117,7 +117,7 @@ public static SpecEvent parseEvent(String eventJson) throws ParseException, Dese
      */
     public static SpecEvent parseEvent(JSONObject eventDto) throws DeserializationException {
         String eventType = JsonUtils.getString(eventDto, "$event");
-        return switch (eventType) {
+        SpecEvent event =  switch (eventType) {
             // meta events
             case "set-info" -> parseSetInfo(eventDto);
             case "end-of-stream" -> new MetaSpecEvent.StreamEndEvent();
@@ -138,6 +138,8 @@ public static SpecEvent parseEvent(JSONObject eventDto) throws DeserializationEx
             default -> throw new DeserializationException(
                     String.format("Unknown specification event \"%s\"", eventType), "$event");
         };
+
+        return event;
     }
 
     /**
@@ -164,13 +166,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");
             }
@@ -196,6 +198,7 @@ private static DefineFunctionEvent parseDefineFunction(JSONObject eventDto) thro
 
         TypedVar[] arguments = new TypedVar[declEvent.argumentTypes().size()];
         SmtTerm body;
+        HashMap<String, AttributeValue> annotationMap = new HashMap<>();
         try {
             List<String> argNames = JsonUtils.getStrings(defnDto, "arguments");
             if (argNames.size() != arguments.length) {
@@ -210,11 +213,31 @@ private static DefineFunctionEvent parseDefineFunction(JSONObject eventDto) thro
             }
 
             body = SmtTerm.deserializeAt(defnDto, "body");
+
+            var bodyObj = JsonUtils.getObject(defnDto, "body");
+
+            if (bodyObj.containsKey("annotations")) {
+                Object annotationsObj = bodyObj.get("annotations");
+
+                if (!(annotationsObj instanceof JSONArray annotations)) {
+                    throw new DeserializationException("Annotation is neither null nor an array");
+                }
+
+                JsonUtils.ensureObjects(annotations);
+                for (Object annotationItemObj : annotations) {
+                    var annotationItem = (JSONObject) annotationItemObj;
+                    var keywordObj = JsonUtils.getObject(annotationItem, "keyword");
+                    var keyword = JsonUtils.getString(keywordObj, "name");
+                    var value = AttributeValue.deserializeAt(annotationItem, "value");
+                    annotationMap.put(keyword, value);
+                }
+            }
         } catch (DeserializationException e) {
             throw e.prepend("definition");
         }
 
-        return new DefineFunctionEvent(declEvent.name(), declEvent.returnType(), Arrays.asList(arguments), body);
+        return new DefineFunctionEvent(declEvent.name(), declEvent.returnType(),
+                Arrays.asList(arguments), body, annotationMap);
     }
 
     /**
@@ -246,9 +269,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 +354,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,10 +1,13 @@
 package org.semgus.java.event;
 
-import org.semgus.java.object.Identifier;
+import org.semgus.java.object.AttributeValue;
+import org.semgus.java.object.Sort;
 import org.semgus.java.object.SmtTerm;
 import org.semgus.java.object.TypedVar;
 
+import java.util.HashMap;
 import java.util.List;
+import java.util.Map;
 import java.util.stream.Collectors;
 
 /**
@@ -21,8 +24,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
     }
@@ -34,14 +37,21 @@ record DeclareFunctionEvent(
      * @param returnType The return type of the function.
      * @param arguments  The arguments to the function.
      * @param body       The body of the function.
+     * @param annotations The annotations (usually about input/output variables) on the function body. (optional)
      */
     record DefineFunctionEvent(
             String name,
-            Identifier returnType,
+            Sort returnType,
             List<TypedVar> arguments,
-            SmtTerm body
+            SmtTerm body,
+            Map<String, AttributeValue> annotations
     ) implements SmtSpecEvent {
 
+        public DefineFunctionEvent(String name, Sort returnType, List<TypedVar> arguments,
+                            SmtTerm body) {
+            this(name, returnType, arguments, body, new HashMap<>());
+        }
+
         /**
          * Constructs a {@link org.semgus.java.object.SmtTerm.Lambda} lambda abstraction from the function definition.
          *
@@ -76,7 +86,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

@@ -48,54 +48,38 @@ public static Identifier deserialize(Object idDtoRaw) throws DeserializationExce
             }
 
             return new Identifier((String)nameRaw, indices);
-        }
-        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);
+        } else if (idDtoRaw instanceof JSONObject idDto) {
+            // it's possibly a (Seq Int) or other types defined in a similar way
+            Object nameRaw = idDto.get("kind");
+            if (!(nameRaw instanceof String name)) {
+                throw new DeserializationException("Identifier name must be a string!", 0);
+            }
+            Object paramsRaw = idDto.get("params");
+            if (!(paramsRaw instanceof JSONArray params)) {
+                throw new DeserializationException("'params' is not a JSON array!", 1);
+            }
+            Index[] indices = new Index[params.size()];
+            for (int i = 0; i < indices.length; i++) {
+                try {
+                    indices[i] = Index.deserialize(params.get(i));
+                } catch (DeserializationException e) {
+                    throw e.prepend(i + 1);
+                }
             }
+
+            return new Identifier(name, indices);
         }
-        return Arrays.asList(ids);
+        throw new DeserializationException("Identifier must either be a string, an array or an object containing keys 'kind' and 'params'!");
     }
 
     @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 +97,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();