From 3ff9805089df60c364836e5d4dcafb0865262b21 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Fri, 15 Nov 2013 20:20:53 +0100
Subject: [PATCH] Add/Fix support for (a: Type) patterns
---
src/main/scala/leon/plugin/CodeExtraction.scala | 9 +++++++--
src/main/scala/leon/purescala/TreeOps.scala | 9 ++++++++-
2 files changed, 15 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index dd71afeec..8e19f1008 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -317,16 +317,21 @@ trait CodeExtraction extends Extractors {
private def extractPattern(p: Tree, binder: Option[Identifier] = None): Pattern = p match {
- case b @ Bind(name, Typed(pat, tpe)) =>
+ case b @ Bind(name, t @ Typed(pat, tpe)) =>
val newID = FreshIdentifier(name.toString).setType(extractType(tpe.tpe))
varSubsts(b.symbol) = (() => Variable(newID))
- extractPattern(pat, Some(newID))
+ extractPattern(t, Some(newID))
case b @ Bind(name, pat) =>
val newID = FreshIdentifier(name.toString).setType(extractType(b.symbol.tpe))
varSubsts(b.symbol) = (() => Variable(newID))
extractPattern(pat, Some(newID))
+ case t @ Typed(Ident(nme.WILDCARD), tpe) if t.tpe.typeSymbol.isCase &&
+ classesToClasses.contains(t.tpe.typeSymbol) =>
+ val cd = classesToClasses(t.tpe.typeSymbol).asInstanceOf[CaseClassDef]
+ InstanceOfPattern(binder, cd)
+
case Ident(nme.WILDCARD) =>
WildcardPattern(binder)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 1d0cb59f3..8371b8f0c 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -691,7 +691,14 @@ object TreeOps {
def rec(in: Expr, pattern: Pattern): Expr = {
pattern match {
case WildcardPattern(ob) => bind(ob, in)
- case InstanceOfPattern(_,_) => scala.sys.error("InstanceOfPattern not yet supported.")
+ case InstanceOfPattern(ob, ct) =>
+ ct match {
+ case _: AbstractClassDef =>
+ bind(ob, in)
+
+ case cd: CaseClassDef =>
+ And(CaseClassInstanceOf(cd, in), bind(ob, in))
+ }
case CaseClassPattern(ob, ccd, subps) => {
assert(ccd.fields.size == subps.size)
val pairs = ccd.fields.map(_.id).toList zip subps.toList
--
GitLab