From d516b3efe6d691c2ffca2c0a0d8c66b81e76e989 Mon Sep 17 00:00:00 2001
From: Mirco Dotta <mirco.dotta@gmail.com>
Date: Wed, 8 Jul 2009 12:45:31 +0000
Subject: [PATCH] Examples from Matcheck.
---
tests/plugin/LambdaEvaluator.scala | 91 +++++++++++++++++++++++++++
tests/plugin/PropositionalLogic.scala | 59 +++++++++++++++++
2 files changed, 150 insertions(+)
create mode 100644 tests/plugin/LambdaEvaluator.scala
create mode 100644 tests/plugin/PropositionalLogic.scala
diff --git a/tests/plugin/LambdaEvaluator.scala b/tests/plugin/LambdaEvaluator.scala
new file mode 100644
index 000000000..8f0686f76
--- /dev/null
+++ b/tests/plugin/LambdaEvaluator.scala
@@ -0,0 +1,91 @@
+package plugin
+
+/** =================================================
+ * Evaluator for the untyped lambda calculus using
+ * The de Bruijn notation for lambda-terms
+ * =================================================
+ */
+
+import funcheck.lib.Specs._
+
+object LambdaEvaluator {
+ /** =================================================
+ * Lambda Terms for Untyped Lambda Calculus
+ * =================================================
+ */
+ @generator
+ sealed abstract class Term
+ case class App(val t1: Term, val t2: Term) extends Term
+ case class Abstr(val t: Term) extends Term
+ case class Var(val index: Int) extends Term
+ case class Const() extends Term
+
+ def reduce(that: Term): Term = {
+ if(reduceCallByValue(that) == that)
+ that
+ else
+ reduce(reduceCallByValue(that))
+ }
+
+ def isValue(that: Term): Boolean = that.isInstanceOf[Abstr]
+
+ def reduceCallByValue(that: Term): Term = that match {
+
+ case App(Abstr(t1:Term),v2:Term) if isValue(v2) =>
+ subst(t1,1,v2)
+
+ case App(v1: Abstr, t2: Term) if !isValue(t2) =>
+ App(v1, reduceCallByValue(t2))
+
+ case App(t1: Term, t2: Term) if !isValue(t1) =>
+ App(reduceCallByValue(t1), t2)
+
+ case Abstr(t1: Term) => Abstr(reduceCallByValue(t1))
+ case Var(_) => that
+ case Const() => that
+ }
+
+ def subst(t: Term, index: Int, s: Term): Term = t match {
+ case Const() => t
+
+ case Var(y) =>
+ if (y == index) { s } else { t }
+
+ case Abstr(t1: Term) => Abstr(subst(t1,index+1,s))
+
+ case App(t1: Term, t2: Term) =>
+ App(subst(t1,index,s), subst(t2,index,s))
+ }
+
+ // this fails (which is correct!)
+ // counter-example: p._1=Var(13) , p._2 = 13 , p._3 = Const()
+ //forAll[(Term,Int,Term)]{p => p._1 == subst(subst(p._1,p._2,p._3),p._2,p._1)}
+
+
+ def main(args: Array[String]) = {
+ /** =================================================
+ * \\z. (\\y. y (\\x. x)) (\\x. z x)
+ * is in de Bruijn notation
+ * \\ (\\ 1 (\\ 1)) (\\ 2 1)
+ * and it evaluates to:
+ * \\ 2 (\\ 1) that is \\z. z (\\x. x)
+ * =================================================
+ */
+ assert(
+ reduce(
+ Abstr(
+ App(
+ Abstr(App(Var(1), Abstr(Var(1)))),
+ Abstr(App(Var(2),Var(1)))
+ )
+ )
+ )
+ ==
+ Abstr(App(Var(2), Abstr(Var(1))))
+ )
+ }
+
+}
+
+
+
diff --git a/tests/plugin/PropositionalLogic.scala b/tests/plugin/PropositionalLogic.scala
new file mode 100644
index 000000000..a32ba3871
--- /dev/null
+++ b/tests/plugin/PropositionalLogic.scala
@@ -0,0 +1,59 @@
+package plugin
+
+import funcheck.lib.Specs._
+
+object PropositionalLogic {
+
+
+
+ // This crash because there are too many non-terminals, and the automatically
+ // injected generator may end up generating infinite formulas, which produce
+ // java.lang.StackOverflowError
+ @generator
+ sealed abstract class Formula
+ case class And(left: Formula, right: Formula) extends Formula
+ case class Or(left: Formula, right: Formula) extends Formula
+ case class Neg(f: Formula) extends Formula
+ case class True() extends Formula
+ case class False() extends Formula
+ case class Imply(left: Formula,right: Formula) extends Formula
+
+
+
+
+ def desugar(f: Formula): Formula = f match {
+ case True() => f
+ case False() => f
+ case And(left,right) => And(desugar(left),desugar(right))
+ case Or(left,right) => Or(desugar(left),desugar(right))
+ case Neg(f) => Neg(desugar(f))
+ case Imply(left,right) => Or(Neg(desugar(left)),desugar(right))
+ }
+
+ def isDesugared(f: Formula): Boolean = f match {
+ case And(left,right) => isDesugared(left) && isDesugared(right)
+ case Or(left,right) => isDesugared(left) && isDesugared(right)
+ case Neg(f) => isDesugared(f)
+ case True() => true
+ case False() => true
+ case i: Imply => false
+ }
+
+ forAll{f : Formula => isDesugared(f) ==> desugar(f) == f }
+ // the above forAll invariant replaces the below somewhat cummbersome Matcheck spec
+ /** Type refinement: A desugarized formula does not contain an Imply node.
+ This condition must hold recursively over the whole tree
+ */
+ /* constraint (\forall f. f \in DesugaredFormula <-->
+ ( f \in Tru |
+ f \in Flse |
+ (f \in Neg & Neg_getField_f(f) \in DesugaredFormula) |
+ (f \in IOr & IOr_getField_left(f) \in DesugaredFormula & IOr_getField_right(f) \in DesugaredFormula) |
+ (f \in IAnd & IAnd_getField_left(f) \in DesugaredFormula & IAnd_getField_right(f) \in DesugaredFormula)
+ ))
+ */
+
+ def main(args: Array[String]) =
+ assert(isDesugared(desugar(Imply(Imply(True(),False()),False()))))
+}
+
--
GitLab