JSON post process - re added

k-distribution/tests/regression-new/imp-haskell/Makefile

@@ -2,7 +2,7 @@ DEF=imp
 EXT=imp
 TESTDIR=.
 KOMPILE_BACKEND=haskell
-KOMPILE_FLAGS=--no-haskell-binary
+KOMPILE_FLAGS=--post-process 'cat' --no-haskell-binary
 KPROVE_FLAGS=--def-module VERIFICATION
 export KOMPILE_BACKEND
 export KPROVE_FLAGS

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

@@ -1 +1 @@
-{"format":"KAST","version":2,"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","originalName":"N"}]},{"node":"KApply","label":{"node":"KLabel","name":"_>=Int_","params":[]},"variable":false,"arity":2,"args":[{"node":"KVariable","name":"N","originalName":"N"},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0"}]}]}}
+{"format":"KAST","version":2,"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","att":{"node":"KAtt","att":{}}}]},{"node":"KApply","label":{"node":"KLabel","name":"_>=Int_","params":[]},"variable":false,"arity":2,"args":[{"node":"KVariable","name":"N","att":{"node":"KAtt","att":{}}},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0"}]}]}}

kernel/src/main/java/org/kframework/kompile/Kompile.java

@@ -2,6 +2,7 @@
 package org.kframework.kompile;
 
 import com.google.inject.Inject;
+import org.apache.commons.io.FileUtils;
 import org.kframework.Strategy;
 import org.kframework.attributes.Att;
 import org.kframework.attributes.Location;
@@ -29,8 +30,10 @@
 import org.kframework.definition.Sentence;
 import org.kframework.kore.KLabel;
 import org.kframework.kore.Sort;
+import org.kframework.krun.RunProcess;
 import org.kframework.main.GlobalOptions;
 import org.kframework.parser.InputModes;
+import org.kframework.parser.json.JsonParser;
 import org.kframework.parser.KRead;
 import org.kframework.parser.ParserUtils;
 import org.kframework.parser.inner.RuleGrammarGenerator;
@@ -55,10 +58,13 @@
 import java.io.UnsupportedEncodingException;
 import java.nio.file.Files;
 import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.Collections;
 import java.util.EnumSet;
+import java.util.HashMap;
 import java.util.HashSet;
 import java.util.List;
+import java.util.Map;
 import java.util.Optional;
 import java.util.Set;
 import java.util.function.Consumer;
@@ -150,6 +156,11 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String
         // final check for sort correctness
         for (Module m : mutable(kompiledDefinition.modules()))
             m.checkSorts();
+        if (kompileOptions.postProcess != null) {
+            kompiledDefinition = postProcessJSON(kompiledDefinition, kompileOptions.postProcess);
+            files.saveToKompiled("post-processed.txt", kompiledDefinition.toString());
+        }
+
         files.saveToKompiled("allRules.txt", ruleSourceMap(kompiledDefinition));
 
         if (kompileOptions.emitJson) {
@@ -218,6 +229,29 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String
         return def;
     }
 
+    private Definition postProcessJSON(Definition defn, String postProcess) {
+        List<String> command = new ArrayList<>(Arrays.asList(postProcess.split(" ")));
+        Map<String, String> environment = new HashMap<>();
+        File compiledJson;
+        try {
+            String inputDefinition = new String(ToJson.apply(defn), "UTF-8");
+            compiledJson = files.resolveTemp("post-process-compiled.json");
+            FileUtils.writeStringToFile(compiledJson, inputDefinition);
+        } catch (UnsupportedEncodingException e) {
+            throw KEMException.criticalError("Could not encode definition to JSON!");
+        } catch (IOException e) {
+            throw KEMException.criticalError("Could not make temporary file!");
+        }
+        command.add(compiledJson.getAbsolutePath());
+        RunProcess.ProcessOutput output = RunProcess.execute(environment, files.getProcessBuilder(), command.toArray(new String[command.size()]));
+        sw.printIntermediate("Post process JSON: " + String.join(" ", command));
+        if (output.exitCode != 0) {
+            throw KEMException.criticalError("Post-processing returned a non-zero exit code: "
+                    + output.exitCode + "\nStdout:\n" + new String(output.stdout) + "\nStderr:\n" + new String(output.stderr));
+        }
+        return JsonParser.parseDefinition(new String(output.stdout));
+    }
+
     private static String ruleSourceMap(Definition def) {
         List<String> ruleLocs = new ArrayList<String>();
         for (Sentence s: JavaConverters.setAsJavaSet(def.mainModule().sentences())) {

kernel/src/main/java/org/kframework/kompile/KompileOptions.java

@@ -133,4 +133,7 @@ public boolean isKore() {
 
     @Parameter(names="--debug-type-inference", description="Filename and source line of rule to debug type inference for. This is generally an option used only by maintaners.")
     public String debugTypeInference;
+
+    @Parameter(names={"--post-process"}, description="JSON KAST => JSON KAST converter to run on definition after kompile pipeline.")
+    public String postProcess;
 }

kernel/src/main/java/org/kframework/parser/json/JsonParser.java

@@ -2,6 +2,8 @@
 package org.kframework.parser.json;
 
 import org.kframework.attributes.Att;
+import org.kframework.attributes.Location;
+import org.kframework.attributes.Source;
 import org.kframework.definition.Associativity;
 import org.kframework.definition.Bubble;
 import org.kframework.definition.Claim;
@@ -145,7 +147,7 @@ public static FlatModule toFlatModule(JsonObject data) throws IOException {
 
         JsonArray jsonimports = data.getJsonArray("imports");
         Set<FlatImport> imports = new HashSet<>();
-        jsonimports.getValuesAs(JsonObject.class).forEach(i -> imports.add(FlatImport.apply(i.getString("name"), i.getBoolean("public"), Att.empty())));
+        jsonimports.getValuesAs(JsonObject.class).forEach(i -> imports.add(FlatImport.apply(i.getString("name"), i.getBoolean("isPublic"), Att.empty())));
 
         JsonArray sentences = data.getJsonArray("localSentences");
         Set<Sentence> localSentences = new HashSet<>();
@@ -160,7 +162,7 @@ public static FlatModule toFlatModule(JsonObject data) throws IOException {
 // Parsing Sentence Json //
 ///////////////////////////
 
-    public static Sentence toSentence(JsonObject data) throws IOException {
+    public static Sentence toSentence(JsonObject data) {
         switch(data.getString("node")) {
             case KCONTEXT: {
                 K body     = toK(data.getJsonObject("body"));
@@ -187,7 +189,7 @@ public static Sentence toSentence(JsonObject data) throws IOException {
                 Att att = toAtt(data.getJsonObject("att"));
                 List<scala.collection.Set<Tag>> syntaxPriorities = new ArrayList<>();
                 priorities.getValuesAs(JsonArray.class).forEach(tags -> syntaxPriorities.add(toTags(tags)));
-                return new SyntaxPriority(JavaConverters.iterableAsScalaIterableConverter(syntaxPriorities).asScala().toSeq(), att);
+                return new SyntaxPriority(immutable(syntaxPriorities), att);
             }
             case KSYNTAXASSOCIATIVITY: {
                 String assocString = data.getString("assoc");
@@ -212,7 +214,7 @@ public static Sentence toSentence(JsonObject data) throws IOException {
                 for (JsonObject s : data.getJsonArray("params").getValuesAs(JsonObject.class)) {
                     params.add(toSort(s));
                 }
-                return new SyntaxSort(JavaConverters.asScalaIteratorConverter(params.iterator()).asScala().toSeq(), sort, att);
+                return new SyntaxSort(immutable(params), sort, att);
             }
             case KSORTSYNONYM: {
                 Sort newSort = toSort(data.getJsonObject("newSort"));
@@ -233,7 +235,7 @@ public static Sentence toSentence(JsonObject data) throws IOException {
                 return new Bubble(sentenceType, contents, att);
             }
             case KPRODUCTION: {
-                Option<KLabel> klabel = Option.apply(data.containsKey("klabel") ? KLabel(data.getString("klabel")) : null);
+                Option<KLabel> klabel = Option.apply(data.containsKey("klabel") ? toKLabel(data.getJsonObject("klabel")) : null);
                 Sort sort             = toSort(data.getJsonObject("sort"));
                 Att att               = toAtt(data.getJsonObject("att"));
 
@@ -245,7 +247,7 @@ public static Sentence toSentence(JsonObject data) throws IOException {
                 for (JsonObject s : data.getJsonArray("params").getValuesAs(JsonObject.class)) {
                     params.add(toSort(s));
                 }
-                return new Production(klabel, JavaConverters.asScalaIteratorConverter(params.iterator()).asScala().toSeq(), sort, JavaConverters.asScalaIteratorConverter(pItems.iterator()).asScala().toSeq(), att);
+                return new Production(klabel, immutable(params), sort, immutable(pItems), att);
             }
             default:
                 throw KEMException.criticalError("Unexpected node found in KAST Json term: " + data.getString("node"));
@@ -296,7 +298,27 @@ public static Att toAtt(JsonObject data) {
         JsonObject attMap = data.getJsonObject("att");
         Att newAtt = Att.empty();
         for (String key: attMap.keySet()) {
-            newAtt = newAtt.add(key, attMap.getString(key));
+            if (key.equals(Location.class.getName())) {
+                JsonArray locarr = attMap.getJsonArray(Location.class.getName());
+                newAtt = newAtt.add(Location.class, Location(locarr.getInt(0), locarr.getInt(1), locarr.getInt(2), locarr.getInt(3)));
+            } else if (key.equals(Source.class.getName())) {
+                newAtt = newAtt.add(Source.class, Source.apply(attMap.getString(key)));
+            } else if (key.equals(Production.class.getName())) {
+                newAtt = newAtt.add(Production.class, (Production) toSentence(attMap.getJsonObject(key)));
+            } else if (key.equals(Sort.class.getName())) {
+                newAtt = newAtt.add(Sort.class, toSort(attMap.getJsonObject(key)));
+            } else if (key.equals("bracketLabel")) {
+                newAtt = newAtt.add("bracketLabel", KLabel.class, toKLabel(attMap.getJsonObject(key)));
+            } else if (key.equals(Att.PREDICATE())) {
+                newAtt = newAtt.add(Att.PREDICATE(), Sort.class, toSort(attMap.getJsonObject(key)));
+            } else if (key.equals("cellOptAbsent")) {
+                newAtt = newAtt.add("cellOptAbsent", Sort.class, toSort(attMap.getJsonObject(key)));
+            } else if (key.equals("cellFragment")) {
+                newAtt = newAtt.add("cellFragment", Sort.class, toSort(attMap.getJsonObject(key)));
+            } else if (key.equals("sortParams")) {
+                newAtt = newAtt.add("sortParams", Sort.class, toSort(attMap.getJsonObject(key)));
+            } else
+                newAtt = newAtt.add(key, attMap.getString(key));
         }
         return newAtt;
     }
@@ -319,23 +341,19 @@ public static K parse(String data) {
     }
 
     public static K parseJson(JsonObject data) {
-        try {
-            if (! (data.containsKey("format") && data.containsKey("version") && data.containsKey("term"))) {
-                throw KEMException.criticalError("Must have `format`, `version`, and `term` fields in serialized Json!");
-            }
-            if (! data.getString("format").equals("KAST")) {
-                throw KEMException.criticalError("Only can deserialize 'KAST' format Json! Found: " + data.getString("format"));
-            }
-            if (data.getInt("version") != ToJson.version) {
-                throw KEMException.criticalError("Only can deserialize KAST version '" + ToJson.version + "'! Found: " + data.getInt("version"));
-            }
-            return toK(data.getJsonObject("term"));
-        } catch (IOException e) {
-            throw KEMException.criticalError("Could not read K term from json", e);
+        if (! (data.containsKey("format") && data.containsKey("version") && data.containsKey("term"))) {
+            throw KEMException.criticalError("Must have `format`, `version`, and `term` fields in serialized Json!");
+        }
+        if (! data.getString("format").equals("KAST")) {
+            throw KEMException.criticalError("Only can deserialize 'KAST' format Json! Found: " + data.getString("format"));
+        }
+        if (data.getInt("version") != ToJson.version) {
+            throw KEMException.criticalError("Only can deserialize KAST version '" + ToJson.version + "'! Found: " + data.getInt("version"));
         }
+        return toK(data.getJsonObject("term"));
     }
 
-    private static K toK(JsonObject data) throws IOException {
+    private static K toK(JsonObject data) {
         KLabel klabel;
 
         switch (data.getString("node")) {
@@ -355,17 +373,17 @@ private static K toK(JsonObject data) throws IOException {
                 return KSequence(items);
 
             case KVARIABLE:
-                return KVariable(data.getString("name"));
+                return KVariable(data.getString("name"), toAtt(data.getJsonObject("att")));
 
             case KREWRITE:
                 K lhs = toK(data.getJsonObject("lhs"));
                 K rhs = toK(data.getJsonObject("rhs"));
-                return KRewrite(lhs, rhs);
+                return KRewrite(lhs, rhs, toAtt(data.getJsonObject("att")));
 
             case KAS:
                 K pattern = toK(data.getJsonObject("pattern"));
                 K alias   = toK(data.getJsonObject("alias"));
-                return KORE.KAs(pattern, alias);
+                return KORE.KAs(pattern, alias, toAtt(data.getJsonObject("att")));
 
             case INJECTEDKLABEL:
                 klabel    = toKLabel(data.getJsonObject("label"));
@@ -386,7 +404,7 @@ private static KLabel toKLabel(JsonObject data) {
         return KLabel(data.getString("name"), sarray);
     }
 
-    private static K[] toKs(int arity, JsonArray data) throws IOException {
+    private static K[] toKs(int arity, JsonArray data) {
         K[] items = new K[arity];
         for (int i = 0; i < arity; i++) {
             items[i] = toK(data.getValuesAs(JsonObject.class).get(i));

kernel/src/main/java/org/kframework/unparser/ToJson.java

@@ -2,6 +2,8 @@
 package org.kframework.unparser;
 
 import org.kframework.attributes.Att;
+import org.kframework.attributes.Location;
+import org.kframework.attributes.Source;
 import org.kframework.definition.Associativity;
 import org.kframework.definition.Bubble;
 import org.kframework.definition.Claim;
@@ -137,7 +139,32 @@ public static JsonStructure toJson(Att att) {
 
         JsonObjectBuilder jattKeys = Json.createObjectBuilder();
         for (Tuple2<String,String> key: JavaConverters.seqAsJavaList(att.att().keys().toSeq())) {
-            jattKeys.add(key._1(), att.att().get(key).get().toString());
+            if (key._1().equals(Location.class.getName())) {
+                JsonArrayBuilder locarr = Json.createArrayBuilder();
+                Location loc = att.get(Location.class);
+                locarr.add(loc.startLine());
+                locarr.add(loc.startColumn());
+                locarr.add(loc.endLine());
+                locarr.add(loc.endColumn());
+                jattKeys.add(key._1(), locarr.build());
+            } else if (key._1().equals(Source.class.getName())){
+                jattKeys.add(key._1(), att.get(Source.class).source());
+            } else if (key._1().equals(Production.class.getName())){
+                jattKeys.add(key._1(), toJson(att.get(Production.class)));
+            } else if (key._1().equals(Sort.class.getName())){
+                jattKeys.add(key._1(), toJson(att.get(Sort.class)));
+            } else if (key._1().equals("bracketLabel")) {
+                jattKeys.add(key._1(), toJson(att.get("bracketLabel", KLabel.class)));
+            } else if (key._1().equals(Att.PREDICATE())) {
+                jattKeys.add(key._1(), toJson(att.get(Att.PREDICATE(), Sort.class)));
+            } else if (key._1().equals("cellOptAbsent")) {
+                jattKeys.add(key._1(), toJson(att.get("cellOptAbsent", Sort.class)));
+            } else if (key._1().equals("cellFragment")) {
+                jattKeys.add(key._1(), toJson(att.get("cellFragment", Sort.class)));
+            } else if (key._1().equals("sortParams")) {
+                jattKeys.add(key._1(), toJson(att.get("sortParams", Sort.class)));
+            } else
+                jattKeys.add(key._1(), att.att().get(key).get().toString());
         }
         jatt.add("att", jattKeys.build());
 
@@ -320,7 +347,7 @@ public static JsonStructure toJson(Production pro) {
 
         Option<KLabel> klabel = pro.klabel();
         if (! klabel.isEmpty()) {
-            jpro.add("klabel", klabel.get().name());
+            jpro.add("klabel", toJson(klabel.get()));
         }
 
         JsonArrayBuilder productionItems = Json.createArrayBuilder();
@@ -408,6 +435,7 @@ public static JsonStructure toJson(K k) {
             knode.add("node", JsonParser.KTOKEN);
             knode.add("sort", toJson(tok.sort()));
             knode.add("token", tok.s());
+            knode.add("att", toJson(k.att()));
 
         } else if (k instanceof KApply) {
             KApply app = (KApply) k;
@@ -422,6 +450,7 @@ public static JsonStructure toJson(K k) {
 
             knode.add("arity", app.klist().size());
             knode.add("args", args.build());
+            knode.add("att", toJson(k.att()));
 
         } else if (k instanceof KSequence) {
             KSequence seq = (KSequence) k;
@@ -441,34 +470,30 @@ public static JsonStructure toJson(K k) {
 
             knode.add("node", JsonParser.KVARIABLE);
             knode.add("name", var.name());
-            Optional<String> origName = var.att().getOptional("originalName");
-            if (origName.isPresent()) {
-                knode.add("originalName", origName.get());
-            } else {
-                knode.add("originalName", var.name());
-            }
+            knode.add("att", toJson(k.att()));
 
         } else if (k instanceof KRewrite) {
             KRewrite rew = (KRewrite) k;
 
             knode.add("node", JsonParser.KREWRITE);
             knode.add("lhs", toJson(rew.left()));
             knode.add("rhs", toJson(rew.right()));
-            knode.add("att", rew.att().toString());
+            knode.add("att", toJson(k.att()));
 
         } else if (k instanceof KAs) {
             KAs alias = (KAs) k;
 
             knode.add("node", JsonParser.KAS);
             knode.add("pattern", toJson(alias.pattern()));
             knode.add("alias",   toJson(alias.alias()));
-            knode.add("att", alias.att().toString());
+            knode.add("att", toJson(k.att()));
 
         } else if (k instanceof InjectedKLabel) {
             InjectedKLabel inj = (InjectedKLabel) k;
 
             knode.add("node", JsonParser.INJECTEDKLABEL);
             knode.add("label", toJson(inj.klabel()));
+            knode.add("att", toJson(k.att()));
 
         } else {
             throw KEMException.criticalError("Unimplemented for JSON serialization: ", k);