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']
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):
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..535dcac7e94
--- /dev/null
+++ b/k-distribution/tests/regression-new/imp-json/imp.k
@@ -0,0 +1,68 @@
+// Copyright (c) 2014-2019 K Team. All Rights Reserved.
+
+module IMP-SYNTAX
+ imports DOMAINS-SYNTAX
+
+ 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)]
+
+ syntax Pgm ::= "int" Ids ";" Stmt [format(%1 %2%3%n%4), colors(yellow,pink)]
+ syntax Ids ::= List{Id,","} [format(%1%2 %3)]
+endmodule
+
+module IMP
+ imports IMP-SYNTAX
+ imports INT
+ imports BOOL
+ imports MAP
+
+ syntax KResult ::= Int | Bool
+
+ configuration
+ $PGM:Pgm
+ .Map
+
+
+ rule X:Id => I ... ... X |-> I ...
+
+ rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0
+ rule I1 + I2 => I1 +Int I2
+ rule - I1 => 0 -Int I1
+
+ rule I1 <= I2 => I1 <=Int I2
+ rule ! T => notBool T
+ rule true && B => B
+ rule false && _ => false
+
+ rule {} => . [structural]
+ rule {S} => S [structural]
+
+ rule X = I:Int; => . ... ... X |-> (_ => I) ...
+
+ rule S1:Stmt S2:Stmt => S1 ~> S2 [structural]
+
+ rule if (true) S else _ => S
+ rule if (false) _ else S => S
+
+ rule while (B) S => if (B) {S while (B) S} else {} [structural]
+
+ rule int (X,Xs => Xs);_ Rho:Map (.Map => X|->0)
+ requires notBool (X in keys(Rho))
+ rule int .Ids; S => S [structural]
+endmodule
diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java
index 377b04ab21c..d7320a99f52 100644
--- a/kernel/src/main/java/org/kframework/kompile/Kompile.java
+++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java
@@ -23,6 +23,7 @@
import org.kframework.kore.Sort;
import org.kframework.parser.concrete2kore.ParserUtils;
import org.kframework.parser.concrete2kore.generator.RuleGrammarGenerator;
+import org.kframework.unparser.ToJson;
import org.kframework.utils.Stopwatch;
import org.kframework.utils.errorsystem.KEMException;
import org.kframework.utils.errorsystem.KExceptionManager;
@@ -31,6 +32,7 @@
import scala.Function1;
import java.io.File;
+import java.io.UnsupportedEncodingException;
import java.util.Collections;
import java.util.EnumSet;
import java.util.HashSet;
@@ -126,6 +128,15 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String
files.saveToKompiled("compiled.txt", kompiledDefinition.toString());
sw.printIntermediate("Apply compile pipeline");
+ 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"));
+ } 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 01bfd410ff7..accbf135c69 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,18 @@ public boolean isKore() {
return backend.equals("kore") || backend.equals("haskell") || backend.equals("llvm");
}
+ 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
@@ -112,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;
}
}
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..0727a18a94d 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,26 @@
// Copyright (c) 2018-2019 K Team. All Rights Reserved.
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.FlatModule;
+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;
@@ -11,33 +31,265 @@
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;
import java.io.IOException;
-import java.io.UnsupportedEncodingException;
import java.io.StringReader;
+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;
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.
*/
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 INJECTEDKLABEL = "InjectedKLabel"
+ , KAPPLY = "KApply"
+ , KAS = "KAs"
+ , KATT = "KAtt"
+ , KBUBBLE = "KBubble"
+ , KCONFIGURATION = "KConfiguration"
+ , KCONTEXT = "KContext"
+ , KDEFINITION = "KDefinition"
+ , KNONTERMINAL = "KNonTerminal"
+ , KMODULE = "KModule"
+ , KFLATMODULE = "KFlatModule"
+ , KMODULECOMMENT = "KModuleComment"
+ , KPRODUCTION = "KProduction"
+ , KREGEXTERMINAL = "KRegexTerminal"
+ , KREWRITE = "KRewrite"
+ , KRULE = "KRule"
+ , KSEQUENCE = "KSequence"
+ , KSORT = "KSort"
+ , KSYNTAXASSOCIATIVITY = "KSyntaxAssociativity"
+ , KSYNTAXPRIORITY = "KSyntaxPriority"
+ , KSYNTAXSORT = "KSyntaxSort"
+ , KTERMINAL = "KTerminal"
+ , KTOKEN = "KToken"
+ , KVARIABLE = "KVariable"
;
+/////////////////////////////
+// Parsing Definition Json //
+/////////////////////////////
+
+ public static Definition parseDefinition(byte[] data) {
+ try {
+ return parseDefinition(new String(data, "UTF-8"));
+ } catch (UnsupportedEncodingException e) {
+ throw new AssertionError("UTF-8 encoding not supported");
+ }
+ }
+
+ public static Definition parseDefinition(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 toDefinition(data.getJsonObject("term"));
+ } catch (IOException e) {
+ throw KEMException.criticalError("Could not read Definition term from json", e);
+ }
+ }
+
+ 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("modules");
+ 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());
+
+ return new Definition(mainMod, immutable(new HashSet<>(koreModules.values())), toAtt(data.getJsonObject("att")));
+ }
+
+/////////////////////////
+// Parsing Module Json //
+/////////////////////////
+
+ 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");
+
+ JsonArray jsonimports = data.getJsonArray("imports");
+ Set imports = new HashSet<>();
+ 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));
+ }
+
+ return new FlatModule(name, immutable(imports), immutable(localSentences), toAtt(data.getJsonObject("att")));
+ }
+
+///////////////////////////
+// Parsing Sentence Json //
+///////////////////////////
+
+ public static Sentence toSentence(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: {
+ JsonArray priorities = data.getJsonArray("priorities");
+ Att att = toAtt(data.getJsonObject("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: {
+ 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: {
+ 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: {
+ 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"));
+ }
+ }
+
+ private static scala.collection.Set toTags(JsonArray data) {
+ Set tags = new HashSet<>();
+ data.getValuesAs(JsonString.class).forEach(s -> tags.add(new Tag(s.getString())));
+ 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"));
+ }
+
+ 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 //
+//////////////////////
+
+ 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..789ec286acc 100644
--- a/kernel/src/main/java/org/kframework/unparser/ToJson.java
+++ b/kernel/src/main/java/org/kframework/unparser/ToJson.java
@@ -1,14 +1,36 @@
// 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.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;
+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;
@@ -30,11 +52,273 @@
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;
+
/**
* 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("modules", 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) {
+ return toJson(mod.flattened());
+ }
+
+ public static JsonStructure toJson(FlatModule mod) {
+ JsonObjectBuilder jmod = Json.createObjectBuilder();
+
+ jmod.add("node", JsonParser.KFLATMODULE);
+
+ JsonArrayBuilder imports = Json.createArrayBuilder();
+ mod.imports().foreach(i -> imports.add(i));
+
+ JsonArrayBuilder sentences = Json.createArrayBuilder();
+ mod.localSentences().foreach(s -> 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);
+
+ JsonArrayBuilder priArray = Json.createArrayBuilder();
+ for (Set pri : JavaConverters.seqAsJavaList(syn.priorities())) {
+ JsonArrayBuilder tagArray = Json.createArrayBuilder();
+ pri.foreach(t -> 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();
+ syn.tags().foreach(t -> 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);
+ jcon.add("body", toJson(con.body()));
+ jcon.add("ensures", toJson(con.ensures()));
+ jcon.add("att", toJson(con.att()));
+
+ return jcon.build();
+ }
+
+ 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 syn) {
+ JsonObjectBuilder jsyn = Json.createObjectBuilder();
+
+ jsyn.add("node", JsonParser.KSYNTAXSORT);
+ jsyn.add("sort", toJson(syn.sort()));
+ jsyn.add("att", toJson(syn.att()));
+
+ return jsyn.build();
+ }
+
+ public static JsonStructure toJson(Production pro) {
+ JsonObjectBuilder jpro = Json.createObjectBuilder();
+
+ jpro.add("node", JsonParser.KPRODUCTION);
+
+ Option klabel = pro.klabel();
+ if (! klabel.isEmpty()) {
+ jpro.add("klabel", klabel.get().name());
+ }
+
+ JsonArrayBuilder productionItems = Json.createArrayBuilder();
+ 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()));
+
+ 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();
+
+ jsort.add("node", JsonParser.KSORT);
+ jsort.add("name", sort.name());
+
+ return jsort.build();
+ }
+
+//////////////////////
+// ToJson K Objects //
+//////////////////////
+
public static void apply(OutputStream out, K k) {
try {
DataOutputStream data = new DataOutputStream(out);
@@ -59,11 +343,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) {
diff --git a/kore/src/main/scala/org/kframework/definition/outer.scala b/kore/src/main/scala/org/kframework/definition/outer.scala
index 5b4d63da524..a8197376918 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, imports.map(m => m.name), sentences, att)
+ def flatModules() : (String, Set[FlatModule]) = (name, Set(flattened) ++ imports.map(m => m.flatModules._2).flatten)
}
object Import {