From 8b5a1abd803acbc954703f67a45a6663ec631904 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 20 Oct 2014 16:58:55 +0100
Subject: [PATCH] Literal patterns
---
.../leon/frontends/scalac/CodeExtraction.scala | 5 +++++
src/main/scala/leon/purescala/FunctionClosure.scala | 1 +
src/main/scala/leon/purescala/PrettyPrinter.scala | 4 ++++
src/main/scala/leon/purescala/ScopeSimplifier.scala | 2 ++
src/main/scala/leon/purescala/TreeOps.scala | 13 +++++++++++++
src/main/scala/leon/purescala/Trees.scala | 9 +++++++--
.../synthesis/heuristics/ADTLongInduction.scala | 2 +-
7 files changed, 33 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index b79616a39..fee0e7e4b 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -913,6 +913,11 @@ trait CodeExtraction extends ASTExtractors {
outOfSubsetError(a, "Invalid type "+a.tpe+" for .isInstanceOf")
}
+ case ExInt32Literal(i) => (LiteralPattern(binder, IntLiteral(i)), dctx)
+ case ExBooleanLiteral(b) => (LiteralPattern(binder, BooleanLiteral(b)), dctx)
+ case ExUnitLiteral() => (LiteralPattern(binder, UnitLiteral()), dctx)
+ case ExStringLiteral(s) => (LiteralPattern(binder, StringLiteral(s)), dctx)
+
case _ =>
outOfSubsetError(p, "Unsupported pattern: "+p.getClass)
}
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index c80deca87..20058923c 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -177,6 +177,7 @@ object FunctionClosure extends TransformationPhase {
case WildcardPattern(binder) => WildcardPattern(binder.map(id2freshId(_)))
case CaseClassPattern(binder, caseClassDef, subPatterns) => CaseClassPattern(binder.map(id2freshId(_)), caseClassDef, subPatterns.map(freshIdInPat(_, id2freshId)))
case TuplePattern(binder, subPatterns) => TuplePattern(binder.map(id2freshId(_)), subPatterns.map(freshIdInPat(_, id2freshId)))
+ case LiteralPattern(binder, lit) => LiteralPattern(binder.map(id2freshId(_)), lit)
}
//filter the list of constraints, only keeping those relevant to the set of variables
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index f48d424aa..bc9e2fd88 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -414,6 +414,10 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
ob.foreach { b => p"$b @ " }
p"($subps)"
+ case LiteralPattern(ob, lit) =>
+ ob foreach { b => p"$b @ " }
+ p"$lit"
+
// Types
case Untyped => p"<untyped>"
case UnitType => p"Unit"
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index 91c6afd02..238d6c720 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -103,6 +103,8 @@ class ScopeSimplifier extends Transformer {
CaseClassPattern(newBinder, ccd, newSubPatterns)
case TuplePattern(b, sub) =>
TuplePattern(newBinder, newSubPatterns)
+ case LiteralPattern(_, lit) =>
+ LiteralPattern(newBinder, lit)
}
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 8e8b831ec..4bd86173f 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -403,6 +403,7 @@ object TreeOps {
case WildcardPattern(Some(b)) => WildcardPattern(Some(sm(b)))
case TuplePattern(ob, sps) => TuplePattern(ob.map(sm(_)), sps.map(rewritePattern(_, sm)))
case CaseClassPattern(ob, ccd, sps) => CaseClassPattern(ob.map(sm(_)), ccd, sps.map(rewritePattern(_, sm)))
+ case LiteralPattern(Some(bind), lit) => LiteralPattern(Some(sm(bind)), lit)
case other => other
}
@@ -694,6 +695,7 @@ object TreeOps {
val subTests = subps.zipWithIndex.map{case (p, i) => rec(TupleSelect(in, i+1).setType(tpes(i)), p)}
And(bind(ob, in) +: subTests)
}
+ case LiteralPattern(ob,lit) => And(Equals(in,lit), bind(ob,in))
}
}
@@ -727,6 +729,8 @@ object TreeOps {
case None => map
}
}
+ case LiteralPattern(None, lit) => Map()
+ case LiteralPattern(Some(id), lit) => Map(id -> in)
}
def rewritePM(e: Expr) : Option[Expr] = e match {
@@ -1081,6 +1085,7 @@ object TreeOps {
WildcardPattern(simplerBinder(ob))
case TuplePattern(ob, patterns) =>
TuplePattern(simplerBinder(ob), patterns map simplifyPattern)
+ case LiteralPattern(ob,lit) => LiteralPattern(simplerBinder(ob), lit)
case _ =>
p
}
@@ -1119,6 +1124,14 @@ object TreeOps {
} else {
TuplePattern(ob, subs)
}
+ case LiteralPattern(ob, lit) => // TODO: is this correct?
+ if (ob == Some(anchor)) {
+ sys.error("WOOOT: "+to+" <<= "+pat +" on "+anchor)
+ pat
+ } else {
+ LiteralPattern(ob,lit)
+ }
+
}
val newCases = resCases.flatMap { c => c match {
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index c5a648ccc..cc3bd4280 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -169,8 +169,9 @@ object Trees {
case CaseClassPattern(_, cct, _) if cct.classDef != c.classDef => false
case _ => true
}))
- case t: TupleType => new MatchExpr(scrutinee, cases)
- case _ => scala.sys.error("Constructing match expression on non-class type.")
+ case _: TupleType | Int32Type | BooleanType | UnitType => new MatchExpr(scrutinee, cases)
+
+ case _ => scala.sys.error("Constructing match expression on non-supported type.")
}
}
@@ -229,6 +230,10 @@ object Trees {
case class TuplePattern(binder: Option[Identifier], subPatterns: Seq[Pattern]) extends Pattern
+ case class LiteralPattern[T](binder: Option[Identifier], lit : Literal[T]) extends Pattern {
+ val subPatterns = Seq()
+ }
+
/* Propositional logic */
object And {
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
index ca9d99d88..165b3ab66 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
@@ -57,7 +57,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") with Heuristic {
case CaseClassPattern(binder, sccd, sub) =>
CaseClassPattern(binder, sccd, sub.map(unrollPattern(id, cct, withIds) _))
-
+
case _ => on
}
--
GitLab