From 954287265bc84fa7ba96f740782fbc4d84bcc393 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Fri, 14 Mar 2014 14:15:19 +0100
Subject: [PATCH] Fix case-study
---
testcases/case-studies/Lambda.scala | 64 +++++++++++++++++++----------
1 file changed, 42 insertions(+), 22 deletions(-)
diff --git a/testcases/case-studies/Lambda.scala b/testcases/case-studies/Lambda.scala
index f268a9c2f..ecc82053d 100644
--- a/testcases/case-studies/Lambda.scala
+++ b/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)
+ }
}
}
--
GitLab