Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add AA Tree and tests #203

Open
wants to merge 11 commits into
base: master
Choose a base branch
from
Open

Add AA Tree and tests #203

Changes from 1 commit
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
434122d
Add AA Tree and tests
hummy123 Dec 12, 2022
7990983
edit project file to include AaTree and tests, add labels for AaTree …
hummy123 Dec 14, 2022
e7e1732
one Expect assertion for each test in AaTreeTest.fs
hummy123 Dec 19, 2022
50d31b6
AAA structure for a couple of more tests
hummy123 Dec 19, 2022
9053d20
AaTree toSeq
hummy123 Dec 19, 2022
8ccd82f
fix incorrect functions in paper by Isabelle HOL proof below: https:/…
hummy123 Jan 2, 2023
dda2bd0
use isEmpty in delete case as in HOL proof
hummy123 Jan 2, 2023
cb72994
Merge branch 'fsprojects:master' into master
hummy123 Jan 2, 2023
56bac48
Merge branch 'fsprojects:master' into master
hummy123 Jan 4, 2023
8d1a93c
fix formatting using FAKE and fix typo in comment
hummy123 Jan 4, 2023
171dd41
fix my own implementation error in AaTree.splitMax (private function
hummy123 Jan 5, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 20 additions & 12 deletions src/FSharpx.Collections.Experimental/AaTree.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,10 @@ module AaTree =
| E -> true
| _ -> false

let private isLeaf = function
| T(_, E, _, R) -> true
| _ -> false

let private sngl = function
| E -> false
| T(_, _, _, E) -> true
Expand All @@ -47,13 +51,6 @@ module AaTree =
| E -> 0
| T(lvt, _, _, _) -> lvt

let private nlvl = function
| T(lvt, _, _, _) as t ->
if sngl t
then (lvt - 1)
else lvt
| _ -> failwith "unexpected nlvl case"

let private skew = function
| T(lvx, T(lvy, a, ky, b), kx, c) when lvx = lvy
-> T(lvx, a, ky, T(lvx, b, kx, c))
Expand All @@ -75,6 +72,15 @@ module AaTree =
then split <| (skew <| T(h, l, v, insert item r))
else node

(* nlvl function fixed according to Isabelle HOL prrof below: *)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

prrof -> proof

(* https://isabelle.in.tum.de/library/HOL/HOL-Data_Structures/AA_Set.html#:~:text=text%E2%80%B9In%20the%20paper%2C%20the%20last%20case%20of%20%5C%3C%5Econst%3E%E2%80%B9adjust%E2%80%BA%20is%20expressed%20with%20the%20help%20of%20an%0Aincorrect%20auxiliary%20function%20%5Ctexttt%7Bnlvl%7D. *)
let private nlvl = function
| T(lvt, _, _, _) as t ->
if sngl t
then lvt
else lvt + 1
| _ -> failwith "unexpected nlvl case"

let private adjust = function
| T(lvt, lt, kt, rt) as t when lvl lt >= lvt - 1 && lvl rt >= (lvt - 1)
-> t
Expand All @@ -89,11 +95,13 @@ module AaTree =
T(lva + 1, T(lvt - 1, lt, kt, c), ka, (split (T(nlvl a, d, kr, b))))
| _ -> failwith "unexpected adjust case"

let rec private dellrg = function
(* splitMax fixed as in Isabelle HOL proof below: *)
(* https://isabelle.in.tum.de/library/HOL/HOL-Data_Structures/AA_Set.html#:~:text=Function%20%E2%80%B9split_max%E2%80%BA%20below%20is%20called%20%5Ctexttt%7Bdellrg%7D%20in%20the%20paper.%0AThe%20latter%20is%20incorrect%20for%20two%20reasons%3A%20%5Ctexttt%7Bdellrg%7D%20is%20meant%20to%20delete%20the%20largest%0Aelement%20but%20recurses%20on%20the%20left%20instead%20of%20the%20right%20subtree%3B%20the%20invariant%0Ais%20not%20restored.%E2%80%BA *)
let rec private splitMax = function
| T(_, l, v, E) -> (l, v)
| T(h, l, v, r) ->
let (newLeft, newVal) = dellrg l
T(h, newLeft, v, r), newVal
| T(h, l, v, r) as node ->
let (r', b) = splitMax r
in adjust <| node, b
| _ -> failwith "unexpected dellrg case"

/// O(log n): Returns an AaTree with the parameter removed.
Expand All @@ -107,7 +115,7 @@ module AaTree =
elif item > v
then T(h, l, v, delete item r)
else
let (newLeft, newVal) = dellrg l
let (newLeft, newVal) = splitMax l
T(h, newLeft, newVal, r)

/// O(log n): Returns true if the given item exists in the tree.
Expand Down