diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala index cb3278c096a7f76c96480e85cb151516cad77cb8..58a86ac6a3ee57f7cd477ed877e06489793c3712 100644 --- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala +++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala @@ -477,6 +477,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int } else { None } + case (LiteralPattern(ob, l1) , l2 : Literal[_]) if l1 == l2 => + Some(obind(ob,l1)) case _ => None } diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala index 6e1a2d0413fa523ae8e4e0c5ee2aaac3595db383..ee74c46b6053943697b74753f07cb3b1e2a49671 100644 --- a/src/main/scala/leon/purescala/TreeOps.scala +++ b/src/main/scala/leon/purescala/TreeOps.scala @@ -1646,6 +1646,10 @@ object TreeOps { } else { (false, Map()) } + + case (LiteralPattern(ob1, lit1), LiteralPattern(ob2,lit2)) => + (ob1.size == ob2.size && lit1 == lit2, (ob1 zip ob2).toMap) + case _ => (false, Map()) } @@ -1789,6 +1793,27 @@ object TreeOps { } } + case BooleanType => + // make sure ps contains either + // - Wildcard or + // - both true and false + (ps exists { _.isInstanceOf[WildcardPattern] }) || { + var found = Set[Boolean]() + ps foreach { + case LiteralPattern(_, BooleanLiteral(b)) => found += b + case _ => () + } + (found contains true) && (found contains false) + } + + case UnitType => + // Anything matches () + !ps.isEmpty + + case Int32Type => + // Can't possibly pattern match against all Ints one by one + ps exists (_.isInstanceOf[WildcardPattern]) + case _ => true } diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeTreeOps.scala index 469b7606b6fdb9756c092e29f740164ab716582d..2f6ff8c36e1caec52bfa29f5c94e2435356b7f83 100644 --- a/src/main/scala/leon/purescala/TypeTreeOps.scala +++ b/src/main/scala/leon/purescala/TypeTreeOps.scala @@ -245,6 +245,10 @@ object TypeTreeOps { (WildcardPattern(newOb), (ob zip newOb).toMap) + case (LiteralPattern(ob, lit), expType) => + val newOb = ob.map(id => freshId(id, expType)) + (LiteralPattern(newOb,lit), (ob zip newOb).toMap) + case _ => sys.error("woot!?") }