Parsing and Scanning fixes (runtimeverification#780)

dwightguth · web-flow · commit bb0c539447d5 · 2019-09-16T15:18:19.000-05:00
* hack to make cell names not collide with terminals

* fix bug involving tags in syntax priorities
diff --git a/kernel/src/main/java/org/kframework/parser/concrete2kore/ParserUtils.java b/kernel/src/main/java/org/kframework/parser/concrete2kore/ParserUtils.java
@@ -174,6 +174,7 @@ private String loadDefinitionText(File definitionFile) {
 
     public Set<Module> loadModules(
             Set<Module> previousModules,
+            Context context,
             String definitionText,
             Source source,
             File currentDirectory,
@@ -187,7 +188,6 @@ public Set<Module> loadModules(
         Definition def = new Definition();
         def.setItems((List<DefinitionItem>) (Object) kilModules);
 
-        Context context = new Context();
         new CollectProductionsVisitor(kore, context).visit(def);
 
         KILtoKORE kilToKore = new KILtoKORE(context, false, kore);
@@ -207,7 +207,7 @@ public org.kframework.definition.Definition loadDefinition(
             File currentDirectory,
             List<File> lookupDirectories,
             boolean kore) {
-        Set<Module> modules = loadModules(previousModules, definitionText, source, currentDirectory, lookupDirectories, new HashSet<>(), kore);
+        Set<Module> modules = loadModules(previousModules, new Context(), definitionText, source, currentDirectory, lookupDirectories, new HashSet<>(), kore);
         Set<Module> allModules = new HashSet<>(modules);
         allModules.addAll(previousModules);
         Module mainModule = getMainModule(mainModuleName, allModules);
@@ -239,9 +239,10 @@ public org.kframework.definition.Definition loadDefinition(
             boolean kore) {
         Set<Module> previousModules = new HashSet<>();
         Set<File> requiredFiles = new HashSet<>();
+        Context context = new Context();
         if (autoImportDomains)
-            previousModules.addAll(loadModules(new HashSet<>(), Kompile.REQUIRE_PRELUDE_K, source, currentDirectory, lookupDirectories, requiredFiles, kore));
-        Set<Module> modules = loadModules(previousModules, definitionText, source, currentDirectory, lookupDirectories, requiredFiles, kore);
+            previousModules.addAll(loadModules(new HashSet<>(), context, Kompile.REQUIRE_PRELUDE_K, source, currentDirectory, lookupDirectories, requiredFiles, kore));
+        Set<Module> modules = loadModules(previousModules, context, definitionText, source, currentDirectory, lookupDirectories, requiredFiles, kore);
         modules.addAll(previousModules); // add the previous modules, since load modules is not additive
         Module mainModule = getMainModule(mainModuleName, modules);
         Optional<Module> opt;
diff --git a/kernel/src/main/java/org/kframework/parser/concrete2kore/generator/RuleGrammarGenerator.java b/kernel/src/main/java/org/kframework/parser/concrete2kore/generator/RuleGrammarGenerator.java
@@ -308,6 +308,17 @@ public static ParseInModule getCombinedGrammar(Module mod, boolean strict, boole
             }).collect(Collectors.toSet());
         } else if (addConfigCells) {
             // remove cells from parsing config cells so they don't conflict with the production in kast.k
+            // also add all matching terminals to the #CellName sort
+            for (Production prod : iterable(mod.productions())) {
+              for (ProductionItem pi : iterable(prod.items())) {
+                if (pi instanceof Terminal) {
+                  Terminal t = (Terminal)pi;
+                  if (t.value().matches("[A-Za-z][A-Za-z0-9\\-]*")) {
+                    prods.add(Production(Sorts.CellName(), Seq(t), Att().add("token")));
+                  }
+                }
+              }
+            }
             parseProds = Stream.concat(prods.stream(), stream(mod.sentences()).filter(s -> !s.att().contains("cell"))).collect(Collectors.toSet());
         } else
             parseProds = Stream.concat(prods.stream(), stream(mod.sentences())).collect(Collectors.toSet());
diff --git a/kore/src/main/scala/org/kframework/builtin/Sorts.scala b/kore/src/main/scala/org/kframework/builtin/Sorts.scala
@@ -36,6 +36,7 @@ object Sorts {
 
   val Bag = Sort("Bag")
   val Cell = Sort("Cell")
+  val CellName = Sort("#CellName");
 
   val GeneratedTopCell = Sort("GeneratedTopCell")
   val GeneratedCounterCell = Sort("GeneratedCounterCell")
diff --git a/ocaml-backend/src/main/java/org/kframework/backend/ocaml/DefinitionToOcaml.java b/ocaml-backend/src/main/java/org/kframework/backend/ocaml/DefinitionToOcaml.java
@@ -34,6 +34,7 @@
 import org.kframework.definition.Rule;
 import org.kframework.definition.Sentence;
 import org.kframework.kil.Attribute;
+import org.kframework.kil.loader.Context;
 import org.kframework.kompile.CompiledDefinition;
 import org.kframework.kompile.Kompile;
 import org.kframework.kompile.KompileOptions;
@@ -1093,6 +1094,7 @@ private void addOpaqueKLabels(Set<KLabel> klabels) {
         lookupDirectories.add(Kompile.BUILTIN_DIRECTORY);
         java.util.Set<Module> mods = new ParserUtils(files::resolveWorkingDirectory, kem, globalOptions).loadModules(
                 new HashSet<>(),
+                new Context(),
                 "require " + StringUtil.enquoteCString(definitionFile.getPath()),
                 Source.apply(definitionFile.getAbsolutePath()),
                 definitionFile.getParentFile(),
