Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

update scala kore parser to use multi-ary and and or everywhere #3678

Merged
merged 6 commits into from
Oct 2, 2023
Merged

update scala kore parser to use multi-ary and and or everywhere #3678

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
dd5b8e2
update scala code to use multi-ary and/or everywhere
Sep 28, 2023
1d61395
update k-distribution scala tests
Sep 28, 2023
6310d51
when constructing multi-ary And/Or, desugar 0 or 1 arguments
Sep 29, 2023
0f2d3e7
add comment
Oct 2, 2023
0abe315
delete dead case
Oct 2, 2023
3a9a70d
Merge branch 'develop' into and_or2
Oct 2, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 10 additions & 10 deletions k-distribution/src/test/scala/org/kframework/backend/kore/KoreTest.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,15 +68,15 @@ class KoreTest {
def getRewrite(axiom: AxiomDeclaration): Option[GeneralizedRewrite] = {
def go(pattern: Pattern): Option[GeneralizedRewrite] = {
pattern match {
case And(_, Equals(_, _, _, _), And(_, _, rw @ Rewrites(_, _, _))) => Some(rw)
case And(_, Top(_), And(_, _, rw @ Rewrites(_, _, _))) => Some(rw)
case Rewrites(s, And(_, Equals(_, _, _, _), l), And(_, _, r)) => Some(B.Rewrites(s, l, r))
case Rewrites(s, And(_, Top(_), l), And(_, _, r)) => Some(B.Rewrites(s, l, r))
case And(_, Equals(_, _, _, _) +: And(_, _ +: (rw @ Rewrites(_, _, _)) +: Seq()) +: Seq()) => Some(rw)
case And(_, Top(_) +: And(_, _ +: (rw @ Rewrites(_, _, _)) +: Seq()) +: Seq()) => Some(rw)
case Rewrites(s, And(_, Equals(_, _, _, _) +: l +: Seq()), And(_, _ +: r +: Seq())) => Some(B.Rewrites(s, l, r))
case Rewrites(s, And(_, Top(_) +: l +: Seq()), And(_, _ +: r +: Seq())) => Some(B.Rewrites(s, l, r))
case Implies(_, Bottom(_), p) => go(p)
case Implies(_, Equals(_, _, _, _), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq)
case Implies(_, Top(_), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq)
case Implies(_, And(_, _, Equals(_, _, _, _)), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq)
case Implies(_, And(_, _, Top(_)), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq)
case Implies(_, Equals(_, _, _, _), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
case Implies(_, Top(_), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
case Implies(_, And(_, _ +: Equals(_, _, _, _) +: Seq()), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
case Implies(_, And(_, _ +: Top(_) +: Seq()), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
case eq @ Equals(_, _, Application(_, _), _) => Some(eq)
case _ => None

Expand All @@ -91,7 +91,7 @@ class KoreTest {

def symbols(pat: Pattern): Seq[SymbolOrAlias] = {
pat match {
case And(_, p1, p2) => symbols(p1) ++ symbols(p2)
case And(_, ps) => ps.flatMap(symbols)
case Application(s, ps) => Seq(s).filter(isConcrete) ++ ps.flatMap(symbols)
case Ceil(_, _, p) => symbols(p)
case Equals(_, _, p1, p2) => symbols(p1) ++ symbols(p2)
Expand All @@ -103,7 +103,7 @@ class KoreTest {
case Mem(_, _, p1, p2) => symbols(p1) ++ symbols(p2)
// case Next(_, p) => symbols(p)
case Not(_, p) => symbols(p)
case Or(_, p1, p2) => symbols(p1) ++ symbols(p2)
case Or(_, ps) => ps.flatMap(symbols)
case Rewrites(_, p1, p2) => symbols(p1) ++ symbols(p2)
case _ => Seq()
}
Expand Down
28 changes: 16 additions & 12 deletions kore/src/main/scala/org/kframework/parser/kore/Default.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,17 +40,9 @@ object implementation {

case class Bottom(s: i.Sort) extends i.Bottom

case class And(s: i.Sort, args: Seq[i.Pattern]) extends i.And {
val _1 = args(0)
case class And(s: i.Sort, args: Seq[i.Pattern]) extends i.And

val _2 = args(1)
}

case class Or(s: i.Sort, args: Seq[i.Pattern]) extends i.Or {
val _1 = args(0)

val _2 = args(1)
}
case class Or(s: i.Sort, args: Seq[i.Pattern]) extends i.Or

case class Not(s: i.Sort, _1: i.Pattern) extends i.Not

Expand Down Expand Up @@ -138,11 +130,23 @@ object implementation {

def And(s: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Pattern = d.And(s, Seq(_1, _2))

def And(s: i.Sort, args: Seq[i.Pattern]): i.Pattern = d.And(s, args)
def And(s: i.Sort, args: Seq[i.Pattern]): i.Pattern = {
args.size match {
case 0 => Top(s)
case 1 => args(0)
case _ => d.And(s, args)
}
}

def Or(s: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Pattern = d.Or(s, Seq(_1, _2))

def Or(s: i.Sort, args: Seq[i.Pattern]): i.Pattern = d.Or(s, args)
def Or(s: i.Sort, args: Seq[i.Pattern]): i.Pattern = {
args.size match {
case 0 => Bottom(s)
case 1 => args(0)
case _ => d.Or(s, args)
}
}

def Not(s: i.Sort, _1: i.Pattern): i.Pattern = d.Not(s, _1)

Expand Down
12 changes: 2 additions & 10 deletions kore/src/main/scala/org/kframework/parser/kore/Interface.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -164,29 +164,21 @@ object Bottom {
trait And extends Pattern {
def s: Sort

def _1: Pattern

def _2: Pattern

def args: Seq[Pattern]
}

object And {
def unapply(arg: And): Option[(Sort, Pattern, Pattern)] = Some(arg.s, arg._1, arg._2)
def unapply(arg: And): Option[(Sort, Seq[Pattern])] = Some(arg.s, arg.args)
}

trait Or extends Pattern {
def s: Sort

def _1: Pattern

def _2: Pattern

def args: Seq[Pattern]
}

object Or {
def unapply(arg: Or): Option[(Sort, Pattern, Pattern)] = Some(arg.s, arg._1, arg._2)
def unapply(arg: Or): Option[(Sort, Seq[Pattern])] = Some(arg.s, arg.args)
}

trait Not extends Pattern {
Expand Down
11 changes: 7 additions & 4 deletions kore/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
package org.kframework.parser.kore.parser

import org.kframework.builtin.{KLabels, Sorts}
import org.kframework.kore.Assoc
import org.kframework.kore.KVariable
import org.kframework.kore.KORE
import org.kframework.attributes.Att
Expand Down Expand Up @@ -133,10 +134,12 @@ class KoreToK (sortAtt : Map[String, String]) {
KORE.KApply(KORE.KLabel(KLabels.ML_TRUE.name, apply(s)))
case kore.Bottom(s) =>
KORE.KApply(KORE.KLabel(KLabels.ML_FALSE.name, apply(s)))
case kore.And(s, p, q) =>
KORE.KApply(KORE.KLabel(KLabels.ML_AND.name, apply(s)), apply(p), apply(q))
case kore.Or(s, p, q) =>
KORE.KApply(KORE.KLabel(KLabels.ML_OR.name, apply(s)), apply(p), apply(q))
case kore.And(s, items) =>
val and = KORE.KLabel(KLabels.ML_AND.name, apply(s))
KORE.KApply(and, Assoc.flatten(and, items.map(apply), KORE.KLabel(KLabels.ML_TRUE.name, apply(s))))
case kore.Or(s, items) =>
val or = KORE.KLabel(KLabels.ML_OR.name, apply(s))
KORE.KApply(or, Assoc.flatten(or, items.map(apply), KORE.KLabel(KLabels.ML_FALSE.name, apply(s))))
case kore.Not(s, p) =>
KORE.KApply(KORE.KLabel(KLabels.ML_NOT.name, apply(s)), apply(p))
case kore.Implies(s, p, q) =>
Expand Down