From 15b584a670c77d206477bc666ccce60b9003c713 Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Thu, 18 May 2017 13:42:54 -0500 Subject: [PATCH 01/34] more cleanup --- .../main/java/org/kframework/ktest/CmdArgs/KTestOptions.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/src/main/java/org/kframework/ktest/CmdArgs/KTestOptions.java b/kernel/src/main/java/org/kframework/ktest/CmdArgs/KTestOptions.java index 058ae94951..8c0729bebd 100644 --- a/kernel/src/main/java/org/kframework/ktest/CmdArgs/KTestOptions.java +++ b/kernel/src/main/java/org/kframework/ktest/CmdArgs/KTestOptions.java @@ -145,7 +145,7 @@ public Class enumClass() { * Timeout for processes spawned by ktest. (in seconds) */ @Parameter(names="--timeout", description="Time limit for each process (milliseconds).") - private int timeout = 900000; + private int timeout = 3000000; /** * Update existing .out files. From 45fa8990343baf0d7bad6144c3626972fdedb1fa Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Thu, 18 May 2017 14:13:40 -0500 Subject: [PATCH 02/34] adjust timeout --- .../main/java/org/kframework/ktest/CmdArgs/KTestOptions.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/src/main/java/org/kframework/ktest/CmdArgs/KTestOptions.java b/kernel/src/main/java/org/kframework/ktest/CmdArgs/KTestOptions.java index 8c0729bebd..e51cfbb052 100644 --- a/kernel/src/main/java/org/kframework/ktest/CmdArgs/KTestOptions.java +++ b/kernel/src/main/java/org/kframework/ktest/CmdArgs/KTestOptions.java @@ -145,7 +145,7 @@ public Class enumClass() { * Timeout for processes spawned by ktest. (in seconds) */ @Parameter(names="--timeout", description="Time limit for each process (milliseconds).") - private int timeout = 3000000; + private int timeout = 600000; /** * Update existing .out files. From c52b2c4b62fe044c2eadb20b1f6865f99ce31516 Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Wed, 24 May 2017 20:32:57 -0500 Subject: [PATCH 03/34] begin working on hooking frontend --- .../org/kframework/kale/KaleRewriter.scala | 391 ++++++++++-------- 1 file changed, 210 insertions(+), 181 deletions(-) diff --git a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala b/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala index c194e5ac5b..8ed4b48bbe 100644 --- a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala +++ b/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala @@ -4,203 +4,35 @@ import java.util import java.util.Optional import org.kframework.attributes.Att +import org.kframework.backend.skala.SkalaBackend import org.kframework.definition._ import org.kframework.frontend.Unapply.KRewrite import org.kframework.frontend._ import org.kframework.rewriter.SearchType import org.kframework.{RewriterResult, frontend} +import org.kframework.kore +import org.kframework.kore.Pattern +import org.kframework.minikore.converters.{KoreToMini, MiniToKore} import scala.collection._ -object KaleRewriter { - val self = this +class SkalaRewriter(d: kore.Definition, m: kore.Module) extends org.kframework.rewriter.Rewriter { - def apply(m: Module): KaleRewriter = new KaleRewriter(m) + val skalaBackend = SkalaBackend(d, m) - private def isEffectivelyAssoc(att: Att): Boolean = - att.contains(Att.assoc) || att.contains(Att.bag) -} - -class KaleRewriter(m: Module) extends org.kframework.rewriter.Rewriter { - - private val productionWithUniqueKLabel: Set[Sentence] = (m.sentences.collect({ - case p: Production if p.klabel.isDefined => p - }) groupBy {_.klabel.get} map {_._2.head}).toSet - - private val syntaxSortDeclarations: Set[Sentence] = m.sentences.collect({ - case p: SyntaxSort => p - }) toSet - - private val assocProductions: Set[Sentence] = productionWithUniqueKLabel.filter(p => KaleRewriter.isEffectivelyAssoc(p.att)).toSet - - private val nonAssocProductions = (productionWithUniqueKLabel | syntaxSortDeclarations) &~ assocProductions + val frontendToKore = KoreToMini - implicit val env = Environment() - - import env._ - import env.builtin._ - - val converters = new KaleConverters(m) - - import converters._ - - case class IsSort(s: Sort)(implicit val env: Environment) extends Named("is" + s.name) with PurelyFunctionalLabel1 with FormulaLabel { - def f(_1: Term): Option[Term] = - kSortOf(_1).map(ss => BOOLEAN(m.subsorts.<=(ss, m.resolve(frontend.KORE.Sort(s.name))))) - } - - private val nonAssocLabels: Set[Label] = nonAssocProductions flatMap { - case SyntaxSort(s, att) => None - case p@Production(s, items, att) if !att.contains(Att.relativeHook) => - implicit val envv = env - att.get(Att.hook) - .flatMap({ hookName: String => Hook(hookName, p.klabel.get.name) }) // use the hook if there - .orElse({ - if (att.contains(Att.token)) { - // it is a token, but not hooked - if (!env.labels.exists(l => l.name == "TOKEN_" + s.name)) - Some(GENERIC_TOKEN(Sort(s.name))) - else - None - } else { - if (p.klabel.isDefined) { - val nonTerminals = items.filter(_.isInstanceOf[NonTerminal]) - val label = if (att.contains(Att.Function)) { - if (p.klabel.get.name.startsWith("is")) { - IsSort(Sort(p.klabel.get.name.substring(2))) - } else { - nonTerminals match { - case Seq() => FunctionDefinedByRewritingLabel0(p.klabel.get.name)(env) - case Seq(_) => FunctionDefinedByRewritingLabel1(p.klabel.get.name)(env) - case Seq(_, _) => FunctionDefinedByRewritingLabel2(p.klabel.get.name)(env) - case Seq(_, _, _) => FunctionDefinedByRewritingLabel3(p.klabel.get.name)(env) - case Seq(_, _, _, _) => FunctionDefinedByRewritingLabel4(p.klabel.get.name)(env) - } - } - } else { - nonTerminals match { - case Seq() => FreeLabel0(p.klabel.get.name) - case Seq(_) => FreeLabel1(p.klabel.get.name) - case Seq(_, _) => FreeLabel2(p.klabel.get.name) - case Seq(_, _, _) => FreeLabel3(p.klabel.get.name) - case Seq(_, _, _, _) => FreeLabel4(p.klabel.get.name) - } - } - Some(label) - } else - None - } - }) - case _ => None - } - - private val nonConstantLabels: Map[String, NodeLabel] = nonAssocLabels collect { - case l: NodeLabel => (l.name, l) - } toMap - - def getLabelForAtt(p: Production, att: String): Label = { - val labels = nonAssocLabels.filter(l => l.name == p.att.get[String](att).get) - assert(labels.size == 1) - labels.head - } - - assocProductions foreach { - case p@Production(s, items, att) => - val unitLabel = getLabelForAtt(p, "unit").asInstanceOf[Label0] - val opLabelName = p.klabel.get.name - env.uniqueLabels.getOrElse(opLabelName, { - val index = att.get[String]("index") - if (index.isDefined && att.contains(Att.comm)) { - def indexFunction(t: Term): Term = t.iterator().toList(index.get.toInt) - MapLabel(opLabelName, indexFunction, unitLabel())(env) - } else { - new AssocWithIdListLabel(opLabelName, unitLabel())(env) - } - }) - } - - nonAssocProductions collect { - case p@Production(s, items, att) if att.contains(Att.relativeHook) => - Hook.relativeHook(att.get(Att.relativeHook).get)(env) - } - - val functionRulesAsLeftRight: Set[(Label, Rewrite)] = m.rules collect { - case rule@Rule(KRewrite(l@Unapply.KApply(klabel, _), r), requires, ensures, att) - if m.attributesFor(klabel).contains(Att.`Function`) => - val res = (env.label(klabel.name), Rewrite(And(convert(l), Equality(convert(requires), BOOLEAN(true))), convert(r))) - res - } - - val functionRules: Map[Label, Set[Rewrite]] = functionRulesAsLeftRight groupBy (_._1) map { case (k, set) => (k, set.map(_._2)) } - - val functionRulesWithRenamedVariables: Map[Label, Set[Rewrite]] = functionRules map { case (k, v) => (k, v map env.renameVariables) } - - env.seal() - - def setFunctionRules(functionRules: Map[Label, Set[Rewrite]]) { - env.labels.collect({ - // TODO: Add an warning for when a function is not defined by either a hook or rules - case l: FunctionDefinedByRewriting => l.setRules(functionRules.getOrElse(l, Set())) - }) - } - - setFunctionRules(functionRulesWithRenamedVariables) - - def reconstruct(inhibitForLabel: Label)(t: Term): Term = t match { - case Node(label, children) if label != inhibitForLabel => label(children map reconstruct(inhibitForLabel) toIterable) - case t => t - } - - def resolveFunctionRHS(functionRules: Map[Label, Set[Rewrite]]): Map[Label, Set[Rewrite]] = { - functionRules map { case (label, rewrites) => (label, rewrites map (rw => reconstruct(label)(rw).asInstanceOf[Rewrite])) } toMap - } - - val finalFunctionRules = Util.fixpoint(resolveFunctionRHS)(functionRules) - setFunctionRules(finalFunctionRules) - - val rules: Set[Rewrite] = m.rules collect { - case rule@Rule(KRewrite(l@Unapply.KApply(klabel, _), r), requires, ensures, att) - if !att.contains(Att.`macro`) && !m.attributesFor(klabel).contains(Att.`Function`) => - val rw = Rewrite(And(convert(l), Equality(convert(requires), BOOLEAN(true))), convert(r)) - rw - } - - val matcher = Matcher(env).default - val substitutionApplier = SubstitutionApply(env) - val rewriterConstructor = Rewriter(substitutionApplier, matcher, env) _ - - // TODO: log this information cleanly - // println("\nFunction rules\n") - // finalFunctionRules.foreach({ case (l, rules) => println(l); println(rules.map(" " + _).mkString("\n")) }) - // println("\nRewriting rules\n") - // println(rules.mkString("\n")) - - val rewrite = rewriterConstructor(rules) + val koreToFrontend = MiniToKore override def execute(k: K, depth: Optional[Integer]): RewriterResult = { - var i = 0 - var term: Term = null - var next: Term = convert(k) - while (term != next && depth.map[Boolean](i == _).orElse(true)) { - term = next - next = rewrite.step(term).headOption.getOrElse(term) - i += 1 - } - term = next - new RewriterResult(Optional.of(0), convertBack(term)) - } + val koreK = frontendToKore(k) - override def `match`(k: K, rule: Rule): K = { - val kaleO = convert(k) - val kaleRule = rule match { - case rule@Rule(KRewrite(l@Unapply.KApply(klabel, _), r), requires, ensures, att) => - val rw = Rewrite(And(convert(l), Equality(convert(requires), BOOLEAN(true))), convert(r)) - rw - } - val res = matcher(kaleRule._1, kaleO) - convertBack(res) + val result: Pattern = skalaBackend.step(koreK) + + new RewriterResult(depth, koreToFrontend(k)) } + override def `match`(k: K, rule: Rule): K = ??? override def search(initialConfiguration: K, depth: Optional[Integer], bound: Optional[Integer], pattern: Rule, searchType: SearchType, resultsAsSubstitution: Boolean): K = ??? @@ -208,3 +40,200 @@ class KaleRewriter(m: Module) extends org.kframework.rewriter.Rewriter { override def prove(rules: util.List[Rule]): util.List[K] = ??? } + +//object KaleRewriter { +// val self = this +// +// def apply(m: Module): KaleRewriter = new KaleRewriter(m) +// +// private def isEffectivelyAssoc(att: Att): Boolean = +// att.contains(Att.assoc) || att.contains(Att.bag) +//} +// +//class KaleRewriter(m: Module) extends org.kframework.rewriter.Rewriter { +// +// private val productionWithUniqueKLabel: Set[Sentence] = (m.sentences.collect({ +// case p: Production if p.klabel.isDefined => p +// }) groupBy {_.klabel.get} map {_._2.head}).toSet +// +// private val syntaxSortDeclarations: Set[Sentence] = m.sentences.collect({ +// case p: SyntaxSort => p +// }) toSet +// +// private val assocProductions: Set[Sentence] = productionWithUniqueKLabel.filter(p => KaleRewriter.isEffectivelyAssoc(p.att)).toSet +// +// private val nonAssocProductions = (productionWithUniqueKLabel | syntaxSortDeclarations) &~ assocProductions +// +// implicit val env = Environment() +// +// import env._ +// import env.builtin._ +// +// val converters = new KaleConverters(m) +// +// import converters._ +// +// case class IsSort(s: Sort)(implicit val env: Environment) extends Named("is" + s.name) with PurelyFunctionalLabel1 with FormulaLabel { +// def f(_1: Term): Option[Term] = +// kSortOf(_1).map(ss => BOOLEAN(m.subsorts.<=(ss, m.resolve(frontend.KORE.Sort(s.name))))) +// } +// +// private val nonAssocLabels: Set[Label] = nonAssocProductions flatMap { +// case SyntaxSort(s, att) => None +// case p@Production(s, items, att) if !att.contains(Att.relativeHook) => +// implicit val envv = env +// att.get(Att.hook) +// .flatMap({ hookName: String => Hook(hookName, p.klabel.get.name) }) // use the hook if there +// .orElse({ +// if (att.contains(Att.token)) { +// // it is a token, but not hooked +// if (!env.labels.exists(l => l.name == "TOKEN_" + s.name)) +// Some(GENERIC_TOKEN(Sort(s.name))) +// else +// None +// } else { +// if (p.klabel.isDefined) { +// val nonTerminals = items.filter(_.isInstanceOf[NonTerminal]) +// val label = if (att.contains(Att.Function)) { +// if (p.klabel.get.name.startsWith("is")) { +// IsSort(Sort(p.klabel.get.name.substring(2))) +// } else { +// nonTerminals match { +// case Seq() => FunctionDefinedByRewritingLabel0(p.klabel.get.name)(env) +// case Seq(_) => FunctionDefinedByRewritingLabel1(p.klabel.get.name)(env) +// case Seq(_, _) => FunctionDefinedByRewritingLabel2(p.klabel.get.name)(env) +// case Seq(_, _, _) => FunctionDefinedByRewritingLabel3(p.klabel.get.name)(env) +// case Seq(_, _, _, _) => FunctionDefinedByRewritingLabel4(p.klabel.get.name)(env) +// } +// } +// } else { +// nonTerminals match { +// case Seq() => FreeLabel0(p.klabel.get.name) +// case Seq(_) => FreeLabel1(p.klabel.get.name) +// case Seq(_, _) => FreeLabel2(p.klabel.get.name) +// case Seq(_, _, _) => FreeLabel3(p.klabel.get.name) +// case Seq(_, _, _, _) => FreeLabel4(p.klabel.get.name) +// } +// } +// Some(label) +// } else +// None +// } +// }) +// case _ => None +// } +// +// private val nonConstantLabels: Map[String, NodeLabel] = nonAssocLabels collect { +// case l: NodeLabel => (l.name, l) +// } toMap +// +// def getLabelForAtt(p: Production, att: String): Label = { +// val labels = nonAssocLabels.filter(l => l.name == p.att.get[String](att).get) +// assert(labels.size == 1) +// labels.head +// } +// +// assocProductions foreach { +// case p@Production(s, items, att) => +// val unitLabel = getLabelForAtt(p, "unit").asInstanceOf[Label0] +// val opLabelName = p.klabel.get.name +// env.uniqueLabels.getOrElse(opLabelName, { +// val index = att.get[String]("index") +// if (index.isDefined && att.contains(Att.comm)) { +// def indexFunction(t: Term): Term = t.iterator().toList(index.get.toInt) +// MapLabel(opLabelName, indexFunction, unitLabel())(env) +// } else { +// new AssocWithIdListLabel(opLabelName, unitLabel())(env) +// } +// }) +// } +// +// nonAssocProductions collect { +// case p@Production(s, items, att) if att.contains(Att.relativeHook) => +// Hook.relativeHook(att.get(Att.relativeHook).get)(env) +// } +// +// val functionRulesAsLeftRight: Set[(Label, Rewrite)] = m.rules collect { +// case rule@Rule(KRewrite(l@Unapply.KApply(klabel, _), r), requires, ensures, att) +// if m.attributesFor(klabel).contains(Att.`Function`) => +// val res = (env.label(klabel.name), Rewrite(And(convert(l), Equality(convert(requires), BOOLEAN(true))), convert(r))) +// res +// } +// +// val functionRules: Map[Label, Set[Rewrite]] = functionRulesAsLeftRight groupBy (_._1) map { case (k, set) => (k, set.map(_._2)) } +// +// val functionRulesWithRenamedVariables: Map[Label, Set[Rewrite]] = functionRules map { case (k, v) => (k, v map env.renameVariables) } +// +// env.seal() +// +// def setFunctionRules(functionRules: Map[Label, Set[Rewrite]]) { +// env.labels.collect({ +// // TODO: Add an warning for when a function is not defined by either a hook or rules +// case l: FunctionDefinedByRewriting => l.setRules(functionRules.getOrElse(l, Set())) +// }) +// } +// +// setFunctionRules(functionRulesWithRenamedVariables) +// +// def reconstruct(inhibitForLabel: Label)(t: Term): Term = t match { +// case Node(label, children) if label != inhibitForLabel => label(children map reconstruct(inhibitForLabel) toIterable) +// case t => t +// } +// +// def resolveFunctionRHS(functionRules: Map[Label, Set[Rewrite]]): Map[Label, Set[Rewrite]] = { +// functionRules map { case (label, rewrites) => (label, rewrites map (rw => reconstruct(label)(rw).asInstanceOf[Rewrite])) } toMap +// } +// +// val finalFunctionRules = Util.fixpoint(resolveFunctionRHS)(functionRules) +// setFunctionRules(finalFunctionRules) +// +// val rules: Set[Rewrite] = m.rules collect { +// case rule@Rule(KRewrite(l@Unapply.KApply(klabel, _), r), requires, ensures, att) +// if !att.contains(Att.`macro`) && !m.attributesFor(klabel).contains(Att.`Function`) => +// val rw = Rewrite(And(convert(l), Equality(convert(requires), BOOLEAN(true))), convert(r)) +// rw +// } +// +// val matcher = Matcher(env).default +// val substitutionApplier = SubstitutionApply(env) +// val rewriterConstructor = Rewriter(substitutionApplier, matcher, env) _ +// +// // TODO: log this information cleanly +// // println("\nFunction rules\n") +// // finalFunctionRules.foreach({ case (l, rules) => println(l); println(rules.map(" " + _).mkString("\n")) }) +// // println("\nRewriting rules\n") +// // println(rules.mkString("\n")) +// +// val rewrite = rewriterConstructor(rules) +// +// override def execute(k: K, depth: Optional[Integer]): RewriterResult = { +// var i = 0 +// var term: Term = null +// var next: Term = convert(k) +// while (term != next && depth.map[Boolean](i == _).orElse(true)) { +// term = next +// next = rewrite.step(term).headOption.getOrElse(term) +// i += 1 +// } +// term = next +// new RewriterResult(Optional.of(0), convertBack(term)) +// } +// +// override def `match`(k: K, rule: Rule): K = { +// val kaleO = convert(k) +// val kaleRule = rule match { +// case rule@Rule(KRewrite(l@Unapply.KApply(klabel, _), r), requires, ensures, att) => +// val rw = Rewrite(And(convert(l), Equality(convert(requires), BOOLEAN(true))), convert(r)) +// rw +// } +// val res = matcher(kaleRule._1, kaleO) +// convertBack(res) +// } +// +// +// override def search(initialConfiguration: K, depth: Optional[Integer], bound: Optional[Integer], pattern: Rule, searchType: SearchType, resultsAsSubstitution: Boolean): K = ??? +// +// override def executeAndMatch(k: K, depth: Optional[Integer], rule: Rule): (RewriterResult, K) = ??? +// +// override def prove(rules: util.List[Rule]): util.List[K] = ??? +//} From 696a6ae49b44537ac297a1817f20abd5686f7a6f Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Thu, 25 May 2017 00:17:57 -0500 Subject: [PATCH 04/34] wip on integrating new skala backend with k --- .../src/main/scala/org/kframework/kale/KaleRewriter.scala | 2 ++ .../org/kframework/utils/inject/DefinitionLoadingModule.java | 3 ++- shell/src/main/java/org/kframework/main/Main.java | 5 +++-- 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala b/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala index 8ed4b48bbe..da4475a322 100644 --- a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala +++ b/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala @@ -16,6 +16,8 @@ import org.kframework.minikore.converters.{KoreToMini, MiniToKore} import scala.collection._ + + class SkalaRewriter(d: kore.Definition, m: kore.Module) extends org.kframework.rewriter.Rewriter { val skalaBackend = SkalaBackend(d, m) diff --git a/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java b/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java index 49a1ba41f0..05c3eaeb2b 100644 --- a/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java +++ b/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java @@ -79,7 +79,8 @@ public static KompileMetaInfo kompilemetaInfo(FileUtil files){ // NOTE: should be matched with org.kframework.kompile.KompileFrontEnd.save() public static CompiledDefinition koreDefinition(BinaryLoader loader, FileUtil files) { // org.kframework.definition.Definition kompiledDefinition = loader.loadOrDie(org.kframework.definition.Definition.class, files.resolveKompiled(FileUtil.KOMPILED_DEFINITION_BIN)); // deprecated - org.kframework.definition.Definition kompiledDefinition = MiniToKore.apply(parseKore(files)); + org.kframework.kore.Definition koreDefition = parseKore(files); + org.kframework.definition.Definition kompiledDefinition = MiniToKore.apply(koreDefition); KompileOptions kompileOptions = loader.loadOrDie(KompileOptions.class, files.resolveKompiled(FileUtil.KOMPILE_OPTIONS_BIN)); org.kframework.definition.Definition parsedDefinition = loader.loadOrDie(org.kframework.definition.Definition.class, files.resolveKompiled(FileUtil.PARSED_DEFINITION_BIN)); org.kframework.frontend.KLabel topCellInitializer = loader.loadOrDie(org.kframework.frontend.KLabel.class, files.resolveKompiled(FileUtil.TOP_CELL_INITIALIZER_BIN)); diff --git a/shell/src/main/java/org/kframework/main/Main.java b/shell/src/main/java/org/kframework/main/Main.java index 173603bc86..1159e5fbe3 100644 --- a/shell/src/main/java/org/kframework/main/Main.java +++ b/shell/src/main/java/org/kframework/main/Main.java @@ -17,6 +17,7 @@ import org.kframework.definition.ProcessedDefinition; import org.kframework.kale.KaleBackend; import org.kframework.kale.KaleRewriter; +import org.kframework.kale.SkalaRewriter; import org.kframework.kast.KastFrontEnd; import org.kframework.kast.KastOptions; import org.kframework.kdep.KDepFrontEnd; @@ -240,8 +241,8 @@ public static int runApplication(String toolName, String[] args, File workingDir kRunOptions.global, kem, kRunOptions.experimental.smt, hookProvider, kompileOptions.transition, kRunOptions, files, initializeDefinition); } else if (kompileOptions.backend.equals(Backends.KALE)) { - initializeRewriter = KaleRewriter::apply; - intializeMiniKoreRewriter = null; + initializeRewriter = null; + intializeMiniKoreRewriter = (x -> new SkalaRewriter(x.getRight(), null)); } else { throw new AssertionError("Backend not hooked to the shell."); } From 9ffbc075a141c566b9b5bbf1712357a2293eea87 Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Thu, 25 May 2017 11:38:46 -0500 Subject: [PATCH 05/34] make build pass + temporarily disable tests --- .../frontend/compile/IMPonKale.java | 84 +++++----- kale-backend/pom.xml | 4 +- .../main/scala/org/kframework/kale/Hook.scala | 35 ---- .../org/kframework/kale/KaleConverters.scala | 154 +++++++++--------- .../org/kframework/kale/KaleRewriter.scala | 2 +- .../main/java/org/kframework/main/Main.java | 2 +- 6 files changed, 123 insertions(+), 158 deletions(-) delete mode 100644 kale-backend/src/main/scala/org/kframework/kale/Hook.scala diff --git a/k-distribution/src/test/java/org/kframework/frontend/compile/IMPonKale.java b/k-distribution/src/test/java/org/kframework/frontend/compile/IMPonKale.java index 7cdf23f68f..b989e50e3d 100644 --- a/k-distribution/src/test/java/org/kframework/frontend/compile/IMPonKale.java +++ b/k-distribution/src/test/java/org/kframework/frontend/compile/IMPonKale.java @@ -13,7 +13,7 @@ import org.kframework.frontend.KORE; import org.kframework.frontend.KToken; import org.kframework.kale.KaleBackend; -import org.kframework.kale.KaleRewriter; +//import org.kframework.kale.KaleRewriter; import org.kframework.kompile.CompiledDefinition; import org.kframework.kompile.Kompile; import org.kframework.kompile.KompileOptions; @@ -46,46 +46,46 @@ protected File testResource(String baseName) throws URISyntaxException { @Test public void simple() throws IOException, URISyntaxException { - String fileName = "tutorial/1_k/2_imp/lesson_4/imp.k"; - String program = "int n, sum;\n" + - "n = 10;\n" + - "sum = 0;\n" + - "while (!(n <= 0)) {\n" + - " sum = sum + n;\n" + - " n = n + -1;\n" + - "}"; - Source source = Source.apply("from test"); - String mainModuleName = "IMP"; - - KExceptionManager kem = new KExceptionManager(new GlobalOptions()); - File definitionFile = testResource(fileName); - KompileOptions kompileOptions = new KompileOptions(); - kompileOptions.backend = Backends.KALE; - GlobalOptions globalOptions = new GlobalOptions(); - globalOptions.debug = true; - globalOptions.warnings = GlobalOptions.Warnings.ALL; - - Kompile kompile = new Kompile(kompileOptions, FileUtil.testFileUtil(), kem, false); - - CompiledDefinition compiledDef = kompile.run(definitionFile, mainModuleName, mainModuleName, new KaleBackend(kompileOptions, kem).steps()); - - BiFunction programParser = compiledDef.getProgramParser(kem); - - K parsed = programParser.apply(program, source); - - Map map = new HashMap<>(); - map.put(KORE.KToken("$PGM", Sorts.KConfigVar()), parsed); - - KApply input = KORE.KApply(compiledDef.topCellInitializer, map.entrySet().stream().map(e -> KApply(KLabel("_|->_"), e.getKey(), e.getValue())).reduce(KApply(KLabel(".Map")), (a, b) -> KApply(KLabel("_Map_"), a, b))); - - KaleRewriter kaleRewriter = new KaleRewriter(compiledDef.executionModule()); - - K kResult = kaleRewriter.execute(input, Optional.empty()).k(); - - Module unparsingModule = compiledDef.getExtensionModule(compiledDef.languageParsingModule()); - - String actual = KOREToTreeNodes.toString(new AddBrackets(unparsingModule).addBrackets((ProductionReference) KOREToTreeNodes.apply(KOREToTreeNodes.up(unparsingModule, kResult), unparsingModule))); - - assertEquals("Execution failed", " . sum |-> 55 n |-> 0 ", actual); +// String fileName = "tutorial/1_k/2_imp/lesson_4/imp.k"; +// String program = "int n, sum;\n" + +// "n = 10;\n" + +// "sum = 0;\n" + +// "while (!(n <= 0)) {\n" + +// " sum = sum + n;\n" + +// " n = n + -1;\n" + +// "}"; +// Source source = Source.apply("from test"); +// String mainModuleName = "IMP"; +// +// KExceptionManager kem = new KExceptionManager(new GlobalOptions()); +// File definitionFile = testResource(fileName); +// KompileOptions kompileOptions = new KompileOptions(); +// kompileOptions.backend = Backends.KALE; +// GlobalOptions globalOptions = new GlobalOptions(); +// globalOptions.debug = true; +// globalOptions.warnings = GlobalOptions.Warnings.ALL; +// +// Kompile kompile = new Kompile(kompileOptions, FileUtil.testFileUtil(), kem, false); +// +// CompiledDefinition compiledDef = kompile.run(definitionFile, mainModuleName, mainModuleName, new KaleBackend(kompileOptions, kem).steps()); +// +// BiFunction programParser = compiledDef.getProgramParser(kem); +// +// K parsed = programParser.apply(program, source); +// +// Map map = new HashMap<>(); +// map.put(KORE.KToken("$PGM", Sorts.KConfigVar()), parsed); + +// KApply input = KORE.KApply(compiledDef.topCellInitializer, map.entrySet().stream().map(e -> KApply(KLabel("_|->_"), e.getKey(), e.getValue())).reduce(KApply(KLabel(".Map")), (a, b) -> KApply(KLabel("_Map_"), a, b))); + +// KaleRewriter kaleRewriter = new KaleRewriter(compiledDef.executionModule()); + +// K kResult = kaleRewriter.execute(input, Optional.empty()).k(); + +// Module unparsingModule = compiledDef.getExtensionModule(compiledDef.languageParsingModule()); + +// String actual = KOREToTreeNodes.toString(new AddBrackets(unparsingModule).addBrackets((ProductionReference) KOREToTreeNodes.apply(KOREToTreeNodes.up(unparsingModule, kResult), unparsingModule))); + +// assertEquals("Execution failed", " . sum |-> 55 n |-> 0 ", actual); } } diff --git a/kale-backend/pom.xml b/kale-backend/pom.xml index 340c6895e0..4f014eb0d5 100644 --- a/kale-backend/pom.xml +++ b/kale-backend/pom.xml @@ -21,9 +21,9 @@ ${project.version} - org.kframework.kale + org.kframework kale_2.12 - 0.4-SNAPSHOT + 0.6-SNAPSHOT diff --git a/kale-backend/src/main/scala/org/kframework/kale/Hook.scala b/kale-backend/src/main/scala/org/kframework/kale/Hook.scala deleted file mode 100644 index 7579adb0b3..0000000000 --- a/kale-backend/src/main/scala/org/kframework/kale/Hook.scala +++ /dev/null @@ -1,35 +0,0 @@ -package org.kframework.kale - -object Hook { - def apply(hookName: String, labelName: String)(implicit env: Environment): Option[Label] = { - import env.builtin.{INT, BOOLEAN} - Some(hookName) collect { - case "INT.le" => Operator(labelName, INT, BOOLEAN, (a: Int, b: Int) => a <= b) - case "INT.add" => PrimitiveFunction2(labelName, INT, (a: Int, b: Int) => a + b) - case "INT.tdiv" => PrimitiveFunction2(labelName, INT, (a: Int, b: Int) => a / b) - case "INT.ne" => Operator(labelName, INT, BOOLEAN, (a: Int, b: Int) => a != b) - case "BOOL.and" => PrimitiveFunction2[Boolean](labelName, BOOLEAN, _ && _) - case "BOOL.or" => PrimitiveFunction2[Boolean](labelName, BOOLEAN, _ || _) - case "BOOL.not" => PrimitiveFunction1[Boolean](labelName, BOOLEAN, !_) - case "SET.unit" => assert(labelName == ".Set"); env.builtin.BuiltinSetUnit - case "SET.concat" => assert(labelName == "_Set_"); env.builtin.BuiltinSet - } - } - - def relativeHook(relativeHook: String)(implicit env: Environment): Option[Label] = relativeHook.split('.').toSeq match { - case Seq(baseLabel: String, hookName: String) => relativeHookByBaseLabel(baseLabel, hookName) - case _ => None - } - - def relativeHookByBaseLabel(baseLabel: String, hookName: String)(implicit env: Environment): Option[Label] = env.label(baseLabel) match { - case l: env.builtin.MapLabel => hookName match { - case "lookup" => Some(l.lookup) - case "keys" => Some(l.keys) - case _ => None - } - case s: env.builtin.SetLabel => hookName match { - case "in" => Some(s.in) - } - case _ => None - } -} diff --git a/kale-backend/src/main/scala/org/kframework/kale/KaleConverters.scala b/kale-backend/src/main/scala/org/kframework/kale/KaleConverters.scala index 9cb2579917..0fac572931 100644 --- a/kale-backend/src/main/scala/org/kframework/kale/KaleConverters.scala +++ b/kale-backend/src/main/scala/org/kframework/kale/KaleConverters.scala @@ -9,81 +9,81 @@ import scala.collection.Map class KaleConverters(m: Module)(implicit val env: Environment) { - import env._ - import env.builtin._ - - private val emptyKSeq = FreeLabel0(".K")(env) - private val kseq = new AssocWithIdListLabel("~>", emptyKSeq()) - - val klabelToLabelRename = Map( - "keys" -> "_Map_.keys", - "lookup" -> "_Map_.lookup", - "Set:in" -> "_Set_.in", - "Map:lookup" -> "_Map_.lookup" - ) - - val labelToKLabelRename = klabelToLabelRename.map(p => (p._2, p._1)).toMap - - def renames(labelName: String) = klabelToLabelRename.getOrElse(labelName, labelName) - - def kSortOf(t: Term): Option[frontend.Sort] = - if (!t.isGround) - None - else - m.sortFor - .get(KORE.KLabel(t.label.name)) - .orElse( - t.label match { - case tokenLabel: GENERIC_TOKEN => Some(m.resolve(frontend.KORE.Sort(tokenLabel.sort.name))) - case BOOLEAN => Some(m.resolve(Sorts.Bool)) - case INT => - Some(m.resolve(Sorts.Int)) - case STRING => Some(m.resolve(Sorts.String)) - case `kseq` => Some(m.Sort("KItem")) - case `emptyKSeq` => Some(m.Sort("K")) - // TODO: handle sorting for conjunctions - // case And => - // val nonFormulas = And.asSubstitutionAndTerms(t)._2.filter(!_.label.isInstanceOf[FormulaLabel]) - // if (nonFormulas.size == 1) - // kSortOf(nonFormulas.head) - // else - // ??? // we have more than one non-formula term. computer the least sort? - case Variable => None - }) - - private lazy val uninterpretedTokenLabels: Map[Sort, ConstantLabel[String]] = (labels collect { - case l@GENERIC_TOKEN(s) => (s, l) - }).toMap + (Sort("KConfigVar@BASIC-K") -> GENERIC_TOKEN(Sort("KConfigVar@BASIC-K"))) - - def convert(klabel: KLabel): Label = label(klabelToLabelRename.getOrElse(klabel.name, klabel.name)) - - def convert(body: K): Term = body match { - case Unapply.KToken(s, sort) => sort match { - case Sorts.Bool => BOOLEAN(s.toBoolean) - case Sorts.Int => INT(s.toInt) - case Sorts.String => STRING(s) - case _ => uninterpretedTokenLabels(Sort(sort.name))(s) - } - case Unapply.KApply(klabel, list) if klabel.name == "#KSequence" => kseq(list map convert) - case Unapply.KApply(klabel, list) => convert(klabel).asInstanceOf[NodeLabel](list map convert) - case v: KVariable => Variable(v.name) - // val kaleV = Variable(v.name) - // v.att.get(Att.sort) - // .map(sort => env.And( - // kaleV, - // Equality(env.label("is" + sort.name).asInstanceOf[Label1](kaleV), BOOLEAN(true))) - // ) - // .getOrElse(kaleV) - case r: KRewrite => Rewrite(convert(r.left), convert(r.right)) - } - - def convertBack(l: Label): KLabel = KORE.KLabel(labelToKLabelRename.getOrElse(l.name, l.name)) - - def convertBack(term: Term): K = term match { - case Variable(x) => KORE.KVariable(x) - case emptyKSeq() => KORE.KSequence() - case t@Node(`kseq`, _) => KORE.KSequence(kseq.asList(t).toList map convertBack: _*) - case Node(label, subterms) => KORE.KApply(convertBack(label), (subterms map convertBack).toSeq: _*) - case t@Constant(label, value) => KORE.KToken(value.toString, kSortOf(t).get) - } +// import env._ +// import env.builtin._ +// +// private val emptyKSeq = FreeLabel0(".K")(env) +// private val kseq = new AssocWithIdListLabel("~>", emptyKSeq()) +// +// val klabelToLabelRename = Map( +// "keys" -> "_Map_.keys", +// "lookup" -> "_Map_.lookup", +// "Set:in" -> "_Set_.in", +// "Map:lookup" -> "_Map_.lookup" +// ) +// +// val labelToKLabelRename = klabelToLabelRename.map(p => (p._2, p._1)).toMap +// +// def renames(labelName: String) = klabelToLabelRename.getOrElse(labelName, labelName) +// +// def kSortOf(t: Term): Option[frontend.Sort] = +// if (!t.isGround) +// None +// else +// m.sortFor +// .get(KORE.KLabel(t.label.name)) +// .orElse( +// t.label match { +// case tokenLabel: GENERIC_TOKEN => Some(m.resolve(frontend.KORE.Sort(tokenLabel.sort.name))) +// case BOOLEAN => Some(m.resolve(Sorts.Bool)) +// case INT => +// Some(m.resolve(Sorts.Int)) +// case STRING => Some(m.resolve(Sorts.String)) +// case `kseq` => Some(m.Sort("KItem")) +// case `emptyKSeq` => Some(m.Sort("K")) +// // TODO: handle sorting for conjunctions +// // case And => +// // val nonFormulas = And.asSubstitutionAndTerms(t)._2.filter(!_.label.isInstanceOf[FormulaLabel]) +// // if (nonFormulas.size == 1) +// // kSortOf(nonFormulas.head) +// // else +// // ??? // we have more than one non-formula term. computer the least sort? +// case Variable => None +// }) +// +// private lazy val uninterpretedTokenLabels: Map[Sort, ConstantLabel[String]] = (labels collect { +// case l@GENERIC_TOKEN(s) => (s, l) +// }).toMap + (Sort("KConfigVar@BASIC-K") -> GENERIC_TOKEN(Sort("KConfigVar@BASIC-K"))) +// +// def convert(klabel: KLabel): Label = label(klabelToLabelRename.getOrElse(klabel.name, klabel.name)) +// +// def convert(body: K): Term = body match { +// case Unapply.KToken(s, sort) => sort match { +// case Sorts.Bool => BOOLEAN(s.toBoolean) +// case Sorts.Int => INT(s.toInt) +// case Sorts.String => STRING(s) +// case _ => uninterpretedTokenLabels(Sort(sort.name))(s) +// } +// case Unapply.KApply(klabel, list) if klabel.name == "#KSequence" => kseq(list map convert) +// case Unapply.KApply(klabel, list) => convert(klabel).asInstanceOf[NodeLabel](list map convert) +// case v: KVariable => Variable(v.name) +// // val kaleV = Variable(v.name) +// // v.att.get(Att.sort) +// // .map(sort => env.And( +// // kaleV, +// // Equality(env.label("is" + sort.name).asInstanceOf[Label1](kaleV), BOOLEAN(true))) +// // ) +// // .getOrElse(kaleV) +// case r: KRewrite => Rewrite(convert(r.left), convert(r.right)) +// } +// +// def convertBack(l: Label): KLabel = KORE.KLabel(labelToKLabelRename.getOrElse(l.name, l.name)) +// +// def convertBack(term: Term): K = term match { +// case Variable(x) => KORE.KVariable(x) +// case emptyKSeq() => KORE.KSequence() +// case t@Node(`kseq`, _) => KORE.KSequence(kseq.asList(t).toList map convertBack: _*) +// case Node(label, subterms) => KORE.KApply(convertBack(label), (subterms map convertBack).toSeq: _*) +// case t@Constant(label, value) => KORE.KToken(value.toString, kSortOf(t).get) +// } } diff --git a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala b/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala index da4475a322..f4544c4871 100644 --- a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala +++ b/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala @@ -40,7 +40,7 @@ class SkalaRewriter(d: kore.Definition, m: kore.Module) extends org.kframework.r override def executeAndMatch(k: K, depth: Optional[Integer], rule: Rule): (RewriterResult, K) = ??? - override def prove(rules: util.List[Rule]): util.List[K] = ??? + override def prove(rules: java.util.List[Rule]): java.util.List[K] = ??? } //object KaleRewriter { diff --git a/shell/src/main/java/org/kframework/main/Main.java b/shell/src/main/java/org/kframework/main/Main.java index 1159e5fbe3..41230c3d27 100644 --- a/shell/src/main/java/org/kframework/main/Main.java +++ b/shell/src/main/java/org/kframework/main/Main.java @@ -16,7 +16,7 @@ import org.kframework.definition.Module; import org.kframework.definition.ProcessedDefinition; import org.kframework.kale.KaleBackend; -import org.kframework.kale.KaleRewriter; +//import org.kframework.kale.KaleRewriter; import org.kframework.kale.SkalaRewriter; import org.kframework.kast.KastFrontEnd; import org.kframework.kast.KastOptions; From 5db8c10949a5dbc88a7330ec4731569fded1df3f Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Fri, 26 May 2017 14:41:53 -0500 Subject: [PATCH 06/34] small changes --- frontend/pom.xml | 2 +- .../src/main/scala/org/kframework/kale/KaleRewriter.scala | 8 ++++++-- shell/src/main/java/org/kframework/main/Main.java | 4 ++-- 3 files changed, 9 insertions(+), 5 deletions(-) diff --git a/frontend/pom.xml b/frontend/pom.xml index 001f383eb8..29512afd15 100644 --- a/frontend/pom.xml +++ b/frontend/pom.xml @@ -48,7 +48,7 @@ org.kframework.k kore_2.12 - 1.0-SNAPSHOT + 0.6-SNAPSHOT diff --git a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala b/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala index f4544c4871..90cb73ecbb 100644 --- a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala +++ b/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala @@ -13,14 +13,18 @@ import org.kframework.{RewriterResult, frontend} import org.kframework.kore import org.kframework.kore.Pattern import org.kframework.minikore.converters.{KoreToMini, MiniToKore} +import org.kframework.kore.extended.implicits._ +import org.kframework.kore.implementation.{DefaultBuilders => db} import scala.collection._ -class SkalaRewriter(d: kore.Definition, m: kore.Module) extends org.kframework.rewriter.Rewriter { +class KaleRewriter(mainModule: Module, koreDefinition: kore.Definition) extends org.kframework.rewriter.Rewriter { - val skalaBackend = SkalaBackend(d, m) + val mainKoreModule = koreDefinition.modulesMap(db.ModuleName(mainModule.name)) + + val skalaBackend = SkalaBackend(koreDefinition, mainKoreModule) val frontendToKore = KoreToMini diff --git a/shell/src/main/java/org/kframework/main/Main.java b/shell/src/main/java/org/kframework/main/Main.java index 41230c3d27..7c77518431 100644 --- a/shell/src/main/java/org/kframework/main/Main.java +++ b/shell/src/main/java/org/kframework/main/Main.java @@ -17,7 +17,7 @@ import org.kframework.definition.ProcessedDefinition; import org.kframework.kale.KaleBackend; //import org.kframework.kale.KaleRewriter; -import org.kframework.kale.SkalaRewriter; +import org.kframework.kale.KaleRewriter; import org.kframework.kast.KastFrontEnd; import org.kframework.kast.KastOptions; import org.kframework.kdep.KDepFrontEnd; @@ -242,7 +242,7 @@ public static int runApplication(String toolName, String[] args, File workingDir kRunOptions, files, initializeDefinition); } else if (kompileOptions.backend.equals(Backends.KALE)) { initializeRewriter = null; - intializeMiniKoreRewriter = (x -> new SkalaRewriter(x.getRight(), null)); + intializeMiniKoreRewriter = (x -> new KaleRewriter(x.getKey(), x.getRight())); } else { throw new AssertionError("Backend not hooked to the shell."); } From cbf36d5bdfe619220a3233c7227ce755077f08f0 Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Mon, 29 May 2017 00:49:01 -0500 Subject: [PATCH 07/34] changes to Kale Rewriter --- .../src/main/scala/org/kframework/kale/KaleRewriter.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala b/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala index 90cb73ecbb..0aafffa1dc 100644 --- a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala +++ b/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala @@ -35,7 +35,7 @@ class KaleRewriter(mainModule: Module, koreDefinition: kore.Definition) extends val result: Pattern = skalaBackend.step(koreK) - new RewriterResult(depth, koreToFrontend(k)) + new RewriterResult(depth, koreToFrontend(result)) } override def `match`(k: K, rule: Rule): K = ??? From 06003465fcf440817cb2eaf2b90d7ed3bb58afa2 Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Mon, 29 May 2017 14:25:37 -0500 Subject: [PATCH 08/34] changes to k-distribution's pom to use current version of Kale --- k-distribution/pom.xml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/pom.xml b/k-distribution/pom.xml index b3fa4254d5..800280212f 100644 --- a/k-distribution/pom.xml +++ b/k-distribution/pom.xml @@ -54,9 +54,9 @@ ${project.version} - org.kframework.kale + org.kframework kale_2.12 - 0.4-SNAPSHOT + 0.6-SNAPSHOT From c952c89f4b12561db187b0cf432e2479bce178c6 Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Mon, 29 May 2017 18:39:09 -0500 Subject: [PATCH 09/34] renaming + adding tests --- k-distribution/pom.xml | 2 +- .../frontend/compile/IMPonKale.java | 91 ------- .../tutorial/1_k/2_imp/lesson_1/tests/sum.imp | 2 +- .../org/kframework/kale/KaleConverters.scala | 89 ------- .../org/kframework/kale/KaleRewriter.scala | 245 ------------------ pom.xml | 2 +- shell/pom.xml | 2 +- .../main/java/org/kframework/main/Main.java | 10 +- {kale-backend => skala-backend}/pom.xml | 4 +- .../services/org.kframework.main.KModule | 0 .../backend/skala/SkalaKompile.scala | 4 +- .../backend/skala/SkalaRewriter.scala | 43 +++ 12 files changed, 56 insertions(+), 438 deletions(-) delete mode 100644 k-distribution/src/test/java/org/kframework/frontend/compile/IMPonKale.java delete mode 100644 kale-backend/src/main/scala/org/kframework/kale/KaleConverters.scala delete mode 100644 kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala rename {kale-backend => skala-backend}/pom.xml (95%) rename {kale-backend => skala-backend}/src/main/resources/META-INF/services/org.kframework.main.KModule (100%) rename kale-backend/src/main/scala/org/kframework/kale/KaleBackend.scala => skala-backend/src/main/scala/org/kframework/backend/skala/SkalaKompile.scala (92%) create mode 100644 skala-backend/src/main/scala/org/kframework/backend/skala/SkalaRewriter.scala diff --git a/k-distribution/pom.xml b/k-distribution/pom.xml index 800280212f..1163d44732 100644 --- a/k-distribution/pom.xml +++ b/k-distribution/pom.xml @@ -50,7 +50,7 @@ org.kframework.k - kale-backend + skala-backend ${project.version} diff --git a/k-distribution/src/test/java/org/kframework/frontend/compile/IMPonKale.java b/k-distribution/src/test/java/org/kframework/frontend/compile/IMPonKale.java deleted file mode 100644 index b989e50e3d..0000000000 --- a/k-distribution/src/test/java/org/kframework/frontend/compile/IMPonKale.java +++ /dev/null @@ -1,91 +0,0 @@ -// Copyright (c) 2015-2016 K Team. All Rights Reserved. - -package org.kframework.frontend.compile; - -import org.junit.Test; -import org.junit.rules.TestName; -import org.kframework.attributes.Source; -import org.kframework.backend.Backends; -import org.kframework.builtin.Sorts; -import org.kframework.definition.Module; -import org.kframework.frontend.K; -import org.kframework.frontend.KApply; -import org.kframework.frontend.KORE; -import org.kframework.frontend.KToken; -import org.kframework.kale.KaleBackend; -//import org.kframework.kale.KaleRewriter; -import org.kframework.kompile.CompiledDefinition; -import org.kframework.kompile.Kompile; -import org.kframework.kompile.KompileOptions; -import org.kframework.main.GlobalOptions; -import org.kframework.parser.ProductionReference; -import org.kframework.unparser.AddBrackets; -import org.kframework.unparser.KOREToTreeNodes; -import org.kframework.utils.errorsystem.KExceptionManager; -import org.kframework.utils.file.FileUtil; - -import java.io.File; -import java.io.IOException; -import java.net.URISyntaxException; -import java.util.HashMap; -import java.util.Map; -import java.util.Optional; -import java.util.function.BiFunction; - -import static org.junit.Assert.*; -import static org.kframework.frontend.KORE.*; - -public class IMPonKale { - - @org.junit.Rule - public TestName name = new TestName(); - - protected File testResource(String baseName) throws URISyntaxException { - return new File(baseName); - } - - @Test - public void simple() throws IOException, URISyntaxException { -// String fileName = "tutorial/1_k/2_imp/lesson_4/imp.k"; -// String program = "int n, sum;\n" + -// "n = 10;\n" + -// "sum = 0;\n" + -// "while (!(n <= 0)) {\n" + -// " sum = sum + n;\n" + -// " n = n + -1;\n" + -// "}"; -// Source source = Source.apply("from test"); -// String mainModuleName = "IMP"; -// -// KExceptionManager kem = new KExceptionManager(new GlobalOptions()); -// File definitionFile = testResource(fileName); -// KompileOptions kompileOptions = new KompileOptions(); -// kompileOptions.backend = Backends.KALE; -// GlobalOptions globalOptions = new GlobalOptions(); -// globalOptions.debug = true; -// globalOptions.warnings = GlobalOptions.Warnings.ALL; -// -// Kompile kompile = new Kompile(kompileOptions, FileUtil.testFileUtil(), kem, false); -// -// CompiledDefinition compiledDef = kompile.run(definitionFile, mainModuleName, mainModuleName, new KaleBackend(kompileOptions, kem).steps()); -// -// BiFunction programParser = compiledDef.getProgramParser(kem); -// -// K parsed = programParser.apply(program, source); -// -// Map map = new HashMap<>(); -// map.put(KORE.KToken("$PGM", Sorts.KConfigVar()), parsed); - -// KApply input = KORE.KApply(compiledDef.topCellInitializer, map.entrySet().stream().map(e -> KApply(KLabel("_|->_"), e.getKey(), e.getValue())).reduce(KApply(KLabel(".Map")), (a, b) -> KApply(KLabel("_Map_"), a, b))); - -// KaleRewriter kaleRewriter = new KaleRewriter(compiledDef.executionModule()); - -// K kResult = kaleRewriter.execute(input, Optional.empty()).k(); - -// Module unparsingModule = compiledDef.getExtensionModule(compiledDef.languageParsingModule()); - -// String actual = KOREToTreeNodes.toString(new AddBrackets(unparsingModule).addBrackets((ProductionReference) KOREToTreeNodes.apply(KOREToTreeNodes.up(unparsingModule, kResult), unparsingModule))); - -// assertEquals("Execution failed", " . sum |-> 55 n |-> 0 ", actual); - } -} diff --git a/k-distribution/tutorial/1_k/2_imp/lesson_1/tests/sum.imp b/k-distribution/tutorial/1_k/2_imp/lesson_1/tests/sum.imp index 23e8bb6df0..552576a250 100644 --- a/k-distribution/tutorial/1_k/2_imp/lesson_1/tests/sum.imp +++ b/k-distribution/tutorial/1_k/2_imp/lesson_1/tests/sum.imp @@ -2,7 +2,7 @@ // the sum of numbers from 1 to n. int n, sum; -n = 100; +n = 10; sum = 0; while (!(n <= 0)) { sum = sum + n; diff --git a/kale-backend/src/main/scala/org/kframework/kale/KaleConverters.scala b/kale-backend/src/main/scala/org/kframework/kale/KaleConverters.scala deleted file mode 100644 index 0fac572931..0000000000 --- a/kale-backend/src/main/scala/org/kframework/kale/KaleConverters.scala +++ /dev/null @@ -1,89 +0,0 @@ -package org.kframework.kale - -import org.kframework.builtin.Sorts -import org.kframework.definition.Module -import org.kframework.frontend -import org.kframework.frontend._ - -import scala.collection.Map - -class KaleConverters(m: Module)(implicit val env: Environment) { - -// import env._ -// import env.builtin._ -// -// private val emptyKSeq = FreeLabel0(".K")(env) -// private val kseq = new AssocWithIdListLabel("~>", emptyKSeq()) -// -// val klabelToLabelRename = Map( -// "keys" -> "_Map_.keys", -// "lookup" -> "_Map_.lookup", -// "Set:in" -> "_Set_.in", -// "Map:lookup" -> "_Map_.lookup" -// ) -// -// val labelToKLabelRename = klabelToLabelRename.map(p => (p._2, p._1)).toMap -// -// def renames(labelName: String) = klabelToLabelRename.getOrElse(labelName, labelName) -// -// def kSortOf(t: Term): Option[frontend.Sort] = -// if (!t.isGround) -// None -// else -// m.sortFor -// .get(KORE.KLabel(t.label.name)) -// .orElse( -// t.label match { -// case tokenLabel: GENERIC_TOKEN => Some(m.resolve(frontend.KORE.Sort(tokenLabel.sort.name))) -// case BOOLEAN => Some(m.resolve(Sorts.Bool)) -// case INT => -// Some(m.resolve(Sorts.Int)) -// case STRING => Some(m.resolve(Sorts.String)) -// case `kseq` => Some(m.Sort("KItem")) -// case `emptyKSeq` => Some(m.Sort("K")) -// // TODO: handle sorting for conjunctions -// // case And => -// // val nonFormulas = And.asSubstitutionAndTerms(t)._2.filter(!_.label.isInstanceOf[FormulaLabel]) -// // if (nonFormulas.size == 1) -// // kSortOf(nonFormulas.head) -// // else -// // ??? // we have more than one non-formula term. computer the least sort? -// case Variable => None -// }) -// -// private lazy val uninterpretedTokenLabels: Map[Sort, ConstantLabel[String]] = (labels collect { -// case l@GENERIC_TOKEN(s) => (s, l) -// }).toMap + (Sort("KConfigVar@BASIC-K") -> GENERIC_TOKEN(Sort("KConfigVar@BASIC-K"))) -// -// def convert(klabel: KLabel): Label = label(klabelToLabelRename.getOrElse(klabel.name, klabel.name)) -// -// def convert(body: K): Term = body match { -// case Unapply.KToken(s, sort) => sort match { -// case Sorts.Bool => BOOLEAN(s.toBoolean) -// case Sorts.Int => INT(s.toInt) -// case Sorts.String => STRING(s) -// case _ => uninterpretedTokenLabels(Sort(sort.name))(s) -// } -// case Unapply.KApply(klabel, list) if klabel.name == "#KSequence" => kseq(list map convert) -// case Unapply.KApply(klabel, list) => convert(klabel).asInstanceOf[NodeLabel](list map convert) -// case v: KVariable => Variable(v.name) -// // val kaleV = Variable(v.name) -// // v.att.get(Att.sort) -// // .map(sort => env.And( -// // kaleV, -// // Equality(env.label("is" + sort.name).asInstanceOf[Label1](kaleV), BOOLEAN(true))) -// // ) -// // .getOrElse(kaleV) -// case r: KRewrite => Rewrite(convert(r.left), convert(r.right)) -// } -// -// def convertBack(l: Label): KLabel = KORE.KLabel(labelToKLabelRename.getOrElse(l.name, l.name)) -// -// def convertBack(term: Term): K = term match { -// case Variable(x) => KORE.KVariable(x) -// case emptyKSeq() => KORE.KSequence() -// case t@Node(`kseq`, _) => KORE.KSequence(kseq.asList(t).toList map convertBack: _*) -// case Node(label, subterms) => KORE.KApply(convertBack(label), (subterms map convertBack).toSeq: _*) -// case t@Constant(label, value) => KORE.KToken(value.toString, kSortOf(t).get) -// } -} diff --git a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala b/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala deleted file mode 100644 index 0aafffa1dc..0000000000 --- a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala +++ /dev/null @@ -1,245 +0,0 @@ -package org.kframework.kale - -import java.util -import java.util.Optional - -import org.kframework.attributes.Att -import org.kframework.backend.skala.SkalaBackend -import org.kframework.definition._ -import org.kframework.frontend.Unapply.KRewrite -import org.kframework.frontend._ -import org.kframework.rewriter.SearchType -import org.kframework.{RewriterResult, frontend} -import org.kframework.kore -import org.kframework.kore.Pattern -import org.kframework.minikore.converters.{KoreToMini, MiniToKore} -import org.kframework.kore.extended.implicits._ -import org.kframework.kore.implementation.{DefaultBuilders => db} - -import scala.collection._ - - - -class KaleRewriter(mainModule: Module, koreDefinition: kore.Definition) extends org.kframework.rewriter.Rewriter { - - val mainKoreModule = koreDefinition.modulesMap(db.ModuleName(mainModule.name)) - - val skalaBackend = SkalaBackend(koreDefinition, mainKoreModule) - - val frontendToKore = KoreToMini - - val koreToFrontend = MiniToKore - - override def execute(k: K, depth: Optional[Integer]): RewriterResult = { - val koreK = frontendToKore(k) - - val result: Pattern = skalaBackend.step(koreK) - - new RewriterResult(depth, koreToFrontend(result)) - } - - override def `match`(k: K, rule: Rule): K = ??? - - override def search(initialConfiguration: K, depth: Optional[Integer], bound: Optional[Integer], pattern: Rule, searchType: SearchType, resultsAsSubstitution: Boolean): K = ??? - - override def executeAndMatch(k: K, depth: Optional[Integer], rule: Rule): (RewriterResult, K) = ??? - - override def prove(rules: java.util.List[Rule]): java.util.List[K] = ??? -} - -//object KaleRewriter { -// val self = this -// -// def apply(m: Module): KaleRewriter = new KaleRewriter(m) -// -// private def isEffectivelyAssoc(att: Att): Boolean = -// att.contains(Att.assoc) || att.contains(Att.bag) -//} -// -//class KaleRewriter(m: Module) extends org.kframework.rewriter.Rewriter { -// -// private val productionWithUniqueKLabel: Set[Sentence] = (m.sentences.collect({ -// case p: Production if p.klabel.isDefined => p -// }) groupBy {_.klabel.get} map {_._2.head}).toSet -// -// private val syntaxSortDeclarations: Set[Sentence] = m.sentences.collect({ -// case p: SyntaxSort => p -// }) toSet -// -// private val assocProductions: Set[Sentence] = productionWithUniqueKLabel.filter(p => KaleRewriter.isEffectivelyAssoc(p.att)).toSet -// -// private val nonAssocProductions = (productionWithUniqueKLabel | syntaxSortDeclarations) &~ assocProductions -// -// implicit val env = Environment() -// -// import env._ -// import env.builtin._ -// -// val converters = new KaleConverters(m) -// -// import converters._ -// -// case class IsSort(s: Sort)(implicit val env: Environment) extends Named("is" + s.name) with PurelyFunctionalLabel1 with FormulaLabel { -// def f(_1: Term): Option[Term] = -// kSortOf(_1).map(ss => BOOLEAN(m.subsorts.<=(ss, m.resolve(frontend.KORE.Sort(s.name))))) -// } -// -// private val nonAssocLabels: Set[Label] = nonAssocProductions flatMap { -// case SyntaxSort(s, att) => None -// case p@Production(s, items, att) if !att.contains(Att.relativeHook) => -// implicit val envv = env -// att.get(Att.hook) -// .flatMap({ hookName: String => Hook(hookName, p.klabel.get.name) }) // use the hook if there -// .orElse({ -// if (att.contains(Att.token)) { -// // it is a token, but not hooked -// if (!env.labels.exists(l => l.name == "TOKEN_" + s.name)) -// Some(GENERIC_TOKEN(Sort(s.name))) -// else -// None -// } else { -// if (p.klabel.isDefined) { -// val nonTerminals = items.filter(_.isInstanceOf[NonTerminal]) -// val label = if (att.contains(Att.Function)) { -// if (p.klabel.get.name.startsWith("is")) { -// IsSort(Sort(p.klabel.get.name.substring(2))) -// } else { -// nonTerminals match { -// case Seq() => FunctionDefinedByRewritingLabel0(p.klabel.get.name)(env) -// case Seq(_) => FunctionDefinedByRewritingLabel1(p.klabel.get.name)(env) -// case Seq(_, _) => FunctionDefinedByRewritingLabel2(p.klabel.get.name)(env) -// case Seq(_, _, _) => FunctionDefinedByRewritingLabel3(p.klabel.get.name)(env) -// case Seq(_, _, _, _) => FunctionDefinedByRewritingLabel4(p.klabel.get.name)(env) -// } -// } -// } else { -// nonTerminals match { -// case Seq() => FreeLabel0(p.klabel.get.name) -// case Seq(_) => FreeLabel1(p.klabel.get.name) -// case Seq(_, _) => FreeLabel2(p.klabel.get.name) -// case Seq(_, _, _) => FreeLabel3(p.klabel.get.name) -// case Seq(_, _, _, _) => FreeLabel4(p.klabel.get.name) -// } -// } -// Some(label) -// } else -// None -// } -// }) -// case _ => None -// } -// -// private val nonConstantLabels: Map[String, NodeLabel] = nonAssocLabels collect { -// case l: NodeLabel => (l.name, l) -// } toMap -// -// def getLabelForAtt(p: Production, att: String): Label = { -// val labels = nonAssocLabels.filter(l => l.name == p.att.get[String](att).get) -// assert(labels.size == 1) -// labels.head -// } -// -// assocProductions foreach { -// case p@Production(s, items, att) => -// val unitLabel = getLabelForAtt(p, "unit").asInstanceOf[Label0] -// val opLabelName = p.klabel.get.name -// env.uniqueLabels.getOrElse(opLabelName, { -// val index = att.get[String]("index") -// if (index.isDefined && att.contains(Att.comm)) { -// def indexFunction(t: Term): Term = t.iterator().toList(index.get.toInt) -// MapLabel(opLabelName, indexFunction, unitLabel())(env) -// } else { -// new AssocWithIdListLabel(opLabelName, unitLabel())(env) -// } -// }) -// } -// -// nonAssocProductions collect { -// case p@Production(s, items, att) if att.contains(Att.relativeHook) => -// Hook.relativeHook(att.get(Att.relativeHook).get)(env) -// } -// -// val functionRulesAsLeftRight: Set[(Label, Rewrite)] = m.rules collect { -// case rule@Rule(KRewrite(l@Unapply.KApply(klabel, _), r), requires, ensures, att) -// if m.attributesFor(klabel).contains(Att.`Function`) => -// val res = (env.label(klabel.name), Rewrite(And(convert(l), Equality(convert(requires), BOOLEAN(true))), convert(r))) -// res -// } -// -// val functionRules: Map[Label, Set[Rewrite]] = functionRulesAsLeftRight groupBy (_._1) map { case (k, set) => (k, set.map(_._2)) } -// -// val functionRulesWithRenamedVariables: Map[Label, Set[Rewrite]] = functionRules map { case (k, v) => (k, v map env.renameVariables) } -// -// env.seal() -// -// def setFunctionRules(functionRules: Map[Label, Set[Rewrite]]) { -// env.labels.collect({ -// // TODO: Add an warning for when a function is not defined by either a hook or rules -// case l: FunctionDefinedByRewriting => l.setRules(functionRules.getOrElse(l, Set())) -// }) -// } -// -// setFunctionRules(functionRulesWithRenamedVariables) -// -// def reconstruct(inhibitForLabel: Label)(t: Term): Term = t match { -// case Node(label, children) if label != inhibitForLabel => label(children map reconstruct(inhibitForLabel) toIterable) -// case t => t -// } -// -// def resolveFunctionRHS(functionRules: Map[Label, Set[Rewrite]]): Map[Label, Set[Rewrite]] = { -// functionRules map { case (label, rewrites) => (label, rewrites map (rw => reconstruct(label)(rw).asInstanceOf[Rewrite])) } toMap -// } -// -// val finalFunctionRules = Util.fixpoint(resolveFunctionRHS)(functionRules) -// setFunctionRules(finalFunctionRules) -// -// val rules: Set[Rewrite] = m.rules collect { -// case rule@Rule(KRewrite(l@Unapply.KApply(klabel, _), r), requires, ensures, att) -// if !att.contains(Att.`macro`) && !m.attributesFor(klabel).contains(Att.`Function`) => -// val rw = Rewrite(And(convert(l), Equality(convert(requires), BOOLEAN(true))), convert(r)) -// rw -// } -// -// val matcher = Matcher(env).default -// val substitutionApplier = SubstitutionApply(env) -// val rewriterConstructor = Rewriter(substitutionApplier, matcher, env) _ -// -// // TODO: log this information cleanly -// // println("\nFunction rules\n") -// // finalFunctionRules.foreach({ case (l, rules) => println(l); println(rules.map(" " + _).mkString("\n")) }) -// // println("\nRewriting rules\n") -// // println(rules.mkString("\n")) -// -// val rewrite = rewriterConstructor(rules) -// -// override def execute(k: K, depth: Optional[Integer]): RewriterResult = { -// var i = 0 -// var term: Term = null -// var next: Term = convert(k) -// while (term != next && depth.map[Boolean](i == _).orElse(true)) { -// term = next -// next = rewrite.step(term).headOption.getOrElse(term) -// i += 1 -// } -// term = next -// new RewriterResult(Optional.of(0), convertBack(term)) -// } -// -// override def `match`(k: K, rule: Rule): K = { -// val kaleO = convert(k) -// val kaleRule = rule match { -// case rule@Rule(KRewrite(l@Unapply.KApply(klabel, _), r), requires, ensures, att) => -// val rw = Rewrite(And(convert(l), Equality(convert(requires), BOOLEAN(true))), convert(r)) -// rw -// } -// val res = matcher(kaleRule._1, kaleO) -// convertBack(res) -// } -// -// -// override def search(initialConfiguration: K, depth: Optional[Integer], bound: Optional[Integer], pattern: Rule, searchType: SearchType, resultsAsSubstitution: Boolean): K = ??? -// -// override def executeAndMatch(k: K, depth: Optional[Integer], rule: Rule): (RewriterResult, K) = ??? -// -// override def prove(rules: util.List[Rule]): util.List[K] = ??? -//} diff --git a/pom.xml b/pom.xml index 14323c9594..20062ac65d 100644 --- a/pom.xml +++ b/pom.xml @@ -18,7 +18,7 @@ API kdoc shell - kale-backend + skala-backend diff --git a/shell/pom.xml b/shell/pom.xml index 3bb4bd45a0..40f06de093 100644 --- a/shell/pom.xml +++ b/shell/pom.xml @@ -31,7 +31,7 @@ org.kframework.k - kale-backend + skala-backend ${project.version} diff --git a/shell/src/main/java/org/kframework/main/Main.java b/shell/src/main/java/org/kframework/main/Main.java index 7c77518431..17168f236f 100644 --- a/shell/src/main/java/org/kframework/main/Main.java +++ b/shell/src/main/java/org/kframework/main/Main.java @@ -15,9 +15,9 @@ import org.kframework.backend.java.symbolic.ProofExecutionMode; import org.kframework.definition.Module; import org.kframework.definition.ProcessedDefinition; -import org.kframework.kale.KaleBackend; -//import org.kframework.kale.KaleRewriter; -import org.kframework.kale.KaleRewriter; +import org.kframework.backend.skala.SkalaKompile; +//import KaleRewriter; +import org.kframework.backend.skala.SkalaRewriter; import org.kframework.kast.KastFrontEnd; import org.kframework.kast.KastOptions; import org.kframework.kdep.KDepFrontEnd; @@ -124,7 +124,7 @@ public static int runApplication(String toolName, String[] args, File workingDir if (kompileOptions.backend.equals(Backends.JAVA)) { koreBackend = new JavaBackend(kem, files, kompileOptions.global, kompileOptions); } else if (kompileOptions.backend.equals(Backends.KALE)) { - koreBackend = new KaleBackend(kompileOptions, kem); + koreBackend = new SkalaKompile(kompileOptions, kem); } else throw new AssertionError("Backend not hooked to the shell."); KompileFrontEnd frontEnd = new KompileFrontEnd(kompileOptions, koreBackend, sw, kem, loader, files); @@ -242,7 +242,7 @@ public static int runApplication(String toolName, String[] args, File workingDir kRunOptions, files, initializeDefinition); } else if (kompileOptions.backend.equals(Backends.KALE)) { initializeRewriter = null; - intializeMiniKoreRewriter = (x -> new KaleRewriter(x.getKey(), x.getRight())); + intializeMiniKoreRewriter = (x -> new SkalaRewriter(x.getKey(), x.getRight())); } else { throw new AssertionError("Backend not hooked to the shell."); } diff --git a/kale-backend/pom.xml b/skala-backend/pom.xml similarity index 95% rename from kale-backend/pom.xml rename to skala-backend/pom.xml index 4f014eb0d5..016e2749a9 100644 --- a/kale-backend/pom.xml +++ b/skala-backend/pom.xml @@ -9,10 +9,10 @@ 4.0.1-SNAPSHOT ../pom.xml - kale-backend + skala-backend jar - K Framework Kale Backend + K Framework Skala Backend diff --git a/kale-backend/src/main/resources/META-INF/services/org.kframework.main.KModule b/skala-backend/src/main/resources/META-INF/services/org.kframework.main.KModule similarity index 100% rename from kale-backend/src/main/resources/META-INF/services/org.kframework.main.KModule rename to skala-backend/src/main/resources/META-INF/services/org.kframework.main.KModule diff --git a/kale-backend/src/main/scala/org/kframework/kale/KaleBackend.scala b/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaKompile.scala similarity index 92% rename from kale-backend/src/main/scala/org/kframework/kale/KaleBackend.scala rename to skala-backend/src/main/scala/org/kframework/backend/skala/SkalaKompile.scala index 3132d2aa0e..9420c79a13 100644 --- a/kale-backend/src/main/scala/org/kframework/kale/KaleBackend.scala +++ b/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaKompile.scala @@ -1,4 +1,4 @@ -package org.kframework.kale +package org.kframework.backend.skala import java.util.function.Function @@ -9,7 +9,7 @@ import org.kframework.frontend.KORE import org.kframework.frontend.compile._ import org.kframework.utils.errorsystem.KExceptionManager -class KaleBackend(kompileOptions: KompileOptions, kem: KExceptionManager) extends Backend { +class SkalaKompile(kompileOptions: KompileOptions, kem: KExceptionManager) extends Backend { override def accept(d: CompiledDefinition): Unit = { // probably a redundant function } diff --git a/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaRewriter.scala b/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaRewriter.scala new file mode 100644 index 0000000000..c6fc76e8b2 --- /dev/null +++ b/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaRewriter.scala @@ -0,0 +1,43 @@ +package org.kframework.backend.skala + +import java.util.Optional + +import org.kframework.definition._ +import org.kframework.frontend._ +import org.kframework.{RewriterResult, kore} +import org.kframework.kore.Pattern +import org.kframework.kore.extended.implicits._ +import org.kframework.kore.implementation.{DefaultBuilders => db} +import org.kframework.minikore.converters.{KoreToMini, MiniToKore} +import org.kframework.rewriter.SearchType + + + +class SkalaRewriter(mainModule: Module, koreDefinition: kore.Definition) extends org.kframework.rewriter.Rewriter { + + val mainKoreModule = koreDefinition.modulesMap(db.ModuleName(mainModule.name)) + + val skalaBackend = SkalaBackend(koreDefinition, mainKoreModule) + + val frontendToKore = KoreToMini + + val koreToFrontend = MiniToKore + + override def execute(k: K, depth: Optional[Integer]): RewriterResult = { + val koreK = frontendToKore(k) + + val result: Pattern = skalaBackend.step(koreK) + + new RewriterResult(depth, koreToFrontend(result)) + } + + override def `match`(k: K, rule: Rule): K = ??? + + override def search(initialConfiguration: K, depth: Optional[Integer], bound: Optional[Integer], pattern: Rule, searchType: SearchType, resultsAsSubstitution: Boolean): K = ??? + + override def executeAndMatch(k: K, depth: Optional[Integer], rule: Rule): (RewriterResult, K) = ??? + + override def prove(rules: java.util.List[Rule]): java.util.List[K] = ??? +} + + From 9052701a8cc1c5d452639c160b23ffda133abaf9 Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Mon, 29 May 2017 20:09:55 -0500 Subject: [PATCH 10/34] changes to Basic.k + Imp test --- .../java/org/kframework/backend/Backends.java | 2 +- .../main/java/org/kframework/main/Main.java | 4 +- .../src/test/resources/basic/basic.k | 9 +++ skala-backend/src/test/resources/imp/imp.k | 61 ++++++++++++++ .../backend/skala/BasicOnSkalaTest.java | 75 ++++++++++++++++++ .../backend/skala/ImpOnSkalaTest.java | 79 +++++++++++++++++++ 6 files changed, 227 insertions(+), 3 deletions(-) create mode 100644 skala-backend/src/test/resources/basic/basic.k create mode 100644 skala-backend/src/test/resources/imp/imp.k create mode 100644 skala-backend/src/test/scala/org/kframework/backend/skala/BasicOnSkalaTest.java create mode 100644 skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java diff --git a/kernel/src/main/java/org/kframework/backend/Backends.java b/kernel/src/main/java/org/kframework/backend/Backends.java index cbdf4b0c34..37898baab1 100644 --- a/kernel/src/main/java/org/kframework/backend/Backends.java +++ b/kernel/src/main/java/org/kframework/backend/Backends.java @@ -8,7 +8,7 @@ public class Backends { public static final String DOC = "doc"; public static final String HTML = "html"; public static final String JAVA = "java"; - public static final String KALE = "kale"; + public static final String SKALA = "skala"; public static final String AUTOINCLUDE_JAVA = "autoinclude-java.k"; } diff --git a/shell/src/main/java/org/kframework/main/Main.java b/shell/src/main/java/org/kframework/main/Main.java index 17168f236f..fb0b00a3a6 100644 --- a/shell/src/main/java/org/kframework/main/Main.java +++ b/shell/src/main/java/org/kframework/main/Main.java @@ -123,7 +123,7 @@ public static int runApplication(String toolName, String[] args, File workingDir Backend koreBackend; if (kompileOptions.backend.equals(Backends.JAVA)) { koreBackend = new JavaBackend(kem, files, kompileOptions.global, kompileOptions); - } else if (kompileOptions.backend.equals(Backends.KALE)) { + } else if (kompileOptions.backend.equals(Backends.SKALA)) { koreBackend = new SkalaKompile(kompileOptions, kem); } else throw new AssertionError("Backend not hooked to the shell."); @@ -240,7 +240,7 @@ public static int runApplication(String toolName, String[] args, File workingDir intializeMiniKoreRewriter = new InitializeRewriter(fs, javaExecutionOptions.deterministicFunctions, kRunOptions.global, kem, kRunOptions.experimental.smt, hookProvider, kompileOptions.transition, kRunOptions, files, initializeDefinition); - } else if (kompileOptions.backend.equals(Backends.KALE)) { + } else if (kompileOptions.backend.equals(Backends.SKALA)) { initializeRewriter = null; intializeMiniKoreRewriter = (x -> new SkalaRewriter(x.getKey(), x.getRight())); } else { diff --git a/skala-backend/src/test/resources/basic/basic.k b/skala-backend/src/test/resources/basic/basic.k new file mode 100644 index 0000000000..50c8104ef4 --- /dev/null +++ b/skala-backend/src/test/resources/basic/basic.k @@ -0,0 +1,9 @@ +module BASIC-SYNTAX + syntax Exp ::= Int + | Exp "+" Exp +endmodule +module BASIC + imports BASIC-SYNTAX + configuration $PGM:Exp + rule A:Int + B:Int => A +Int B +endmodule \ No newline at end of file diff --git a/skala-backend/src/test/resources/imp/imp.k b/skala-backend/src/test/resources/imp/imp.k new file mode 100644 index 0000000000..cdcfcdcca5 --- /dev/null +++ b/skala-backend/src/test/resources/imp/imp.k @@ -0,0 +1,61 @@ +// Copyright (c) 2014-2016 K Team. All Rights Reserved. + +module IMP-SYNTAX + syntax AExp ::= Int | Id + | AExp "/" AExp [left, strict] + > AExp "+" AExp [left, strict] + | "(" AExp ")" [bracket] + syntax BExp ::= Bool + | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | "!" BExp [strict] + > BExp "&&" BExp [left, strict(1)] + | "(" BExp ")" [bracket] + syntax Block ::= "{" "}" + | "{" Stmt "}" + syntax Stmt ::= Block + | Id "=" AExp ";" [strict(2)] + | "if" "(" BExp ")" + Block "else" Block [strict(1)] + | "while" "(" BExp ")" Block + > Stmt Stmt [left] + syntax Pgm ::= "int" Ids ";" Stmt + syntax Ids ::= List{Id,","} +endmodule + + +module IMP + imports IMP-SYNTAX + syntax KResult ::= Int | Bool + + configuration + $PGM:Pgm + .Map + + +// AExp + rule X:Id => I ... ... X |-> I ... + rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0 + rule I1 + I2 => I1 +Int I2 +// BExp + rule I1 <= I2 => I1 <=Int I2 + rule ! T => notBool T + rule true && B => B + rule false && _ => false +// Block + rule {} => . [structural] + rule {S} => S [structural] +// Stmt + 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] +// Pgm + rule int (X,Xs => Xs);_ Rho:Map (.Map => X|->0) + requires notBool (X in keys(Rho)) + rule int .Ids; S => S [structural] + +// verification ids + syntax Id ::= "n" [token] + | "sum" [token] +endmodule diff --git a/skala-backend/src/test/scala/org/kframework/backend/skala/BasicOnSkalaTest.java b/skala-backend/src/test/scala/org/kframework/backend/skala/BasicOnSkalaTest.java new file mode 100644 index 0000000000..aca46009d2 --- /dev/null +++ b/skala-backend/src/test/scala/org/kframework/backend/skala/BasicOnSkalaTest.java @@ -0,0 +1,75 @@ +package org.kframework.backend.skala; + +import org.junit.Test; +import org.kframework.attributes.Source; +import org.kframework.backend.Backends; +import org.kframework.builtin.Sorts; +import org.kframework.definition.Module; +import org.kframework.frontend.K; +import org.kframework.frontend.KApply; +import org.kframework.frontend.KORE; +import org.kframework.frontend.KToken; +import org.kframework.kompile.CompiledDefinition; +import org.kframework.kompile.Kompile; +import org.kframework.kompile.KompileOptions; +import org.kframework.kore.Definition; +import org.kframework.main.GlobalOptions; +import org.kframework.minikore.converters.KoreToMini; +import org.kframework.unparser.AddBrackets; +import org.kframework.unparser.KOREToTreeNodes; +import org.kframework.utils.errorsystem.KExceptionManager; +import org.kframework.utils.file.FileUtil; + +import java.io.File; +import java.util.HashMap; +import java.util.Map; +import java.util.Optional; +import java.util.function.BiFunction; + +import static org.junit.Assert.assertEquals; + + +public class BasicOnSkalaTest { + @Test + public void basicOnSkalaTest1() { + String fileName = "src/test/resources/basic/basic.k"; + String program = "1 + 2"; + Source source = Source.apply("from test"); + String mainModuleName = "BASIC"; + + KExceptionManager kem = new KExceptionManager(new GlobalOptions()); + File definitionFile = new File(fileName); + KompileOptions kompileOptions = new KompileOptions(); + kompileOptions.backend = Backends.SKALA; + GlobalOptions globalOptions = new GlobalOptions(); + globalOptions.debug = true; + globalOptions.warnings = GlobalOptions.Warnings.ALL; + + Kompile kompile = new Kompile(kompileOptions, FileUtil.testFileUtil(), kem, false); + + CompiledDefinition compiledDef = kompile.run(definitionFile, mainModuleName, mainModuleName, new SkalaKompile(kompileOptions, kem).steps()); + + BiFunction programParser = compiledDef.getProgramParser(kem); + + K parsed = programParser.apply(program, source); + + Map map = new HashMap<>(); + + map.put(KORE.KToken("$PGM", Sorts.KConfigVar()), parsed); + + KApply input = KORE.KApply(compiledDef.topCellInitializer, map.entrySet().stream().map(e -> KORE.KApply(KORE.KLabel("_|->_"), e.getKey(), e.getValue())).reduce(KORE.KApply(KORE.KLabel(".Map")), (a, b) -> KORE.KApply(KORE.KLabel("_Map_"), a, b))); + + Definition definition = KoreToMini.apply(compiledDef.kompiledDefinition); + + SkalaRewriter skalaBackendRewriter = new SkalaRewriter(compiledDef.executionModule(), definition); + + K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); + + Module unparsingModule = compiledDef.getExtensionModule(compiledDef.languageParsingModule()); + + String actual = KOREToTreeNodes.toString(new AddBrackets(unparsingModule).addBrackets((org.kframework.parser.ProductionReference) KOREToTreeNodes.apply(KOREToTreeNodes.up(unparsingModule, kResult), unparsingModule))); + + assertEquals("Execution failed", " 3 ", actual); + + } +} diff --git a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java new file mode 100644 index 0000000000..d7b8fdc830 --- /dev/null +++ b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java @@ -0,0 +1,79 @@ +package org.kframework.backend.skala; + + +import org.junit.Ignore; +import org.junit.Test; +import org.kframework.attributes.Source; +import org.kframework.backend.Backends; +import org.kframework.builtin.Sorts; +import org.kframework.definition.Module; +import org.kframework.frontend.K; +import org.kframework.frontend.KApply; +import org.kframework.frontend.KORE; +import org.kframework.frontend.KToken; +import org.kframework.kompile.CompiledDefinition; +import org.kframework.kompile.Kompile; +import org.kframework.kompile.KompileOptions; +import org.kframework.kore.Definition; +import org.kframework.main.GlobalOptions; +import org.kframework.minikore.converters.KoreToMini; +import org.kframework.unparser.AddBrackets; +import org.kframework.unparser.KOREToTreeNodes; +import org.kframework.utils.errorsystem.KExceptionManager; +import org.kframework.utils.file.FileUtil; + +import java.io.File; +import java.util.HashMap; +import java.util.Map; +import java.util.Optional; +import java.util.function.BiFunction; + +import static org.junit.Assert.assertEquals; + +public class ImpOnSkalaTest { + + @Ignore + @Test + public void impOnSkalaTest1() { + String fileName = "src/test/resources/imp/imp.k"; + //Todo: Change to include program from resources folder + String program = "int n;" + + "n = 1;"; + Source source = Source.apply("from test"); + String mainModuleName = "IMP"; + + KExceptionManager kem = new KExceptionManager(new GlobalOptions()); + File definitionFile = new File(fileName); + KompileOptions kompileOptions = new KompileOptions(); + kompileOptions.backend = Backends.SKALA; + GlobalOptions globalOptions = new GlobalOptions(); + globalOptions.debug = true; + globalOptions.warnings = GlobalOptions.Warnings.ALL; + + Kompile kompile = new Kompile(kompileOptions, FileUtil.testFileUtil(), kem, false); + + CompiledDefinition compiledDef = kompile.run(definitionFile, mainModuleName, mainModuleName, new SkalaKompile(kompileOptions, kem).steps()); + + BiFunction programParser = compiledDef.getProgramParser(kem); + + K parsed = programParser.apply(program, source); + + Map map = new HashMap<>(); + + map.put(KORE.KToken("$PGM", Sorts.KConfigVar()), parsed); + + KApply input = KORE.KApply(compiledDef.topCellInitializer, map.entrySet().stream().map(e -> KORE.KApply(KORE.KLabel("_|->_"), e.getKey(), e.getValue())).reduce(KORE.KApply(KORE.KLabel(".Map")), (a, b) -> KORE.KApply(KORE.KLabel("_Map_"), a, b))); + + Definition definition = KoreToMini.apply(compiledDef.kompiledDefinition); + + SkalaRewriter skalaBackendRewriter = new SkalaRewriter(compiledDef.executionModule(), definition); + + K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); + + Module unparsingModule = compiledDef.getExtensionModule(compiledDef.languageParsingModule()); + + String actual = KOREToTreeNodes.toString(new AddBrackets(unparsingModule).addBrackets((org.kframework.parser.ProductionReference) KOREToTreeNodes.apply(KOREToTreeNodes.up(unparsingModule, kResult), unparsingModule))); + +// assertEquals("Execution failed", " 3 ", actual); + } +} From afc2113992331a18842ce7a1451991449402ed76 Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Tue, 30 May 2017 20:34:01 -0500 Subject: [PATCH 11/34] ignore test until issue with stack overflow is resolved --- .../scala/org/kframework/backend/skala/BasicOnSkalaTest.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/skala-backend/src/test/scala/org/kframework/backend/skala/BasicOnSkalaTest.java b/skala-backend/src/test/scala/org/kframework/backend/skala/BasicOnSkalaTest.java index aca46009d2..e27ddbfee3 100644 --- a/skala-backend/src/test/scala/org/kframework/backend/skala/BasicOnSkalaTest.java +++ b/skala-backend/src/test/scala/org/kframework/backend/skala/BasicOnSkalaTest.java @@ -1,5 +1,6 @@ package org.kframework.backend.skala; +import org.junit.Ignore; import org.junit.Test; import org.kframework.attributes.Source; import org.kframework.backend.Backends; @@ -30,6 +31,7 @@ public class BasicOnSkalaTest { + @Ignore @Test public void basicOnSkalaTest1() { String fileName = "src/test/resources/basic/basic.k"; From e197123736852f6f3a60ce4376d949da2749afcf Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Tue, 6 Jun 2017 18:11:07 -0500 Subject: [PATCH 12/34] make sum.imp pass with Skala Backend --- .../minikore/converters/MiniToKore.scala | 1 + .../backend/skala/SkalaRewriter.scala | 25 +++++++++++++++---- skala-backend/src/test/resources/imp/sum.imp | 8 ++++++ .../backend/skala/BasicOnSkalaTest.java | 7 +++--- .../backend/skala/ImpOnSkalaTest.java | 10 ++++---- 5 files changed, 37 insertions(+), 14 deletions(-) create mode 100644 skala-backend/src/test/resources/imp/sum.imp diff --git a/frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala b/frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala index 1295a1f614..328525ba55 100644 --- a/frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala +++ b/frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala @@ -133,6 +133,7 @@ object MiniToKore { 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) diff --git a/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaRewriter.scala b/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaRewriter.scala index c6fc76e8b2..855ea16d0c 100644 --- a/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaRewriter.scala +++ b/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaRewriter.scala @@ -4,10 +4,10 @@ import java.util.Optional import org.kframework.definition._ import org.kframework.frontend._ +import org.kframework.kale.builtin.MapImplementation import org.kframework.{RewriterResult, kore} import org.kframework.kore.Pattern import org.kframework.kore.extended.implicits._ -import org.kframework.kore.implementation.{DefaultBuilders => db} import org.kframework.minikore.converters.{KoreToMini, MiniToKore} import org.kframework.rewriter.SearchType @@ -15,6 +15,8 @@ import org.kframework.rewriter.SearchType class SkalaRewriter(mainModule: Module, koreDefinition: kore.Definition) extends org.kframework.rewriter.Rewriter { + import org.kframework.kore.implementation.{DefaultBuilders => db} + val mainKoreModule = koreDefinition.modulesMap(db.ModuleName(mainModule.name)) val skalaBackend = SkalaBackend(koreDefinition, mainKoreModule) @@ -23,12 +25,25 @@ class SkalaRewriter(mainModule: Module, koreDefinition: kore.Definition) extends val koreToFrontend = MiniToKore - override def execute(k: K, depth: Optional[Integer]): RewriterResult = { - val koreK = frontendToKore(k) - val result: Pattern = skalaBackend.step(koreK) + //Todo: Needed only temporarily until we have pretty printers over Kore. + private def filterForPrettyPrinting(p: Pattern): Pattern = p match { + case kore.Application(kore.Symbol(".K"), _) => db.Application(KoreToMini.iKSeqNil, Seq()) + case kore.Application(symbol , args) => db.Application(symbol, args.map(filterForPrettyPrinting)) + case p:MapImplementation => db.Application(db.Symbol(p.label.name), p.children.map(filterForPrettyPrinting).toSeq) + case p@_ => p + } - new RewriterResult(depth, koreToFrontend(result)) + override def execute(k: K, depth: Optional[Integer]): RewriterResult = { + val p: Pattern = frontendToKore(k) + var res = p + if(depth.isPresent()) { + res = skalaBackend.step(p, depth.get) + } else { + res = skalaBackend.execute(p) + } + + new RewriterResult(depth, koreToFrontend(filterForPrettyPrinting(res))) } override def `match`(k: K, rule: Rule): K = ??? diff --git a/skala-backend/src/test/resources/imp/sum.imp b/skala-backend/src/test/resources/imp/sum.imp new file mode 100644 index 0000000000..69d0df74b8 --- /dev/null +++ b/skala-backend/src/test/resources/imp/sum.imp @@ -0,0 +1,8 @@ +int n, sum; +n = 10; +sum = 0; +while (!(n <= 0)) { + sum = sum + n; + n = n + -1; +} + diff --git a/skala-backend/src/test/scala/org/kframework/backend/skala/BasicOnSkalaTest.java b/skala-backend/src/test/scala/org/kframework/backend/skala/BasicOnSkalaTest.java index e27ddbfee3..7ac24cf876 100644 --- a/skala-backend/src/test/scala/org/kframework/backend/skala/BasicOnSkalaTest.java +++ b/skala-backend/src/test/scala/org/kframework/backend/skala/BasicOnSkalaTest.java @@ -1,6 +1,5 @@ package org.kframework.backend.skala; -import org.junit.Ignore; import org.junit.Test; import org.kframework.attributes.Source; import org.kframework.backend.Backends; @@ -21,17 +20,17 @@ import org.kframework.utils.errorsystem.KExceptionManager; import org.kframework.utils.file.FileUtil; +import javax.swing.text.html.Option; import java.io.File; import java.util.HashMap; import java.util.Map; import java.util.Optional; import java.util.function.BiFunction; -import static org.junit.Assert.assertEquals; +import static org.junit.Assert.*; public class BasicOnSkalaTest { - @Ignore @Test public void basicOnSkalaTest1() { String fileName = "src/test/resources/basic/basic.k"; @@ -65,7 +64,7 @@ public void basicOnSkalaTest1() { SkalaRewriter skalaBackendRewriter = new SkalaRewriter(compiledDef.executionModule(), definition); - K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); + K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); Module unparsingModule = compiledDef.getExtensionModule(compiledDef.languageParsingModule()); diff --git a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java index d7b8fdc830..269b22bb89 100644 --- a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java +++ b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java @@ -22,6 +22,7 @@ import org.kframework.utils.errorsystem.KExceptionManager; import org.kframework.utils.file.FileUtil; +import javax.swing.text.html.Option; import java.io.File; import java.util.HashMap; import java.util.Map; @@ -32,13 +33,12 @@ public class ImpOnSkalaTest { - @Ignore @Test public void impOnSkalaTest1() { String fileName = "src/test/resources/imp/imp.k"; //Todo: Change to include program from resources folder - String program = "int n;" + - "n = 1;"; + String programFileName = "src/test/resources/imp/sum.imp"; + String program = FileUtil.load(new File(programFileName)); Source source = Source.apply("from test"); String mainModuleName = "IMP"; @@ -68,12 +68,12 @@ public void impOnSkalaTest1() { SkalaRewriter skalaBackendRewriter = new SkalaRewriter(compiledDef.executionModule(), definition); - K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); + K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); Module unparsingModule = compiledDef.getExtensionModule(compiledDef.languageParsingModule()); String actual = KOREToTreeNodes.toString(new AddBrackets(unparsingModule).addBrackets((org.kframework.parser.ProductionReference) KOREToTreeNodes.apply(KOREToTreeNodes.up(unparsingModule, kResult), unparsingModule))); -// assertEquals("Execution failed", " 3 ", actual); + assertEquals("Execution with Skala Backend Failed", " . 'sum |-> 55 'n |-> 0 ", actual); } } From e66d9e353b2385b5d214529572f0faab12a232c0 Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Wed, 7 Jun 2017 11:27:34 -0500 Subject: [PATCH 13/34] reorganize tests + add test for collatz conjecture --- .../tutorial/1_k/2_imp/lesson_1/tests/sum.imp | 2 +- .../src/test/resources/imp/collatz.imp | 14 ++++ .../src/test/resources/imp/initialization.imp | 3 + .../backend/skala/ImpOnSkalaTest.java | 74 +++++++++++++------ 4 files changed, 68 insertions(+), 25 deletions(-) create mode 100644 skala-backend/src/test/resources/imp/collatz.imp create mode 100644 skala-backend/src/test/resources/imp/initialization.imp diff --git a/k-distribution/tutorial/1_k/2_imp/lesson_1/tests/sum.imp b/k-distribution/tutorial/1_k/2_imp/lesson_1/tests/sum.imp index 552576a250..fefbfdc3b9 100644 --- a/k-distribution/tutorial/1_k/2_imp/lesson_1/tests/sum.imp +++ b/k-distribution/tutorial/1_k/2_imp/lesson_1/tests/sum.imp @@ -2,7 +2,7 @@ // the sum of numbers from 1 to n. int n, sum; -n = 10; +n = 50; sum = 0; while (!(n <= 0)) { sum = sum + n; diff --git a/skala-backend/src/test/resources/imp/collatz.imp b/skala-backend/src/test/resources/imp/collatz.imp new file mode 100644 index 0000000000..860bde549d --- /dev/null +++ b/skala-backend/src/test/resources/imp/collatz.imp @@ -0,0 +1,14 @@ +int m, n, q, r, s; +m = 10; +while (!(m<=2)) { + n = m; + m = m + -1; + while (!(n<=1)) { + s = s+1; + q = n/2; + r = q+q+1; + if (r<=n) { + n = n+n+n+1; + } else {n=q;} + } +} \ No newline at end of file diff --git a/skala-backend/src/test/resources/imp/initialization.imp b/skala-backend/src/test/resources/imp/initialization.imp new file mode 100644 index 0000000000..8c36cf5e35 --- /dev/null +++ b/skala-backend/src/test/resources/imp/initialization.imp @@ -0,0 +1,3 @@ +int a, b; +a = 1; +b = 2; diff --git a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java index 269b22bb89..2cc100a081 100644 --- a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java +++ b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java @@ -1,6 +1,9 @@ package org.kframework.backend.skala; +import org.junit.AfterClass; +import org.junit.Before; +import org.junit.BeforeClass; import org.junit.Ignore; import org.junit.Test; import org.kframework.attributes.Source; @@ -19,11 +22,13 @@ import org.kframework.minikore.converters.KoreToMini; import org.kframework.unparser.AddBrackets; import org.kframework.unparser.KOREToTreeNodes; +import org.kframework.utils.errorsystem.KException; import org.kframework.utils.errorsystem.KExceptionManager; import org.kframework.utils.file.FileUtil; import javax.swing.text.html.Option; import java.io.File; +import java.nio.file.Path; import java.util.HashMap; import java.util.Map; import java.util.Optional; @@ -33,47 +38,68 @@ public class ImpOnSkalaTest { - @Test - public void impOnSkalaTest1() { - String fileName = "src/test/resources/imp/imp.k"; - //Todo: Change to include program from resources folder - String programFileName = "src/test/resources/imp/sum.imp"; - String program = FileUtil.load(new File(programFileName)); - Source source = Source.apply("from test"); + private static CompiledDefinition compiledDef; + private static String resources; + private static KExceptionManager kem; + private static SkalaRewriter skalaBackendRewriter; + private static Module unparsingModule; + private static BiFunction programParser; + + @BeforeClass + public static void kompileSetup() { + resources = "src/test/resources/imp/"; + File definitionFile = new File(resources + "imp.k"); String mainModuleName = "IMP"; - KExceptionManager kem = new KExceptionManager(new GlobalOptions()); - File definitionFile = new File(fileName); KompileOptions kompileOptions = new KompileOptions(); kompileOptions.backend = Backends.SKALA; GlobalOptions globalOptions = new GlobalOptions(); globalOptions.debug = true; globalOptions.warnings = GlobalOptions.Warnings.ALL; - + kem = new KExceptionManager(globalOptions); Kompile kompile = new Kompile(kompileOptions, FileUtil.testFileUtil(), kem, false); + compiledDef = kompile.run(definitionFile, mainModuleName, mainModuleName, new SkalaKompile(kompileOptions, kem).steps()); + Definition definition = KoreToMini.apply(compiledDef.kompiledDefinition); + skalaBackendRewriter = new SkalaRewriter(compiledDef.executionModule(), definition); + unparsingModule = compiledDef.getExtensionModule(compiledDef.languageParsingModule()); + programParser = compiledDef.getProgramParser(kem); + } - CompiledDefinition compiledDef = kompile.run(definitionFile, mainModuleName, mainModuleName, new SkalaKompile(kompileOptions, kem).steps()); - - BiFunction programParser = compiledDef.getProgramParser(kem); - + private K getParsedProgram(String pgmName) { + String program = FileUtil.load(new File(resources + pgmName)); + Source source = Source.apply("from test"); K parsed = programParser.apply(program, source); - Map map = new HashMap<>(); - map.put(KORE.KToken("$PGM", Sorts.KConfigVar()), parsed); - KApply input = KORE.KApply(compiledDef.topCellInitializer, map.entrySet().stream().map(e -> KORE.KApply(KORE.KLabel("_|->_"), e.getKey(), e.getValue())).reduce(KORE.KApply(KORE.KLabel(".Map")), (a, b) -> KORE.KApply(KORE.KLabel("_Map_"), a, b))); + return input; + } - Definition definition = KoreToMini.apply(compiledDef.kompiledDefinition); - - SkalaRewriter skalaBackendRewriter = new SkalaRewriter(compiledDef.executionModule(), definition); + private String unparseResult(K result) { + return KOREToTreeNodes.toString(new AddBrackets(unparsingModule).addBrackets((org.kframework.parser.ProductionReference) KOREToTreeNodes.apply(KOREToTreeNodes.up(unparsingModule, result), unparsingModule))); + } + @Test + public void basicInitializationTest() { + K input = getParsedProgram("initialization.imp"); K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); + String actual = unparseResult(kResult); + assertEquals("Execution with Skala Backend Failed", " . 'a |-> 1 'b |-> 2 ", actual); + } - Module unparsingModule = compiledDef.getExtensionModule(compiledDef.languageParsingModule()); - - String actual = KOREToTreeNodes.toString(new AddBrackets(unparsingModule).addBrackets((org.kframework.parser.ProductionReference) KOREToTreeNodes.apply(KOREToTreeNodes.up(unparsingModule, kResult), unparsingModule))); - + @Test + public void sumTest() { + K input = getParsedProgram("sum.imp"); + K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); + String actual = unparseResult(kResult); assertEquals("Execution with Skala Backend Failed", " . 'sum |-> 55 'n |-> 0 ", actual); } + + @Test + public void collatzTest() { + K input = getParsedProgram("collatz.imp"); + K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); + String actual = unparseResult(kResult); + assertEquals("Execution with Skala Backend Failed", " . 's |-> 66 'r |-> 3 'q |-> 1 'n |-> 1 'm |-> 2 ", actual); + } } From 171fe4c87c84e358e2251f2e5876da567d66d530 Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Wed, 7 Jun 2017 11:37:54 -0500 Subject: [PATCH 14/34] added test for primes, the remaining imp program --- .../src/test/resources/imp/primes.imp | 20 +++++++++++++++++++ .../backend/skala/ImpOnSkalaTest.java | 8 ++++++++ 2 files changed, 28 insertions(+) create mode 100644 skala-backend/src/test/resources/imp/primes.imp diff --git a/skala-backend/src/test/resources/imp/primes.imp b/skala-backend/src/test/resources/imp/primes.imp new file mode 100644 index 0000000000..e206f8d8ae --- /dev/null +++ b/skala-backend/src/test/resources/imp/primes.imp @@ -0,0 +1,20 @@ +int i, m, n, q, r, s, t, x, y, z; +m = 10; n = 2; +while (n <= m) { + i = 2; q = n/i; t = 1; + while (i<=q && 1<=t) { + x = i; + y = q; + z = 0; + while (!(x <= 0)) { + q = x/2; + r = q+q+1; + if (r <= x) { z = z+y; } else {} + x = q; + y = y+y; + } + if (n <= z) { t = 0; } else { i = i+1; q = n/i; } + } + if (1 <= t) { s = s+1; } else {} + n = n+1; +} \ No newline at end of file diff --git a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java index 2cc100a081..be24a36053 100644 --- a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java +++ b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java @@ -102,4 +102,12 @@ public void collatzTest() { String actual = unparseResult(kResult); assertEquals("Execution with Skala Backend Failed", " . 's |-> 66 'r |-> 3 'q |-> 1 'n |-> 1 'm |-> 2 ", actual); } + + @Test + public void primesTest() { + K input = getParsedProgram("primes.imp"); + K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); + String actual = unparseResult(kResult); + assertEquals("Execution with Skala Backend Failed", " . 's |-> 4 'r |-> 1 'y |-> 20 'x |-> 0 'z |-> 10 'i |-> 2 'q |-> 0 't |-> 0 'n |-> 11 'm |-> 10 ", actual); + } } From 793183c5aadaf33501652404dfaa463f88063f41 Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Wed, 7 Jun 2017 11:52:50 -0500 Subject: [PATCH 15/34] small fix to test file --- .../test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java | 1 - 1 file changed, 1 deletion(-) diff --git a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java index be24a36053..b1c08b37d6 100644 --- a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java +++ b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java @@ -50,7 +50,6 @@ public static void kompileSetup() { resources = "src/test/resources/imp/"; File definitionFile = new File(resources + "imp.k"); String mainModuleName = "IMP"; - KExceptionManager kem = new KExceptionManager(new GlobalOptions()); KompileOptions kompileOptions = new KompileOptions(); kompileOptions.backend = Backends.SKALA; GlobalOptions globalOptions = new GlobalOptions(); From b72684e24e88bc05a4d282cbe9dc3254b75c19f6 Mon Sep 17 00:00:00 2001 From: Cosmin Radoi Date: Fri, 30 Jun 2017 22:04:46 -0500 Subject: [PATCH 16/34] speeeeedy well, at least compared to before :-) --- .../src/test/resources/imp/sum100.imp | 8 ++++ .../src/test/resources/imp/sum1000.imp | 8 ++++ .../backend/skala/ImpOnSkalaTest.java | 42 +++++++++++++++---- 3 files changed, 50 insertions(+), 8 deletions(-) create mode 100644 skala-backend/src/test/resources/imp/sum100.imp create mode 100644 skala-backend/src/test/resources/imp/sum1000.imp diff --git a/skala-backend/src/test/resources/imp/sum100.imp b/skala-backend/src/test/resources/imp/sum100.imp new file mode 100644 index 0000000000..b185eb4564 --- /dev/null +++ b/skala-backend/src/test/resources/imp/sum100.imp @@ -0,0 +1,8 @@ +int n, sum; +n = 100; +sum = 0; +while (!(n <= 0)) { + sum = sum + n; + n = n + -1; +} + diff --git a/skala-backend/src/test/resources/imp/sum1000.imp b/skala-backend/src/test/resources/imp/sum1000.imp new file mode 100644 index 0000000000..50b73fddcb --- /dev/null +++ b/skala-backend/src/test/resources/imp/sum1000.imp @@ -0,0 +1,8 @@ +int n, sum; +n = 1000; +sum = 0; +while (!(n <= 0)) { + sum = sum + n; + n = n + -1; +} + diff --git a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java index b1c08b37d6..43db121cf7 100644 --- a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java +++ b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java @@ -45,8 +45,16 @@ public class ImpOnSkalaTest { private static Module unparsingModule; private static BiFunction programParser; + static long timeBefore = System.nanoTime(); + + public static void logTime(String what) { + System.out.println(what + ": " + ((System.nanoTime() - timeBefore) / 1000000) + "ms"); + timeBefore = System.nanoTime(); + } + @BeforeClass public static void kompileSetup() { + logTime("start"); resources = "src/test/resources/imp/"; File definitionFile = new File(resources + "imp.k"); String mainModuleName = "IMP"; @@ -58,13 +66,22 @@ public static void kompileSetup() { kem = new KExceptionManager(globalOptions); Kompile kompile = new Kompile(kompileOptions, FileUtil.testFileUtil(), kem, false); compiledDef = kompile.run(definitionFile, mainModuleName, mainModuleName, new SkalaKompile(kompileOptions, kem).steps()); + logTime("kompile"); Definition definition = KoreToMini.apply(compiledDef.kompiledDefinition); + logTime("frontend kore to kore"); skalaBackendRewriter = new SkalaRewriter(compiledDef.executionModule(), definition); + logTime("make Scala Rewriter"); unparsingModule = compiledDef.getExtensionModule(compiledDef.languageParsingModule()); programParser = compiledDef.getProgramParser(kem); + logTime("parse-unparse stuff"); + + // warmup + K input = getParsedProgram("initialization.imp"); + K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); + String actual = unparseResult(kResult); } - private K getParsedProgram(String pgmName) { + private static K getParsedProgram(String pgmName) { String program = FileUtil.load(new File(resources + pgmName)); Source source = Source.apply("from test"); K parsed = programParser.apply(program, source); @@ -74,24 +91,33 @@ private K getParsedProgram(String pgmName) { return input; } - private String unparseResult(K result) { + private static String unparseResult(K result) { return KOREToTreeNodes.toString(new AddBrackets(unparsingModule).addBrackets((org.kframework.parser.ProductionReference) KOREToTreeNodes.apply(KOREToTreeNodes.up(unparsingModule, result), unparsingModule))); } + @Test - public void basicInitializationTest() { - K input = getParsedProgram("initialization.imp"); + public void sumTest() { + K input = getParsedProgram("sum.imp"); K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); String actual = unparseResult(kResult); - assertEquals("Execution with Skala Backend Failed", " . 'a |-> 1 'b |-> 2 ", actual); + assertEquals("Execution with Skala Backend Failed", " . 'sum |-> 55 'n |-> 0 ", actual); } @Test - public void sumTest() { - K input = getParsedProgram("sum.imp"); + public void sum100Test() { + K input = getParsedProgram("sum100.imp"); K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); String actual = unparseResult(kResult); - assertEquals("Execution with Skala Backend Failed", " . 'sum |-> 55 'n |-> 0 ", actual); + assertEquals("Execution with Skala Backend Failed", " . 'sum |-> 5050 'n |-> 0 ", actual); + } + + @Test + public void sum1000Test() { + K input = getParsedProgram("sum1000.imp"); + K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); + String actual = unparseResult(kResult); + assertEquals("Execution with Skala Backend Failed", " . 'sum |-> 500500 'n |-> 0 ", actual); } @Test From 6bd78ccbfc6c2ab0170cf67493f0256d59a830f1 Mon Sep 17 00:00:00 2001 From: Cosmin Radoi Date: Sat, 1 Jul 2017 12:08:41 -0500 Subject: [PATCH 17/34] major refactoring --- API/src/main/java/org/kframework/Kapi.java | 4 +-- .../minikore/converters/MiniToKore.scala | 34 ++++++++++++------- .../backend/java/symbolic/JavaBackend.java | 15 ++------ .../java/symbolic/ProofExecutionMode.java | 2 +- .../java/org/kframework/kompile/Kompile.java | 15 +++++++- .../backend/skala/SkalaKompile.scala | 9 +++-- 6 files changed, 44 insertions(+), 35 deletions(-) diff --git a/API/src/main/java/org/kframework/Kapi.java b/API/src/main/java/org/kframework/Kapi.java index d023f2a0bf..c305079599 100644 --- a/API/src/main/java/org/kframework/Kapi.java +++ b/API/src/main/java/org/kframework/Kapi.java @@ -335,7 +335,7 @@ public static Info getInfo(CompiledDefinition compiledDef, String proofFile, Str List 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 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)) diff --git a/frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala b/frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala index 328525ba55..ff99e875fa 100644 --- a/frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala +++ b/frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala @@ -19,18 +19,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 +44,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 +54,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 +87,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 +101,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,7 +116,8 @@ 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) } @@ -119,7 +125,7 @@ object MiniToKore { 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,17 +135,19 @@ object MiniToKore { case Application(`iKSeqNil`, Seq()) => ADT.KSequence(List(), att) - case Application(`iAtt`, Seq(p1,p2)) => + case Application(`iAtt`, Seq(p1, p2)) => val a2 = apply(Seq(p2)) apply(att ++ a2)(p1) + case Application(Symbol("_Map_.lookup"), args) => KORE.KApply(KORE.KLabel("Map:lookup"), args.map(apply), att) 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] = { diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaBackend.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaBackend.java index 7fce18c7d6..6ec8184242 100644 --- a/java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaBackend.java +++ b/java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaBackend.java @@ -109,7 +109,7 @@ public Function 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 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. diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/ProofExecutionMode.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/ProofExecutionMode.java index c0c969b5e5..7f538e3fbe 100644 --- a/java-backend/src/main/java/org/kframework/backend/java/symbolic/ProofExecutionMode.java +++ b/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)) diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java index ba7d513aa0..915bbd1044 100644 --- a/kernel/src/main/java/org/kframework/kompile/Kompile.java +++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java @@ -20,7 +20,9 @@ import org.kframework.frontend.KApply; import org.kframework.frontend.KORE; import org.kframework.frontend.KSequence; +import org.kframework.frontend.KVariable; import org.kframework.frontend.Sort; +import org.kframework.frontend.SortedADT; import org.kframework.frontend.TransformK; import org.kframework.frontend.compile.AddImplicitComputationCell; import org.kframework.frontend.compile.ConcretizeCells; @@ -247,7 +249,7 @@ public K apply(KApply kk) { }.apply(k), "Module-qualify sort predicates"); /** - * In the Java backend, {@link KSequence}s are treated like {@link KApply}s, so tranform them. + * In all our current backends, {@link KSequence}s are treated like {@link KApply}s, so tranform them. */ public static K convertKSeqToKApply(K ruleBody) { return new TransformK() { @@ -256,4 +258,15 @@ public K apply(KSequence kseq) { } }.apply(ruleBody); } + + /** + * 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); + } } diff --git a/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaKompile.scala b/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaKompile.scala index 9420c79a13..d677d0258b 100644 --- a/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaKompile.scala +++ b/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaKompile.scala @@ -2,8 +2,9 @@ package org.kframework.backend.skala import java.util.function.Function +import org.kframework.attributes.Att import org.kframework.compile.{AddBottomSortForListsWithIdenticalLabels, NormalizeKSeq} -import org.kframework.definition.{Definition, DefinitionTransformer} +import org.kframework.definition.{Definition, DefinitionTransformer, Rule, Sentence} import org.kframework.kompile.{CompiledDefinition, Kompile, KompileOptions} import org.kframework.frontend.KORE import org.kframework.frontend.compile._ @@ -20,13 +21,11 @@ class SkalaKompile(kompileOptions: KompileOptions, kem: KExceptionManager) exten (d => Kompile.defaultSteps(kompileOptions, kem)(d)) .andThen(DefinitionTransformer.fromRuleBodyTranformer(RewriteToTop.rewriteToTop, "rewrite to top")) - .andThen(DefinitionTransformer.fromSentenceTransformer(new NormalizeAssoc(KORE), "normalize assoc")) .andThen(DefinitionTransformer.fromHybrid(AddBottomSortForListsWithIdenticalLabels, "AddBottomSortForListsWithIdenticalLabels")) .andThen(Kompile.moduleQualifySortPredicates) +// .andThen(DefinitionTransformer.fromRuleBodyTranformer(Kompile.ADTKVariableToSortedVariable, "ADT.KVariable to SortedVariable")) // .andThen(new ExpandMacrosDefinitionTransformer(kem, files, globalOptions, kompileOptions)) - .andThen(DefinitionTransformer.fromSentenceTransformer(new NormalizeAssoc(KORE), "normalize assoc")) - // .andThen(DefinitionTransformer.fromRuleBodyTranformer(ADTKVariableToSortedVariable, "ADT.KVariable to SortedVariable")) .andThen(DefinitionTransformer.fromRuleBodyTranformer(Kompile.convertKSeqToKApply, "kseq to kapply")) - .andThen(DefinitionTransformer.fromRuleBodyTranformer(NormalizeKSeq, "normalize kseq")) + // .andThen(DefinitionTransformer.fromRuleBodyTranformer(NormalizeKSeq, "normalize kseq")) } } From cc3f0c532c31a07f0f7bce7df0ace02e2092e400 Mon Sep 17 00:00:00 2001 From: Cosmin Radoi Date: Sat, 1 Jul 2017 16:52:16 -0500 Subject: [PATCH 18/34] imp with local rewriting working --- k-distribution/include/builtin/domains.k | 2 +- .../org/kframework/backend/skala/SkalaKompile.scala | 5 +++-- .../org/kframework/backend/skala/ImpOnSkalaTest.java | 10 +++++----- 3 files changed, 9 insertions(+), 8 deletions(-) diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index 11b28ad6c7..2dc924b8ab 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -40,7 +40,7 @@ module MAP syntax Map ::= "(" Map ")" [bracket] /*@ Construct a singleton Map (a Map with only one key/value pair). The key is on the left and the value is on the right */ - syntax Map ::= K "|->" K [function, hook(MAP.element), latex({#1}\mapsto{#2})] + syntax Map ::= K "|->" K [hook(MAP.element), latex({#1}\mapsto{#2})] syntax priorities _|->_ > _Map_ .Map syntax non-assoc _|->_ diff --git a/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaKompile.scala b/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaKompile.scala index d677d0258b..13505bec8c 100644 --- a/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaKompile.scala +++ b/skala-backend/src/main/scala/org/kframework/backend/skala/SkalaKompile.scala @@ -8,6 +8,7 @@ import org.kframework.definition.{Definition, DefinitionTransformer, Rule, Sente import org.kframework.kompile.{CompiledDefinition, Kompile, KompileOptions} import org.kframework.frontend.KORE import org.kframework.frontend.compile._ +import org.kframework.kore.Rewrite import org.kframework.utils.errorsystem.KExceptionManager class SkalaKompile(kompileOptions: KompileOptions, kem: KExceptionManager) extends Backend { @@ -20,10 +21,10 @@ class SkalaKompile(kompileOptions: KompileOptions, kem: KExceptionManager) exten def defaultSteps(): Definition => Definition = { (d => Kompile.defaultSteps(kompileOptions, kem)(d)) - .andThen(DefinitionTransformer.fromRuleBodyTranformer(RewriteToTop.rewriteToTop, "rewrite to top")) +// .andThen(DefinitionTransformer.fromRuleBodyTranformer(RewriteToTop.rewriteToTop, "rewrite to top")) .andThen(DefinitionTransformer.fromHybrid(AddBottomSortForListsWithIdenticalLabels, "AddBottomSortForListsWithIdenticalLabels")) .andThen(Kompile.moduleQualifySortPredicates) -// .andThen(DefinitionTransformer.fromRuleBodyTranformer(Kompile.ADTKVariableToSortedVariable, "ADT.KVariable to SortedVariable")) + .andThen(DefinitionTransformer.fromRuleBodyTranformer(Kompile.ADTKVariableToSortedVariable, "ADT.KVariable to SortedVariable")) // .andThen(new ExpandMacrosDefinitionTransformer(kem, files, globalOptions, kompileOptions)) .andThen(DefinitionTransformer.fromRuleBodyTranformer(Kompile.convertKSeqToKApply, "kseq to kapply")) // .andThen(DefinitionTransformer.fromRuleBodyTranformer(NormalizeKSeq, "normalize kseq")) diff --git a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java index 43db121cf7..32fb21b933 100644 --- a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java +++ b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java @@ -101,7 +101,7 @@ public void sumTest() { K input = getParsedProgram("sum.imp"); K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); String actual = unparseResult(kResult); - assertEquals("Execution with Skala Backend Failed", " . 'sum |-> 55 'n |-> 0 ", actual); + assertEquals("Execution with Skala Backend Failed", " . 'n |-> 0 'sum |-> 55 ", actual); } @Test @@ -109,7 +109,7 @@ public void sum100Test() { K input = getParsedProgram("sum100.imp"); K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); String actual = unparseResult(kResult); - assertEquals("Execution with Skala Backend Failed", " . 'sum |-> 5050 'n |-> 0 ", actual); + assertEquals("Execution with Skala Backend Failed", " . 'n |-> 0 'sum |-> 5050 ", actual); } @Test @@ -117,7 +117,7 @@ public void sum1000Test() { K input = getParsedProgram("sum1000.imp"); K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); String actual = unparseResult(kResult); - assertEquals("Execution with Skala Backend Failed", " . 'sum |-> 500500 'n |-> 0 ", actual); + assertEquals("Execution with Skala Backend Failed", " . 'n |-> 0 'sum |-> 500500 ", actual); } @Test @@ -125,7 +125,7 @@ public void collatzTest() { K input = getParsedProgram("collatz.imp"); K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); String actual = unparseResult(kResult); - assertEquals("Execution with Skala Backend Failed", " . 's |-> 66 'r |-> 3 'q |-> 1 'n |-> 1 'm |-> 2 ", actual); + assertEquals("Execution with Skala Backend Failed", " . 'n |-> 1 'r |-> 3 'q |-> 1 's |-> 66 'm |-> 2 ", actual); } @Test @@ -133,6 +133,6 @@ public void primesTest() { K input = getParsedProgram("primes.imp"); K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); String actual = unparseResult(kResult); - assertEquals("Execution with Skala Backend Failed", " . 's |-> 4 'r |-> 1 'y |-> 20 'x |-> 0 'z |-> 10 'i |-> 2 'q |-> 0 't |-> 0 'n |-> 11 'm |-> 10 ", actual); + assertEquals("Execution with Skala Backend Failed", " . 'n |-> 11 't |-> 0 'y |-> 20 'x |-> 0 'z |-> 10 'r |-> 1 'q |-> 0 'i |-> 2 's |-> 4 'm |-> 10 ", actual); } } From f6ef6d457d06bf97b82699568db19e0448dee034 Mon Sep 17 00:00:00 2001 From: Cosmin Radoi Date: Sun, 2 Jul 2017 10:16:14 -0500 Subject: [PATCH 19/34] local-only sort checks -- sum to 1000 in 22s --- kernel/src/main/java/org/kframework/kompile/Kompile.java | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java index 915bbd1044..d1df43bbeb 100644 --- a/kernel/src/main/java/org/kframework/kompile/Kompile.java +++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java @@ -150,7 +150,10 @@ public static Function defaultSteps(KompileOptions kompi d = new ResolveAnonVar().apply(d); d = new ConvertContextsToHeatCoolRules(kompileOptions).resolve(d); d = new ResolveHeatCoolAttribute(new HashSet<>(kompileOptions.transition)).apply(d); - d = new ResolveSemanticCasts(kompileOptions.backend.equals(Backends.JAVA)).apply(d); + d = new ResolveSemanticCasts( + kompileOptions.backend.equals(Backends.JAVA) + || kompileOptions.backend.equals(Backends.SKALA) + ).apply(d); d = DefinitionTransformer.fromWithInputDefinitionTransformerClass(GenerateSortPredicateSyntax.class).apply(d); d = resolveFreshConstants(d); d = AddImplicitComputationCell.transformDefinition(d); @@ -213,7 +216,7 @@ public static Definition resolveFreshConstants(Definition input) { public Rule compileRule(CompiledDefinition compiledDef, Rule parsedRule) { return (Rule) asScalaFunc((Sentence s) -> new ResolveAnonVar().process(s)) - .andThen((Sentence s) -> new ResolveSemanticCasts(kompileOptions.backend.equals(Backends.JAVA)).process(s)) + .andThen((Sentence s) -> new ResolveSemanticCasts(kompileOptions.backend.equals(Backends.JAVA)).process(s)) .andThen(s -> concretizeSentence(s, compiledDef.kompiledDefinition)) .apply(parsedRule); } From be9534f382eb603db25249622fd0910691eb82ef Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Tue, 11 Jul 2017 11:57:40 -0500 Subject: [PATCH 20/34] Add Java file that runs sample programs for Plutus Core --- .../backend/skala/PlutusOnSkalaTest.java | 91 +++++++++++++++++++ 1 file changed, 91 insertions(+) create mode 100644 skala-backend/src/test/scala/org/kframework/backend/skala/PlutusOnSkalaTest.java diff --git a/skala-backend/src/test/scala/org/kframework/backend/skala/PlutusOnSkalaTest.java b/skala-backend/src/test/scala/org/kframework/backend/skala/PlutusOnSkalaTest.java new file mode 100644 index 0000000000..20e9ed9e2d --- /dev/null +++ b/skala-backend/src/test/scala/org/kframework/backend/skala/PlutusOnSkalaTest.java @@ -0,0 +1,91 @@ +package org.kframework.backend.skala; + + +import org.junit.BeforeClass; +import org.junit.Test; +import org.kframework.attributes.Source; +import org.kframework.backend.Backends; +import org.kframework.builtin.Sorts; +import org.kframework.definition.Module; +import org.kframework.frontend.K; +import org.kframework.frontend.KApply; +import org.kframework.frontend.KORE; +import org.kframework.frontend.KToken; +import org.kframework.kompile.CompiledDefinition; +import org.kframework.kompile.Kompile; +import org.kframework.kompile.KompileOptions; +import org.kframework.kore.Definition; +import org.kframework.main.GlobalOptions; +import org.kframework.minikore.converters.KoreToMini; +import org.kframework.unparser.AddBrackets; +import org.kframework.unparser.KOREToTreeNodes; +import org.kframework.utils.errorsystem.KExceptionManager; +import org.kframework.utils.file.FileUtil; + +import java.io.File; +import java.util.HashMap; +import java.util.Map; +import java.util.Optional; +import java.util.function.BiFunction; + +import static org.junit.Assert.*; + +public class PlutusOnSkalaTest { + + private static CompiledDefinition compiledDef; + private static String resources; + private static KExceptionManager kem; + private static SkalaRewriter skalaBackendRewriter; + private static Module unparsingModule; + private static BiFunction programParser; + + static long timeBefore = System.nanoTime(); + + public static void logTime(String what) { + System.out.println(what + ": " + ((System.nanoTime() - timeBefore) / 1000000) + "ms"); + timeBefore = System.nanoTime(); + } + + @BeforeClass + public static void kompileSetup() { + logTime("start"); + resources = "src/test/resources/plutus/"; + File definitionFile = new File(resources + "plutus-core.k"); + String mainModuleName = "PLUTUS-CORE"; + KompileOptions kompileOptions = new KompileOptions(); + kompileOptions.backend = Backends.SKALA; + GlobalOptions globalOptions = new GlobalOptions(); + globalOptions.debug = true; + globalOptions.warnings = GlobalOptions.Warnings.ALL; + kem = new KExceptionManager(globalOptions); + Kompile kompile = new Kompile(kompileOptions, FileUtil.testFileUtil(), kem, false); + compiledDef = kompile.run(definitionFile, mainModuleName, mainModuleName, new SkalaKompile(kompileOptions, kem).steps()); + logTime("kompile"); + Definition definition = KoreToMini.apply(compiledDef.kompiledDefinition); + logTime("frontend kore to kore"); + skalaBackendRewriter = new SkalaRewriter(compiledDef.executionModule(), definition); + logTime("make Scala Rewriter"); + unparsingModule = compiledDef.getExtensionModule(compiledDef.languageParsingModule()); + programParser = compiledDef.getProgramParser(kem); + logTime("parse-unparse stuff"); + + // warmup + K input = getParsedProgram("empty.plcore"); + K kResult = skalaBackendRewriter.execute(input, Optional.empty()).k(); + String actual = unparseResult(kResult); + } + + private static K getParsedProgram(String pgmName) { + String program = FileUtil.load(new File(resources + pgmName)); + Source source = Source.apply("from test"); + K parsed = programParser.apply(program, source); + Map map = new HashMap<>(); + map.put(KORE.KToken("$PGM", Sorts.KConfigVar()), parsed); + KApply input = KORE.KApply(compiledDef.topCellInitializer, map.entrySet().stream().map(e -> KORE.KApply(KORE.KLabel("_|->_"), KORE.KList(e.getKey(), e.getValue()))).reduce(KORE.KApply(KORE.KLabel(".Map")), (a, b) -> KORE.KApply(KORE.KLabel("_Map_"), a, b))); + return input; + } + + private static String unparseResult(K result) { + return KOREToTreeNodes.toString(new AddBrackets(unparsingModule).addBrackets((org.kframework.parser.ProductionReference) KOREToTreeNodes.apply(KOREToTreeNodes.up(unparsingModule, result), unparsingModule))); + } +} From 6a1b835f89f8afa3797f686b387a081233c1b9cf Mon Sep 17 00:00:00 2001 From: Cosmin Radoi Date: Tue, 11 Jul 2017 13:14:17 -0500 Subject: [PATCH 21/34] fix for intellij bug thingy --- .../scala/org/kframework/backend/skala/ImpOnSkalaTest.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java index 32fb21b933..c35f7e36a5 100644 --- a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java +++ b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java @@ -1,6 +1,7 @@ package org.kframework.backend.skala; +import com.sun.tools.javac.util.List; import org.junit.AfterClass; import org.junit.Before; import org.junit.BeforeClass; @@ -87,7 +88,7 @@ private static K getParsedProgram(String pgmName) { K parsed = programParser.apply(program, source); Map map = new HashMap<>(); map.put(KORE.KToken("$PGM", Sorts.KConfigVar()), parsed); - KApply input = KORE.KApply(compiledDef.topCellInitializer, map.entrySet().stream().map(e -> KORE.KApply(KORE.KLabel("_|->_"), e.getKey(), e.getValue())).reduce(KORE.KApply(KORE.KLabel(".Map")), (a, b) -> KORE.KApply(KORE.KLabel("_Map_"), a, b))); + KApply input = KORE.KApply(compiledDef.topCellInitializer, map.entrySet().stream().map(e -> KORE.KApply(KORE.KLabel("_|->_"), KORE.KList(List.of(e.getKey(), e.getValue())))).reduce(KORE.KApply(KORE.KLabel(".Map")), (a, b) -> KORE.KApply(KORE.KLabel("_Map_"), a, b))); return input; } From af0c0bb19bcff6ba2da0198b3ab0a0a58f81cb61 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 12 Jul 2017 17:55:13 -0500 Subject: [PATCH 22/34] modified domains.k to reflect how we're handling hooks --- k-distribution/include/builtin/domains.k | 50 ++++++++++++------------ 1 file changed, 26 insertions(+), 24 deletions(-) diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index 2dc924b8ab..3e7611739c 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -24,7 +24,7 @@ module MAP imports LIST imports SET - syntax Map [hook(MAP.Map)] + syntax Map /*@\section{Description} The Map represents a generalized associative array. Each key can be paired with an arbitrary value, and can be used to reference @@ -46,7 +46,7 @@ module MAP syntax non-assoc _|->_ /*@ Retrieve the value associated with the given key */ - syntax K ::= Map "[" K "]" [function, hook(MAP.lookup), klabel(Map:lookup), relativeHook(_Map_.lookup)] + syntax K ::= Map "[" K "]" [function, hook(MAP.lookup), klabel(Map:lookup)] /*@ Update a Map in form of of keys and values: */ syntax Map ::= Map "[" K "<-" K "]" [function, hook(MAP.update), prefer] @@ -67,7 +67,7 @@ module MAP syntax Map ::= removeAll(Map, Set) [function, hook(MAP.removeAll)] /*@ Get a Set consisting of all keys in the Map:*/ - syntax Set ::= keys(Map) [function, hook(MAP.keys), relativeHook(_Map_.keys)] + syntax Set ::= keys(Map) [function, hook(MAP.keys)] syntax Bool ::= K "in_keys" "(" Map ")" [function, hook(MAP.in_keys)] @@ -89,13 +89,14 @@ module SET imports BASIC-K imports BOOL-SYNTAX - syntax Set [hook(SET.Set)] + syntax Set /*@ \section{Description} The Set represents a mathematical set (a collection of unique items). */ /*@ Construct a new Set as the union of two different sets ($A \cup B$) */ - syntax Set ::= Set Set [left, function, hook(SET.concat), klabel(_Set_), assoc, comm, unit(.Set), idem, element(SetItem)] + // TODO: .Set here needs to be the element of an empty set + syntax Set ::= Set Set [left, function, hook(SET.concat,.Set()), klabel(Set), assoc, comm, unit(.Set), idem, element(SetItem)] /*@ Construct an empty Set */ syntax Set ::= ".Set" [function, hook(SET.unit), latex(\dotCt{Set})] //| "." @@ -112,7 +113,7 @@ module SET syntax Set ::= Set "-Set" Set [function, hook(SET.difference), latex({#1}-_{\it Set}{#2}), klabel(Set:difference)] /*@ Check element membership in a set ($a \in A$) */ - syntax Bool ::= K "in" Set [function, hook(SET.in), klabel(Set:in), relativeHook(_Set_.in)] + syntax Bool ::= K "in" Set [function, hook(SET.in), klabel(Set:in)] /*@ Check set inclusion ($A \subseteq B$) */ syntax Bool ::= Set "<=Set" Set [function, hook(SET.inclusion)] @@ -135,7 +136,7 @@ module LIST imports BASIC-K imports BOOL-SYNTAX - syntax List [hook(LIST.List)] + syntax List /*@ \section{Description} \K lists are ordered collections that may contain duplicate elements. These behave more like lists in functional programming @@ -168,9 +169,10 @@ module LIST /*@ Construct a new List as the concatenation of two Lists. This is similar to the append "@" operation in many functional programming languages. */ - syntax List ::= List List [left, function, hook(LIST.concat), klabel(_List_), smtlib(smt_seq_concat), assoc, unit(.List), element(ListItem)] + // TODO: .Set here needs to be the element of an empty list + syntax List ::= List List [left, function, hook(LIST.concat,.List()), klabel(List), smtlib(smt_seq_concat), assoc, unit(.List), element(ListItem)] /*@ Construct an empty List: */ - syntax List ::= ".List" [function, hook(LIST.unit), smtlib(smt_seq_nil), latex(\dotCt{List})] + syntax List ::= ".List" [function, smtlib(smt_seq_nil), latex(\dotCt{List})] //| "." /*@ Construct a singleton List (a list with only one element) */ syntax List ::= ListItem(K) [smtlib(smt_seq_elem)] @@ -193,9 +195,9 @@ endmodule module BOOL-SYNTAX imports SORT-K - syntax Bool [hook(BOOL.Bool)] - syntax Bool ::= "true" [token] - syntax Bool ::= "false" [token] + syntax Bool + syntax Bool ::= "true" [hook(BOOL.Bool), token] + syntax Bool ::= "false" [hook(BOOL.Bool), token] endmodule module BOOL @@ -251,8 +253,8 @@ module BOOL endmodule module INT-SYNTAX - syntax Int [hook(INT.Int)] - syntax Int ::= r"[\\+-]?[0-9]+" [prefer, token] + syntax Int + syntax Int ::= r"[\\+-]?[0-9]+" [prefer, token, hook(INT)] endmodule module INT @@ -317,10 +319,10 @@ module INT endmodule module FLOAT-SYNTAX - syntax Float [hook(FLOAT.Float)] - syntax Float ::= r"([\\+\\-]?[0-9]+(\\.[0-9]*)?|\\.[0-9]+)([eE][\\+\\-]?([0-9]+(\\.[0-9]*)?|\\.[0-9]+))?([fFdD]|([pP][0-9]+[xX][0-9]+))?" [token] - syntax Float ::= r"[\\+\\-]?Infinity([fFdD]|([pP][0-9]+[xX][0-9]+))?" [token] - syntax Float ::= r"NaN([fFdD]|([pP][0-9]+[xX][0-9]+))?" [token] + syntax Float + syntax Float ::= r"([\\+\\-]?[0-9]+(\\.[0-9]*)?|\\.[0-9]+)([eE][\\+\\-]?([0-9]+(\\.[0-9]*)?|\\.[0-9]+))?([fFdD]|([pP][0-9]+[xX][0-9]+))?" [hook(FLOAT.Float), token] + syntax Float ::= r"[\\+\\-]?Infinity([fFdD]|([pP][0-9]+[xX][0-9]+))?" [hook(FLOAT.Float), token] + syntax Float ::= r"NaN([fFdD]|([pP][0-9]+[xX][0-9]+))?" [hook(FLOAT.Float), token] endmodule module FLOAT @@ -401,8 +403,8 @@ module STRING-SYNTAX // | [\\][u] 4*Hex // "\uFFFF" Backslash 'u' followed by four hexadecimal characters // | [\\][U] 8*Hex // "\UFFffFFff" Backslash 'U' followed by eight hexadecimal characters // // the code must not be in the range [0xdfff, 0xd800] or exceed 0x10ffff - syntax String [hook(STRING.String)] - syntax String ::= r"[\\\"](([^\\\"\n\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]" [token] + syntax String + syntax String ::= r"[\\\"](([^\\\"\n\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]" [token, hook(STRING.String)] endmodule module STRING @@ -431,8 +433,8 @@ module STRING syntax Int ::= String2Int ( String ) [function, hook(STRING.string2int)] syntax String ::= Int2String ( Int ) [function, hook(STRING.int2string)] syntax String ::= Base2String ( Int , Int ) [function, hook(STRING.base2string)] - syntax Int ::= String2Base ( String , Int ) [function, hook(STRING.string2base)] - syntax KItem ::= "#parseToken" "(" String "," String ")" [function, hook(STRING.string2token)] + syntax Int ::= String2Base ( String , Int ) [function, hook(String.string2base,Int)] + syntax KItem ::= "#parseToken" "(" String "," String ")" [function, hook(String.string2token)] syntax String ::= "replaceAll" "(" String "," String "," String ")" [function, hook(STRING.replaceAll)] @@ -759,13 +761,13 @@ module MINT imports K-EQUAL imports LIST - syntax MInt [hook(MINT.MInt)] + syntax MInt /*@\section{Description} The MInt implements machine integers of arbitrary * bit width represented in 2's complement. */ /*@ Machine integer of bit width and value. */ - syntax MInt ::= mi(Int, Int) [function, hook(MINT.constructor)] + syntax MInt ::= mi(Int, Int) [function, hook(MINT.constructor), klabel(MInt)] /*@ Function returning the bit width of this machine integer. */ syntax Int ::= bitwidthMInt(MInt) [function, hook(MINT.bitwidth)] From 6a18e3e14fe2227b873fbc5f456ea8815393de0b Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Thu, 13 Jul 2017 14:07:41 -0500 Subject: [PATCH 23/34] fixed domains.k --- k-distribution/include/builtin/domains.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index 3e7611739c..791ab61036 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -433,7 +433,7 @@ module STRING syntax Int ::= String2Int ( String ) [function, hook(STRING.string2int)] syntax String ::= Int2String ( Int ) [function, hook(STRING.int2string)] syntax String ::= Base2String ( Int , Int ) [function, hook(STRING.base2string)] - syntax Int ::= String2Base ( String , Int ) [function, hook(String.string2base,Int)] + syntax Int ::= String2Base ( String , Int ) [function, hook(String.string2base)] syntax KItem ::= "#parseToken" "(" String "," String ")" [function, hook(String.string2token)] From 10a50348ddbfae05085bb62db2a621291d2441ff Mon Sep 17 00:00:00 2001 From: Cosmin Radoi Date: Thu, 13 Jul 2017 14:08:05 -0500 Subject: [PATCH 24/34] fixes to token declarations --- .../minikore/converters/KoreToMini.scala | 22 ++++++++++++++----- .../kframework/minikore/KoreToMiniTest.scala | 2 +- .../src/main/scala/MiniKoreUtils.scala | 3 ++- 3 files changed, 19 insertions(+), 8 deletions(-) diff --git a/frontend/src/main/scala/org/kframework/minikore/converters/KoreToMini.scala b/frontend/src/main/scala/org/kframework/minikore/converters/KoreToMini.scala index f1ef711442..536b7c7f4b 100644 --- a/frontend/src/main/scala/org/kframework/minikore/converters/KoreToMini.scala +++ b/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._ @@ -31,6 +32,8 @@ object KoreToMini { Module(ModuleName(m.name), importSentences ++ localSentences, Attributes(apply(m.att))) } + private val tokenPrefix = "TOKEN_" + def apply(s: definition.Sentence): Sentence = s match { case definition.SyntaxSort(sort, att) => SortDeclaration(b.Sort(sort.name), Attributes(apply(att))) @@ -40,8 +43,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(tokenPrefix + 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) => @@ -114,7 +126,7 @@ object KoreToMini { case KApply(klabel, klist) => b.Application(Symbol(klabel.name), klist.map(apply)) case kvar@SortedKVariable(name, _) => b.SortedVariable(Name(name), b.Sort(kvar.sort.name)) // assert(att == k.att) case KVariable(name) => b.SortedVariable(b.Name(name), b.Sort("_")) // TODO(Daejun): apply(SortedKVariable(name, k.att)) // from SortedADT in ADT.scala - case KToken(s, sort) => b.DomainValue(Symbol(sort.name), Value(s)) + case KToken(s, sort) => b.DomainValue(Symbol(tokenPrefix + sort.name), Value(s)) case KSequence(ks) => encodeKSeq(ks.map(apply)) case KRewrite(left, right) => b.Rewrite(apply(left), apply(right)) case InjectedKLabel(klabel) => ??? @@ -172,6 +184,4 @@ object KoreToMini { val iAtt = Symbol("#") val iKSeq = Symbol("#kseq") val iKSeqNil = Symbol("#kseqnil") - - val iNone = Symbol("#None") } diff --git a/frontend/src/test/scala/org/kframework/minikore/KoreToMiniTest.scala b/frontend/src/test/scala/org/kframework/minikore/KoreToMiniTest.scala index 57a985ced5..b2a9c04c9a 100644 --- a/frontend/src/test/scala/org/kframework/minikore/KoreToMiniTest.scala +++ b/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)))))) ) } diff --git a/java-backend/src/main/scala/MiniKoreUtils.scala b/java-backend/src/main/scala/MiniKoreUtils.scala index 32bd55fdc2..0f23337364 100644 --- a/java-backend/src/main/scala/MiniKoreUtils.scala +++ b/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 => From cf3903af61bd663acc924d63176894f85437aefb Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Thu, 13 Jul 2017 17:05:55 -0500 Subject: [PATCH 25/34] wip on changing hook infrastructure, can now step --- .../kframework/minikore/converters/KoreToMini.scala | 9 +++------ .../kframework/minikore/converters/MiniToKore.scala | 7 +++---- k-distribution/include/builtin/domains.k | 12 ++++++------ .../java/org/kframework/kil/DataStructureSort.java | 8 +------- .../kframework/frontend/compile/CloseCellsTest.java | 11 ++++++----- .../org/kframework/backend/skala/ImpOnSkalaTest.java | 2 +- 6 files changed, 20 insertions(+), 29 deletions(-) diff --git a/frontend/src/main/scala/org/kframework/minikore/converters/KoreToMini.scala b/frontend/src/main/scala/org/kframework/minikore/converters/KoreToMini.scala index 536b7c7f4b..13a318ad9b 100644 --- a/frontend/src/main/scala/org/kframework/minikore/converters/KoreToMini.scala +++ b/frontend/src/main/scala/org/kframework/minikore/converters/KoreToMini.scala @@ -32,8 +32,6 @@ object KoreToMini { Module(ModuleName(m.name), importSentences ++ localSentences, Attributes(apply(m.att))) } - private val tokenPrefix = "TOKEN_" - def apply(s: definition.Sentence): Sentence = s match { case definition.SyntaxSort(sort, att) => SortDeclaration(b.Sort(sort.name), Attributes(apply(att))) @@ -47,7 +45,7 @@ object KoreToMini { 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(tokenPrefix + sort.name), args, Attributes(newAtt)) + SymbolDeclaration(b.Sort(sort.name), b.Symbol(sort.name), args, Attributes(newAtt)) } else { assert(args.size == 1) val subsort: Sort = args.head @@ -126,7 +124,7 @@ object KoreToMini { case KApply(klabel, klist) => b.Application(Symbol(klabel.name), klist.map(apply)) case kvar@SortedKVariable(name, _) => b.SortedVariable(Name(name), b.Sort(kvar.sort.name)) // assert(att == k.att) case KVariable(name) => b.SortedVariable(b.Name(name), b.Sort("_")) // TODO(Daejun): apply(SortedKVariable(name, k.att)) // from SortedADT in ADT.scala - case KToken(s, sort) => b.DomainValue(Symbol(tokenPrefix + sort.name), Value(s)) + case KToken(s, sort) => b.DomainValue(Symbol(sort.name), Value(s)) case KSequence(ks) => encodeKSeq(ks.map(apply)) case KRewrite(left, right) => b.Rewrite(apply(left), apply(right)) case InjectedKLabel(klabel) => ??? @@ -138,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)) }) } @@ -181,7 +179,6 @@ object KoreToMini { Symbol("#None")) val encodingLabels = encodingLabelTuple.productIterator.toSet - val iAtt = Symbol("#") val iKSeq = Symbol("#kseq") val iKSeqNil = Symbol("#kseqnil") } diff --git a/frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala b/frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala index ff99e875fa..ddf72049a6 100644 --- a/frontend/src/main/scala/org/kframework/minikore/converters/MiniToKore.scala +++ b/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 { @@ -135,12 +136,10 @@ 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("_Map_.lookup"), args) => KORE.KApply(KORE.KLabel("Map:lookup"), args.map(apply), att) - 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) diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index 791ab61036..2eb3e8b4d6 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -32,9 +32,9 @@ module MAP /*@ Construct a new Map consisting of key/value pairs of two Maps (the keys of the two Maps are assumed disjoint) */ - syntax Map ::= Map Map [left, function, hook(MAP.concat), klabel(_Map_), assoc, comm, unit(.Map), element(_|->_), index(0)] + syntax Map ::= Map Map [left, function, hook(MAP.concat,.Map(),1), klabel(Map@MAP), assoc, comm, unit(.Map), element(_|->_), index(0)] /*@ Construct an empty Map */ - syntax Map ::= ".Map" [function, hook(MAP.unit), latex(\dotCt{Map})] + syntax Map ::= ".Map" [function, latex(\dotCt{Map}), klabel(.Map)] // breaks klabel uniqueness //| "." [function, hook(MAP.unit)] syntax Map ::= "(" Map ")" [bracket] @@ -42,7 +42,7 @@ module MAP is on the left and the value is on the right */ syntax Map ::= K "|->" K [hook(MAP.element), latex({#1}\mapsto{#2})] - syntax priorities _|->_ > _Map_ .Map + syntax priorities _|->_ > Map@MAP .Map syntax non-assoc _|->_ /*@ Retrieve the value associated with the given key */ @@ -96,9 +96,9 @@ module SET /*@ Construct a new Set as the union of two different sets ($A \cup B$) */ // TODO: .Set here needs to be the element of an empty set - syntax Set ::= Set Set [left, function, hook(SET.concat,.Set()), klabel(Set), assoc, comm, unit(.Set), idem, element(SetItem)] + syntax Set ::= Set Set [left, function, hook(SET.concat,.Set()), klabel(Set@SET), assoc, comm, unit(.Set), idem, element(SetItem)] /*@ Construct an empty Set */ - syntax Set ::= ".Set" [function, hook(SET.unit), latex(\dotCt{Set})] + syntax Set ::= ".Set" [function, latex(\dotCt{Set})] //| "." syntax Set ::= "(" Set ")" [bracket] /*@ Construct a singleton Set (a Set with only one element $\{ a \}$). To add @@ -170,7 +170,7 @@ module LIST /*@ Construct a new List as the concatenation of two Lists. This is similar to the append "@" operation in many functional programming languages. */ // TODO: .Set here needs to be the element of an empty list - syntax List ::= List List [left, function, hook(LIST.concat,.List()), klabel(List), smtlib(smt_seq_concat), assoc, unit(.List), element(ListItem)] + syntax List ::= List List [left, function, hook(LIST.concat,.List()), klabel(List@LIST), smtlib(smt_seq_concat), assoc, unit(.List), element(ListItem)] /*@ Construct an empty List: */ syntax List ::= ".List" [function, smtlib(smt_seq_nil), latex(\dotCt{List})] //| "." diff --git a/kernel/src/main/java/org/kframework/kil/DataStructureSort.java b/kernel/src/main/java/org/kframework/kil/DataStructureSort.java index 1f7e560cb8..6a25e5d04c 100644 --- a/kernel/src/main/java/org/kframework/kil/DataStructureSort.java +++ b/kernel/src/main/java/org/kframework/kil/DataStructureSort.java @@ -4,6 +4,7 @@ import com.google.common.collect.ImmutableMap; import com.google.common.collect.ImmutableSet; import org.kframework.kil.loader.Context; +import org.kframework.kore.implementation; import java.io.Serializable; import java.util.Map; @@ -64,15 +65,8 @@ public enum Label { CONSTRUCTOR, ELEMENT, UNIT } public static final Sort DEFAULT_LIST_SORT = Sort.LIST; public static final Sort DEFAULT_MAP_SORT = Sort.MAP; public static final Sort DEFAULT_SET_SORT = Sort.SET; - public static final String DEFAULT_LIST_LABEL = "_List_"; public static final String DEFAULT_LIST_ITEM_LABEL = "ListItem"; - public static final String DEFAULT_LIST_UNIT_LABEL = ".List"; - public static final String DEFAULT_MAP_LABEL = "_Map_"; - public static final String DEFAULT_MAP_ITEM_LABEL = "_|->_"; public static final String DEFAULT_MAP_UNIT_LABEL = ".Map"; - public static final String DEFAULT_SET_LABEL = "_Set_"; - public static final String DEFAULT_SET_ITEM_LABEL = "SetItem"; - public static final String DEFAULT_SET_UNIT_LABEL = ".Set"; /** Name of this data structure sort. */ private final String name; diff --git a/kernel/src/test/java/org/kframework/frontend/compile/CloseCellsTest.java b/kernel/src/test/java/org/kframework/frontend/compile/CloseCellsTest.java index ccd92efaa4..be3308e4f4 100644 --- a/kernel/src/test/java/org/kframework/frontend/compile/CloseCellsTest.java +++ b/kernel/src/test/java/org/kframework/frontend/compile/CloseCellsTest.java @@ -10,6 +10,7 @@ import org.junit.Test; import org.junit.Assert; +import org.kframework.kore.implementation; import org.kframework.utils.errorsystem.KEMException; import java.util.Arrays; @@ -19,8 +20,8 @@ public class CloseCellsTest { final SortInfo sortInfo = new SortInfo() {{ - addOp("Map", "_Map_"); - addOp("List", "_List_"); + addOp("Map", "Map@MAP"); + addOp("List", "List@LIST"); }}; final TestConfiguration cfgInfo = new TestConfiguration() {{ addCell(null, "ThreadCell", "", Multiplicity.STAR); @@ -35,8 +36,8 @@ public class CloseCellsTest { addLabel("EnvCell", ""); addLabel("ThreadCell", ""); addLabel("ListCell", ""); - addLabel("Map", "_Map_", true, true, true); - addLabel("List", "_List_", true, false, true); + addLabel("Map", "Map@MAP", true, true, true); + addLabel("List", "List@LIST", true, false, true); }}; @Test @@ -50,7 +51,7 @@ public void testSimpleClosure() { @Test public void testCloseMap() { K term = cell("", true, false, KORE.KApply(KLabel("'_|=>_"), intToToken(1), intToToken(2))); - K expected = ccell("", KORE.KApply(KLabel("_Map_"), KORE.KApply(KLabel("'_|=>_"), intToToken(1), intToToken(2)), KVariable("DotVar0"))); + K expected = ccell("", KORE.KApply(KLabel("Map@MAP"), KORE.KApply(KLabel("'_|=>_"), intToToken(1), intToToken(2)), KVariable("DotVar0"))); Assert.assertEquals(expected, new CloseCells(cfgInfo, sortInfo, labelInfo).close(term)); } diff --git a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java index c35f7e36a5..79900f76fc 100644 --- a/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java +++ b/skala-backend/src/test/scala/org/kframework/backend/skala/ImpOnSkalaTest.java @@ -88,7 +88,7 @@ private static K getParsedProgram(String pgmName) { K parsed = programParser.apply(program, source); Map map = new HashMap<>(); map.put(KORE.KToken("$PGM", Sorts.KConfigVar()), parsed); - KApply input = KORE.KApply(compiledDef.topCellInitializer, map.entrySet().stream().map(e -> KORE.KApply(KORE.KLabel("_|->_"), KORE.KList(List.of(e.getKey(), e.getValue())))).reduce(KORE.KApply(KORE.KLabel(".Map")), (a, b) -> KORE.KApply(KORE.KLabel("_Map_"), a, b))); + KApply input = KORE.KApply(compiledDef.topCellInitializer, map.entrySet().stream().map(e -> KORE.KApply(KORE.KLabel("_|->_"), KORE.KList(List.of(e.getKey(), e.getValue())))).reduce(KORE.KApply(KORE.KLabel(".Map")), (a, b) -> KORE.KApply(KORE.KLabel("Map@MAP"), a, b))); return input; } From a04307e8f715062acadbe9f019d0e1455a042440 Mon Sep 17 00:00:00 2001 From: Cosmin Radoi Date: Tue, 18 Jul 2017 12:05:29 -0500 Subject: [PATCH 26/34] Outer.jj allows quotes for nested attributes --- kernel/src/main/javacc/Outer.jj | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/kernel/src/main/javacc/Outer.jj b/kernel/src/main/javacc/Outer.jj index cc6f5e0431..cb29720ab1 100644 --- a/kernel/src/main/javacc/Outer.jj +++ b/kernel/src/main/javacc/Outer.jj @@ -724,7 +724,7 @@ void Group(StringBuilder sb, int state) : {} | "]" { matchedToken.kind = RSQUARE; } | "(" { matchedToken.kind = LPAREN; } | ")" { matchedToken.kind = RPAREN; } -| ")?> +| ")?> } /** The same as 'Attributes()', but requires that the entire input be @@ -770,7 +770,8 @@ void TagContent(StringBuilder sb) : {} { ( { sb.append(specialAndImage()); } | "(" { sb.append(specialAndImage()); } - TagContent(sb) + ( String() + | TagContent(sb) ) ")" { sb.append(specialAndImage()); } )* } From 4c79b14e4d3e89a2a0d5d7728ac749d5248f1902 Mon Sep 17 00:00:00 2001 From: Cosmin Radoi Date: Tue, 18 Jul 2017 12:05:46 -0500 Subject: [PATCH 27/34] outer.jj param allows @ in label name --- kernel/src/main/javacc/KoreParser.jj | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/src/main/javacc/KoreParser.jj b/kernel/src/main/javacc/KoreParser.jj index 34521935e7..e075eb6d9f 100644 --- a/kernel/src/main/javacc/KoreParser.jj +++ b/kernel/src/main/javacc/KoreParser.jj @@ -77,7 +77,7 @@ TOKEN : | | | -| +| } MORE : From 5a5d6237d1ecffa8eda6d909de8d6dfc1f235672 Mon Sep 17 00:00:00 2001 From: Cosmin Radoi Date: Tue, 18 Jul 2017 12:07:05 -0500 Subject: [PATCH 28/34] made the Map hook match the Scala backend convention --- k-distribution/include/builtin/domains.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index 2eb3e8b4d6..d259c7ee39 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -32,7 +32,7 @@ module MAP /*@ Construct a new Map consisting of key/value pairs of two Maps (the keys of the two Maps are assumed disjoint) */ - syntax Map ::= Map Map [left, function, hook(MAP.concat,.Map(),1), klabel(Map@MAP), assoc, comm, unit(.Map), element(_|->_), index(0)] + syntax Map ::= Map Map [left, function, hook(MAP.concat,.Map(),Int@INT-SYNTAX("0")), klabel(Map@MAP), assoc, comm, unit(.Map), element(_|->_), index(0)] /*@ Construct an empty Map */ syntax Map ::= ".Map" [function, latex(\dotCt{Map}), klabel(.Map)] // breaks klabel uniqueness From 570400687d875f43e6bb5ac6884e90d34682e983 Mon Sep 17 00:00:00 2001 From: Cosmin Radoi Date: Tue, 18 Jul 2017 12:07:52 -0500 Subject: [PATCH 29/34] hack for attribute label marker --- java-backend/src/main/scala/MiniKoreUtils.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/java-backend/src/main/scala/MiniKoreUtils.scala b/java-backend/src/main/scala/MiniKoreUtils.scala index 0f23337364..ab72447a7d 100644 --- a/java-backend/src/main/scala/MiniKoreUtils.scala +++ b/java-backend/src/main/scala/MiniKoreUtils.scala @@ -140,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()) From b325fb38a4ca1d04fc977425ebd7e109463d1357 Mon Sep 17 00:00:00 2001 From: Cosmin Radoi Date: Tue, 18 Jul 2017 13:58:47 -0500 Subject: [PATCH 30/34] move KConfigVar so that it's available everywhere --- k-distribution/include/builtin/kast.k | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/include/builtin/kast.k b/k-distribution/include/builtin/kast.k index 320181a67f..1d727be92b 100644 --- a/k-distribution/include/builtin/kast.k +++ b/k-distribution/include/builtin/kast.k @@ -13,7 +13,7 @@ module BASIC-K syntax KLabel syntax KItem [hook(K.KItem)] syntax K ::= KItem [allowChainSubsort] - syntax KConfigVar + syntax KConfigVar ::= r"(? Date: Tue, 18 Jul 2017 16:18:14 -0500 Subject: [PATCH 31/34] Outer.jj fix to allow strings in attributes --- kernel/src/main/javacc/Outer.jj | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kernel/src/main/javacc/Outer.jj b/kernel/src/main/javacc/Outer.jj index cb29720ab1..9cdaa77b4b 100644 --- a/kernel/src/main/javacc/Outer.jj +++ b/kernel/src/main/javacc/Outer.jj @@ -769,9 +769,9 @@ void Tag(ASTNode node) : void TagContent(StringBuilder sb) : {} { ( { sb.append(specialAndImage()); } +| { sb.append(specialAndImage()); } | "(" { sb.append(specialAndImage()); } - ( String() - | TagContent(sb) ) + TagContent(sb) ")" { sb.append(specialAndImage()); } )* } From 0da8aafadc1a715de5a71b1ca9c357f4526cfeed Mon Sep 17 00:00:00 2001 From: Cosmin Radoi Date: Tue, 18 Jul 2017 17:00:19 -0500 Subject: [PATCH 32/34] change label of map lookup to match Scala backend --- frontend/src/main/java/org/kframework/builtin/KLabels.java | 2 +- k-distribution/include/builtin/domains.k | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/frontend/src/main/java/org/kframework/builtin/KLabels.java b/frontend/src/main/java/org/kframework/builtin/KLabels.java index c623ca2a47..5dc210bcb6 100644 --- a/frontend/src/main/java/org/kframework/builtin/KLabels.java +++ b/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"; } diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index d259c7ee39..8b3a3244f3 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -46,7 +46,7 @@ module MAP syntax non-assoc _|->_ /*@ Retrieve the value associated with the given key */ - syntax K ::= Map "[" K "]" [function, hook(MAP.lookup), klabel(Map:lookup)] + syntax K ::= Map "[" K "]" [function, hook(MAP.lookup), klabel(Map@MAP.lookup)] /*@ Update a Map in form of of keys and values: */ syntax Map ::= Map "[" K "<-" K "]" [function, hook(MAP.update), prefer] From 134eed8e36f986d4f77bf170a4e572bd7f429d2f Mon Sep 17 00:00:00 2001 From: Cosmin Radoi Date: Tue, 18 Jul 2017 19:45:19 -0500 Subject: [PATCH 33/34] change labels for Map.keys and SET.in to match the Scala backend --- k-distribution/include/builtin/domains.k | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index 8b3a3244f3..ff8fe4b247 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -67,7 +67,7 @@ module MAP syntax Map ::= removeAll(Map, Set) [function, hook(MAP.removeAll)] /*@ Get a Set consisting of all keys in the Map:*/ - syntax Set ::= keys(Map) [function, hook(MAP.keys)] + syntax Set ::= keys(Map) [function, hook(MAP.keys), klabel(Map@MAP.keys)] syntax Bool ::= K "in_keys" "(" Map ")" [function, hook(MAP.in_keys)] @@ -113,7 +113,7 @@ module SET syntax Set ::= Set "-Set" Set [function, hook(SET.difference), latex({#1}-_{\it Set}{#2}), klabel(Set:difference)] /*@ Check element membership in a set ($a \in A$) */ - syntax Bool ::= K "in" Set [function, hook(SET.in), klabel(Set:in)] + syntax Bool ::= K "in" Set [function, hook(SET.in), klabel(Set@SET.in)] /*@ Check set inclusion ($A \subseteq B$) */ syntax Bool ::= Set "<=Set" Set [function, hook(SET.inclusion)] From e9a593248b4773eb0f9895c1cdb5d8b85734cebb Mon Sep 17 00:00:00 2001 From: cos Date: Mon, 24 Jul 2017 16:08:19 -0500 Subject: [PATCH 34/34] hook Map.update correctly --- k-distribution/include/builtin/domains.k | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index ff8fe4b247..e93e1c9075 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -40,7 +40,7 @@ module MAP syntax Map ::= "(" Map ")" [bracket] /*@ Construct a singleton Map (a Map with only one key/value pair). The key is on the left and the value is on the right */ - syntax Map ::= K "|->" K [hook(MAP.element), latex({#1}\mapsto{#2})] + syntax Map ::= K "|->" K [latex({#1}\mapsto{#2})] syntax priorities _|->_ > Map@MAP .Map syntax non-assoc _|->_ @@ -49,7 +49,7 @@ module MAP syntax K ::= Map "[" K "]" [function, hook(MAP.lookup), klabel(Map@MAP.lookup)] /*@ Update a Map in form of of keys and values: */ - syntax Map ::= Map "[" K "<-" K "]" [function, hook(MAP.update), prefer] + syntax Map ::= Map "[" K "<-" K "]" [function, hook(MAP.update, label("_|->_")), prefer] /*@ Remove key/value pair associated with the key from map? */ syntax Map ::= Map "[" K "<-" "undef" "]" [function, hook(MAP.remove)]