Fix case-study

testcases/case-studies/Lambda.scala

@@ -9,26 +9,21 @@ object Lang {
   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
+  case class Param(k : Int) extends Type
+  case class TFunction(from: Type, to: Type) extends Type
+  //case class TRecord(fields: Map[Id, Type]) extends Type
 }
 
 
@@ -45,15 +40,9 @@ object TypeChecker {
           None()
         }
 
-      case _: IntLit =>
-        Some(TInt)
-
-      case _: BoolLit =>
-        Some(TBool)
-
       case App(f, arg) =>
         typeOf(f, None(), env) match {
-          case Some(TApp(from, to)) =>
+          case Some(TFunction(from, to)) =>
             typeOf(arg, Some(from), env) match {
               case Some(_) => Some(to)
               case _ => None()
@@ -63,10 +52,10 @@ object TypeChecker {
       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 (Some(TFunction(from, to)), Some(to2)) if (from == tpe) && (to == to2) =>
+            Some(TFunction(tpe, to2))
           case (None(), Some(to2)) =>
-            Some(TApp(tpe, to2))
+            Some(TFunction(tpe, to2))
           case _ =>
             None()
         }
@@ -82,6 +71,10 @@ object TypeChecker {
   def typeChecks(e: Expr): Boolean = {
     typeOf(e, None(), Map[Id, Type]()).isDefined
   }
+
+  def typeOf(e: Expr): Option[Type] = {
+    typeOf(e, None(), Map[Id, Type]())
+  }
 }
 
 object Evaluator {
@@ -111,11 +104,38 @@ object Evaluator {
 object Main {
   import Lang._
   import Evaluator._
+  import TypeChecker._
+
+  def synthesize_identity() : Expr = {
+    choose { (e : Expr) =>
+      val t_identity : Type = TFunction(Param(1), Param(1))
+      typeOf(e) == Some(t_identity)
+    }
+  }
+
+  def synthesize_K() : Expr = {
+    choose { (e : Expr) =>
+      val t1 : Type = TFunction(Param(1), TFunction(Param(2), Param(1)))
+      typeOf(e) == Some(t1)
+    }
+  }
+  def synthesize_K2() : Expr = {
+    choose { (e : Expr) =>
+      val t1 : Type = TFunction(Param(1), TFunction(Param(2), Param(2)))
+      typeOf(e) == Some(t1)
+    }
+  }
 
-  def test() : Expr = {
-    val x = Var(Id(0))
-    val y = Var(Id(1))
 
-    eval(App(Abs(Id(0), TInt, x), IntLit(42)))
+  def synthesize_S() : Expr = {
+    choose { (e : Expr) =>
+      val tz = Param(1)
+      val ty = TFunction(Param(1), Param(2))
+      val tx = TFunction(Param(1), TFunction(Param(2), Param(3)))
+      val t1 : Type = TFunction(tx,
+                        TFunction(ty, 
+                          TFunction(tz, Param(3))))
+      typeOf(e) == Some(t1)
+    }
   }
 }