Skip to content
Snippets Groups Projects
Commit d516b3ef authored by Mirco Dotta's avatar Mirco Dotta
Browse files

Examples from Matcheck.

parent e53d017e
No related branches found
No related tags found
No related merge requests found
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))))
)
}
}
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()))))
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment