From 06dec9c19000918715fd12b9975c4e5f13dcb51a Mon Sep 17 00:00:00 2001 From: Guy Repta Date: Tue, 18 Jun 2019 16:24:02 +0000 Subject: [PATCH 01/27] {JsonParser,ToJson}.java: Started implementing serialize/deserialize of Definitions --- .../kframework/parser/json/JsonParser.java | 169 ++++++++++++- .../java/org/kframework/unparser/ToJson.java | 232 +++++++++++++++++- 2 files changed, 389 insertions(+), 12 deletions(-) diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index f28b2ee2bfc..fd2cec96f31 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -1,6 +1,13 @@ // Copyright (c) 2018-2019 K Team. All Rights Reserved. package org.kframework.parser.json; +import org.kframework.attributes.Att; +import org.kframework.definition.Context; +import org.kframework.definition.Definition; +import org.kframework.definition.Module; +import org.kframework.definition.ModuleComment; +import org.kframework.definition.Rule; +import org.kframework.definition.Sentence; import org.kframework.kore.K; import org.kframework.kore.KLabel; import static org.kframework.kore.KORE.KLabel; @@ -18,26 +25,174 @@ import java.io.UnsupportedEncodingException; import java.io.StringReader; import java.util.Arrays; +import java.util.HashSet; +import java.util.Set; import javax.json.Json; import javax.json.JsonArray; import javax.json.JsonObject; import javax.json.JsonReader; +import scala.collection.JavaConverters; + /** * Parses a Json term into the KORE data structures. */ public class JsonParser { - public static final String KTOKEN = "KToken" - , KAPPLY = "KApply" - , KSEQUENCE = "KSequence" - , KVARIABLE = "KVariable" - , KREWRITE = "KRewrite" - , KAS = "KAs" - , INJECTEDKLABEL = "InjectedKLabel" + public static final String KDEFINITION = "KDefinition" + , KATT = "KAtt" + , KCONFIGURATION = "KConfiguration" + , KBUBBLE = "KBubble" + , KMODULE = "KModule" + , KCONTEXT = "KContext" + , KRULE = "KRule" + , KMODULECOMMENT = "KModuleComment" + , KSYNTAXPRIORITY = "KSyntaxPriority" + , KSYNTAXASSOCIATIVITY = "KSyntaxAssociativity" + , KTOKEN = "KToken" + , KSYNTAXSORT = "KSyntaxSort" + , KPRODUCTION = "KProduction" + , KAPPLY = "KApply" + , KSEQUENCE = "KSequence" + , KVARIABLE = "KVariable" + , KREWRITE = "KRewrite" + , KAS = "KAs" + , INJECTEDKLABEL = "InjectedKLabel" ; +///////////////////////////// +// Parsing Definition Json // +///////////////////////////// + + public static Definition parseDef(byte[] data) { + try { + return parseDef(new String(data, "UTF-8")); + } catch (UnsupportedEncodingException e) { + throw new AssertionError("UTF-8 encoding not supported"); + } + } + + public static Definition parseDef(String data) { + JsonReader reader = Json.createReader(new StringReader(data)); + return parseJsonDef(reader.readObject()); + } + + public static Definition parseJsonDef(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") != 1) { + throw KEMException.criticalError("Only can deserialize KAST version '1'! Found: " + data.getInt("version")); + } + return toDef(data.getJsonObject("term")); + } catch (IOException e) { + throw KEMException.criticalError("Could not read Definition term from json", e); + } + } + + public static Definition toDef(JsonObject data) throws IOException { + if (! data.getString("node").equals(KDEFINITION)) + throw KEMException.criticalError("Unexpected node found in KAST Json term: " + data.getString("node")); + + Module mainModule = toMod(data.getJsonObject("mainModule")); + JsonArray mods = data.getJsonArray("entryModules"); + Module[] modArray = toMods(mods.size(), mods); + Set entryModules = new HashSet<>(Arrays.asList(modArray)); + return new Definition(mainModule, JavaConverters.asScalaSet(entryModules), toAtt(data.getJsonObject("att"))); + } + +///////////////////////// +// Parsing Module Json // +///////////////////////// + + public static Module toMod(JsonObject data) throws IOException { + if (! data.getString("node").equals(KMODULE)) + throw KEMException.criticalError("Unexpected node found in KAST Json term: " + data.getString("node")); + + String name = data.getString("name"); + + JsonArray mods = data.getJsonArray("imports"); + Module[] modArray = toMods(mods.size(), mods); + Set modImports = new HashSet<>(Arrays.asList(modArray)); + + JsonArray sens = data.getJsonArray("localSentences"); + Sentence[] senArray = toSens(sens.size(), sens); + Set localSentences = new HashSet<>(Arrays.asList(senArray)); + + return new Module(name, JavaConverters.asScalaSet(modImports), JavaConverters.asScalaSet(localSentences), toAtt(data.getJsonObject("att"))); + } + + private static Module[] toMods(int arity, JsonArray data) throws IOException { + Module[] items = new Module[arity]; + for (int i = 0; i < arity; i++) { + items[i] = toMod(data.getValuesAs(JsonObject.class).get(i)); + } + return items; + } + +/////////////////////////// +// Parsing Sentence Json // +/////////////////////////// + + public static Sentence toSen(JsonObject data) throws IOException { + switch(data.getString("node")) { + case KCONTEXT: { + K body = toK(data.getJsonObject("body")); + K requires = toK(data.getJsonObject("requires")); + Att att = toAtt(data.getJsonObject("att")); + return new Context(body, requires, att); + } + case KRULE: { + K body = toK(data.getJsonObject("body")); + K requires = toK(data.getJsonObject("requires")); + K ensures = toK(data.getJsonObject("ensures")); + Att att = toAtt(data.getJsonObject("att")); + return new Rule(body, requires, ensures, att); + } + case KMODULECOMMENT:{ + String comment = data.getString("comment"); + Att att = toAtt(data.getJsonObject("att")); + return new ModuleComment(comment, att); + } + case KSYNTAXPRIORITY: { + + } + case KSYNTAXASSOCIATIVITY: { + + } + default: + throw KEMException.criticalError("Unexpected node found in KAST Json term: " + data.getString("node")); + } + } + + private static Sentence[] toSens(int arity, JsonArray data) throws IOException { + Sentence[] items = new Sentence[arity]; + for (int i = 0; i < arity; i++) { + items[i] = toSen(data.getValuesAs(JsonObject.class).get(i)); + } + return items; + } + +////////////////////// +// Parsing Att Json // +////////////////////// + + public static Att toAtt(JsonObject data) throws IOException { + if (! data.getString("node").equals(KATT)) + throw KEMException.criticalError("Unexpected node found in KAST Json term: " + data.getString("node")); + + return Att.empty(); + } + +//////////////////// +// Parsing K Json // +//////////////////// + public static K parse(byte[] data) { try { return parse(new String(data, "UTF-8")); diff --git a/kernel/src/main/java/org/kframework/unparser/ToJson.java b/kernel/src/main/java/org/kframework/unparser/ToJson.java index 392e38d5514..5d0c37402e6 100644 --- a/kernel/src/main/java/org/kframework/unparser/ToJson.java +++ b/kernel/src/main/java/org/kframework/unparser/ToJson.java @@ -1,6 +1,21 @@ // Copyright (c) 2015-2019 K Team. All Rights Reserved. package org.kframework.unparser; +import org.kframework.attributes.Att; +import org.kframework.definition.Associativity; +import org.kframework.definition.Bubble; +import org.kframework.definition.Context; +import org.kframework.definition.Configuration; +import org.kframework.definition.Definition; +import org.kframework.definition.Module; +import org.kframework.definition.ModuleComment; +import org.kframework.definition.Production; +import org.kframework.definition.Rule; +import org.kframework.definition.Sentence; +import org.kframework.definition.SyntaxAssociativity; +import org.kframework.definition.SyntaxPriority; +import org.kframework.definition.SyntaxSort; +import org.kframework.definition.Tag; import org.kframework.kore.InjectedKLabel; import org.kframework.kore.K; import org.kframework.kore.KApply; @@ -30,11 +45,223 @@ import javax.json.JsonWriter; import javax.json.JsonStructure; +import scala.collection.JavaConverters; +import scala.collection.Seq; +import scala.collection.Set; +import scala.Enumeration; + /** * Writes a KAST term to the KAST Json format. */ public class ToJson { + private DataOutputStream data; + private ToJson(DataOutputStream data) { + this.data = data; + } + +/////////////////////////////// +// ToJson Definition Objects // +/////////////////////////////// + + public static byte[] apply(Definition def) { + ByteArrayOutputStream out = new ByteArrayOutputStream(); + try { + DataOutputStream data = new DataOutputStream(out); + JsonWriter jsonWriter = Json.createWriter(data); + + JsonObjectBuilder term = Json.createObjectBuilder(); + term.add("format", "KAST"); + term.add("version", 1); + term.add("term", toJson(def)); + + jsonWriter.write(term.build()); + jsonWriter.close(); + data.close(); + } catch (IOException e) { + throw KEMException.criticalError("Could not write Definition to Json", e); + } + return out.toByteArray(); + } + + public static JsonStructure toJson(Definition def) { + JsonObjectBuilder jdef = Json.createObjectBuilder(); + + JsonArrayBuilder mods = Json.createArrayBuilder(); + for (Module m : JavaConverters.setAsJavaSet(def.modules())) { + mods.add(toJson(m)); + } + + jdef.add("node", JsonParser.KDEFINITION); + jdef.add("mainModule", def.mainModule().name()); + jdef.add("entryModules", mods); + jdef.add("att", toJson(def.att())); + + return jdef.build(); + } + + public static JsonStructure toJson(Att att) { + JsonObjectBuilder jatt = Json.createObjectBuilder(); + jatt.add("node", JsonParser.KATT); + jatt.add("att", att.toString()); + + return jatt.build(); + } + +/////////////////////////// +// ToJson Module Objects // +/////////////////////////// + + public static JsonStructure toJson(Module mod) { + JsonObjectBuilder jmod = Json.createObjectBuilder(); + + jmod.add("node", JsonParser.KMODULE); + + JsonArrayBuilder imports = Json.createArrayBuilder(); + for (String s: JavaConverters.setAsJavaSet(mod.importedModuleNames())) { + imports.add(s); + } + + JsonArrayBuilder sentences = Json.createArrayBuilder(); + for (Sentence s: JavaConverters.setAsJavaSet(mod.localSentences())) { + sentences.add(toJson(s)); + } + + jmod.add("name", mod.name()); + jmod.add("imports", imports); + jmod.add("localSentences", sentences); + jmod.add("att", toJson(mod.att())); + + return jmod.build(); + } + +///////////////////////////// +// ToJSon Sentence Objects // +///////////////////////////// + + public static JsonStructure toJson(Sentence sen) { + if (sen instanceof Context) return toJson((Context) sen); + if (sen instanceof Rule) return toJson((Rule) sen); + if (sen instanceof ModuleComment) return toJson((ModuleComment) sen); + if (sen instanceof SyntaxPriority) return toJson((SyntaxPriority) sen); + if (sen instanceof SyntaxAssociativity) return toJson((SyntaxAssociativity) sen); + if (sen instanceof Configuration) return toJson((Configuration) sen); + if (sen instanceof Bubble) return toJson((Bubble) sen); + if (sen instanceof SyntaxSort) return toJson((SyntaxSort) sen); + if (sen instanceof Production) return toJson((Production) sen); + + JsonObjectBuilder jsen = Json.createObjectBuilder(); + jsen.add("node", "badsentence"); + return jsen.build(); + } + + public static JsonStructure toJson(Context con) { + JsonObjectBuilder jcon = Json.createObjectBuilder(); + + jcon.add("node", JsonParser.KCONTEXT); + jcon.add("body", toJson(con.body())); + jcon.add("requires", toJson(con.requires())); + jcon.add("att", toJson(con.att())); + + return jcon.build(); + } + + public static JsonStructure toJson(Rule rule) { + JsonObjectBuilder jrule = Json.createObjectBuilder(); + + jrule.add("node", JsonParser.KRULE); + jrule.add("body", toJson(rule.body())); + jrule.add("requires", toJson(rule.requires())); + jrule.add("ensures", toJson(rule.ensures())); + jrule.add("att", toJson(rule.att())); + + return jrule.build(); + } + + public static JsonStructure toJson(ModuleComment mcom) { + JsonObjectBuilder jmcom = Json.createObjectBuilder(); + + jmcom.add("node", JsonParser.KMODULECOMMENT); + jmcom.add("comment", mcom.comment()); + jmcom.add("att", toJson(mcom.att())); + + return jmcom.build(); + } + + public static JsonStructure toJson(SyntaxPriority syn) { + JsonObjectBuilder jsyn = Json.createObjectBuilder(); + + jsyn.add("node", JsonParser.KSYNTAXPRIORITY); + + Seq> priSeq = syn.priorities(); + JsonArrayBuilder priArray = Json.createArrayBuilder(); + for (Set pri : JavaConverters.seqAsJavaList(priSeq)) { + JsonArrayBuilder tagArray = Json.createArrayBuilder(); + for (Tag t : JavaConverters.setAsJavaSet(pri)) { + tagArray.add(t.name()); + } + priArray.add(tagArray); + } + jsyn.add("priorities", priArray); + + jsyn.add("att", toJson(syn.att())); + + return jsyn.build(); + } + + public static JsonStructure toJson(SyntaxAssociativity syn) { + JsonObjectBuilder jsyn = Json.createObjectBuilder(); + + jsyn.add("node", JsonParser.KSYNTAXASSOCIATIVITY); + jsyn.add("assoc", syn.assoc().toString()); + + JsonArrayBuilder tagArray = Json.createArrayBuilder(); + for (Tag t : JavaConverters.setAsJavaSet(syn.tags())) { + tagArray.add(t.name()); + } + jsyn.add("tags", tagArray); + + jsyn.add("att", toJson(syn.att())); + + return jsyn.build(); + } + + public static JsonStructure toJson(Configuration con) { + JsonObjectBuilder jcon = Json.createObjectBuilder(); + + jcon.add("node", JsonParser.KCONFIGURATION); + + return jcon.build(); + } + + public static JsonStructure toJson(Bubble bub) { + JsonObjectBuilder jbub = Json.createObjectBuilder(); + + jbub.add("node", JsonParser.KBUBBLE); + + return jbub.build(); + } + + public static JsonStructure toJson(SyntaxSort sort) { + JsonObjectBuilder jsort = Json.createObjectBuilder(); + + jsort.add("node", JsonParser.KSYNTAXSORT); + + return jsort.build(); + } + + public static JsonStructure toJson(Production pro) { + JsonObjectBuilder jpro = Json.createObjectBuilder(); + + jpro.add("node", JsonParser.KPRODUCTION); + + return jpro.build(); + } + +////////////////////// +// ToJson K Objects // +////////////////////// + public static void apply(OutputStream out, K k) { try { DataOutputStream data = new DataOutputStream(out); @@ -59,11 +286,6 @@ public static byte[] apply(K k) { return out.toByteArray(); } - private DataOutputStream data; - private ToJson(DataOutputStream data) { - this.data = data; - } - private static JsonStructure toJson(K k) { JsonObjectBuilder knode = Json.createObjectBuilder(); if (k instanceof KToken) { From 333cc19724378ff7fe10dc8e8573d0460ebd104a Mon Sep 17 00:00:00 2001 From: Guy Repta Date: Wed, 19 Jun 2019 22:00:19 +0000 Subject: [PATCH 02/27] {JsonParser,ToJson}.java,outer.scala: Serializing work is done, deserializing is being implemented and discussed --- .../kframework/parser/json/JsonParser.java | 116 ++++++++++++++---- .../java/org/kframework/unparser/ToJson.java | 69 ++++++++++- .../org/kframework/definition/outer.scala | 6 + 3 files changed, 165 insertions(+), 26 deletions(-) diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index fd2cec96f31..b597f6a91ad 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -2,12 +2,24 @@ package org.kframework.parser.json; import org.kframework.attributes.Att; +import org.kframework.definition.Associativity; +import org.kframework.definition.Bubble; import org.kframework.definition.Context; +import org.kframework.definition.Configuration; import org.kframework.definition.Definition; +import org.kframework.definition.NonTerminal; import org.kframework.definition.Module; import org.kframework.definition.ModuleComment; +import org.kframework.definition.Production; +import org.kframework.definition.ProductionItem; +import org.kframework.definition.RegexTerminal; import org.kframework.definition.Rule; import org.kframework.definition.Sentence; +import org.kframework.definition.SyntaxAssociativity; +import org.kframework.definition.SyntaxPriority; +import org.kframework.definition.SyntaxSort; +import org.kframework.definition.Tag; +import org.kframework.definition.Terminal; import org.kframework.kore.K; import org.kframework.kore.KLabel; import static org.kframework.kore.KORE.KLabel; @@ -25,6 +37,8 @@ import java.io.UnsupportedEncodingException; import java.io.StringReader; import java.util.Arrays; +import java.util.List; +import java.util.ArrayList; import java.util.HashSet; import java.util.Set; @@ -32,33 +46,41 @@ import javax.json.JsonArray; import javax.json.JsonObject; import javax.json.JsonReader; +import javax.json.JsonStructure; +import scala.Option; import scala.collection.JavaConverters; +import scala.collection.Seq; +import scala.collection.IndexedSeq; /** * Parses a Json term into the KORE data structures. */ public class JsonParser { - public static final String KDEFINITION = "KDefinition" + public static final String INJECTEDKLABEL = "InjectedKLabel" + , KAPPLY = "KApply" + , KAS = "KAs" , KATT = "KAtt" - , KCONFIGURATION = "KConfiguration" , KBUBBLE = "KBubble" - , KMODULE = "KModule" + , KCONFIGURATION = "KConfiguration" , KCONTEXT = "KContext" - , KRULE = "KRule" + , KDEFINITION = "KDefinition" + , KNONTERMINAL = "KNonTerminal" + , KMODULE = "KModule" , KMODULECOMMENT = "KModuleComment" - , KSYNTAXPRIORITY = "KSyntaxPriority" - , KSYNTAXASSOCIATIVITY = "KSyntaxAssociativity" - , KTOKEN = "KToken" - , KSYNTAXSORT = "KSyntaxSort" , KPRODUCTION = "KProduction" - , KAPPLY = "KApply" + , KREGEXTERMINAL = "KRegexTerminal" + , KREWRITE = "KRewrite" + , KRULE = "KRule" , KSEQUENCE = "KSequence" + , KSORT = "KSort" + , KSYNTAXASSOCIATIVITY = "KSyntaxAssociativity" + , KSYNTAXPRIORITY = "KSyntaxPriority" + , KSYNTAXSORT = "KSyntaxSort" + , KTERMINAL = "KTerminal" + , KTOKEN = "KToken" , KVARIABLE = "KVariable" - , KREWRITE = "KRewrite" - , KAS = "KAs" - , INJECTEDKLABEL = "InjectedKLabel" ; ///////////////////////////// @@ -99,11 +121,31 @@ public static Definition toDef(JsonObject data) throws IOException { if (! data.getString("node").equals(KDEFINITION)) throw KEMException.criticalError("Unexpected node found in KAST Json term: " + data.getString("node")); - Module mainModule = toMod(data.getJsonObject("mainModule")); + /* First pass of parsing modules: Get the modules without their imports */ + String mainModuleName = data.getString("mainModule"); JsonArray mods = data.getJsonArray("entryModules"); Module[] modArray = toMods(mods.size(), mods); - Set entryModules = new HashSet<>(Arrays.asList(modArray)); - return new Definition(mainModule, JavaConverters.asScalaSet(entryModules), toAtt(data.getJsonObject("att"))); + scala.collection.Set entryModules = JavaConverters.asScalaSet(new HashSet<>(Arrays.asList(modArray))); + + /* Second pass: Add in the imports for each Module */ + Set modulesWithImports = new HashSet<>(); + for (int i = 0; i < mods.size(); i++) { + JsonObject modJson = mods.getValuesAs(JsonObject.class).get(i); + String modName = modJson.getString("name"); + Module mod = Module.withName(modName, entryModules).get(); + JsonArray modImportStrings = modJson.getJsonArray("imports"); + for (int j = 0; j < modImportStrings.size(); j++) { + String importName = modImportStrings.getString(j); + mod = mod.addImport( Module.withName(importName, entryModules).get() ); + } + modulesWithImports.add(mod); + } + + scala.collection.Set finalModules = JavaConverters.asScalaSet(modulesWithImports); + Option maybeMainModule = Module.withName(mainModuleName, finalModules); + Module mainModule = maybeMainModule.get(); + + return new Definition(mainModule, finalModules, toAtt(data.getJsonObject("att"))); } ///////////////////////// @@ -116,15 +158,11 @@ public static Module toMod(JsonObject data) throws IOException { String name = data.getString("name"); - JsonArray mods = data.getJsonArray("imports"); - Module[] modArray = toMods(mods.size(), mods); - Set modImports = new HashSet<>(Arrays.asList(modArray)); - JsonArray sens = data.getJsonArray("localSentences"); Sentence[] senArray = toSens(sens.size(), sens); Set localSentences = new HashSet<>(Arrays.asList(senArray)); - return new Module(name, JavaConverters.asScalaSet(modImports), JavaConverters.asScalaSet(localSentences), toAtt(data.getJsonObject("att"))); + return Module.apply(name, JavaConverters.asScalaSet(localSentences), toAtt(data.getJsonObject("att"))); } private static Module[] toMods(int arity, JsonArray data) throws IOException { @@ -160,10 +198,24 @@ public static Sentence toSen(JsonObject data) throws IOException { return new ModuleComment(comment, att); } case KSYNTAXPRIORITY: { - + JsonArray priorities = data.getJsonArray("priorities"); + Att att = toAtt(data.getJsonObject("att")); + return new SyntaxPriority(toPriorities(priorities.size(), priorities), att); } case KSYNTAXASSOCIATIVITY: { + } + case KCONFIGURATION: { + + } + case KSYNTAXSORT: { + + } + case KBUBBLE: { + + } + case KPRODUCTION: { + return new ModuleComment("Dummy comment", Att.empty()); } default: throw KEMException.criticalError("Unexpected node found in KAST Json term: " + data.getString("node")); @@ -178,6 +230,28 @@ private static Sentence[] toSens(int arity, JsonArray data) throws IOException { return items; } + private static scala.collection.Set toTags(int arity, JsonArray data) { + Set tags = new HashSet<>(); + for (int i = 0; i < arity; i++) { + String tagString = data.getString(i); + Tag tag = new Tag(tagString); + tags.add(tag); + } + return JavaConverters.asScalaSet(tags); + } + + /* Used only for parsing KSYNTAXPRIORITY */ + private static Seq> toPriorities(int arity, JsonArray data) { + List> priorities = new ArrayList<>(); + + for (int i = 0; i < arity; i++) { + JsonArray tags = data.getValuesAs(JsonArray.class).get(i); + priorities.add(toTags(tags.size(), tags)); + } + + return JavaConverters.iterableAsScalaIterableConverter(priorities).asScala().toSeq(); + } + ////////////////////// // Parsing Att Json // ////////////////////// diff --git a/kernel/src/main/java/org/kframework/unparser/ToJson.java b/kernel/src/main/java/org/kframework/unparser/ToJson.java index 5d0c37402e6..6f6ba3f4e78 100644 --- a/kernel/src/main/java/org/kframework/unparser/ToJson.java +++ b/kernel/src/main/java/org/kframework/unparser/ToJson.java @@ -7,23 +7,29 @@ import org.kframework.definition.Context; import org.kframework.definition.Configuration; import org.kframework.definition.Definition; +import org.kframework.definition.NonTerminal; import org.kframework.definition.Module; import org.kframework.definition.ModuleComment; import org.kframework.definition.Production; +import org.kframework.definition.ProductionItem; +import org.kframework.definition.RegexTerminal; import org.kframework.definition.Rule; import org.kframework.definition.Sentence; import org.kframework.definition.SyntaxAssociativity; import org.kframework.definition.SyntaxPriority; import org.kframework.definition.SyntaxSort; import org.kframework.definition.Tag; +import org.kframework.definition.Terminal; import org.kframework.kore.InjectedKLabel; import org.kframework.kore.K; import org.kframework.kore.KApply; import org.kframework.kore.KAs; +import org.kframework.kore.KLabel; import org.kframework.kore.KRewrite; import org.kframework.kore.KSequence; import org.kframework.kore.KToken; import org.kframework.kore.KVariable; +import org.kframework.kore.Sort; import org.kframework.parser.json.JsonParser; import org.kframework.utils.errorsystem.KEMException; @@ -45,10 +51,11 @@ import javax.json.JsonWriter; import javax.json.JsonStructure; +import scala.Enumeration; +import scala.Option; import scala.collection.JavaConverters; import scala.collection.Seq; import scala.collection.Set; -import scala.Enumeration; /** * Writes a KAST term to the KAST Json format. @@ -230,6 +237,9 @@ public static JsonStructure toJson(Configuration con) { JsonObjectBuilder jcon = Json.createObjectBuilder(); jcon.add("node", JsonParser.KCONFIGURATION); + jcon.add("body", toJson(con.body())); + jcon.add("ensures", toJson(con.ensures())); + jcon.add("att", toJson(con.att())); return jcon.build(); } @@ -238,16 +248,21 @@ public static JsonStructure toJson(Bubble bub) { JsonObjectBuilder jbub = Json.createObjectBuilder(); jbub.add("node", JsonParser.KBUBBLE); + jbub.add("sentenceType", bub.sentenceType()); + jbub.add("contents", bub.contents()); + jbub.add("att", toJson(bub.att())); return jbub.build(); } - public static JsonStructure toJson(SyntaxSort sort) { - JsonObjectBuilder jsort = Json.createObjectBuilder(); + public static JsonStructure toJson(SyntaxSort syn) { + JsonObjectBuilder jsyn = Json.createObjectBuilder(); - jsort.add("node", JsonParser.KSYNTAXSORT); + jsyn.add("node", JsonParser.KSYNTAXSORT); + jsyn.add("sort", toJson(syn.sort())); + jsyn.add("att", toJson(syn.att())); - return jsort.build(); + return jsyn.build(); } public static JsonStructure toJson(Production pro) { @@ -255,9 +270,53 @@ public static JsonStructure toJson(Production pro) { jpro.add("node", JsonParser.KPRODUCTION); + Option klabel = pro.klabel(); + if (! klabel.isEmpty()) { + jpro.add("klabel", klabel.get().name()); + } + + Seq items = pro.items(); + JsonArrayBuilder productionItems = Json.createArrayBuilder(); + for (ProductionItem p : JavaConverters.seqAsJavaList(items)) { + JsonObjectBuilder obj = Json.createObjectBuilder(); + + if (p instanceof NonTerminal) { + NonTerminal t = (NonTerminal) p; + obj.add("node", JsonParser.KNONTERMINAL); + obj.add("sort", toJson(t.sort())); + Option name = t.name(); + if (! name.isEmpty()) + obj.add("name", name.get()); + } else if (p instanceof RegexTerminal) { + RegexTerminal t = (RegexTerminal) p; + obj.add("node", JsonParser.KREGEXTERMINAL); + obj.add("precedeRegex", t.precedeRegex()); + obj.add("regex", t.regex()); + obj.add("followRegex", t.followRegex()); + } else if (p instanceof Terminal) { + Terminal t = (Terminal) p; + obj.add("node", JsonParser.KTERMINAL); + obj.add("value", t.value()); + } + + productionItems.add(obj.build()); + } + + jpro.add("sort", toJson(pro.sort())); + jpro.add("att", toJson(pro.att())); + return jpro.build(); } + public static JsonStructure toJson(Sort sort) { + JsonObjectBuilder jsort = Json.createObjectBuilder(); + + jsort.add("node", JsonParser.KSORT); + jsort.add("name", sort.name()); + + return jsort.build(); + } + ////////////////////// // ToJson K Objects // ////////////////////// diff --git a/kore/src/main/scala/org/kframework/definition/outer.scala b/kore/src/main/scala/org/kframework/definition/outer.scala index 5b4d63da524..58a473d39ea 100644 --- a/kore/src/main/scala/org/kframework/definition/outer.scala +++ b/kore/src/main/scala/org/kframework/definition/outer.scala @@ -84,6 +84,12 @@ object Module { def apply(name: String, unresolvedLocalSentences: Set[Sentence]): Module = { new Module(name, Set(), unresolvedLocalSentences, Att.empty) } + + def apply(name: String, unresolvedLocalSentences: Set[Sentence], att: Att): Module = { + new Module(name, Set(), unresolvedLocalSentences, att) + } + + def withName(name: String, modules: Set[Module]): Option[Module] = modules.find(M => M.name.equals(name)) } case class Module(val name: String, val imports: Set[Module], localSentences: Set[Sentence], @(Nonnull@param) val att: Att = Att.empty) From ca9167e200777cc55f2d24de6f1f73eb6ac0d1ca Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 22 Aug 2019 14:47:22 -0600 Subject: [PATCH 03/27] kernel/.../{Kompile,KompileOptions}: `--input json` allows feeding in json-formatted definitions --- .../java/org/kframework/kompile/Kompile.java | 5 +++++ .../kframework/kompile/KompileOptions.java | 19 +++++++++++++++++++ 2 files changed, 24 insertions(+) diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java index 377b04ab21c..641574d6ed0 100644 --- a/kernel/src/main/java/org/kframework/kompile/Kompile.java +++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java @@ -23,6 +23,8 @@ import org.kframework.kore.Sort; import org.kframework.parser.concrete2kore.ParserUtils; import org.kframework.parser.concrete2kore.generator.RuleGrammarGenerator; +import org.kframework.parser.json.JsonParser; +import org.kframework.unparser.OutputModes; import org.kframework.utils.Stopwatch; import org.kframework.utils.errorsystem.KEMException; import org.kframework.utils.errorsystem.KExceptionManager; @@ -132,6 +134,9 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String } public Definition parseDefinition(File definitionFile, String mainModuleName, String mainProgramsModule, Set excludedModuleTags) { + if (kompileOptions.input == OutputModes.JSON) { + return JsonParser.parseDef(files.load(definitionFile)); + } return definitionParsing.parseDefinitionAndResolveBubbles(definitionFile, mainModuleName, mainProgramsModule, excludedModuleTags); } diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java index 01bfd410ff7..9a4d372f1b4 100644 --- a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java +++ b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java @@ -4,12 +4,15 @@ import com.beust.jcommander.Parameter; import com.beust.jcommander.ParametersDelegate; import org.apache.commons.io.FilenameUtils; + import org.kframework.backend.Backends; import org.kframework.main.GlobalOptions; +import org.kframework.unparser.OutputModes; import org.kframework.utils.file.FileUtil; import org.kframework.utils.inject.RequestScoped; import org.kframework.utils.options.OuterParsingOptions; import org.kframework.utils.options.SMTOptions; +import org.kframework.utils.options.BaseEnumConverter; import org.kframework.utils.options.StringListConverter; import java.io.Serializable; @@ -83,6 +86,22 @@ public boolean isKore() { return backend.equals("kore") || backend.equals("haskell") || backend.equals("llvm"); } + @Parameter(names={"--input", "-i"}, converter=OutputModeConverter.class, + description="Format to read definition in. is either [pretty|json].") + public OutputModes input = OutputModes.PRETTY; + + public static class OutputModeConverter extends BaseEnumConverter { + + public OutputModeConverter(String optionName) { + super(optionName); + } + + @Override + public Class enumClass() { + return OutputModes.class; + } + } + public static final class Experimental implements Serializable { // Experimental options From d834935a7ebefd868032904d0f09fc956954973d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 22 Aug 2019 17:10:57 -0600 Subject: [PATCH 04/27] kernel/.../{Kompile,KompileOptions}: `--emit-json` will dump JSON encoded definition --- .../src/main/java/org/kframework/kompile/Kompile.java | 11 +++++++++++ .../java/org/kframework/kompile/KompileOptions.java | 3 +++ 2 files changed, 14 insertions(+) diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java index 641574d6ed0..5a23e8aa1ac 100644 --- a/kernel/src/main/java/org/kframework/kompile/Kompile.java +++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java @@ -25,6 +25,7 @@ import org.kframework.parser.concrete2kore.generator.RuleGrammarGenerator; import org.kframework.parser.json.JsonParser; import org.kframework.unparser.OutputModes; +import org.kframework.unparser.ToJson; import org.kframework.utils.Stopwatch; import org.kframework.utils.errorsystem.KEMException; import org.kframework.utils.errorsystem.KExceptionManager; @@ -33,6 +34,7 @@ import scala.Function1; import java.io.File; +import java.io.UnsupportedEncodingException; import java.util.Collections; import java.util.EnumSet; import java.util.HashSet; @@ -128,6 +130,15 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String files.saveToKompiled("compiled.txt", kompiledDefinition.toString()); sw.printIntermediate("Apply compile pipeline"); + if (kompileOptions.emitJson) { + try { + files.saveToKompiled("parsed.json", new String(ToJson.apply(parsedDef), "UTF-8")); + files.saveToKompiled("compiled.json", new String(ToJson.apply(kompiledDefinition), "UTF-8")); + } catch (UnsupportedEncodingException e) { + throw KEMException.criticalError("Unsupported encoding `UTF-8` when saving JSON definition."); + } + } + ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(kompiledDefinition.mainModule()); return new CompiledDefinition(kompileOptions, parsedDef, kompiledDefinition, files, kem, configInfo.getDefaultCell(configInfo.getRootCell()).klabel()); diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java index 9a4d372f1b4..071e0acb2d0 100644 --- a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java +++ b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java @@ -102,6 +102,9 @@ public Class enumClass() { } } + @Parameter(names="--emit-json", description="Emit JSON serialized version of parsed and kompiled definitions.") + public boolean emitJson = false; + public static final class Experimental implements Serializable { // Experimental options From dcf026c210209ade6bf951f8c3261796aeee4e2b Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 22 Aug 2019 17:12:42 -0600 Subject: [PATCH 05/27] k-distribution/regression-new: test that --emit-json works --- .../tests/regression-new/imp-json/Makefile | 7 + .../tests/regression-new/imp-json/imp.k | 205 ++++++++++++++++++ 2 files changed, 212 insertions(+) create mode 100644 k-distribution/tests/regression-new/imp-json/Makefile create mode 100644 k-distribution/tests/regression-new/imp-json/imp.k diff --git a/k-distribution/tests/regression-new/imp-json/Makefile b/k-distribution/tests/regression-new/imp-json/Makefile new file mode 100644 index 00000000000..262191952a5 --- /dev/null +++ b/k-distribution/tests/regression-new/imp-json/Makefile @@ -0,0 +1,7 @@ +DEF=imp +EXT=imp +TESTDIR=. +KOMPILE_BACKEND?=llvm +KOMPILE_FLAGS=--emit-json + +include ../../../include/ktest.mak diff --git a/k-distribution/tests/regression-new/imp-json/imp.k b/k-distribution/tests/regression-new/imp-json/imp.k new file mode 100644 index 00000000000..d5188142b0c --- /dev/null +++ b/k-distribution/tests/regression-new/imp-json/imp.k @@ -0,0 +1,205 @@ +// Copyright (c) 2014-2019 K Team. All Rights Reserved. + +/*! +\setlength{\parindent}{1em} +\title{IMP} +\author{Grigore Ro\c{s}u (\texttt{grosu@illinois.edu})} +\organization{University of Illinois at Urbana-Champaign} +*/ + +/*@ \section{Abstract} +This is the \K semantic definition of the classic IMP language. +IMP is considered a folklore language, without an official inventor, +and has been used in many textbooks and papers, often with slight +syntactic variations and often without being called IMP\@. It includes +the most basic imperative language constructs, namely basic constructs +for arithmetic and Boolean expressions, and variable assignment, +conditional, while loop and sequential composition constructs for statements. +*/ + +module IMP-SYNTAX + imports DOMAINS-SYNTAX +/*@ \section{Syntax} +This module defines the syntax of IMP\@. +Note that \texttt{<=} is sequentially strict and has a \LaTeX\ attribute +making it display as $\leq$, and that \texttt{\&\&} is strict only in its first +argument, because we want to give it a short-circuit semantics. */ + + syntax AExp ::= Int | Id + | "-" Int [format(%1%2)] + | AExp "/" AExp [left, strict, color(pink)] + > AExp "+" AExp [left, strict, color(pink)] + | "(" AExp ")" [bracket] + syntax BExp ::= Bool + | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2}), color(pink)] + | "!" BExp [strict, color(pink)] + > BExp "&&" BExp [left, strict(1), color(pink)] + | "(" BExp ")" [bracket] + syntax Block ::= "{" "}" + | "{" Stmt "}" [format(%1%i%n%2%d%n%3)] + syntax Stmt ::= Block + | Id "=" AExp ";" [strict(2), color(pink), format(%1 %2 %3%4)] + | "if" "(" BExp ")" + Block "else" Block [strict(1), colors(yellow, white, white, yellow), format(%1 %2%3%4 %5 %6 %7)] + | "while" "(" BExp ")" Block [colors(yellow,white,white), format(%1 %2%3%4 %5)] + > Stmt Stmt [left, format(%1%n%2)] + +/*@ An IMP program declares a set of variables and then executes a +statement in the state obtained after initializing all those variables +to 0. \K provides builtin support for generic syntactic lists: +$\textit{List}\{\textit{Nonterminal},\textit{terminal}\}$ stands for +\textit{terminal}-separated lists of \textit{Nonterminal} elements. */ + + syntax Pgm ::= "int" Ids ";" Stmt [format(%1 %2%3%n%4), colors(yellow,pink)] + syntax Ids ::= List{Id,","} [format(%1%2 %3)] +endmodule + +/*@ We are done with the definition of IMP's syntax. Make sure +that you write and parse several interesting programs before you move to the +semantics. */ + +module IMP + imports IMP-SYNTAX + imports INT + imports BOOL + imports MAP +/*@ \section{Semantics} +This module defines the semantics of IMP\@. +Before you start adding semantic rules to a \K definition, you need to +define the basic semantic infrastructure consisting of definitions for +{\em results} and the {\em configuration}. */ + +/*@ \subsection{Values and results} +IMP only has two types of values, or results of computations: integers +and Booleans. We here use the \K builtin variants for both of them. */ + + syntax KResult ::= Int | Bool + +/*@ \subsection{Configuration} +The configuration of IMP is trivial: it only contains two cells, one +for the computation and another for the state. For good encapsulation +and clarity, we place the two cells inside another cell, the ``top'' cell +which is labeled \textsf{T}. */ + + configuration + $PGM:Pgm + .Map + + +/*@ The configuration variable $\${\it PGM}$ tells the \K tool where to +place the program. More precisely, the command +``\texttt{krun program}'' parses the program and places the resulting +\K abstract syntax tree in the \textsf{k} cell before invoking the +semantic rules described in the sequel. The ``$\kdot$'' in the +\textsf{state} cell, written \texttt{.Map} in ASCII in the +\texttt{imp.k} file, is \K's way to say ``nothing''. Technically, it +is a constant which is the unit, or identity, of all maps in \K +(similar dot units exist for other \K structures, such as lists, sets, +multi-sets, etc.). */ + +/*@ \subsection{Arithmetic expressions} +The \K semantics of each arithmetic construct is defined below. */ + +/*@ \subsubsection{Variable lookup} +A program variable $X$ is looked up in the state by matching a binding +of the form $X \mapsto I$ in the state cell. If such a binding does not +exist, then the rewriting process will get stuck. Thus our semantics of +IMP disallows uses of uninitialized variables. Note that the variable +to be looked up is the first task in the \textsf{k} cell (the cell is +closed to the left and torn to the right), while the binding can be +anywhere in the \textsf{state} cell (the cell is torn at both sides). */ + + rule X:Id => I ... ... X |-> I ... + +/*@ \subsubsection{Arithmetic operators} +There is nothing special about these, but recall that \K's configuration +abstraction mechanism is at work here! That means that the rewrites in the +rules below all happen at the beginning of the \textsf{k} cell. */ + + rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0 + rule I1 + I2 => I1 +Int I2 + rule - I1 => 0 -Int I1 + +/*@ \subsection{Boolean expressions} +The rules below are straightforward. Note the short-circuited semantics +of \texttt{\&\&}; this is the reason we annotated the syntax of +\texttt{\&\&} with the \K attribute \texttt{strict(1)} instead of +\texttt{strict}. */ + + rule I1 <= I2 => I1 <=Int I2 + rule ! T => notBool T + rule true && B => B + rule false && _ => false + +/*@ \subsection{Blocks and Statements} +There is one rule per statement construct except for the conditional, +which needs two rules. */ + +/*@ \subsubsection{Blocks} +The empty block \texttt{\{\}} is simply dissolved. The $\kdot$ below is the +unit of the computation list structure $K$, that is, the empty task. +Similarly, the non-empty blocks are dissolved and replaced by their statement +contents, thus effectively giving them a bracket semantics; we can afford to +do this only because we have no block-local variable declarations yet in IMP. +Since we tagged the rules below as "structural", the \K tool structurally +erases the block constructs from the computation structure, without +considering their erasure as computational steps in the resulting transition +systems. You can make these rules computational (dropping the attribute +\texttt{structural}) if you do want these to count as computational steps. */ + + rule {} => . [structural] + rule {S} => S [structural] + +/*@ \subsubsection{Assignment} +The assigned variable is updated in the state. The variable is expected +to be declared, otherwise the semantics will get stuck. At the same time, +the assignment is dissolved. */ + + rule X = I:Int; => . ... ... X |-> (_ => I) ... + +/*@ \subsubsection{Sequential composition} +Sequential composition is simply structurally translated into \K's +builtin task sequentialization operation. You can make this rule +computational (i.e., remove the \texttt{structural} attribute) if you +want it to count as a computational step. Recall that the semantics +of a program in a programming language defined in \K is the transition +system obtained from the initial configuration holding that program +and counting only the steps corresponding to computational rules as +transitions (i.e., hiding the structural rules as unobservable, or +internal steps). */ + + rule S1:Stmt S2:Stmt => S1 ~> S2 [structural] + +/*@ \subsubsection{Conditional} +The conditional statement has two semantic cases, corresponding to +when its condition evaluates to \texttt{true} or to \texttt{false}. +Recall that the conditional was annotated with the attribute +\texttt{strict(1)} in the syntax module above, so only its first +argument is allowed to be evaluated. */ + + rule if (true) S else _ => S + rule if (false) _ else S => S + +/*@ \subsubsection{While loop} +We give the semantics of the \texttt{while} loop by unrolling. +Note that we preferred to make the rule below structural. */ + + rule while (B) S => if (B) {S while (B) S} else {} [structural] + +/*@ \subsection{Programs} +The semantics of an IMP program is that its body statement is executed +in a state initializing all its global variables to 0. Since \K's +syntactic lists are internally interpreted as cons-lists (i.e., lists +constructed with a head element followed by a tail list), we need to +distinguish two cases, one when the list has at least one element and +another when the list is empty. In the first case we initialize the +variable to 0 in the state, but only when the variable is not already +declared (all variables are global and distinct in IMP). We prefer to +make the second rule structural, thinking of dissolving the residual +empty \texttt{int;} declaration as a structural cleanup rather than as +a computational step. */ + + rule int (X,Xs => Xs);_ Rho:Map (.Map => X|->0) + requires notBool (X in keys(Rho)) + rule int .Ids; S => S [structural] +endmodule From 03bed22dc922e8c898038a8a2e9ccd568dc13004 Mon Sep 17 00:00:00 2001 From: Guy Repta Date: Tue, 2 Jul 2019 14:45:03 -0500 Subject: [PATCH 06/27] JsonParser.java: Now uses FlatModule to assist in deseralizing definitions --- .../kframework/parser/json/JsonParser.java | 47 +++++++++---------- .../org/kframework/definition/outer-ext.scala | 2 + 2 files changed, 24 insertions(+), 25 deletions(-) diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index b597f6a91ad..e137c8ebd8e 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -7,6 +7,7 @@ import org.kframework.definition.Context; import org.kframework.definition.Configuration; import org.kframework.definition.Definition; +import org.kframework.definition.FlatModule; import org.kframework.definition.NonTerminal; import org.kframework.definition.Module; import org.kframework.definition.ModuleComment; @@ -39,20 +40,26 @@ import java.util.Arrays; import java.util.List; import java.util.ArrayList; +import java.util.HashMap; import java.util.HashSet; +import java.util.Map; import java.util.Set; import javax.json.Json; import javax.json.JsonArray; import javax.json.JsonObject; import javax.json.JsonReader; +import javax.json.JsonString; import javax.json.JsonStructure; + import scala.Option; import scala.collection.JavaConverters; import scala.collection.Seq; import scala.collection.IndexedSeq; +import static org.kframework.Collections.*; + /** * Parses a Json term into the KORE data structures. */ @@ -121,52 +128,42 @@ public static Definition toDef(JsonObject data) throws IOException { if (! data.getString("node").equals(KDEFINITION)) throw KEMException.criticalError("Unexpected node found in KAST Json term: " + data.getString("node")); - /* First pass of parsing modules: Get the modules without their imports */ String mainModuleName = data.getString("mainModule"); JsonArray mods = data.getJsonArray("entryModules"); - Module[] modArray = toMods(mods.size(), mods); - scala.collection.Set entryModules = JavaConverters.asScalaSet(new HashSet<>(Arrays.asList(modArray))); - - /* Second pass: Add in the imports for each Module */ - Set modulesWithImports = new HashSet<>(); - for (int i = 0; i < mods.size(); i++) { - JsonObject modJson = mods.getValuesAs(JsonObject.class).get(i); - String modName = modJson.getString("name"); - Module mod = Module.withName(modName, entryModules).get(); - JsonArray modImportStrings = modJson.getJsonArray("imports"); - for (int j = 0; j < modImportStrings.size(); j++) { - String importName = modImportStrings.getString(j); - mod = mod.addImport( Module.withName(importName, entryModules).get() ); - } - modulesWithImports.add(mod); - } + FlatModule[] modArray = toMods(mods.size(), mods); + Set entryModules = new HashSet<>(Arrays.asList(modArray)); + Map koreModules = new HashMap<>(); - scala.collection.Set finalModules = JavaConverters.asScalaSet(modulesWithImports); - Option maybeMainModule = Module.withName(mainModuleName, finalModules); - Module mainModule = maybeMainModule.get(); + FlatModule mainFlatMod = entryModules.stream().filter(mod -> mod.hasName(mainModuleName)).findFirst().get(); + Module mainMod = mainFlatMod.toModule(immutable(entryModules), JavaConverters.mapAsScalaMapConverter(koreModules).asScala(), Seq()); - return new Definition(mainModule, finalModules, toAtt(data.getJsonObject("att"))); + return new Definition(mainMod, immutable(new HashSet<>(koreModules.values())), toAtt(data.getJsonObject("att"))); } ///////////////////////// // Parsing Module Json // ///////////////////////// - public static Module toMod(JsonObject data) throws IOException { + public static FlatModule toMod(JsonObject data) throws IOException { if (! data.getString("node").equals(KMODULE)) throw KEMException.criticalError("Unexpected node found in KAST Json term: " + data.getString("node")); String name = data.getString("name"); JsonArray sens = data.getJsonArray("localSentences"); + JsonArray jsonimports = data.getJsonArray("imports"); + Set imports = new HashSet<>(); + for (JsonString imp : jsonimports.getValuesAs(JsonString.class)) { + imports.add(imp.getString()); + } Sentence[] senArray = toSens(sens.size(), sens); Set localSentences = new HashSet<>(Arrays.asList(senArray)); - return Module.apply(name, JavaConverters.asScalaSet(localSentences), toAtt(data.getJsonObject("att"))); + return new FlatModule(name, immutable(imports), immutable(localSentences), toAtt(data.getJsonObject("att"))); } - private static Module[] toMods(int arity, JsonArray data) throws IOException { - Module[] items = new Module[arity]; + private static FlatModule[] toMods(int arity, JsonArray data) throws IOException { + FlatModule[] items = new FlatModule[arity]; for (int i = 0; i < arity; i++) { items[i] = toMod(data.getValuesAs(JsonObject.class).get(i)); } diff --git a/kore/src/main/scala/org/kframework/definition/outer-ext.scala b/kore/src/main/scala/org/kframework/definition/outer-ext.scala index b116f044236..1e1c61c1d26 100644 --- a/kore/src/main/scala/org/kframework/definition/outer-ext.scala +++ b/kore/src/main/scala/org/kframework/definition/outer-ext.scala @@ -114,4 +114,6 @@ case class FlatModule(name: String, imports: Set[String], localSentences: Set[Se newModule } + + def hasName(name: String) : Boolean = this.name == name } From d995f5cf406c3f22f47ed21526762ba95f42ce6a Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 23 Aug 2019 09:42:16 -0600 Subject: [PATCH 07/27] kore/outer-ext, kernel/JsonParser: remove uneeded hasName --- kernel/src/main/java/org/kframework/parser/json/JsonParser.java | 2 +- kore/src/main/scala/org/kframework/definition/outer-ext.scala | 2 -- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index e137c8ebd8e..e61ea12f09e 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -134,7 +134,7 @@ public static Definition toDef(JsonObject data) throws IOException { Set entryModules = new HashSet<>(Arrays.asList(modArray)); Map koreModules = new HashMap<>(); - FlatModule mainFlatMod = entryModules.stream().filter(mod -> mod.hasName(mainModuleName)).findFirst().get(); + FlatModule mainFlatMod = entryModules.stream().filter(mod -> mod.name().equals(mainModuleName)).findFirst().get(); Module mainMod = mainFlatMod.toModule(immutable(entryModules), JavaConverters.mapAsScalaMapConverter(koreModules).asScala(), Seq()); return new Definition(mainMod, immutable(new HashSet<>(koreModules.values())), toAtt(data.getJsonObject("att"))); diff --git a/kore/src/main/scala/org/kframework/definition/outer-ext.scala b/kore/src/main/scala/org/kframework/definition/outer-ext.scala index 1e1c61c1d26..b116f044236 100644 --- a/kore/src/main/scala/org/kframework/definition/outer-ext.scala +++ b/kore/src/main/scala/org/kframework/definition/outer-ext.scala @@ -114,6 +114,4 @@ case class FlatModule(name: String, imports: Set[String], localSentences: Set[Se newModule } - - def hasName(name: String) : Boolean = this.name == name } From bc20ed0a772743571b120272850cb5e212c1b87f Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 23 Aug 2019 09:43:46 -0600 Subject: [PATCH 08/27] kore/outer.scala: remove unused functions --- kore/src/main/scala/org/kframework/definition/outer.scala | 6 ------ 1 file changed, 6 deletions(-) diff --git a/kore/src/main/scala/org/kframework/definition/outer.scala b/kore/src/main/scala/org/kframework/definition/outer.scala index 58a473d39ea..5b4d63da524 100644 --- a/kore/src/main/scala/org/kframework/definition/outer.scala +++ b/kore/src/main/scala/org/kframework/definition/outer.scala @@ -84,12 +84,6 @@ object Module { def apply(name: String, unresolvedLocalSentences: Set[Sentence]): Module = { new Module(name, Set(), unresolvedLocalSentences, Att.empty) } - - def apply(name: String, unresolvedLocalSentences: Set[Sentence], att: Att): Module = { - new Module(name, Set(), unresolvedLocalSentences, att) - } - - def withName(name: String, modules: Set[Module]): Option[Module] = modules.find(M => M.name.equals(name)) } case class Module(val name: String, val imports: Set[Module], localSentences: Set[Sentence], @(Nonnull@param) val att: Att = Att.empty) From 691406ca43061c3ea80c624ebf4339f7c8d6ac89 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 23 Aug 2019 10:18:38 -0600 Subject: [PATCH 09/27] kore/outer: simplify flatModules --- .../main/scala/org/kframework/definition/outer.scala | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/kore/src/main/scala/org/kframework/definition/outer.scala b/kore/src/main/scala/org/kframework/definition/outer.scala index 5b4d63da524..d77d3cba2a2 100644 --- a/kore/src/main/scala/org/kframework/definition/outer.scala +++ b/kore/src/main/scala/org/kframework/definition/outer.scala @@ -313,16 +313,8 @@ case class Module(val name: String, val imports: Set[Module], localSentences: Se case m: Module => m.name == name && m.sentences == sentences } - def toFlatModules() : (String, Set[FlatModule]) = { - var flatSelf = new FlatModule(name, importedModuleNames, sentences, att) - var flatModules = Set(flatSelf) ++ - (imports.size match { - case 0 => Set() - case _ => imports.map(m => m.toFlatModules._2).flatten - }) - (name, flatModules) - } - + def flattened() : FlatModule = new FlatModule(name, importedModuleNames, sentences, att) + def flatModules() : (String, Set[FlatModule]) = (name, Set(flattened) ++ imports.map(m => m.flatModules._2).flatten) } object Import { From e4a8d02d27bd7338f3badd85ca9fd7c894d7972d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 23 Aug 2019 10:45:38 -0600 Subject: [PATCH 10/27] kernel/ToJson: write FlatModule to Json, not Module --- .../main/java/org/kframework/unparser/ToJson.java | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/kernel/src/main/java/org/kframework/unparser/ToJson.java b/kernel/src/main/java/org/kframework/unparser/ToJson.java index 6f6ba3f4e78..6046ac3bda6 100644 --- a/kernel/src/main/java/org/kframework/unparser/ToJson.java +++ b/kernel/src/main/java/org/kframework/unparser/ToJson.java @@ -9,6 +9,7 @@ import org.kframework.definition.Definition; import org.kframework.definition.NonTerminal; import org.kframework.definition.Module; +import org.kframework.definition.FlatModule; import org.kframework.definition.ModuleComment; import org.kframework.definition.Production; import org.kframework.definition.ProductionItem; @@ -120,19 +121,19 @@ public static JsonStructure toJson(Att att) { /////////////////////////// public static JsonStructure toJson(Module mod) { + return toJson(mod.flattened()); + } + + public static JsonStructure toJson(FlatModule mod) { JsonObjectBuilder jmod = Json.createObjectBuilder(); jmod.add("node", JsonParser.KMODULE); JsonArrayBuilder imports = Json.createArrayBuilder(); - for (String s: JavaConverters.setAsJavaSet(mod.importedModuleNames())) { - imports.add(s); - } + mod.imports().foreach(i -> imports.add(i)); JsonArrayBuilder sentences = Json.createArrayBuilder(); - for (Sentence s: JavaConverters.setAsJavaSet(mod.localSentences())) { - sentences.add(toJson(s)); - } + mod.localSentences().foreach(s -> sentences.add(toJson(s))); jmod.add("name", mod.name()); jmod.add("imports", imports); From a318f34525b6018dafff345e7d0456a7ad9d8aa6 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 23 Aug 2019 10:47:09 -0600 Subject: [PATCH 11/27] k-distribution/regression-new/imp-json: smaller definition --- .../tests/regression-new/imp-json/imp.k | 131 ------------------ 1 file changed, 131 deletions(-) diff --git a/k-distribution/tests/regression-new/imp-json/imp.k b/k-distribution/tests/regression-new/imp-json/imp.k index d5188142b0c..fa2b3a3ef03 100644 --- a/k-distribution/tests/regression-new/imp-json/imp.k +++ b/k-distribution/tests/regression-new/imp-json/imp.k @@ -1,29 +1,7 @@ // Copyright (c) 2014-2019 K Team. All Rights Reserved. -/*! -\setlength{\parindent}{1em} -\title{IMP} -\author{Grigore Ro\c{s}u (\texttt{grosu@illinois.edu})} -\organization{University of Illinois at Urbana-Champaign} -*/ - -/*@ \section{Abstract} -This is the \K semantic definition of the classic IMP language. -IMP is considered a folklore language, without an official inventor, -and has been used in many textbooks and papers, often with slight -syntactic variations and often without being called IMP\@. It includes -the most basic imperative language constructs, namely basic constructs -for arithmetic and Boolean expressions, and variable assignment, -conditional, while loop and sequential composition constructs for statements. -*/ - module IMP-SYNTAX imports DOMAINS-SYNTAX -/*@ \section{Syntax} -This module defines the syntax of IMP\@. -Note that \texttt{<=} is sequentially strict and has a \LaTeX\ attribute -making it display as $\leq$, and that \texttt{\&\&} is strict only in its first -argument, because we want to give it a short-circuit semantics. */ syntax AExp ::= Int | Id | "-" Int [format(%1%2)] @@ -44,34 +22,15 @@ argument, because we want to give it a short-circuit semantics. */ | "while" "(" BExp ")" Block [colors(yellow,white,white), format(%1 %2%3%4 %5)] > Stmt Stmt [left, format(%1%n%2)] -/*@ An IMP program declares a set of variables and then executes a -statement in the state obtained after initializing all those variables -to 0. \K provides builtin support for generic syntactic lists: -$\textit{List}\{\textit{Nonterminal},\textit{terminal}\}$ stands for -\textit{terminal}-separated lists of \textit{Nonterminal} elements. */ - syntax Pgm ::= "int" Ids ";" Stmt [format(%1 %2%3%n%4), colors(yellow,pink)] syntax Ids ::= List{Id,","} [format(%1%2 %3)] endmodule -/*@ We are done with the definition of IMP's syntax. Make sure -that you write and parse several interesting programs before you move to the -semantics. */ - module IMP imports IMP-SYNTAX imports INT imports BOOL imports MAP -/*@ \section{Semantics} -This module defines the semantics of IMP\@. -Before you start adding semantic rules to a \K definition, you need to -define the basic semantic infrastructure consisting of definitions for -{\em results} and the {\em configuration}. */ - -/*@ \subsection{Values and results} -IMP only has two types of values, or results of computations: integers -and Booleans. We here use the \K builtin variants for both of them. */ syntax KResult ::= Int | Bool @@ -86,119 +45,29 @@ which is labeled \textsf{T}. */ .Map -/*@ The configuration variable $\${\it PGM}$ tells the \K tool where to -place the program. More precisely, the command -``\texttt{krun program}'' parses the program and places the resulting -\K abstract syntax tree in the \textsf{k} cell before invoking the -semantic rules described in the sequel. The ``$\kdot$'' in the -\textsf{state} cell, written \texttt{.Map} in ASCII in the -\texttt{imp.k} file, is \K's way to say ``nothing''. Technically, it -is a constant which is the unit, or identity, of all maps in \K -(similar dot units exist for other \K structures, such as lists, sets, -multi-sets, etc.). */ - -/*@ \subsection{Arithmetic expressions} -The \K semantics of each arithmetic construct is defined below. */ - -/*@ \subsubsection{Variable lookup} -A program variable $X$ is looked up in the state by matching a binding -of the form $X \mapsto I$ in the state cell. If such a binding does not -exist, then the rewriting process will get stuck. Thus our semantics of -IMP disallows uses of uninitialized variables. Note that the variable -to be looked up is the first task in the \textsf{k} cell (the cell is -closed to the left and torn to the right), while the binding can be -anywhere in the \textsf{state} cell (the cell is torn at both sides). */ - rule X:Id => I ... ... X |-> I ... -/*@ \subsubsection{Arithmetic operators} -There is nothing special about these, but recall that \K's configuration -abstraction mechanism is at work here! That means that the rewrites in the -rules below all happen at the beginning of the \textsf{k} cell. */ - rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0 rule I1 + I2 => I1 +Int I2 rule - I1 => 0 -Int I1 -/*@ \subsection{Boolean expressions} -The rules below are straightforward. Note the short-circuited semantics -of \texttt{\&\&}; this is the reason we annotated the syntax of -\texttt{\&\&} with the \K attribute \texttt{strict(1)} instead of -\texttt{strict}. */ - rule I1 <= I2 => I1 <=Int I2 rule ! T => notBool T rule true && B => B rule false && _ => false -/*@ \subsection{Blocks and Statements} -There is one rule per statement construct except for the conditional, -which needs two rules. */ - -/*@ \subsubsection{Blocks} -The empty block \texttt{\{\}} is simply dissolved. The $\kdot$ below is the -unit of the computation list structure $K$, that is, the empty task. -Similarly, the non-empty blocks are dissolved and replaced by their statement -contents, thus effectively giving them a bracket semantics; we can afford to -do this only because we have no block-local variable declarations yet in IMP. -Since we tagged the rules below as "structural", the \K tool structurally -erases the block constructs from the computation structure, without -considering their erasure as computational steps in the resulting transition -systems. You can make these rules computational (dropping the attribute -\texttt{structural}) if you do want these to count as computational steps. */ - rule {} => . [structural] rule {S} => S [structural] -/*@ \subsubsection{Assignment} -The assigned variable is updated in the state. The variable is expected -to be declared, otherwise the semantics will get stuck. At the same time, -the assignment is dissolved. */ - rule X = I:Int; => . ... ... X |-> (_ => I) ... -/*@ \subsubsection{Sequential composition} -Sequential composition is simply structurally translated into \K's -builtin task sequentialization operation. You can make this rule -computational (i.e., remove the \texttt{structural} attribute) if you -want it to count as a computational step. Recall that the semantics -of a program in a programming language defined in \K is the transition -system obtained from the initial configuration holding that program -and counting only the steps corresponding to computational rules as -transitions (i.e., hiding the structural rules as unobservable, or -internal steps). */ - rule S1:Stmt S2:Stmt => S1 ~> S2 [structural] -/*@ \subsubsection{Conditional} -The conditional statement has two semantic cases, corresponding to -when its condition evaluates to \texttt{true} or to \texttt{false}. -Recall that the conditional was annotated with the attribute -\texttt{strict(1)} in the syntax module above, so only its first -argument is allowed to be evaluated. */ - rule if (true) S else _ => S rule if (false) _ else S => S -/*@ \subsubsection{While loop} -We give the semantics of the \texttt{while} loop by unrolling. -Note that we preferred to make the rule below structural. */ - rule while (B) S => if (B) {S while (B) S} else {} [structural] -/*@ \subsection{Programs} -The semantics of an IMP program is that its body statement is executed -in a state initializing all its global variables to 0. Since \K's -syntactic lists are internally interpreted as cons-lists (i.e., lists -constructed with a head element followed by a tail list), we need to -distinguish two cases, one when the list has at least one element and -another when the list is empty. In the first case we initialize the -variable to 0 in the state, but only when the variable is not already -declared (all variables are global and distinct in IMP). We prefer to -make the second rule structural, thinking of dissolving the residual -empty \texttt{int;} declaration as a structural cleanup rather than as -a computational step. */ - rule int (X,Xs => Xs);_ Rho:Map (.Map => X|->0) requires notBool (X in keys(Rho)) rule int .Ids; S => S [structural] From 581a92b2bca74797747be8ae899e8c5adba9d186 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 23 Aug 2019 10:52:48 -0600 Subject: [PATCH 12/27] kernel/{ToJson,JsonParser}: use FLATMODULE key for flattened modules --- .../main/java/org/kframework/parser/json/JsonParser.java | 9 +++++---- kernel/src/main/java/org/kframework/unparser/ToJson.java | 2 +- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index e61ea12f09e..fd54743d904 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -75,6 +75,7 @@ public class JsonParser { , KDEFINITION = "KDefinition" , KNONTERMINAL = "KNonTerminal" , KMODULE = "KModule" + , KFLATMODULE = "KFlatModule" , KMODULECOMMENT = "KModuleComment" , KPRODUCTION = "KProduction" , KREGEXTERMINAL = "KRegexTerminal" @@ -144,8 +145,8 @@ public static Definition toDef(JsonObject data) throws IOException { // Parsing Module Json // ///////////////////////// - public static FlatModule toMod(JsonObject data) throws IOException { - if (! data.getString("node").equals(KMODULE)) + public static FlatModule toFlatModule(JsonObject data) throws IOException { + if (! data.getString("node").equals(KFLATMODULE)) throw KEMException.criticalError("Unexpected node found in KAST Json term: " + data.getString("node")); String name = data.getString("name"); @@ -165,7 +166,7 @@ public static FlatModule toMod(JsonObject data) throws IOException { private static FlatModule[] toMods(int arity, JsonArray data) throws IOException { FlatModule[] items = new FlatModule[arity]; for (int i = 0; i < arity; i++) { - items[i] = toMod(data.getValuesAs(JsonObject.class).get(i)); + items[i] = toFlatModule(data.getValuesAs(JsonObject.class).get(i)); } return items; } @@ -200,7 +201,7 @@ public static Sentence toSen(JsonObject data) throws IOException { return new SyntaxPriority(toPriorities(priorities.size(), priorities), att); } case KSYNTAXASSOCIATIVITY: { - + } case KCONFIGURATION: { diff --git a/kernel/src/main/java/org/kframework/unparser/ToJson.java b/kernel/src/main/java/org/kframework/unparser/ToJson.java index 6046ac3bda6..ef7231057ef 100644 --- a/kernel/src/main/java/org/kframework/unparser/ToJson.java +++ b/kernel/src/main/java/org/kframework/unparser/ToJson.java @@ -127,7 +127,7 @@ public static JsonStructure toJson(Module mod) { public static JsonStructure toJson(FlatModule mod) { JsonObjectBuilder jmod = Json.createObjectBuilder(); - jmod.add("node", JsonParser.KMODULE); + jmod.add("node", JsonParser.KFLATMODULE); JsonArrayBuilder imports = Json.createArrayBuilder(); mod.imports().foreach(i -> imports.add(i)); From 4c111a6fc4900ce48376f8b87ff143612d1027ec Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 23 Aug 2019 11:10:32 -0600 Subject: [PATCH 13/27] kernel/ToJson: simpler foreach iterators --- .../src/main/java/org/kframework/unparser/ToJson.java | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/kernel/src/main/java/org/kframework/unparser/ToJson.java b/kernel/src/main/java/org/kframework/unparser/ToJson.java index ef7231057ef..4cee2680e1a 100644 --- a/kernel/src/main/java/org/kframework/unparser/ToJson.java +++ b/kernel/src/main/java/org/kframework/unparser/ToJson.java @@ -201,13 +201,10 @@ public static JsonStructure toJson(SyntaxPriority syn) { jsyn.add("node", JsonParser.KSYNTAXPRIORITY); - Seq> priSeq = syn.priorities(); JsonArrayBuilder priArray = Json.createArrayBuilder(); - for (Set pri : JavaConverters.seqAsJavaList(priSeq)) { + for (Set pri : JavaConverters.seqAsJavaList(syn.priorities())) { JsonArrayBuilder tagArray = Json.createArrayBuilder(); - for (Tag t : JavaConverters.setAsJavaSet(pri)) { - tagArray.add(t.name()); - } + pri.foreach(t -> tagArray.add(t.name())); priArray.add(tagArray); } jsyn.add("priorities", priArray); @@ -224,9 +221,7 @@ public static JsonStructure toJson(SyntaxAssociativity syn) { jsyn.add("assoc", syn.assoc().toString()); JsonArrayBuilder tagArray = Json.createArrayBuilder(); - for (Tag t : JavaConverters.setAsJavaSet(syn.tags())) { - tagArray.add(t.name()); - } + syn.tags().foreach(t -> tagArray.add(t.name())); jsyn.add("tags", tagArray); jsyn.add("att", toJson(syn.att())); From 3439481f5c55a479544239d88b0a890322b80dc1 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 23 Aug 2019 13:41:52 -0600 Subject: [PATCH 14/27] kernel/.../JsonParser: inline several definitions, prefer in-place iterators --- .../kframework/parser/json/JsonParser.java | 72 ++++++------------- 1 file changed, 23 insertions(+), 49 deletions(-) diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index fd54743d904..0e845ebe03a 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -35,15 +35,16 @@ import org.kframework.utils.errorsystem.KEMException; import java.io.IOException; -import java.io.UnsupportedEncodingException; import java.io.StringReader; -import java.util.Arrays; -import java.util.List; +import java.io.UnsupportedEncodingException; import java.util.ArrayList; +import java.util.Arrays; import java.util.HashMap; import java.util.HashSet; +import java.util.List; import java.util.Map; import java.util.Set; +import java.util.stream.Collectors; import javax.json.Json; import javax.json.JsonArray; @@ -119,22 +120,24 @@ public static Definition parseJsonDef(JsonObject data) { if (data.getInt("version") != 1) { throw KEMException.criticalError("Only can deserialize KAST version '1'! Found: " + data.getInt("version")); } - return toDef(data.getJsonObject("term")); + return toDefinition(data.getJsonObject("term")); } catch (IOException e) { throw KEMException.criticalError("Could not read Definition term from json", e); } } - public static Definition toDef(JsonObject data) throws IOException { + public static Definition toDefinition(JsonObject data) throws IOException { if (! data.getString("node").equals(KDEFINITION)) throw KEMException.criticalError("Unexpected node found in KAST Json term: " + data.getString("node")); String mainModuleName = data.getString("mainModule"); JsonArray mods = data.getJsonArray("entryModules"); - FlatModule[] modArray = toMods(mods.size(), mods); - Set entryModules = new HashSet<>(Arrays.asList(modArray)); - Map koreModules = new HashMap<>(); + Set entryModules = new HashSet<>(); + for (JsonObject m: mods.getValuesAs(JsonObject.class)) { + entryModules.add(toFlatModule(m)); + } + Map koreModules = new HashMap<>(); FlatModule mainFlatMod = entryModules.stream().filter(mod -> mod.name().equals(mainModuleName)).findFirst().get(); Module mainMod = mainFlatMod.toModule(immutable(entryModules), JavaConverters.mapAsScalaMapConverter(koreModules).asScala(), Seq()); @@ -151,31 +154,24 @@ public static FlatModule toFlatModule(JsonObject data) throws IOException { String name = data.getString("name"); - JsonArray sens = data.getJsonArray("localSentences"); JsonArray jsonimports = data.getJsonArray("imports"); Set imports = new HashSet<>(); - for (JsonString imp : jsonimports.getValuesAs(JsonString.class)) { - imports.add(imp.getString()); + jsonimports.getValuesAs(JsonString.class).forEach(i -> imports.add(i.getString())); + + JsonArray sentences = data.getJsonArray("localSentences"); + Set localSentences = new HashSet<>(); + for (JsonObject j: sentences.getValuesAs(JsonObject.class)) { + localSentences.add(toSentence(j)); } - Sentence[] senArray = toSens(sens.size(), sens); - Set localSentences = new HashSet<>(Arrays.asList(senArray)); return new FlatModule(name, immutable(imports), immutable(localSentences), toAtt(data.getJsonObject("att"))); } - private static FlatModule[] toMods(int arity, JsonArray data) throws IOException { - FlatModule[] items = new FlatModule[arity]; - for (int i = 0; i < arity; i++) { - items[i] = toFlatModule(data.getValuesAs(JsonObject.class).get(i)); - } - return items; - } - /////////////////////////// // Parsing Sentence Json // /////////////////////////// - public static Sentence toSen(JsonObject data) throws IOException { + public static Sentence toSentence(JsonObject data) throws IOException { switch(data.getString("node")) { case KCONTEXT: { K body = toK(data.getJsonObject("body")); @@ -198,7 +194,9 @@ public static Sentence toSen(JsonObject data) throws IOException { case KSYNTAXPRIORITY: { JsonArray priorities = data.getJsonArray("priorities"); Att att = toAtt(data.getJsonObject("att")); - return new SyntaxPriority(toPriorities(priorities.size(), priorities), att); + List> syntaxPriorities = new ArrayList<>(); + priorities.getValuesAs(JsonArray.class).forEach(tags -> syntaxPriorities.add(toTags(tags))); + return new SyntaxPriority(JavaConverters.iterableAsScalaIterableConverter(syntaxPriorities).asScala().toSeq(), att); } case KSYNTAXASSOCIATIVITY: { @@ -220,36 +218,12 @@ public static Sentence toSen(JsonObject data) throws IOException { } } - private static Sentence[] toSens(int arity, JsonArray data) throws IOException { - Sentence[] items = new Sentence[arity]; - for (int i = 0; i < arity; i++) { - items[i] = toSen(data.getValuesAs(JsonObject.class).get(i)); - } - return items; - } - - private static scala.collection.Set toTags(int arity, JsonArray data) { + private static scala.collection.Set toTags(JsonArray data) { Set tags = new HashSet<>(); - for (int i = 0; i < arity; i++) { - String tagString = data.getString(i); - Tag tag = new Tag(tagString); - tags.add(tag); - } + data.getValuesAs(JsonString.class).forEach(s -> tags.add(new Tag(s.getString()))); return JavaConverters.asScalaSet(tags); } - /* Used only for parsing KSYNTAXPRIORITY */ - private static Seq> toPriorities(int arity, JsonArray data) { - List> priorities = new ArrayList<>(); - - for (int i = 0; i < arity; i++) { - JsonArray tags = data.getValuesAs(JsonArray.class).get(i); - priorities.add(toTags(tags.size(), tags)); - } - - return JavaConverters.iterableAsScalaIterableConverter(priorities).asScala().toSeq(); - } - ////////////////////// // Parsing Att Json // ////////////////////// From 4bcfebba2bc1de4e65a8a64e212523b3be586148 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 23 Aug 2019 14:11:17 -0600 Subject: [PATCH 15/27] kernel/JsonParser: implement KSYNTAXASSOCIATIVITY --- .../main/java/org/kframework/parser/json/JsonParser.java | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index 0e845ebe03a..062a42ec05a 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -199,7 +199,14 @@ public static Sentence toSentence(JsonObject data) throws IOException { return new SyntaxPriority(JavaConverters.iterableAsScalaIterableConverter(syntaxPriorities).asScala().toSeq(), att); } case KSYNTAXASSOCIATIVITY: { - + String assocString = data.getString("assoc"); + scala.Enumeration.Value assoc = assocString == "Left" ? Associativity.Left() + : assocString == "Right" ? Associativity.Right() + : assocString == "NonAssoc" ? Associativity.NonAssoc() + : Associativity.Unspecified(); + scala.collection.Set tags = toTags(data.getJsonArray("tags")); + Att att = toAtt(data.getJsonObject("att")); + return new SyntaxAssociativity(assoc, tags, att); } case KCONFIGURATION: { From bcabf8f0fd1a5db246bef21df0d45eee01d3c9c7 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 23 Aug 2019 14:45:30 -0600 Subject: [PATCH 16/27] kernel/JsonParser: implment KCONFIGURATION, KBUBBLE, KSYNTAXSORT --- .../kframework/parser/json/JsonParser.java | 33 ++++++++++++++----- 1 file changed, 24 insertions(+), 9 deletions(-) diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index 062a42ec05a..e8eac756747 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -31,6 +31,7 @@ import org.kframework.kore.mini.KSequence; import org.kframework.kore.mini.KToken; import org.kframework.kore.mini.KVariable; +import org.kframework.kore.Sort; import org.kframework.parser.outer.Outer; import org.kframework.utils.errorsystem.KEMException; @@ -174,21 +175,21 @@ public static FlatModule toFlatModule(JsonObject data) throws IOException { public static Sentence toSentence(JsonObject data) throws IOException { switch(data.getString("node")) { case KCONTEXT: { - K body = toK(data.getJsonObject("body")); + K body = toK(data.getJsonObject("body")); K requires = toK(data.getJsonObject("requires")); - Att att = toAtt(data.getJsonObject("att")); + Att att = toAtt(data.getJsonObject("att")); return new Context(body, requires, att); } case KRULE: { - K body = toK(data.getJsonObject("body")); + K body = toK(data.getJsonObject("body")); K requires = toK(data.getJsonObject("requires")); - K ensures = toK(data.getJsonObject("ensures")); - Att att = toAtt(data.getJsonObject("att")); + K ensures = toK(data.getJsonObject("ensures")); + Att att = toAtt(data.getJsonObject("att")); return new Rule(body, requires, ensures, att); } case KMODULECOMMENT:{ String comment = data.getString("comment"); - Att att = toAtt(data.getJsonObject("att")); + Att att = toAtt(data.getJsonObject("att")); return new ModuleComment(comment, att); } case KSYNTAXPRIORITY: { @@ -209,13 +210,21 @@ public static Sentence toSentence(JsonObject data) throws IOException { return new SyntaxAssociativity(assoc, tags, att); } case KCONFIGURATION: { - + K body = toK(data.getJsonObject("body")); + K ensures = toK(data.getJsonObject("ensures")); + Att att = toAtt(data.getJsonObject("att")); + return new Configuration(body, ensures, att); } case KSYNTAXSORT: { - + Sort sort = toSort(data.getJsonObject("sort")); + Att att = toAtt(data.getJsonObject("att")); + return new SyntaxSort(sort, att); } case KBUBBLE: { - + String sentenceType = data.getString("sentenceType"); + String contents = data.getString("contents"); + Att att = toAtt(data.getJsonObject("att")); + return new Bubble(sentenceType, contents, att); } case KPRODUCTION: { return new ModuleComment("Dummy comment", Att.empty()); @@ -231,6 +240,12 @@ private static scala.collection.Set toTags(JsonArray data) { return JavaConverters.asScalaSet(tags); } + 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 KORE.Sort(data.getString("name")); + } + ////////////////////// // Parsing Att Json // ////////////////////// From 42cf0e63256c4c8305c406e6808f8ffec12a0800 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 23 Aug 2019 14:52:11 -0600 Subject: [PATCH 17/27] kernel/ToJson: factor out toJson : ProductionItem -> JsonObject --- .../java/org/kframework/unparser/ToJson.java | 52 ++++++++++--------- 1 file changed, 27 insertions(+), 25 deletions(-) diff --git a/kernel/src/main/java/org/kframework/unparser/ToJson.java b/kernel/src/main/java/org/kframework/unparser/ToJson.java index 4cee2680e1a..099f462b730 100644 --- a/kernel/src/main/java/org/kframework/unparser/ToJson.java +++ b/kernel/src/main/java/org/kframework/unparser/ToJson.java @@ -271,32 +271,9 @@ public static JsonStructure toJson(Production pro) { jpro.add("klabel", klabel.get().name()); } - Seq items = pro.items(); JsonArrayBuilder productionItems = Json.createArrayBuilder(); - for (ProductionItem p : JavaConverters.seqAsJavaList(items)) { - JsonObjectBuilder obj = Json.createObjectBuilder(); - - if (p instanceof NonTerminal) { - NonTerminal t = (NonTerminal) p; - obj.add("node", JsonParser.KNONTERMINAL); - obj.add("sort", toJson(t.sort())); - Option name = t.name(); - if (! name.isEmpty()) - obj.add("name", name.get()); - } else if (p instanceof RegexTerminal) { - RegexTerminal t = (RegexTerminal) p; - obj.add("node", JsonParser.KREGEXTERMINAL); - obj.add("precedeRegex", t.precedeRegex()); - obj.add("regex", t.regex()); - obj.add("followRegex", t.followRegex()); - } else if (p instanceof Terminal) { - Terminal t = (Terminal) p; - obj.add("node", JsonParser.KTERMINAL); - obj.add("value", t.value()); - } - - productionItems.add(obj.build()); - } + JavaConverters.seqAsJavaList(pro.items()).forEach(p -> productionItems.add(toJson(p))); + jpro.add("productionItems", productionItems.build()); jpro.add("sort", toJson(pro.sort())); jpro.add("att", toJson(pro.att())); @@ -304,6 +281,31 @@ public static JsonStructure toJson(Production pro) { return jpro.build(); } + public static JsonObject toJson(ProductionItem prod) { + JsonObjectBuilder jsonProduction = Json.createObjectBuilder(); + + if (prod instanceof NonTerminal) { + NonTerminal t = (NonTerminal) prod; + jsonProduction.add("node", JsonParser.KNONTERMINAL); + jsonProduction.add("sort", toJson(t.sort())); + Option name = t.name(); + if (! name.isEmpty()) + jsonProduction.add("name", name.get()); + } else if (prod instanceof RegexTerminal) { + RegexTerminal t = (RegexTerminal) prod; + jsonProduction.add("node", JsonParser.KREGEXTERMINAL); + jsonProduction.add("precedeRegex", t.precedeRegex()); + jsonProduction.add("regex", t.regex()); + jsonProduction.add("followRegex", t.followRegex()); + } else if (prod instanceof Terminal) { + Terminal t = (Terminal) prod; + jsonProduction.add("node", JsonParser.KTERMINAL); + jsonProduction.add("value", t.value()); + } + + return jsonProduction.build(); + } + public static JsonStructure toJson(Sort sort) { JsonObjectBuilder jsort = Json.createObjectBuilder(); From c63af1f0ee80bc1f3d0cbd2ea06b0ead6ae091c6 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 23 Aug 2019 15:23:54 -0600 Subject: [PATCH 18/27] kernel/JsonParser: add case for KPRODUCTION --- .../kframework/parser/json/JsonParser.java | 33 +++++++++++++++++-- 1 file changed, 31 insertions(+), 2 deletions(-) diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index e8eac756747..8177aef5ff2 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -54,7 +54,6 @@ import javax.json.JsonString; import javax.json.JsonStructure; - import scala.Option; import scala.collection.JavaConverters; import scala.collection.Seq; @@ -227,7 +226,15 @@ public static Sentence toSentence(JsonObject data) throws IOException { return new Bubble(sentenceType, contents, att); } case KPRODUCTION: { - return new ModuleComment("Dummy comment", Att.empty()); + Option klabel = Option.apply(data.containsKey("klabel") ? KLabel(data.getString("klabel")) : null); + Sort sort = toSort(data.getJsonObject("sort")); + Att att = toAtt(data.getJsonObject("att")); + + List pItems = new ArrayList<>(); + for (JsonObject pi: data.getJsonArray("productionItems").getValuesAs(JsonObject.class)) { + pItems.add(toProductionItem(pi)); + } + return new Production(klabel, sort, JavaConverters.asScalaIteratorConverter(pItems.iterator()).asScala().toSeq(), att); } default: throw KEMException.criticalError("Unexpected node found in KAST Json term: " + data.getString("node")); @@ -246,6 +253,28 @@ private static Sort toSort(JsonObject data) { return KORE.Sort(data.getString("name")); } + private static ProductionItem toProductionItem(JsonObject data) { + switch(data.getString("node")) { + case KNONTERMINAL: { + Sort sort = toSort(data.getJsonObject("sort")); + Option name = Option.apply(data.containsKey("name") ? data.getString("name") : null); + return new NonTerminal(sort, name); + } + case KREGEXTERMINAL: { + String precedeRegex = data.getString("precedeRegex"); + String regex = data.getString("regex"); + String followRegex = data.getString("followRegex"); + return new RegexTerminal(precedeRegex, regex, followRegex); + } + case KTERMINAL: { + String value = data.getString("value"); + return new Terminal(value); + } + default: + throw KEMException.criticalError("Unexpected node found in ProductionItem Json term: " + data.getString("node")); + } + } + ////////////////////// // Parsing Att Json // ////////////////////// From e406959d5520879e016ac47863b301f0260dfa6f Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 25 Aug 2019 08:45:05 -0600 Subject: [PATCH 19/27] kernel/Kompile: better error handling for unsupported input modes --- .../src/main/java/org/kframework/kompile/Kompile.java | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java index 5a23e8aa1ac..c8dea539f2c 100644 --- a/kernel/src/main/java/org/kframework/kompile/Kompile.java +++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java @@ -145,10 +145,14 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String } public Definition parseDefinition(File definitionFile, String mainModuleName, String mainProgramsModule, Set excludedModuleTags) { - if (kompileOptions.input == OutputModes.JSON) { - return JsonParser.parseDef(files.load(definitionFile)); + switch (kompileOptions.input) { + case JSON: + return JsonParser.parseDef(files.load(definitionFile)); + case PRETTY: + return definitionParsing.parseDefinitionAndResolveBubbles(definitionFile, mainModuleName, mainProgramsModule, excludedModuleTags); + default: + throw KEMException.criticalError("Unsupported input mode for definition parsing: " + kompileOptions.input); } - return definitionParsing.parseDefinitionAndResolveBubbles(definitionFile, mainModuleName, mainProgramsModule, excludedModuleTags); } private static Module filterStreamModules(Module input) { From b44d0befa0d0e1ece2a2b317ec03cc50712ac97d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 25 Aug 2019 08:46:45 -0600 Subject: [PATCH 20/27] kernel/{Kompile,JsonParser}: parseDef => parseDefinition, more informative name --- kernel/src/main/java/org/kframework/kompile/Kompile.java | 2 +- .../main/java/org/kframework/parser/json/JsonParser.java | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java index c8dea539f2c..61a3bab243c 100644 --- a/kernel/src/main/java/org/kframework/kompile/Kompile.java +++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java @@ -147,7 +147,7 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String public Definition parseDefinition(File definitionFile, String mainModuleName, String mainProgramsModule, Set excludedModuleTags) { switch (kompileOptions.input) { case JSON: - return JsonParser.parseDef(files.load(definitionFile)); + return JsonParser.parseDefinition(files.load(definitionFile)); case PRETTY: return definitionParsing.parseDefinitionAndResolveBubbles(definitionFile, mainModuleName, mainProgramsModule, excludedModuleTags); default: diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index 8177aef5ff2..2272e30ef8e 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -96,15 +96,15 @@ public class JsonParser { // Parsing Definition Json // ///////////////////////////// - public static Definition parseDef(byte[] data) { + public static Definition parseDefinition(byte[] data) { try { - return parseDef(new String(data, "UTF-8")); + return parseDefinition(new String(data, "UTF-8")); } catch (UnsupportedEncodingException e) { throw new AssertionError("UTF-8 encoding not supported"); } } - public static Definition parseDef(String data) { + public static Definition parseDefinition(String data) { JsonReader reader = Json.createReader(new StringReader(data)); return parseJsonDef(reader.readObject()); } From e20e26d8cf571ee3efecfa0161218f33dd56ec14 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 25 Aug 2019 09:11:09 -0600 Subject: [PATCH 21/27] kore/outer.scala: flattened module only has direct imports --- kore/src/main/scala/org/kframework/definition/outer.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/main/scala/org/kframework/definition/outer.scala b/kore/src/main/scala/org/kframework/definition/outer.scala index d77d3cba2a2..a8197376918 100644 --- a/kore/src/main/scala/org/kframework/definition/outer.scala +++ b/kore/src/main/scala/org/kframework/definition/outer.scala @@ -313,7 +313,7 @@ case class Module(val name: String, val imports: Set[Module], localSentences: Se case m: Module => m.name == name && m.sentences == sentences } - def flattened() : FlatModule = new FlatModule(name, importedModuleNames, sentences, att) + def flattened() : FlatModule = new FlatModule(name, imports.map(m => m.name), sentences, att) def flatModules() : (String, Set[FlatModule]) = (name, Set(flattened) ++ imports.map(m => m.flatModules._2).flatten) } From f0974fa5c7c9ff69f1454508c79c7637c215c433 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 25 Aug 2019 09:11:42 -0600 Subject: [PATCH 22/27] kernel/{JsonParser,ToJson}: entryModules => modules for modules in definition --- kernel/src/main/java/org/kframework/parser/json/JsonParser.java | 2 +- kernel/src/main/java/org/kframework/unparser/ToJson.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index 2272e30ef8e..0727a18a94d 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -131,7 +131,7 @@ public static Definition toDefinition(JsonObject data) throws IOException { throw KEMException.criticalError("Unexpected node found in KAST Json term: " + data.getString("node")); String mainModuleName = data.getString("mainModule"); - JsonArray mods = data.getJsonArray("entryModules"); + JsonArray mods = data.getJsonArray("modules"); Set entryModules = new HashSet<>(); for (JsonObject m: mods.getValuesAs(JsonObject.class)) { entryModules.add(toFlatModule(m)); diff --git a/kernel/src/main/java/org/kframework/unparser/ToJson.java b/kernel/src/main/java/org/kframework/unparser/ToJson.java index 099f462b730..789ec286acc 100644 --- a/kernel/src/main/java/org/kframework/unparser/ToJson.java +++ b/kernel/src/main/java/org/kframework/unparser/ToJson.java @@ -102,7 +102,7 @@ public static JsonStructure toJson(Definition def) { jdef.add("node", JsonParser.KDEFINITION); jdef.add("mainModule", def.mainModule().name()); - jdef.add("entryModules", mods); + jdef.add("modules", mods); jdef.add("att", toJson(def.att())); return jdef.build(); From 39786940b5870a2f3142215b0ebd5c07fed31b91 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 12 Sep 2019 12:42:18 -0600 Subject: [PATCH 23/27] k-distribution/pyk/kastManip: add function splitConfigFrom for getting config + substitution --- .../src/main/scripts/lib/pyk/kastManip.py | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/k-distribution/src/main/scripts/lib/pyk/kastManip.py b/k-distribution/src/main/scripts/lib/pyk/kastManip.py index 09901f1c1ff..e8bb7c4c758 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kastManip.py +++ b/k-distribution/src/main/scripts/lib/pyk/kastManip.py @@ -120,6 +120,19 @@ def flattenLabel(label, kast): return [ c for cs in constraints for c in cs ] return [kast] +def splitConfigFrom(configuration): + initial_substitution = {} + _mkCellVar = lambda label: label.replace('-', '_').replace('<', '').replace('>', '').upper() + '_CELL' + def _replaceWithVar(k): + if pyk.isKApply(k) and pyk.isCellKLabel(k['label']): + if len(k['args']) == 1 and not (pyk.isKApply(k['args'][0]) and pyk.isCellKLabel(k['args'][0]['label'])): + config_var = _mkCellVar(k['label']) + initial_substitution[config_var] = k['args'][0] + return KApply(k['label'], [KVariable(config_var)]) + return k + symbolic_config = pyk.traverseBottomUp(configuration, _replaceWithVar) + return (symbolic_config, initial_substitution) + def collapseDots(kast): def _collapseDots(_kast): if isKApply(_kast): From 7f7f13e3ebd21a51901d355c2358d5e970b77581 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 11 Sep 2019 22:41:24 -0600 Subject: [PATCH 24/27] k-distribution/pyk/__init__.py: much faster serialization of json to file for some reason --- k-distribution/src/main/scripts/lib/pyk/__init__.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/__init__.py b/k-distribution/src/main/scripts/lib/pyk/__init__.py index 9017c81ee3e..804377dfaa3 100755 --- a/k-distribution/src/main/scripts/lib/pyk/__init__.py +++ b/k-distribution/src/main/scripts/lib/pyk/__init__.py @@ -44,13 +44,13 @@ def kprove(definition, inputFile, kproveArgs = [], teeOutput = True, kRelease = def kastJSON(definition, inputJSON, kastArgs = [], teeOutput = True, kRelease = None): with tempfile.NamedTemporaryFile(mode = 'w') as tempf: - json.dump(inputJSON, tempf) + tempf.write(json.dumps(inputJSON)) tempf.flush() return kast(definition, tempf.name, kastArgs = kastArgs, teeOutput = teeOutput, kRelease = kRelease) def krunJSON(definition, inputJSON, krunArgs = [], teeOutput = True, kRelease = None): with tempfile.NamedTemporaryFile(mode = 'w') as tempf: - json.dump(inputJSON, tempf) + tempf.write(json.dumps(inputJSON)) tempf.flush() (rC, out, err) = krun(definition, tempf.name, krunArgs = krunArgs + ['--output', 'json', '--parser', 'cat'], teeOutput = teeOutput, kRelease = kRelease) out = None if out == '' else json.loads(out)['term'] From e589766093da0d2533085041c938ab66cb962eca Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 12 Sep 2019 13:41:05 -0600 Subject: [PATCH 25/27] kernel/{Kompile,KompileOptions}: remote --input option for now --- .../src/main/java/org/kframework/kompile/Kompile.java | 11 +---------- .../java/org/kframework/kompile/KompileOptions.java | 4 ---- 2 files changed, 1 insertion(+), 14 deletions(-) diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java index 61a3bab243c..91800d8d277 100644 --- a/kernel/src/main/java/org/kframework/kompile/Kompile.java +++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java @@ -23,8 +23,6 @@ import org.kframework.kore.Sort; import org.kframework.parser.concrete2kore.ParserUtils; import org.kframework.parser.concrete2kore.generator.RuleGrammarGenerator; -import org.kframework.parser.json.JsonParser; -import org.kframework.unparser.OutputModes; import org.kframework.unparser.ToJson; import org.kframework.utils.Stopwatch; import org.kframework.utils.errorsystem.KEMException; @@ -145,14 +143,7 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String } public Definition parseDefinition(File definitionFile, String mainModuleName, String mainProgramsModule, Set excludedModuleTags) { - switch (kompileOptions.input) { - case JSON: - return JsonParser.parseDefinition(files.load(definitionFile)); - case PRETTY: - return definitionParsing.parseDefinitionAndResolveBubbles(definitionFile, mainModuleName, mainProgramsModule, excludedModuleTags); - default: - throw KEMException.criticalError("Unsupported input mode for definition parsing: " + kompileOptions.input); - } + return definitionParsing.parseDefinitionAndResolveBubbles(definitionFile, mainModuleName, mainProgramsModule, excludedModuleTags); } private static Module filterStreamModules(Module input) { diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java index 071e0acb2d0..eb1b6615314 100644 --- a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java +++ b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java @@ -86,10 +86,6 @@ public boolean isKore() { return backend.equals("kore") || backend.equals("haskell") || backend.equals("llvm"); } - @Parameter(names={"--input", "-i"}, converter=OutputModeConverter.class, - description="Format to read definition in. is either [pretty|json].") - public OutputModes input = OutputModes.PRETTY; - public static class OutputModeConverter extends BaseEnumConverter { public OutputModeConverter(String optionName) { From cf3360ecce0a02179194823690c8f6d710bb59c7 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 12 Sep 2019 13:43:11 -0600 Subject: [PATCH 26/27] k-distribution/tests/regression-new/imp-json: shorter file --- k-distribution/tests/regression-new/imp-json/imp.k | 6 ------ 1 file changed, 6 deletions(-) diff --git a/k-distribution/tests/regression-new/imp-json/imp.k b/k-distribution/tests/regression-new/imp-json/imp.k index fa2b3a3ef03..535dcac7e94 100644 --- a/k-distribution/tests/regression-new/imp-json/imp.k +++ b/k-distribution/tests/regression-new/imp-json/imp.k @@ -34,12 +34,6 @@ module IMP syntax KResult ::= Int | Bool -/*@ \subsection{Configuration} -The configuration of IMP is trivial: it only contains two cells, one -for the computation and another for the state. For good encapsulation -and clarity, we place the two cells inside another cell, the ``top'' cell -which is labeled \textsf{T}. */ - configuration $PGM:Pgm .Map From a11bf45f73808e7f25e4292da6a83b668391d097 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 13 Sep 2019 10:11:15 -0600 Subject: [PATCH 27/27] kernel/{Kompile,KompileOptions}: move --emit-json to experimental options --- kernel/src/main/java/org/kframework/kompile/Kompile.java | 2 +- .../main/java/org/kframework/kompile/KompileOptions.java | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java index 91800d8d277..d7320a99f52 100644 --- a/kernel/src/main/java/org/kframework/kompile/Kompile.java +++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java @@ -128,7 +128,7 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String files.saveToKompiled("compiled.txt", kompiledDefinition.toString()); sw.printIntermediate("Apply compile pipeline"); - if (kompileOptions.emitJson) { + if (kompileOptions.experimental.emitJson) { try { files.saveToKompiled("parsed.json", new String(ToJson.apply(parsedDef), "UTF-8")); files.saveToKompiled("compiled.json", new String(ToJson.apply(kompiledDefinition), "UTF-8")); diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java index eb1b6615314..accbf135c69 100644 --- a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java +++ b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java @@ -98,9 +98,6 @@ public Class enumClass() { } } - @Parameter(names="--emit-json", description="Emit JSON serialized version of parsed and kompiled definitions.") - public boolean emitJson = false; - public static final class Experimental implements Serializable { // Experimental options @@ -130,5 +127,8 @@ public static final class Experimental implements Serializable { @Parameter(names="--cache-file", description="Location of parse cache file. Default is $KOMPILED_DIR/cache.bin.") public String cacheFile; + + @Parameter(names="--emit-json", description="Emit JSON serialized version of parsed and kompiled definitions.") + public boolean emitJson = false; } }