diff --git a/examples/funpm/bst/BST1.scala b/examples/funpm/bst/BST1.scala
deleted file mode 100644
index 769aa7a7a10fad5ebc00c4d8b1cf68cb5d87d60a..0000000000000000000000000000000000000000
--- a/examples/funpm/bst/BST1.scala
+++ /dev/null
@@ -1,21 +0,0 @@
-package funpm.bst
-
-object BST1 extends Application {
-
- sealed abstract case class BST() {
- // patterns are exhaustive, disjoint and all reachable
- def contains(key: Int): Boolean = this match {
- case Node(left,value,_) if key < value => left.contains(key)
- case Node(_,value,right) if key > value => right.contains(key)
- case Node(_,value, _) if key == value => true
- case e => false
- }
- }
-
- case class Empty() extends BST
- case class Node(val left: BST, val value: Int, val right: BST) extends BST
-
-
- // main, only for testing purposes
- assert(Node(Node(Empty(),3,Empty()),5,Empty()).contains(3))
-}
\ No newline at end of file
diff --git a/examples/funpm/bst/BST2.scala b/examples/funpm/bst/BST2.scala
deleted file mode 100644
index 3ceedc213040233f75871cab7daf55d80aa8508d..0000000000000000000000000000000000000000
--- a/examples/funpm/bst/BST2.scala
+++ /dev/null
@@ -1,28 +0,0 @@
-package funpm.bst
-
-object BST2 extends Application {
-
- sealed abstract case class BST() {
- // patterns are exhaustive, disjoint and all reachable
- def contains(key: Int): Boolean = this match {
- case Node(_,value, _) if key != value =>
- this match {
- case Node(left,value, _) if key < value => left.contains(key)
- case Node(_,value, right) if key > value => right.contains(key)
- }
- case Node(_,value, _) if key == value => true
- case e => false
- }
- }
-
- case class Empty() extends BST
- case class Node(val left: BST, val value: Int, val right: BST) extends BST
-
-
- // main, only for testing purposes
- assert(Node(Node(Empty(),3,Empty()),5,Empty()).contains(3))
-}
-
-
-
-
diff --git a/examples/funpm/bst/BST3.scala b/examples/funpm/bst/BST3.scala
deleted file mode 100644
index 707d89725728be89068c48777a82bf22026c7edc..0000000000000000000000000000000000000000
--- a/examples/funpm/bst/BST3.scala
+++ /dev/null
@@ -1,29 +0,0 @@
-package funpm.bst
-
-object BST3 extends Application {
-
- sealed abstract case class BST() {
- // patterns are exhaustive, disjoint and all reachable
- def contains(key: Int): Boolean = this match {
- case Node(_,value,_) =>
- if(key == value) {
- true
- }
- else {
- this match {
- case Node(left,value,_) if key < value => left.contains(key)
- case Node(_,value,right) if key > value => right.contains(key)
- }
- }
- case e => false
- }
- }
-
- case class Empty() extends BST
- case class Node(val left: BST, val value: Int, val right: BST) extends BST
-
-
-
- // main, only for testing purposes
- assert(Node(Node(Empty(),3,Empty()),5,Empty()).contains(3))
-}
diff --git a/examples/funpm/lambda/LambdaEvaluator.scala b/examples/funpm/lambda/LambdaEvaluator.scala
deleted file mode 100644
index 2096ac82851753f5285356486d569dff0a71670c..0000000000000000000000000000000000000000
--- a/examples/funpm/lambda/LambdaEvaluator.scala
+++ /dev/null
@@ -1,129 +0,0 @@
-/** =================================================
- * Evaluator for the untyped lambda calculus using
- * The de Bruijn notation for lambda-terms
- * =================================================
- */
-
-package funpm.lambda
-
-/** =================================================
- * Lambda Terms for Untyped Lambda Calculus
- * =================================================
- */
-
-sealed abstract case class Term() {
- def isSame(t: Term): Boolean = this match {
- case Const => true
-
- case Var(x) => t match {
- case Var(y) => x == y
- case _ if !t.isInstanceOf[Var] => false
- }
-
- case Abstr(t1) => t match {
- case Abstr(t2) => t1.isSame(t2)
- case _ if !t.isInstanceOf[Abstr] => false
- }
-
- case App(t1,t2) => t match {
- case App(t21,t22) => t1.isSame(t21) && t2.isSame(t22)
- case _ if !t.isInstanceOf[App] => false
- }
- }
-}
-
-case object Const extends Term
-case class Var(val index: Int) extends Term
-case class Abstr(val t: Term) extends Term
-case class App(val t1: Term, val t2: Term) extends Term
-
-/** =================================================
- * Lambda Terms Evaluator
- * CallByValue
- * =================================================
- */
-
-
-class Eval {
-
- def reduce(t: Term): Term =
- if(this.reduceCallByValue(t).isSame(t)) { t }
- else { this.reduce(this.reduceCallByValue(t)) }
-
- def isValue(t: Term): Boolean =
- /* postcondition t \in Abstr <--> res == true
- */
- t.isInstanceOf[Abstr]
-
- def reduceCallByValue(t: Term): Term = (t : Term) match {
-
- case App(Abstr(t1:Term),v2:Term) if this.isValue(v2) =>
- this.subst(t1,1,v2)
-
- case App(v1: Abstr, t2: Term) if !this.isValue(t2) =>
- App(v1, this.reduceCallByValue(t2))
-
- case App(t1: Term, t2: Term) if !this.isValue(t1) =>
- App(this.reduceCallByValue(t1), t2)
-
- case Abstr(t1: Term) => Abstr(this.reduceCallByValue(t1))
- case Var(_) => t
- case Const => t
- }
-
- 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(this.subst(t1,index+1,s))
-
- case App(t1: Term, t2: Term) =>
- App(this.subst(t1,index,s), this.subst(t2,index,s))
- }
-
-}
-
-/** =================================================
- * Printer for Lambda Terms
- * =================================================
- */
-
-class Printer {
- def prompt(t: Term): Unit = {
- printer(t)
- println
- }
- def printer(t: Term): Unit = t match {
- case Var(x) => print(x)
- case Abstr(t) => print("\\. ("); printer(t); print(")")
- case App(t1,t2) => print("("); printer(t1); print(") ");
- print("("); printer(t2); print(") ");
- }
-}
-
-
-/** =================================================
- * \\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)
- * =================================================
- */
-object LambdaEvaluator extends Application {
-
- assert(
- new Eval().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/examples/funpm/logic/PropositionalLogic.scala b/examples/funpm/logic/PropositionalLogic.scala
deleted file mode 100644
index 0eeae80c1a9d5c9df98a70058a19704c087b40b3..0000000000000000000000000000000000000000
--- a/examples/funpm/logic/PropositionalLogic.scala
+++ /dev/null
@@ -1,57 +0,0 @@
-
-/** 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)
- ))
-*/
-
-package funpm.logic
-
-sealed abstract case class IFormula()
-case class IAnd(val left: IFormula, val right: IFormula) extends IFormula
-case class IOr(val left: IFormula, val right: IFormula) extends IFormula
-case class Neg(val f: IFormula) extends IFormula
-case object Tru extends IFormula
-case object Flse extends IFormula
-case class IImply(val left: IFormula, val right: IFormula) extends IFormula
-
-
-object Desugar {
-
- def apply(f: IFormula): IFormula =
- /* postcondition res \in DesugaredFormula */
- f match {
- case Tru => f
- case Flse => f
- case IAnd(left,right) => IAnd(apply(left),apply(right))
- case IOr(left,right) => IOr(apply(left),apply(right))
- case Neg(f) => Neg(apply(f))
- case IImply(left,right) => IOr(Neg(this.apply(left)),this.apply(right))
- }
-
-
- /**
- This examples is interesting because uses method desugarize postcondition
- in order to prove completeness of the PM.
- */
- def isDesugared(f: IFormula): Boolean = apply(f) match {
- case IAnd(left,right) => isDesugared(left) && isDesugared(right)
- case IOr(left,right) => isDesugared(left) && isDesugared(right)
- case Neg(f) => isDesugared(f)
- case Tru => true
- case Flse => true
- }
-
-
-}
-
-object PropositionalLogic extends Application {
- // main
- assert(Desugar.isDesugared(Desugar.apply(IImply(IImply(Tru,Flse),Flse))))
-}