Updated benchmarks to have better examples for string-render

testcases/web/synthesis/23_String_Grammar.scala

@@ -11,6 +11,16 @@ object GrammarRender {
 
   case class Rule(left: Symbol, right: List[Symbol])
   case class Grammar(start: Symbol, rules: List[Rule])
+  
+  /** Given a grammar, expanding with the first, second or third rule for the symbol should yield the same list each time.
+   *  Obviously wrong, but provides meaningful counter-examples. */
+  def threeExpansionsIsTheSame(g: Grammar, s: Symbol) = {
+    require(isGrammar(g) && noEpsilons(g.rules) && isReasonable(g.rules) && !isTerminal(s))
+    val a = expand(g.rules, s, BigInt(0))
+    val b = expand(g.rules, s, BigInt(1))
+    val c = expand(g.rules, s, BigInt(2))
+    a == b && b == c
+  } holds
 
   /** Synthesis by example specs */
   @inline def psStandard(s: Grammar) = (res: String) => (s, res) passes {
@@ -140,9 +150,12 @@ S0 -> S0 t1"""
     case Nil() => true
     case Cons(r, q) => isReasonableRule(r.right, r.left) && isReasonable(q)
   } 
-  
-  def allGrammarsAreIdentical(g: Grammar, g2: Grammar) = {
-    require(isGrammar(g) && isGrammar(g2) && noEpsilons(g.rules) && noEpsilons(g2.rules) && isReasonable(g.rules) && isReasonable(g2.rules))
-    (g == g2 || g.rules == g2.rules)
-  } holds
+
+  def expand(lr: List[Rule], s: Symbol, index: BigInt): List[Symbol] = if(index < 0) List(s) else (lr match {
+    case Nil() => List(s)
+    case Cons(Rule(l, r), q) =>
+      if(l == s) {
+        if(index == 0) r else expand(q, s, index - 1)
+      } else expand(q, s, index)
+  })
 }
\ No newline at end of file

testcases/web/synthesis/24_String_DoubleList.scala

@@ -12,18 +12,52 @@ object DoubleListRender {
   abstract class AA
   case class BB(i: A, a: AA) extends AA
   case class NN() extends AA
-  
-  // Obviously wrong, but it is useful to use the display function.
-  def twoOutOfThreeAsAreTheSame(a: A, b: A, c: A): Boolean = {
-    a == b || a == c || b == c
+    
+  // Two elements which do not contain each other but are in the same A should be the same.
+  // Obviously wrong, but for the sake of displaying counter-examples.
+  def lemma1(a: A, b: A, c: A): Boolean = {
+    require(containsA_A(a, b) && containsA_A(a, c) && !containsA_A(b, c) && !containsA_A(c, b))
+    b == c
   } holds
 
   def AtoString(a : A): String =  {
     ???
   } ensuring {
     (res : String) => (a, res) passes {
-      case B(BB(N(), BB(B(NN(), B(NN(), N())), NN())), N()) =>
-        "[([], [(), ()])]"
+      case N() =>
+        "[]"
+      case B(NN()) =>
+        "[()]"
     }
   }
+  
+  def structurallyEqualA(a: A, b: A): Boolean = (a, b) match {
+    case (N(), N()) => true
+    case (B(i, k), B(j, l)) => structurallyEqualA(k, l) && structurallyEqualAA(i, j)
+  }
+  
+  def structurallyEqualAA(a: AA, b: AA): Boolean = (a, b) match {
+    case (NN(), NN()) => true
+    case (BB(i, k), BB(j, l)) => structurallyEqualAA(k, l) && structurallyEqualA(i, j)
+  }
+  
+  def containsA_A(a: A, b: A): Boolean = (a match {
+    case N() => false
+    case B(i, k) => containsAA_A(i, b) || containsA_A(k, b)
+  })
+  
+  def containsAA_A(a: AA, b: A): Boolean = (a match {
+    case NN() => false
+    case BB(i, k) => i == b || containsA_A(i, b) || containsAA_A(k, b)
+  })
+  
+  def containsA_AA(a: A, b: AA): Boolean = (a match {
+    case N() => false
+    case B(i, k) => i == b || containsAA_AA(i, b) || containsA_AA(k, b)
+  })
+  
+  def containsAA_AA(a: AA, b: AA): Boolean = (a match {
+    case NN() => false
+    case BB(i, k) => containsA_AA(i, b) || containsAA_AA(k, b)
+  })
 }
\ No newline at end of file