diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 9e07420a2c0bc424460356f414c4c6380e41d28b..f5704454d2677303f9bbe70241f3a215bbcc9f4c 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -472,6 +472,11 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case th: This =>
sb.append("this")
+ case tfd: TypedFunDef =>
+ sb.append("typed def ")
+ pp(tfd.id, p)
+ ppNary(tfd.tps, "[", ", ", "]")
+
case fd: FunDef =>
for(a <- fd.annotations) {
ind
diff --git a/testcases/case-studies/Lambda.scala b/testcases/case-studies/Lambda.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f268a9c2f94f02c365553034f250d841bb801dd3
--- /dev/null
+++ b/testcases/case-studies/Lambda.scala
@@ -0,0 +1,121 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Lang {
+ case class Id(v: Int)
+
+ def isLiteral(l: Expr) = l match {
+ case _: Var => true
+ case _: Abs => true
+ case _: BoolLit => true
+ case _: IntLit => true
+ //case _: Record => true
+ case _ => false
+ }
+
+ abstract class Expr
+ case class Var(id: Id) extends Expr
+ case class IntLit(v: Int) extends Expr
+ case class BoolLit(v: Boolean) extends Expr
+ case class App(f: Expr, arg: Expr) extends Expr
+ case class Abs(b: Id, tpe: Type, e: Expr) extends Expr
+ //case class Record(fields: Map[Id, Expr]) extends Expr
+ //case class Select(r: Expr, f: Var) extends Expr
+
+ abstract class Type
+ case object TBool extends Type
+ case object TInt extends Type
+ case class TApp(from: Type, to: Type) extends Type
+ //case class TRecord(fields: Map[Id, Type]) extends Type
+}
+
+
+
+object TypeChecker {
+ import Lang._
+
+ def typeOf(e: Expr, exp: Option[Type], env: Map[Id, Type]): Option[Type] = {
+ val t: Option[Type] = e match {
+ case Var(id) =>
+ if (env contains id) {
+ Some(env(id))
+ } else {
+ None()
+ }
+
+ case _: IntLit =>
+ Some(TInt)
+
+ case _: BoolLit =>
+ Some(TBool)
+
+ case App(f, arg) =>
+ typeOf(f, None(), env) match {
+ case Some(TApp(from, to)) =>
+ typeOf(arg, Some(from), env) match {
+ case Some(_) => Some(to)
+ case _ => None()
+ }
+ case _ => None()
+ }
+ case Abs(id, tpe, e) =>
+ val nenv = env.updated(id, tpe)
+ (exp, typeOf(e, None(), nenv)) match {
+ case (Some(TApp(from, to)), Some(to2)) if (from == tpe) && (to == to2) =>
+ Some(TApp(tpe, to2))
+ case (None(), Some(to2)) =>
+ Some(TApp(tpe, to2))
+ case _ =>
+ None()
+ }
+ }
+
+ if(exp.orElse(t) == t) {
+ t
+ } else {
+ None()
+ }
+ }
+
+ def typeChecks(e: Expr): Boolean = {
+ typeOf(e, None(), Map[Id, Type]()).isDefined
+ }
+}
+
+object Evaluator {
+ import Lang._
+ import TypeChecker._
+
+ def subst(e: Expr, t: (Id, Expr)): Expr = e match {
+ case Var(id) if id == t._1 => t._2
+ case App(f, arg) => App(subst(f, t), subst(arg, t))
+ case Abs(b, id, e) => Abs(b, id, subst(e, t))
+ case _ => e
+ }
+
+ def eval(e: Expr): Expr = {
+ require(typeChecks(e))
+ e match {
+ case App(f, arg) =>
+ eval(f) match {
+ case Abs(id, _, e) => eval(subst(e, id -> arg))
+ case _ => e // stuck
+ }
+ case _ =>
+ e
+ }} ensuring { res => isLiteral(res) }
+}
+
+object Main {
+ import Lang._
+ import Evaluator._
+
+ def test() : Expr = {
+ val x = Var(Id(0))
+ val y = Var(Id(1))
+
+ eval(App(Abs(Id(0), TInt, x), IntLit(42)))
+ }
+}
diff --git a/testcases/case-studies/Sync.scala b/testcases/case-studies/Sync.scala
new file mode 100644
index 0000000000000000000000000000000000000000..abb9adea549342b3e3783aa53370e9eb7ab3c3c6
--- /dev/null
+++ b/testcases/case-studies/Sync.scala
@@ -0,0 +1,95 @@
+import leon.annotation._
+import leon.lang._
+import leon.collection._
+
+case class Entry(id: Int, version: Int, versionSynced: Int, f1: Int, f2: Int) {
+ def update(f1: Int, f2: Int): Entry = {
+ Entry(id, version+1, versionSynced, f1, f2)
+ }
+ def markSynced = {
+ Entry(id, version, version, f1, f2)
+ } ensuring { _.isSynced }
+
+ def isSynced = {
+ version == versionSynced
+ }
+}
+
+object Sync {
+ def idSorted(l: List[Entry]): Boolean = l match {
+ case Cons(v1, Cons(v2, xs)) => v1.id < v2.id && idSorted(Cons(v2, xs))
+ case _ => true
+ }
+
+ // Raw content (ignoring version/versionSynced)
+ def content(l: List[Entry]): Set[(Int, Int, Int)] = l match {
+ case Cons(h, t) => Set((h.id, h.f1, h.f2)) ++ content(t)
+ case Nil() => Set()
+ }
+
+ def ids(l: List[Entry]): Set[Int] = l match {
+ case Cons(h, t) => Set(h.id) ++ ids(t)
+ case _ => Set()
+ }
+
+ def markSynced(l1: List[Entry]): List[Entry] = {
+ require(idSorted(l1))
+ (l1 match {
+ case Cons(e1, t1) => Cons(e1.markSynced, markSynced(t1))
+ case Nil() => Nil()
+ }) : List[Entry]
+ } ensuring { res =>
+ idSorted(res) &&
+ content(res) == content(l1) &&
+ ids(res) == ids(l1) &&
+ allSynced(res)
+ }
+
+ def allSynced(l1: List[Entry]): Boolean = {
+ l1 match {
+ case Cons(h1, t1) => h1.isSynced && allSynced(t1)
+ case Nil() => true
+ }
+ }
+
+ def sync(v1: List[Entry], v2: List[Entry]): List[Entry] = {
+ require(idSorted(v1) && idSorted(v2))
+
+ ((v1, v2) match {
+ case (Cons(e1, t1), Cons(e2, t2)) =>
+ if (e1.id < e2.id) {
+ Cons(e1.markSynced, sync(t1, v2))
+ } else if (e1.id > e2.id) {
+ Cons(e2.markSynced, sync(v1, t2))
+ } else {
+ if (e1.version > e2.version) {
+ Cons(e1.markSynced, sync(t1, t2))
+ } else {
+ Cons(e2.markSynced, sync(t1, t2))
+ }
+ }
+ case (Nil(), l2) => markSynced(l2)
+ case (l1, Nil()) => markSynced(l1)
+ }): List[Entry]
+
+ } ensuring {
+ res =>
+ idSorted(res) &&
+ (content(res) subsetOf (content(v1) ++ content(v2))) &&
+ (ids(res) == ids(v1) ++ ids(v2)) &&
+ allSynced(res)
+ }
+
+
+ def test() = {
+ val e1 = Entry(1, 1, 0, 1, 1)
+ val e2 = Entry(2, 1, 0, 2, 2)
+ val e3 = Entry(3, 1, 0, 3, 3)
+
+ val l1 = Cons(e1, Cons(e2, Nil()))
+ val l2 = Cons(e2.update(5, 5), Cons(e3, Nil()))
+
+ sync(l1, l2)
+ }
+}
+