From 48c1d6d3a6e67a5f7ddb6cd14085781a1eab5578 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 4 May 2015 15:52:11 +0200
Subject: [PATCH] Set and Map are now implemented in the library and should be
executable
---
library/lang/Map.scala | 15 ++++++---
library/lang/Set.scala | 28 +++++++++-------
.../leon/frontends/scalac/ASTExtractors.scala | 20 ++++++++++++
.../frontends/scalac/CodeExtraction.scala | 32 +++++++++----------
4 files changed, 63 insertions(+), 32 deletions(-)
diff --git a/library/lang/Map.scala b/library/lang/Map.scala
index fec773142..289ca7ad4 100644
--- a/library/lang/Map.scala
+++ b/library/lang/Map.scala
@@ -4,13 +4,18 @@ import leon.annotation._
object Map {
@library
def empty[A,B] = Map[A,B]()
+
+ @ignore
+ def apply[A,B](elems: (A,B)*) = {
+ new Map[A,B](scala.collection.immutable.Map[A,B](elems : _*))
+ }
}
@ignore
-case class Map[A, B](elems: (A, B)*) {
- def apply(k: A): B = ???
- def ++(b: Map[A, B]): Map[A,B] = ???
- def updated(k: A, v: B): Map[A,B] = ???
- def contains(a: A): Boolean = ???
+class Map[A, B](val theMap: scala.collection.immutable.Map[A,B]) {
+ def apply(k: A): B = theMap.apply(k)
+ def ++(b: Map[A, B]): Map[A,B] = new Map (theMap ++ b.theMap)
+ def updated(k: A, v: B): Map[A,B] = new Map(theMap.updated(k, v))
+ def contains(a: A): Boolean = theMap.contains(a)
def isDefinedAt(a: A): Boolean = contains(a)
}
diff --git a/library/lang/Set.scala b/library/lang/Set.scala
index 086b31988..af27ec7ae 100644
--- a/library/lang/Set.scala
+++ b/library/lang/Set.scala
@@ -2,18 +2,24 @@ package leon.lang
import leon.annotation._
object Set {
- @library
- def empty[T] = Set[T]()
+ @library
+ def empty[T] = Set[T]()
+
+ @ignore
+ def apply[T](elems: T*) = {
+ new Set[T](scala.collection.immutable.Set[T](elems : _*))
+ }
}
@ignore
-case class Set[T](elems: T*) {
- def +(a: T): Set[T] = ???
- def ++(a: Set[T]): Set[T] = ???
- def -(a: T): Set[T] = ???
- def --(a: Set[T]): Set[T] = ???
- def contains(a: T): Boolean = ???
- def isEmpty: Boolean = ???
- def subsetOf(b: Set[T]): Boolean = ???
- def &(a: Set[T]): Set[T] = ???
+class Set[T](val theSet: scala.collection.immutable.Set[T]) {
+ def +(a: T): Set[T] = new Set[T](theSet + a)
+ def ++(a: Set[T]): Set[T] = new Set[T](theSet ++ a.theSet)
+ def -(a: T): Set[T] = new Set[T](theSet - a)
+ def --(a: Set[T]): Set[T] = new Set[T](theSet -- a.theSet)
+ def contains(a: T): Boolean = theSet.contains(a)
+ def isEmpty: Boolean = theSet.isEmpty
+ def subsetOf(b: Set[T]): Boolean = theSet.subsetOf(b.theSet)
+ def &(a: Set[T]): Set[T] = new Set[T](theSet & a.theSet)
}
+
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index f7a40b953..e83f51196 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -861,6 +861,26 @@ trait ASTExtractors {
}
}
+ object ExFiniteSet {
+ def unapply(tree: Apply): Option[(Tree,List[Tree])] = tree match {
+ case Apply(TypeApply(ExSelected("Set", "apply"), Seq(tpt)), args) =>
+ Some(tpt, args)
+ case Apply(TypeApply(ExSelected("leon", "lang", "Set", "apply"), Seq(tpt)), args) =>
+ Some(tpt, args)
+ case _ => None
+ }
+ }
+
+ object ExFiniteMap {
+ def unapply(tree: Apply): Option[(Tree, Tree, List[Tree])] = tree match {
+ case Apply(TypeApply(ExSelected("Map", "apply"), Seq(tptFrom, tptTo)), args) =>
+ Some((tptFrom, tptTo, args))
+ case Apply(TypeApply(ExSelected("leon", "lang", "Map", "apply"), Seq(tptFrom, tptTo)), args) =>
+ Some((tptFrom, tptTo, args))
+ case _ => None
+ }
+ }
+
object ExFiniteMultiset {
def unapply(tree: Apply): Option[(Tree,List[Tree])] = tree match {
case Apply(
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 03f1d1778..9e34f76b2 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -917,7 +917,7 @@ trait CodeExtraction extends ASTExtractors {
e.emit()
//val pos = if (body0.pos == NoPosition) NoPosition else leonPosToScalaPos(body0.pos.source, funDef.getPos)
if (ctx.findOptionOrDefault(ExtractionPhase.optStrictCompilation)) {
- reporter.error(funDef.getPos, "Function "+funDef.id.name+" could not be extracted. (Forgot @extern ?)")
+ reporter.error(funDef.getPos, "Function "+funDef.id.name+" could not be extracted. The function likely uses features not supported by Leon.")
} else {
reporter.warning(funDef.getPos, "Function "+funDef.id.name+" is not fully unavailable to Leon.")
}
@@ -1397,25 +1397,25 @@ trait CodeExtraction extends ASTExtractors {
Forall(vds, exBody)
- case ExCaseClassConstruction(tpt, args) =>
- extractType(tpt) match {
- case cct: CaseClassType =>
- CaseClass(cct, args.map(extractTree))
+ case ExFiniteMap(tptFrom, tptTo, args) =>
+ val singletons: Seq[(LeonExpr, LeonExpr)] = args.collect {
+ case ExTuple(tpes, trees) if trees.size == 2 =>
+ (extractTree(trees(0)), extractTree(trees(1)))
+ }
- case SetType(a) =>
- finiteSet(args.map(extractTree).toSet, a)
+ if (singletons.size != args.size) {
+ outOfSubsetError(tr, "Some map elements could not be extracted as Tuple2")
+ }
- case MapType(a, b) =>
- val singletons: Seq[(LeonExpr, LeonExpr)] = args.collect {
- case ExTuple(tpes, trees) if trees.size == 2 =>
- (extractTree(trees(0)), extractTree(trees(1)))
- }
+ finiteMap(singletons, extractType(tptFrom), extractType(tptTo))
- if (singletons.size != args.size) {
- outOfSubsetError(tr, "Some map elements could not be extracted as Tuple2")
- }
+ case ExFiniteSet(tpt, args) =>
+ finiteSet(args.map(extractTree).toSet, extractType(tpt))
- finiteMap(singletons, a, b)
+ case ExCaseClassConstruction(tpt, args) =>
+ extractType(tpt) match {
+ case cct: CaseClassType =>
+ CaseClass(cct, args.map(extractTree))
case _ =>
outOfSubsetError(tr, "Construction of a non-case class.")
--
GitLab