Merge remote-tracking branch 'origin/develop'

k-distribution/src/test/scala/org/kframework/backend/kore/KoreTest.scala

@@ -65,18 +65,28 @@ class KoreTest {
     attributes.patterns.exists { case p: Application => p.head.ctr == name }
   }
 
+  // get the rewrite associated with a rule or equational axiom
+  //
+  // \and(\equals(requires, \dv("true")), \and(_, \rewrites(lhs, rhs)))
+  // \and(\top(), \and(_, \rewrites(lhs, rhs)))
+  // \rewrites(\and(\equals(requires, \dv("true")), lhs), \and(_, rhs))
+  // \rewrites(\and(\top(), lhs), \and(_, rhs))
+  // \implies(\equals(requires, \dv("true")), \and(\equals(lhs, rhs), _))
+  // \implies(\top, \and(\equals(lhs, rhs), _))
+  // \implies(\and(_, \equals(requires, \dv("true"))), \and(\equals(lhs, rhs), _))
+  // \implies(\and(_, \top), \and(\equals(lhs, rhs), _))
+  // \equals(lhs, rhs)
   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 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 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(_, 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
 
@@ -91,7 +101,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)
@@ -103,7 +113,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()
     }

kore/src/main/scala/org/kframework/parser/kore/Default.scala

@@ -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
 
@@ -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)
 

kore/src/main/scala/org/kframework/parser/kore/Interface.scala

@@ -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 {

kore/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala

@@ -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
@@ -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) =>