From 33a68e8bcef7002c4c9ecd081b40e70551857849 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com> Date: Sat, 16 Apr 2016 21:59:23 +0200 Subject: [PATCH] unit test to make sure contract of Extractors is clear --- .../leon/unit/purescala/ExtractorsSuite.scala | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala b/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala index 4e7c7d40a..787304520 100644 --- a/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala +++ b/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala @@ -25,6 +25,27 @@ class ExtractorsSuite extends FunSuite with ExpressionsDSL { assert(e3 === e4) } + test("Extractors do not magically change the syntax") { + val e1 = Equals(bi(1), bi(1)) + val e2 = e1 match { + case Operator(es, builder) => builder(es) + } + assert(e1 === e2) + + val e3 = Equals(BooleanLiteral(true), BooleanLiteral(false)) + val e4 = e3 match { + case Operator(es, builder) => builder(es) + } + assert(e3 === e4) + + val e5 = TupleSelect(Tuple(Seq(bi(1), bi(2))), 2) + val e6 = e5 match { + case Operator(es, builder) => builder(es) + } + assert(e5 === e6) + } + + test("Extractors of NonemptyArray with sparse elements") { val a1 = NonemptyArray(Map(0 -> x, 3 -> y, 5 -> z), Some((BigInt(0), BigInt(10)))) val a2 = a1 match { -- GitLab