From 05156cb23657eaf83469ddacc2b7e35e5e8d6e81 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 18 May 2012 17:42:42 +0200
Subject: [PATCH] add a List imperative and use bestRealType
---
src/main/scala/leon/purescala/Trees.scala | 6 +--
testcases/ListImp.scala | 49 +++++++++++++++++++++++
2 files changed, 52 insertions(+), 3 deletions(-)
create mode 100644 testcases/ListImp.scala
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index aff4f7c55..361cbf4d5 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -45,14 +45,14 @@ object Trees {
/* Like vals */
case class Let(binder: Identifier, value: Expr, body: Expr) extends Expr {
binder.markAsLetBinder
- val et = body.getType
+ val et = binder.getType
if(et != Untyped)
setType(et)
}
//same as let, buf for mutable variable declaration
case class LetVar(binder: Identifier, value: Expr, body: Expr) extends Expr {
binder.markAsLetBinder
- val et = body.getType
+ val et = binder.getType
if(et != Untyped)
setType(et)
}
@@ -77,7 +77,7 @@ object Trees {
case class IfExpr(cond: Expr, then: Expr, elze: Expr) extends Expr
case class Tuple(exprs: Seq[Expr]) extends Expr {
- val subTpes = exprs.map(_.getType)
+ val subTpes = exprs.map(_.getType).map(bestRealType)
if(!subTpes.exists(_ == Untyped)) {
setType(TupleType(subTpes))
}
diff --git a/testcases/ListImp.scala b/testcases/ListImp.scala
new file mode 100644
index 000000000..f3887419e
--- /dev/null
+++ b/testcases/ListImp.scala
@@ -0,0 +1,49 @@
+import leon.Utils._
+
+object ListImp {
+
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def size(l: List) : Int = {
+ var r = 0
+ (while(!l.isInstanceOf[Nil]) {
+ r = r+1
+ }) invariant(r >= 0)
+ r
+ } ensuring(res => res >= 0)
+
+ def reverse(l: List): List = {
+ var r: List = Nil()
+ var l2: List = l
+
+ (while(!l2.isInstanceOf[Nil]) {
+ val Cons(head, tail) = l2
+ l2 = tail
+ r = Cons(head, r)
+ }) invariant(content(r) ++ content(l2) == content(l))
+
+ r
+ } ensuring(res => content(res) == content(l))
+
+ def append(l1 : List, l2 : List) : List = {
+ var r: List = l2
+ var tmp: List = reverse(l1)
+
+ (while(!tmp.isInstanceOf[Nil]) {
+ val Cons(head, tail) = tmp
+ tmp = tail
+ r = Cons(head, r)
+ }) invariant(content(r) ++ content(tmp) == content(l1) ++ content(l2))
+
+ r
+ } ensuring(content(_) == content(l1) ++ content(l2))
+
+
+}
--
GitLab