Skala backend

API/src/main/java/org/kframework/Kapi.java

@@ -335,7 +335,7 @@ public static Info getInfo(CompiledDefinition compiledDef, String proofFile, Str
         List<Rule> specRulesKORE = stream(specModule.localRules())
                 .filter(r -> r.toString().contains("spec.k"))
                 .map(r -> (Rule) macroExpander.expand(r))
-                .map(r -> ProofExecutionMode.transformFunction(JavaBackend::ADTKVariableToSortedVariable, r))
+                .map(r -> ProofExecutionMode.transformFunction(Kompile::ADTKVariableToSortedVariable, r))
                 .map(r -> ProofExecutionMode.transformFunction(Kompile::convertKSeqToKApply, r))
                 .map(r -> ProofExecutionMode.transform(NormalizeKSeq.self(), r))
                         //.map(r -> kompile.compileRule(compiledDefinition, r))
@@ -485,7 +485,7 @@ public void kprove(String proofFile, String prelude, CompiledDefinition compiled
         List<Rule> specRules = stream(specModule.localRules())
                 .filter(r -> r.toString().contains("spec.k"))
                 .map(r -> (Rule) macroExpander.expand(r))
-                .map(r -> ProofExecutionMode.transformFunction(JavaBackend::ADTKVariableToSortedVariable, r))
+                .map(r -> ProofExecutionMode.transformFunction(Kompile::ADTKVariableToSortedVariable, r))
                 .map(r -> ProofExecutionMode.transformFunction(Kompile::convertKSeqToKApply, r))
                 .map(r -> ProofExecutionMode.transform(NormalizeKSeq.self(), r))
                         //.map(r -> kompile.compileRule(compiledDefinition, r))

frontend/pom.xml

@@ -48,7 +48,7 @@
     <dependency>
       <groupId>org.kframework.k</groupId>
       <artifactId>kore_2.12</artifactId>
-      <version>1.0-SNAPSHOT</version>
+      <version>0.6-SNAPSHOT</version>
     </dependency>
   </dependencies>
 

frontend/src/main/java/org/kframework/builtin/KLabels.java

@@ -26,5 +26,5 @@ public class KLabels {
 
     public static final String GENERATED_TOP_CELL = "generatedTop";
     public static final String THIS_CONFIGURATION = "THIS_CONFIGURATION";
-    public static final String MAP_LOOKUP = "Map:lookup";
+    public static final String MAP_LOOKUP = "Map@MAP.lookup";
 }

frontend/src/main/scala/org/kframework/minikore/converters/KoreToMini.scala

@@ -1,6 +1,7 @@
 package org.kframework.minikore.converters
 
-import org.kframework.kore._
+import org.kframework.attributes.Att
+import org.kframework.kore.{Sort, _}
 import org.kframework.kore.implementation.DefaultBuilders
 import org.kframework.frontend.SortedADT.SortedKVariable
 import org.kframework.frontend.Unapply._
@@ -40,8 +41,17 @@ object KoreToMini {
       })
       val newAtt = items.map(encode) ++ apply(att)
       prod.klabel match {
-        case Some(label) => SymbolDeclaration(b.Sort(sort.name), b.Symbol(label.name), args, Attributes(newAtt))
-        case None => SymbolDeclaration(b.Sort(sort.name), iNone, args, Attributes(newAtt)) // TODO(Daejun): either subsort or regex; generate injection label for subsort; dummy sentence for regex
+        case Some(label) if label.name != "" =>
+          SymbolDeclaration(b.Sort(sort.name), b.Symbol(label.name), args, Attributes(newAtt))
+        case _ =>
+          if (att.contains(Att.token)) {
+            SymbolDeclaration(b.Sort(sort.name), b.Symbol(sort.name), args, Attributes(newAtt))
+          } else {
+            assert(args.size == 1)
+            val subsort: Sort = args.head
+            SymbolDeclaration(b.Sort(sort.name), b.Symbol("#inject_" + subsort.str + "_into_" + sort.name), args, Attributes(newAtt)) // TODO(Daejun): either subsort or regex; generate injection label for subsort; dummy sentence for regex
+          }
+
       }
 
     case definition.Rule(body, requires, ensures, att) =>
@@ -126,7 +136,7 @@ object KoreToMini {
   // encodePatternAtt(p, Seq(a1,a2,a3)) = #(#(#(p,a1),a2),a3) // TODO(Daejun): add test
   def encodePatternAtt(p: Pattern, att: Attributes): Pattern = {
     att.patterns.foldLeft(p)((z, a) => {
-      b.Application(iAtt, Seq(z, a))
+      b.Application(DefaultBuilders.knownSymbols.PatternWithAttributes, Seq(z, a))
     })
   }
 
@@ -169,9 +179,6 @@ object KoreToMini {
     Symbol("#None"))
   val encodingLabels = encodingLabelTuple.productIterator.toSet
 
-  val iAtt = Symbol("#")
   val iKSeq = Symbol("#kseq")
   val iKSeqNil = Symbol("#kseqnil")
-
-  val iNone = Symbol("#None")
 }

frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala

@@ -4,10 +4,11 @@ import org.kframework.frontend.SortedADT.SortedKVariable
 import org.kframework.frontend.{KORE, _}
 import org.kframework.{attributes, definition}
 import org.kframework.kore._
+
 import scala.collection.JavaConverters._
 import scala.collection._
-
 import KoreToMini._
+import org.kframework.kore.implementation.DefaultBuilders
 
 object MiniToKore {
 
@@ -19,18 +20,21 @@ object MiniToKore {
     val origModuleMap: Map[String, Module] = seq2map(d.modules)
 
     val mainModuleName = findAtt(d.att, iMainModule.str) match {
-      case Seq(DomainValue(Symbol("S"), Value(name))) => name; case _ => ???
+      case Seq(DomainValue(Symbol("S"), Value(name))) => name;
+      case _ => ???
     }
     val (mainModules, otherModules) = d.modules.partition(m => m.name.str == mainModuleName)
-    val mainModule = mainModules.head; assert(mainModules.size == 1)
+    val mainModule = mainModules.head;
+    assert(mainModules.size == 1)
 
     val entryModules = findAtt(d.att, iEntryModules.str).map({
-      case DomainValue(Symbol("S"), Value(name)) => origModuleMap(name); case _ => ???
+      case DomainValue(Symbol("S"), Value(name)) => origModuleMap(name);
+      case _ => ???
     })
 
     val newModuleMapRef: mutable.Map[String, definition.Module] = mutable.Map.empty // will dynamically grow during translating modules
-    val newMainModule = apply(origModuleMap,newModuleMapRef)(mainModule)
-    val newEntryModules = entryModules.map(apply(origModuleMap,newModuleMapRef))
+    val newMainModule = apply(origModuleMap, newModuleMapRef)(mainModule)
+    val newEntryModules = entryModules.map(apply(origModuleMap, newModuleMapRef))
     definition.Definition(
       newMainModule,
       newEntryModules.toSet,
@@ -41,7 +45,7 @@ object MiniToKore {
   def apply(origModuleMap: Map[String, Module], newModuleMapRef: mutable.Map[String, definition.Module])
            (m: Module): definition.Module = {
     val imports = m.sentences.collect({
-      case Import(name, _) => findOrGenModule(origModuleMap,newModuleMapRef)(name.str)
+      case Import(name, _) => findOrGenModule(origModuleMap, newModuleMapRef)(name.str)
     })
     val sentences = m.sentences.filter({ case Import(_, _) => false; case _ => true })
     definition.Module(m.name.str, imports.toSet, sentences.map(apply).toSet, apply(m.att))
@@ -51,7 +55,7 @@ object MiniToKore {
                      (name: String): definition.Module = {
     if (newModuleMapRef.contains(name)) newModuleMapRef(name)
     else {
-      val m = apply(origModuleMap,newModuleMapRef)(origModuleMap(name))
+      val m = apply(origModuleMap, newModuleMapRef)(origModuleMap(name))
       newModuleMapRef += (name -> m)
       m
     }
@@ -84,7 +88,8 @@ object MiniToKore {
       val priorities = prios.map({
         case Application(`iSyntaxPriorityGroup`, group) =>
           group.map({
-            case DomainValue(Symbol("S"), Value(tag)) => definition.Tag(tag); case _ => ???
+            case DomainValue(Symbol("S"), Value(tag)) => definition.Tag(tag);
+            case _ => ???
           }).toSet
         case _ => ???
       })
@@ -97,7 +102,8 @@ object MiniToKore {
         case _ => ???
       }
       val ts = tags.map({
-        case DomainValue(Symbol("S"), tag) => definition.Tag(tag.str); case _ => ???
+        case DomainValue(Symbol("S"), tag) => definition.Tag(tag.str);
+        case _ => ???
       }).toSet
       definition.SyntaxAssociativity(assoc, ts, apply(att))
     case Application(`iBubble`, Seq(DomainValue(Symbol("S"), Value(sentence)), DomainValue(Symbol("S"), Value(contents)))) +: att =>
@@ -111,15 +117,16 @@ object MiniToKore {
 
   def apply(att: Seq[Pattern]): attributes.Att = {
     def isDummy(p: Pattern): Boolean = p match {
-      case Application(l, _) => encodingLabels.contains(l); case _ => false
+      case Application(l, _) => encodingLabels.contains(l);
+      case _ => false
     }
     attributes.Att(att.filterNot(isDummy).map(apply).toSet)
   }
 
   def apply(p: Pattern): K = apply(attributes.Att())(p)
 
   def apply(att: attributes.Att)(p: Pattern): K = p match {
-    case Application(`iKSeq`, Seq(p1,p2)) =>
+    case Application(`iKSeq`, Seq(p1, p2)) =>
       apply(p2) match {
         case k2: KSequence =>
           val items = apply(p1) +: k2.items.asScala.toList // from KSequence in Unapply.scala
@@ -129,16 +136,17 @@ object MiniToKore {
     case Application(`iKSeqNil`, Seq()) =>
       ADT.KSequence(List(), att)
 
-    case Application(`iAtt`, Seq(p1,p2)) =>
+    case Application(DefaultBuilders.knownSymbols.PatternWithAttributes, Seq(p1, p2)) =>
       val a2 = apply(Seq(p2))
       apply(att ++ a2)(p1)
 
     case Application(Symbol(label), args) => KORE.KApply(KORE.KLabel(label), args.map(apply), att)
+
     case DomainValue(Symbol(label), Value(value)) => KORE.KToken(value, KORE.Sort(label), att)
     case SortedVariable(Name(name), Sort("_")) => KORE.KVariable(name, att)
     case SortedVariable(Name(name), _) => SortedKVariable(name, att)
     case Rewrite(left, right) => KORE.KRewrite(apply(left), apply(right), att)
-    case _ => ???
+    case _ => throw new AssertionError("Implementation missing. Couldn't match: " + p + " of class " + p.getClass)
   }
 
   def findAtt(att: Attributes, key: String): Seq[Pattern] = {

frontend/src/test/scala/org/kframework/minikore/KoreToMiniTest.scala

@@ -30,7 +30,7 @@ class KoreToMiniTest {
   @Test def production2(): Unit = {
     assertEquals(
       apply(new definition.Production(Exp, Seq(NonTerminal(Int)), Att())),
-      SymbolDeclaration(Sort(Exp.name), Symbol("#None"), Seq(Sort(Int.name)), Attributes(Seq(Application(iNonTerminal, Seq(S(Int.name))))))
+      SymbolDeclaration(Sort(Exp.name), Symbol("#inject_Int@INT-SYNTAX_into_Exp@A-SYNTAX"), Seq(Sort(Int.name)), Attributes(Seq(Application(iNonTerminal, Seq(S(Int.name))))))
     )
   }
 

java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaBackend.java

@@ -109,7 +109,7 @@ public Function<Definition, Definition> steps() {
                 .andThen(expandMacrosDefinitionTransformer::apply)
                 .andThen(DefinitionTransformer.fromSentenceTransformer(new NormalizeAssoc(KORE.c()), "normalize assoc"))
                 .andThen(convertDataStructureToLookup)
-                .andThen(DefinitionTransformer.fromRuleBodyTranformer(JavaBackend::ADTKVariableToSortedVariable, "ADT.KVariable to SortedVariable"))
+                .andThen(DefinitionTransformer.fromRuleBodyTranformer(Kompile::ADTKVariableToSortedVariable, "ADT.KVariable to SortedVariable"))
                 .andThen(DefinitionTransformer.fromRuleBodyTranformer(Kompile::convertKSeqToKApply, "kseq to kapply"))
                 .andThen(DefinitionTransformer.fromRuleBodyTranformer(NormalizeKSeq.self(), "normalize kseq"))
                 .andThen(JavaBackend::markRegularRules)
@@ -132,7 +132,7 @@ public Function<Definition, Definition> stepsForProverRules() {
                 .andThen(AddBottomSortForListsWithIdenticalLabels.singleton().lift())
                 .andThen(DefinitionTransformer.fromKTransformerWithModuleInfo(JavaBackend::moduleQualifySortPredicates, "Module-qualify sort predicates"))
                 .andThen(expandMacrosDefinitionTransformer::apply)
-                .andThen(DefinitionTransformer.fromRuleBodyTranformer(JavaBackend::ADTKVariableToSortedVariable, "ADT.KVariable to SortedVariable"))
+                .andThen(DefinitionTransformer.fromRuleBodyTranformer(Kompile::ADTKVariableToSortedVariable, "ADT.KVariable to SortedVariable"))
                 .andThen(DefinitionTransformer.fromRuleBodyTranformer(Kompile::convertKSeqToKApply, "kseq to kapply"))
                 .andThen(DefinitionTransformer.fromRuleBodyTranformer(NormalizeKSeq.self(), "normalize kseq"))
                 .andThen(JavaBackend::markRegularRules)
@@ -157,17 +157,6 @@ private static Definition markRegularRules(Definition d) {
         }, "mark regular rules").apply(d);
     }
 
-    /**
-     * The Java backend expects sorted variables, so transform them to the sorted flavor.
-     */
-    public static K ADTKVariableToSortedVariable(K ruleBody) {
-        return new TransformK() {
-            public K apply(KVariable kvar) {
-                return new SortedADT.SortedKVariable(kvar.name(), kvar.att());
-            }
-        }.apply(ruleBody);
-    }
-
     /**
      * Replace variables which only appear once in the pattern and have no side condition on them (including no sorting),
      * with a special marker called THE_VARIABLE which the backend uses for special speed optimisations.

java-backend/src/main/java/org/kframework/backend/java/symbolic/ProofExecutionMode.java

@@ -153,7 +153,7 @@ public K apply(KVariable k) {
                         cellPlaceholderSubstitutionApplication.apply(r.ensures()),
                         r.att()))
                 .map(r -> (Rule) macroExpander.expand(r))
-                .map(r -> transformFunction(JavaBackend::ADTKVariableToSortedVariable, r))
+                .map(r -> transformFunction(Kompile::ADTKVariableToSortedVariable, r))
                 .map(r -> transformFunction(Kompile::convertKSeqToKApply, r))
                 .map(r -> transform(NormalizeKSeq.self(), r))
                 //.map(r -> kompile.compileRule(compiledDefinition, r))

java-backend/src/main/scala/MiniKoreUtils.scala

@@ -62,7 +62,8 @@ object MiniKoreUtils {
       val filterSet = Set(iTerminal.str, iNonTerminal.str, iRegexTerminal.str)
       val labelDecsMap: Map[String, Seq[Pattern]] =
         allSentences collect {
-          case SymbolDeclaration(_, Symbol(label), _, Attributes(att)) if label != iNone => (label, att)
+          // TODO: may need to handle subsort declarations separately
+          case SymbolDeclaration(_, Symbol(label), _, Attributes(att)) => (label, att)
         } groupBy { x => x._1 } mapValues { z => z map {_._2} } mapValues {_.flatten}
       labelDecsMap.mapValues({ s =>
         s.flatMap({ p =>
@@ -139,7 +140,7 @@ object MiniKoreUtils {
 
   def decodePatternAttributes(p: Pattern): (Pattern, Seq[Pattern]) = {
     p match {
-      case Application(`iAtt`, Seq(pat, att)) => decodePatternAttributes(pat) match {
+      case Application(Symbol("#"), Seq(pat, att)) => decodePatternAttributes(pat) match {
         case (finalPat, attList) => (finalPat, attList :+ att)
       }
       case any@_ => (any, Seq())