Print TypedFunDef, add 2 case studies

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

testcases/case-studies/Lambda.scala

+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)))
+  }
+}

testcases/case-studies/Sync.scala

+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)
+  }
+}
+