From f657ddbd094ff37e61ef19905e97cb7f4e9c37e4 Mon Sep 17 00:00:00 2001 From: Sidonie Bouthors Date: Sun, 5 Jan 2025 22:13:13 +0100 Subject: [PATCH] Add tests for pattern alternatives Co-authored-by: SidonieBouthors Co-authored-by: Mai-LinhC --- .../valid/PatternAlternative1 copy.scala | 20 +++++++++++ .../valid/PatternAlternative2.scala | 33 +++++++++++++++++++ .../valid/PatternAlternative.scala | 33 +++++++++++++++++++ 3 files changed, 86 insertions(+) create mode 100644 frontends/benchmarks/extraction/valid/PatternAlternative1 copy.scala create mode 100644 frontends/benchmarks/extraction/valid/PatternAlternative2.scala create mode 100644 frontends/benchmarks/verification/valid/PatternAlternative.scala diff --git a/frontends/benchmarks/extraction/valid/PatternAlternative1 copy.scala b/frontends/benchmarks/extraction/valid/PatternAlternative1 copy.scala new file mode 100644 index 000000000..2a13c9fb0 --- /dev/null +++ b/frontends/benchmarks/extraction/valid/PatternAlternative1 copy.scala @@ -0,0 +1,20 @@ +object PatternAlternative1 { + sealed trait SignSet + case object None extends SignSet + case object Any extends SignSet + case object Neg extends SignSet + case object Zer extends SignSet + case object Pos extends SignSet + case object NegZer extends SignSet + case object NotZer extends SignSet + case object PosZer extends SignSet + + def subsetOf(a: SignSet, b: SignSet): Boolean = (a, b) match { + case (None, _) => true + case (_, Any) => true + case (Neg, NegZer | NotZer) => true + case (Zer, NegZer | PosZer) => true + case (Pos, NotZer | PosZer) => true + case _ => false + } +} \ No newline at end of file diff --git a/frontends/benchmarks/extraction/valid/PatternAlternative2.scala b/frontends/benchmarks/extraction/valid/PatternAlternative2.scala new file mode 100644 index 000000000..acdf27809 --- /dev/null +++ b/frontends/benchmarks/extraction/valid/PatternAlternative2.scala @@ -0,0 +1,33 @@ +object PatternAlternative2 { + sealed trait Tree + case class Node(left: Tree, right: Tree) extends Tree + case class IntLeaf(value: Int) extends Tree + case class StringLeaf(value: String) extends Tree + case class NoneLeaf() extends Tree + + def containsNoneLeaf(tree: Tree): Boolean = { + tree match { + case Node(left, right) => containsNoneLeaf(left) || containsNoneLeaf(right) + case NoneLeaf() => true + case _ => false + } + } + + def containsOnlyBinaryLeaves(tree: Tree): Boolean = { + tree match { + case Node(left, right) => containsOnlyBinaryLeaves(left) && containsOnlyBinaryLeaves(right) + case IntLeaf(v) => v == 0 || v == 1 + case StringLeaf(v) => v == "0" || v == "1" + case _ => true + } + } + + def hasBinaryLeaves(tree: Tree): Boolean = { + require(!containsNoneLeaf(tree) && containsOnlyBinaryLeaves(tree)) + tree match { + case a @ Node(left: (IntLeaf | StringLeaf), right: (IntLeaf | StringLeaf)) => hasBinaryLeaves(left) && hasBinaryLeaves(right) + case b @ (IntLeaf(0 | 1) | StringLeaf("0" | "1")) => true + case _ => false + } + } ensuring { res => res } +} \ No newline at end of file diff --git a/frontends/benchmarks/verification/valid/PatternAlternative.scala b/frontends/benchmarks/verification/valid/PatternAlternative.scala new file mode 100644 index 000000000..7be570355 --- /dev/null +++ b/frontends/benchmarks/verification/valid/PatternAlternative.scala @@ -0,0 +1,33 @@ +object PatternAlternative { + sealed trait Tree + case class Node(left: Tree, right: Tree) extends Tree + case class IntLeaf(value: Int) extends Tree + case class StringLeaf(value: String) extends Tree + case class NoneLeaf() extends Tree + + def containsNoneLeaf(tree: Tree): Boolean = { + tree match { + case Node(left, right) => containsNoneLeaf(left) || containsNoneLeaf(right) + case NoneLeaf() => true + case _ => false + } + } + + def containsOnlyBinaryLeaves(tree: Tree): Boolean = { + tree match { + case Node(left, right) => containsOnlyBinaryLeaves(left) && containsOnlyBinaryLeaves(right) + case IntLeaf(v) => v == 0 || v == 1 + case StringLeaf(v) => v == "0" || v == "1" + case _ => true + } + } + + def hasBinaryLeaves(tree: Tree): Boolean = { + require(!containsNoneLeaf(tree) && containsOnlyBinaryLeaves(tree)) + tree match { + case a @ Node(left: (IntLeaf | StringLeaf), right: (IntLeaf | StringLeaf)) => hasBinaryLeaves(left) && hasBinaryLeaves(right) + case b @ (IntLeaf(0 | 1) | StringLeaf("0" | "1")) => true + case _ => false + } + } ensuring { res => res } +} \ No newline at end of file