Skip to content
Snippets Groups Projects
Commit 59742127 authored by Viktor Kuncak's avatar Viktor Kuncak
Browse files

more on tree path example

parent 81fc0d06
No related branches found
No related tags found
No related merge requests found
...@@ -10,6 +10,14 @@ object Tree { ...@@ -10,6 +10,14 @@ object Tree {
case object Left extends Dir case object Left extends Dir
case object Right extends Dir case object Right extends Dir
def nil[A]: List[A] = Nil[A]
def cons[A](x: A, lst: List[A]): List[A] = Cons[A](x,lst)
def some[A](x: A): Option[A] = Some[A](x)
def none[A]: Option[A] = None[A]
case class Path(p: List[Dir])
def pnil = Path(nil)
def inside(t: Tree, subtree: Tree): Boolean = { def inside(t: Tree, subtree: Tree): Boolean = {
if (t==subtree) true if (t==subtree) true
else { else {
...@@ -20,25 +28,21 @@ object Tree { ...@@ -20,25 +28,21 @@ object Tree {
} }
} }
def lookup(t: Tree, path : List[Dir]): Option[Tree] = { def lookup(t: Tree, path : Path): Option[Tree] = {
(t,path) match { (t,path.p) match {
case (_,Nil()) => Some[Tree](t) case (_,Nil()) => some(t)
case (Empty,_) => None[Tree]() case (Empty,_) => none
case (Node(left,_,_), Cons(Left,rest)) => lookup(left,rest) case (Node(left,_,_), Cons(Left,rest)) => lookup(left,Path(rest))
case (Node(_,_,right), Cons(Right,rest)) => lookup(right,rest) case (Node(_,_,right), Cons(Right,rest)) => lookup(right,Path(rest))
} }
} }
def nil[A]: List[A] = Nil[A]
def cons[A](x: A, lst: List[A]): List[A] = Cons[A](x,lst)
def some[A](x: A): Option[A] = Some[A](x)
// Function find1 has a counterexample. // Function find1 has a counterexample.
def find1(t: Tree, subtree: Tree): Option[List[Dir]] = ({ def find1(t: Tree, subtree: Tree): Option[Path] = ({
if (t==subtree) some(nil[Dir]) if (t==subtree) some(pnil)
else { else {
t match { t match {
case Empty => None[List[Dir]] case Empty => none
case Node(left,_,right) => { case Node(left,_,right) => {
find1(left,subtree) match { find1(left,subtree) match {
case None() => find1(right,subtree) case None() => find1(right,subtree)
...@@ -47,40 +51,63 @@ object Tree { ...@@ -47,40 +51,63 @@ object Tree {
} }
} }
} }
}: Option[List[Dir]]).ensuring((res:Option[List[Dir]]) => (res match { }: Option[Path]).ensuring(res => (res match {
case None() => !inside(t, subtree) case None() => !inside(t, subtree)
case Some(path) => lookup(t, path)==Some(subtree) case Some(path) => lookup(t, path)==Some(subtree)
})) }))
// Function find is correct // Function find is correct
def find(t: Tree, subtree: Tree): Option[List[Dir]] = ({ def find(t: Tree, subtree: Tree): Option[Path] = ({
if (t==subtree) some(nil[Dir]) if (t==subtree) some(pnil)
else { else {
t match { t match {
case Empty => None[List[Dir]] case Empty => none
case Node(left,_,right) => { case Node(left,_,right) => {
find(left,subtree) match { find(left,subtree) match {
case None() => { find(right,subtree) match { case None() => { find(right,subtree) match {
case None() => None() case None() => None()
case Some(path) => Some(cons(Right,path)) case Some(Path(p)) => Some(Path(cons(Right,p)))
}} }}
case Some(path) => Some(cons(Left, path)) case Some(Path(p)) => Some(Path(cons(Left, p)))
} }
} }
} }
} }
}: Option[List[Dir]]).ensuring((res:Option[List[Dir]]) => (res match { }: Option[Path]).ensuring(res => (res match {
case None() => !inside(t, subtree) case None() => !inside(t, subtree)
case Some(path) => lookup(t, path)==Some(subtree) case Some(path) => lookup(t, path)==Some(subtree)
})) }))
def replace(t: Tree, path: List[Dir], newT: Tree): Tree = { def replace(t: Tree, path: Path, newT: Tree): Tree = {
require(lookup(t, path) != None[Tree]()) require(lookup(t, path) != none[Tree])
(t,path) match { (t,path.p) match {
case (_,Nil()) => newT case (_,Nil()) => newT
case (Node(left,v,right), Cons(Left, rest)) => Node(replace(left,rest, newT), v, right) case (Node(left,v,right), Cons(Left, rest)) => Node(replace(left,Path(rest), newT), v, right)
case (Node(left,v,right), Cons(Right,rest)) => Node(left, v, replace(right, rest, newT)) case (Node(left,v,right), Cons(Right,rest)) => Node(left, v, replace(right, Path(rest), newT))
} }
} ensuring(res => lookup(res, path)==Some(newT)) } ensuring(res => lookup(res, path)==some(newT))
case class Flat(trees: List[(Path, Tree)])
def fnil = Flat(nil)
def subtrees(t: Tree): Flat = {
t match {
case Empty => fnil
case Node(left,v,right) =>
Flat(addLeft(subtrees(left)).trees ++ ((pnil,t) :: addRight(subtrees(right)).trees))
}
}
def addLeft(f: Flat): Flat = {
f.trees match {
case Nil() => fnil
case (p,t) :: trees1 => Flat((Path(Left::p.p),t) :: addLeft(Flat(trees1)).trees)
}
}
def addRight(f: Flat): Flat = {
f.trees match {
case Nil() => fnil
case (p,t) :: trees1 => Flat((Path(Right::p.p),t) :: addRight(Flat(trees1)).trees)
}
}
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment