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

Delete duplicated examples. These are somewhat overlapping with the ones...

Delete duplicated examples. These are somewhat overlapping with the ones defined in tests/plugin/ folder
parent 648a0e46
No related branches found
No related tags found
No related merge requests found
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
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))
}
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))
}
/** =================================================
* 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))))
)
}
/** 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))))
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment