1662 lines
48 KiB
Plaintext
1662 lines
48 KiB
Plaintext
(*------------------------------------------------------------------*)
|
||
|
||
#define ATS_DYNLOADFLAG 0
|
||
|
||
#include "share/atspre_staload.hats"
|
||
|
||
(*------------------------------------------------------------------*)
|
||
|
||
(*
|
||
|
||
Persistent AVL trees.
|
||
|
||
References:
|
||
|
||
* Niklaus Wirth, 1976. Algorithms + Data Structures =
|
||
Programs. Prentice-Hall, Englewood Cliffs, New Jersey.
|
||
|
||
* Niklaus Wirth, 2004. Algorithms and Data Structures. Updated
|
||
by Fyodor Tkachov, 2014.
|
||
|
||
(Note: Wirth’s implementations, which are in Pascal and Oberon, are
|
||
for non-persistent trees.)
|
||
|
||
*)
|
||
|
||
(*------------------------------------------------------------------*)
|
||
|
||
(*
|
||
|
||
For now, a very simple interface, without much provided in the way
|
||
of proofs.
|
||
|
||
You could put all this interface stuff into a .sats file. (You would
|
||
have to remove the word ‘extern’ from the definitions.)
|
||
|
||
You might also make avl_t abstract, and put these details in the
|
||
.dats file; you would use ‘assume’ to identify the abstract type
|
||
with an implemented type. That approach would require some name
|
||
changes, and also would make pattern matching on the trees
|
||
impossible outside their implementation. Having users do pattern
|
||
matching on the AVL trees probably is a terrible idea, anyway.
|
||
|
||
*)
|
||
|
||
datatype bal_t =
|
||
| bal_minus1
|
||
| bal_zero
|
||
| bal_plus1
|
||
|
||
datatype avl_t (key_t : t@ype+,
|
||
data_t : t@ype+,
|
||
size : int) =
|
||
| avl_t_nil (key_t, data_t, 0)
|
||
| {size_L, size_R : nat}
|
||
avl_t_cons (key_t, data_t, size_L + size_R + 1) of
|
||
(key_t, data_t, bal_t,
|
||
avl_t (key_t, data_t, size_L),
|
||
avl_t (key_t, data_t, size_R))
|
||
typedef avl_t (key_t : t@ype+,
|
||
data_t : t@ype+) =
|
||
[size : int] avl_t (key_t, data_t, size)
|
||
|
||
extern prfun
|
||
lemma_avl_t_param :
|
||
{key_t, data_t : t@ype}
|
||
{size : int}
|
||
avl_t (key_t, data_t, size) -<prf> [0 <= size] void
|
||
|
||
(* Implement this template, for whichever type of key you are
|
||
using. It should return a negative number if u < v, zero if
|
||
u = v, or a positive number if u > v. *)
|
||
extern fun {key_t : t@ype}
|
||
avl_t$compare (u : key_t, v : key_t) :<> int
|
||
|
||
(* Is the AVL tree empty? *)
|
||
extern fun
|
||
avl_t_is_empty
|
||
{key_t : t@ype}
|
||
{data_t : t@ype}
|
||
{size : int}
|
||
(avl : avl_t (key_t, data_t, size)) :<>
|
||
[b : bool | b == (size == 0)]
|
||
bool b
|
||
|
||
(* Does the AVL tree contain at least one association? *)
|
||
extern fun
|
||
avl_t_isnot_empty
|
||
{key_t : t@ype}
|
||
{data_t : t@ype}
|
||
{size : int}
|
||
(avl : avl_t (key_t, data_t, size)) :<>
|
||
[b : bool | b == (size <> 0)]
|
||
bool b
|
||
|
||
(* How many associations are stored in the AVL tree? (Currently we
|
||
have no way to do an avl_t_size that preserves the ‘size’ static
|
||
value. This is the best we can do.) *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_size {size : int}
|
||
(avl : avl_t (key_t, data_t, size)) :<>
|
||
[sz : int | (size == 0 && sz == 0) || (0 < size && 0 < sz)]
|
||
size_t sz
|
||
|
||
(* Does the AVL tree contain the given key? *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_has_key
|
||
{size : int}
|
||
(avl : avl_t (key_t, data_t, size),
|
||
key : key_t) :<>
|
||
bool
|
||
|
||
(* Search for a key. If the key is found, return the data value
|
||
associated with it. Otherwise return the value of ‘dflt’. *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_search_dflt
|
||
{size : int}
|
||
(avl : avl_t (key_t, data_t, size),
|
||
key : key_t,
|
||
dflt : data_t) :<>
|
||
data_t
|
||
|
||
(* Search for a key. If the key is found, return
|
||
‘Some(data)’. Otherwise return ‘None()’. *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_search_opt
|
||
{size : int}
|
||
(avl : avl_t (key_t, data_t, size),
|
||
key : key_t) :<>
|
||
Option (data_t)
|
||
|
||
(* Search for a key. If the key is found, set ‘found’ to true, and set
|
||
‘data’. Otherwise set ‘found’ to false. *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_search_ref
|
||
{size : int}
|
||
(avl : avl_t (key_t, data_t, size),
|
||
key : key_t,
|
||
data : &data_t? >> opt (data_t, found),
|
||
found : &bool? >> bool found) :<!wrt>
|
||
#[found : bool]
|
||
void
|
||
|
||
(* Overload avl_t_search; these functions are easy for the compiler to
|
||
distinguish. *)
|
||
overload avl_t_search with avl_t_search_dflt
|
||
overload avl_t_search with avl_t_search_opt
|
||
overload avl_t_search with avl_t_search_ref
|
||
|
||
(* If a key is not present in the AVL tree, insert the key-data
|
||
association; return the new AVL tree. If the key *is* present in
|
||
the AVL tree, then *replace* the key-data association; return the
|
||
new AVL tree. *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_insert
|
||
{size : int}
|
||
(avl : avl_t (key_t, data_t, size),
|
||
key : key_t,
|
||
data : data_t) :<>
|
||
[sz : pos]
|
||
avl_t (key_t, data_t, sz)
|
||
|
||
(* If a key is not present in the AVL tree, insert the key-data
|
||
association; return the new AVL tree and ‘true’. If the key *is*
|
||
present in the AVL tree, then *replace* the key-data association;
|
||
return the new AVL tree and ‘false’. *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_insert_or_replace
|
||
{size : int}
|
||
(avl : avl_t (key_t, data_t, size),
|
||
key : key_t,
|
||
data : data_t) :<>
|
||
[sz : pos]
|
||
(avl_t (key_t, data_t, sz), bool)
|
||
|
||
(* If a key is present in the AVL tree, delete the key-data
|
||
association; otherwise return the tree as it came. *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_delete
|
||
{size : int}
|
||
(avl : avl_t (key_t, data_t, size),
|
||
key : key_t) :<>
|
||
[sz : nat]
|
||
avl_t (key_t, data_t, sz)
|
||
|
||
(* If a key is present in the AVL tree, delete the key-data
|
||
association; otherwise return the tree as it came. Also, return a
|
||
bool to indicate whether or not the key was found; ‘true’ if found,
|
||
‘false’ if not. *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_delete_if_found
|
||
{size : int}
|
||
(avl : avl_t (key_t, data_t, size),
|
||
key : key_t) :<>
|
||
[sz : nat]
|
||
(avl_t (key_t, data_t, sz), bool)
|
||
|
||
(* Return a sorted list of the association pairs in an AVL
|
||
tree. (Currently we have no way to do an avl_t_pairs that preserves
|
||
the ‘size’ static value. This is the best we can do.) *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_pairs {size : int}
|
||
(avl : avl_t (key_t, data_t, size)) :<>
|
||
[sz : int | (size == 0 && sz == 0) || (0 < size && 0 < sz)]
|
||
list ((key_t, data_t), sz)
|
||
|
||
(* Return a sorted list of the keys in an AVL tree. (Currently we have
|
||
no way to do an avl_t_keys that preserves the ‘size’ static
|
||
value. This is the best we can do.) *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_keys {size : int}
|
||
(avl : avl_t (key_t, data_t, size)) :<>
|
||
[sz : int | (size == 0 && sz == 0) || (0 < size && 0 < sz)]
|
||
list (key_t, sz)
|
||
|
||
(* Return a list of the data values in an AVL tree, sorted in the
|
||
order of their keys. (Currently we have no way to do an avl_t_data
|
||
that preserves the ‘size’ static value. This is the best we can
|
||
do.) *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_data {size : int}
|
||
(avl : avl_t (key_t, data_t, size)) :<>
|
||
[sz : int | (size == 0 && sz == 0) || (0 < size && 0 < sz)]
|
||
list (data_t, sz)
|
||
|
||
(* list2avl_t does the reverse of what avl_t_pairs does (although
|
||
they are not inverses of each other).
|
||
Currently we have no way to do a list2avl_t that preserves the
|
||
‘size’ static value. This is the best we can do. *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
list2avl_t {size : int}
|
||
(lst : list ((key_t, data_t), size)) :<>
|
||
[sz : int | (size == 0 && sz == 0) || (0 < size && 0 < sz)]
|
||
avl_t (key_t, data_t, sz)
|
||
|
||
(* Make a closure that returns association pairs in either forwards or
|
||
reverse order. *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_make_pairs_generator
|
||
{size : int}
|
||
(avl : avl_t (key_t, data_t, size),
|
||
direction : int) :
|
||
() -<cloref1> Option @(key_t, data_t)
|
||
|
||
(* Make a closure that returns keys in either forwards or reverse
|
||
order. *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_make_keys_generator
|
||
{size : int}
|
||
(avl : avl_t (key_t, data_t, size),
|
||
direction : int) :
|
||
() -<cloref1> Option key_t
|
||
|
||
(* Make a closure that returns data values in forwards or reverse
|
||
order of their keys. *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_make_data_generator
|
||
{size : int}
|
||
(avl : avl_t (key_t, data_t, size),
|
||
direction : int) :
|
||
() -<cloref1> Option data_t
|
||
|
||
(* Raise an assertion if the AVL condition is not met. This template
|
||
is for testing the code. *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_check_avl_condition
|
||
{size : int}
|
||
(avl : avl_t (key_t, data_t, size)) :
|
||
void
|
||
|
||
(* Print an AVL tree to standard output, in some useful and perhaps
|
||
even pretty format. *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_pretty_print
|
||
{size : int}
|
||
(avl : avl_t (key_t, data_t, size)) :
|
||
void
|
||
|
||
(* Implement this template for whichever types of keys and data you
|
||
wish to pretty print. *)
|
||
extern fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
avl_t_pretty_print$key_and_data
|
||
(key : key_t,
|
||
data : data_t) :
|
||
void
|
||
|
||
(*------------------------------------------------------------------*)
|
||
|
||
(*
|
||
|
||
What follows is the implementation. It would go into a .dats
|
||
file. Note, however, that the .dats file would have to be staloaded!
|
||
(Preferably anonymously.) This is because the implementation
|
||
contains template functions.
|
||
|
||
Notice there are several assertions with ‘$effmask_ntm’ (as opposed
|
||
to proofs) that the routines are terminating. One hopes to remedy
|
||
that problem (with proofs).
|
||
|
||
Also there are some ‘$effmask_wrt’, but these effect masks are safe,
|
||
because the writing is to our own stack variables.
|
||
|
||
*)
|
||
|
||
#define NIL avl_t_nil ()
|
||
#define CONS avl_t_cons
|
||
#define LNIL list_nil ()
|
||
#define :: list_cons
|
||
#define F false
|
||
#define T true
|
||
|
||
typedef fixbal_t = bool
|
||
|
||
primplement
|
||
lemma_avl_t_param avl =
|
||
case+ avl of
|
||
| NIL => ()
|
||
| CONS _ => ()
|
||
|
||
fn {}
|
||
minus_neg_bal (bal : bal_t) :<> bal_t =
|
||
case+ bal of
|
||
| bal_minus1 () => bal_plus1
|
||
| _ => bal_zero ()
|
||
|
||
fn {}
|
||
minus_pos_bal (bal : bal_t) :<> bal_t =
|
||
case+ bal of
|
||
| bal_plus1 () => bal_minus1
|
||
| _ => bal_zero ()
|
||
|
||
fn {}
|
||
bal2int (bal : bal_t) :<> int =
|
||
case+ bal of
|
||
| bal_minus1 () => ~1
|
||
| bal_zero () => 0
|
||
| bal_plus1 () => 1
|
||
|
||
implement
|
||
avl_t_is_empty avl =
|
||
case+ avl of
|
||
| NIL => T
|
||
| CONS _ => F
|
||
|
||
implement
|
||
avl_t_isnot_empty avl =
|
||
~avl_t_is_empty avl
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_size {siz} avl =
|
||
let
|
||
fun
|
||
traverse {size : int}
|
||
(p : avl_t (key_t, data_t, size)) :<!ntm>
|
||
[sz : int | (size == 0 && sz == 0) ||
|
||
(0 < size && 0 < sz)]
|
||
size_t sz =
|
||
case+ p of
|
||
| NIL => i2sz 0
|
||
| CONS (_, _, _, left, right) =>
|
||
let
|
||
val [sz_L : int] sz_L = traverse left
|
||
val [sz_R : int] sz_R = traverse right
|
||
prval _ = prop_verify {0 <= sz_L} ()
|
||
prval _ = prop_verify {0 <= sz_R} ()
|
||
in
|
||
succ (sz_L + sz_R)
|
||
end
|
||
|
||
val [sz : int] sz = $effmask_ntm (traverse {siz} avl)
|
||
prval _ = prop_verify {(siz == 0 && sz == 0) ||
|
||
(0 < siz && 0 < sz)} ()
|
||
in
|
||
sz
|
||
end
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_has_key (avl, key) =
|
||
let
|
||
fun
|
||
search {size : int}
|
||
(p : avl_t (key_t, data_t, size)) :<!ntm>
|
||
bool =
|
||
case+ p of
|
||
| NIL => F
|
||
| CONS (k, _, _, left, right) =>
|
||
begin
|
||
case+ avl_t$compare<key_t> (key, k) of
|
||
| cmp when cmp < 0 => search left
|
||
| cmp when cmp > 0 => search right
|
||
| _ => T
|
||
end
|
||
in
|
||
$effmask_ntm search avl
|
||
end
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_search_dflt (avl, key, dflt) =
|
||
let
|
||
var data : data_t?
|
||
var found : bool?
|
||
val _ = $effmask_wrt avl_t_search_ref (avl, key, data, found)
|
||
in
|
||
if found then
|
||
let
|
||
prval _ = opt_unsome data
|
||
in
|
||
data
|
||
end
|
||
else
|
||
let
|
||
prval _ = opt_unnone data
|
||
in
|
||
dflt
|
||
end
|
||
end
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_search_opt (avl, key) =
|
||
let
|
||
var data : data_t?
|
||
var found : bool?
|
||
val _ = $effmask_wrt avl_t_search_ref (avl, key, data, found)
|
||
in
|
||
if found then
|
||
let
|
||
prval _ = opt_unsome data
|
||
in
|
||
Some {data_t} data
|
||
end
|
||
else
|
||
let
|
||
prval _ = opt_unnone data
|
||
in
|
||
None {data_t} ()
|
||
end
|
||
end
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_search_ref (avl, key, data, found) =
|
||
let
|
||
fun
|
||
search (p : avl_t (key_t, data_t),
|
||
data : &data_t? >> opt (data_t, found),
|
||
found : &bool? >> bool found) :<!wrt,!ntm>
|
||
#[found : bool] void =
|
||
case+ p of
|
||
| NIL =>
|
||
{
|
||
prval _ = opt_none {data_t} data
|
||
val _ = found := F
|
||
}
|
||
| CONS (k, d, _, left, right) =>
|
||
begin
|
||
case+ avl_t$compare<key_t> (key, k) of
|
||
| cmp when cmp < 0 => search (left, data, found)
|
||
| cmp when cmp > 0 => search (right, data, found)
|
||
| _ =>
|
||
{
|
||
val _ = data := d
|
||
prval _ = opt_some {data_t} data
|
||
val _ = found := T
|
||
}
|
||
end
|
||
in
|
||
$effmask_ntm search (avl, data, found)
|
||
end
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_insert (avl, key, data) =
|
||
let
|
||
val (avl, _) =
|
||
avl_t_insert_or_replace<key_t><data_t> (avl, key, data)
|
||
in
|
||
avl
|
||
end
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_insert_or_replace (avl, key, data) =
|
||
let
|
||
fun
|
||
search {size : nat}
|
||
(p : avl_t (key_t, data_t, size),
|
||
fixbal : fixbal_t,
|
||
found : bool) :<!ntm>
|
||
[sz : pos]
|
||
(avl_t (key_t, data_t, sz), fixbal_t, bool) =
|
||
case+ p of
|
||
| NIL =>
|
||
(* The key was not found. Insert a new node. The tree will
|
||
need rebalancing. *)
|
||
(CONS (key, data, bal_zero, NIL, NIL), T, F)
|
||
| CONS (k, d, bal, left, right) =>
|
||
case+ avl_t$compare<key_t> (key, k) of
|
||
| cmp when cmp < 0 =>
|
||
let
|
||
val (p1, fixbal, found) = search (left, fixbal, found)
|
||
in
|
||
(* If fixbal is T, then a node has been inserted
|
||
on the left, and rebalancing may be necessary. *)
|
||
case+ (fixbal, bal) of
|
||
| (F, _) =>
|
||
(* No rebalancing is necessary. *)
|
||
(CONS (k, d, bal, p1, right), F, found)
|
||
| (T, bal_plus1 ()) =>
|
||
(* No rebalancing is necessary. *)
|
||
(CONS (k, d, bal_zero (), p1, right), F, found)
|
||
| (T, bal_zero ()) =>
|
||
(* Rebalancing might still be necessary. *)
|
||
(CONS (k, d, bal_minus1 (), p1, right), fixbal, found)
|
||
| (T, bal_minus1 ()) =>
|
||
(* Rebalancing is necessary. *)
|
||
let
|
||
val+ CONS (k1, d1, bal1, left1, right1) = p1
|
||
in
|
||
case+ bal1 of
|
||
| bal_minus1 () =>
|
||
(* A single LL rotation. *)
|
||
let
|
||
val q = CONS (k, d, bal_zero (), right1, right)
|
||
val q1 = CONS (k1, d1, bal_zero (), left1, q)
|
||
in
|
||
(q1, F, found)
|
||
end
|
||
| _ =>
|
||
(* A double LR rotation. *)
|
||
let
|
||
val p2 = right1
|
||
val- CONS (k2, d2, bal2, left2, right2) = p2
|
||
val q = CONS (k, d, minus_neg_bal bal2,
|
||
right2, right)
|
||
val q1 = CONS (k1, d1, minus_pos_bal bal2,
|
||
left1, left2)
|
||
val q2 = CONS (k2, d2, bal_zero (), q1, q)
|
||
in
|
||
(q2, F, found)
|
||
end
|
||
end
|
||
end
|
||
| cmp when cmp > 0 =>
|
||
let
|
||
val (p1, fixbal, found) = search (right, fixbal, found)
|
||
in
|
||
(* If fixbal is T, then a node has been inserted
|
||
on the right, and rebalancing may be necessary. *)
|
||
case+ (fixbal, bal) of
|
||
| (F, _) =>
|
||
(* No rebalancing is necessary. *)
|
||
(CONS (k, d, bal, left, p1), F, found)
|
||
| (T, bal_minus1 ()) =>
|
||
(* No rebalancing is necessary. *)
|
||
(CONS (k, d, bal_zero (), left, p1), F, found)
|
||
| (T, bal_zero ()) =>
|
||
(* Rebalancing might still be necessary. *)
|
||
(CONS (k, d, bal_plus1 (), left, p1), fixbal, found)
|
||
| (T, bal_plus1 ()) =>
|
||
(* Rebalancing is necessary. *)
|
||
let
|
||
val+ CONS (k1, d1, bal1, left1, right1) = p1
|
||
in
|
||
case+ bal1 of
|
||
| bal_plus1 () =>
|
||
(* A single RR rotation. *)
|
||
let
|
||
val q = CONS (k, d, bal_zero (), left, left1)
|
||
val q1 = CONS (k1, d1, bal_zero (), q, right1)
|
||
in
|
||
(q1, F, found)
|
||
end
|
||
| _ =>
|
||
(* A double RL rotation. *)
|
||
let
|
||
val p2 = left1
|
||
val- CONS (k2, d2, bal2, left2, right2) = p2
|
||
val q = CONS (k, d, minus_pos_bal bal2,
|
||
left, left2)
|
||
val q1 = CONS (k1, d1, minus_neg_bal bal2,
|
||
right2, right1)
|
||
val q2 = CONS (k2, d2, bal_zero (), q, q1)
|
||
in
|
||
(q2, F, found)
|
||
end
|
||
end
|
||
end
|
||
| _ =>
|
||
(* The key was found; p is an existing node. Replace
|
||
it. The tree needs no rebalancing. *)
|
||
(CONS (key, data, bal, left, right), F, T)
|
||
in
|
||
if avl_t_is_empty avl then
|
||
(* Start a new tree. *)
|
||
(CONS (key, data, bal_zero, NIL, NIL), F)
|
||
else
|
||
let
|
||
prval _ = lemma_avl_t_param avl
|
||
val (avl, _, found) = $effmask_ntm search (avl, F, F)
|
||
in
|
||
(avl, found)
|
||
end
|
||
end
|
||
|
||
fn {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
balance_for_shrunken_left
|
||
{size : pos}
|
||
(p : avl_t (key_t, data_t, size)) :<>
|
||
(* Returns a new avl_t, and a ‘fixbal’ flag. *)
|
||
[sz : pos]
|
||
(avl_t (key_t, data_t, sz), fixbal_t) =
|
||
let
|
||
val+ CONS (k, d, bal, left, right) = p
|
||
in
|
||
case+ bal of
|
||
| bal_minus1 () => (CONS (k, d, bal_zero, left, right), T)
|
||
| bal_zero () => (CONS (k, d, bal_plus1, left, right), F)
|
||
| bal_plus1 () =>
|
||
(* Rebalance. *)
|
||
let
|
||
val p1 = right
|
||
val- CONS (k1, d1, bal1, left1, right1) = p1
|
||
in
|
||
case+ bal1 of
|
||
| bal_zero () =>
|
||
(* A single RR rotation. *)
|
||
let
|
||
val q = CONS (k, d, bal_plus1, left, left1)
|
||
val q1 = CONS (k1, d1, bal_minus1, q, right1)
|
||
in
|
||
(q1, F)
|
||
end
|
||
| bal_plus1 () =>
|
||
(* A single RR rotation. *)
|
||
let
|
||
val q = CONS (k, d, bal_zero, left, left1)
|
||
val q1 = CONS (k1, d1, bal_zero, q, right1)
|
||
in
|
||
(q1, T)
|
||
end
|
||
| bal_minus1 () =>
|
||
(* A double RL rotation. *)
|
||
let
|
||
val p2 = left1
|
||
val- CONS (k2, d2, bal2, left2, right2) = p2
|
||
val q = CONS (k, d, minus_pos_bal bal2, left, left2)
|
||
val q1 = CONS (k1, d1, minus_neg_bal bal2, right2, right1)
|
||
val q2 = CONS (k2, d2, bal_zero, q, q1)
|
||
in
|
||
(q2, T)
|
||
end
|
||
end
|
||
end
|
||
|
||
fn {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
balance_for_shrunken_right
|
||
{size : pos}
|
||
(p : avl_t (key_t, data_t, size)) :<>
|
||
(* Returns a new avl_t, and a ‘fixbal’ flag. *)
|
||
[sz : pos]
|
||
(avl_t (key_t, data_t, sz), fixbal_t) =
|
||
let
|
||
val+ CONS (k, d, bal, left, right) = p
|
||
in
|
||
case+ bal of
|
||
| bal_plus1 () => (CONS (k, d, bal_zero, left, right), T)
|
||
| bal_zero () => (CONS (k, d, bal_minus1, left, right), F)
|
||
| bal_minus1 () =>
|
||
(* Rebalance. *)
|
||
let
|
||
val p1 = left
|
||
val- CONS (k1, d1, bal1, left1, right1) = p1
|
||
in
|
||
case+ bal1 of
|
||
| bal_zero () =>
|
||
(* A single LL rotation. *)
|
||
let
|
||
val q = CONS (k, d, bal_minus1, right1, right)
|
||
val q1 = CONS (k1, d1, bal_plus1, left1, q)
|
||
in
|
||
(q1, F)
|
||
end
|
||
| bal_minus1 () =>
|
||
(* A single LL rotation. *)
|
||
let
|
||
val q = CONS (k, d, bal_zero, right1, right)
|
||
val q1 = CONS (k1, d1, bal_zero, left1, q)
|
||
in
|
||
(q1, T)
|
||
end
|
||
| bal_plus1 () =>
|
||
(* A double LR rotation. *)
|
||
let
|
||
val p2 = right1
|
||
val- CONS (k2, d2, bal2, left2, right2) = p2
|
||
val q = CONS (k, d, minus_neg_bal bal2, right2, right)
|
||
val q1 = CONS (k1, d1, minus_pos_bal bal2, left1, left2)
|
||
val q2 = CONS (k2, d2, bal_zero, q1, q)
|
||
in
|
||
(q2, T)
|
||
end
|
||
end
|
||
end
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_delete (avl, key) =
|
||
(avl_t_delete_if_found (avl, key)).0
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_delete_if_found (avl, key) =
|
||
let
|
||
fn
|
||
balance_L__ {size : pos}
|
||
(p : avl_t (key_t, data_t, size)) :<>
|
||
[sz : pos]
|
||
(avl_t (key_t, data_t, sz), fixbal_t) =
|
||
balance_for_shrunken_left<key_t><data_t> p
|
||
fn
|
||
balance_R__ {size : pos}
|
||
(p : avl_t (key_t, data_t, size)) :<>
|
||
[sz : pos]
|
||
(avl_t (key_t, data_t, sz), fixbal_t) =
|
||
balance_for_shrunken_right<key_t><data_t> p
|
||
|
||
fn {}
|
||
balance_L {size : pos}
|
||
(p : avl_t (key_t, data_t, size),
|
||
fixbal : fixbal_t) :<>
|
||
[sz : pos]
|
||
(avl_t (key_t, data_t, sz), fixbal_t) =
|
||
if fixbal then
|
||
balance_L__ p
|
||
else
|
||
(p, F)
|
||
|
||
fn {}
|
||
balance_R {size : pos}
|
||
(p : avl_t (key_t, data_t, size),
|
||
fixbal : fixbal_t) :<>
|
||
[sz : pos]
|
||
(avl_t (key_t, data_t, sz), fixbal_t) =
|
||
if fixbal then
|
||
balance_R__ p
|
||
else
|
||
(p, F)
|
||
|
||
fun
|
||
del {size : pos}
|
||
(r : avl_t (key_t, data_t, size),
|
||
fixbal : fixbal_t) :<!ntm>
|
||
(* Returns a new avl_t, a new fixbal, and key and data to be
|
||
‘moved up the tree’. *)
|
||
[sz : nat]
|
||
(avl_t (key_t, data_t, sz), fixbal_t, key_t, data_t) =
|
||
case+ r of
|
||
| CONS (k, d, bal, left, right) =>
|
||
begin
|
||
case+ right of
|
||
| CONS _ =>
|
||
let
|
||
val (q, fixbalq, kq, dq) = del (right, fixbal)
|
||
val q1 = CONS (k, d, bal, left, q)
|
||
val (q1bal, fixbal) = balance_R (q1, fixbalq)
|
||
in
|
||
(q1bal, fixbal, kq, dq)
|
||
end
|
||
| NIL => (left, T, k, d)
|
||
end
|
||
|
||
fun
|
||
search {size : nat}
|
||
(p : avl_t (key_t, data_t, size),
|
||
fixbal : fixbal_t) :<!ntm>
|
||
(* Return three values: a new avl_t, a new fixbal, and
|
||
whether the key was found. *)
|
||
[sz : nat]
|
||
(avl_t (key_t, data_t, sz), fixbal_t, bool) =
|
||
case+ p of
|
||
| NIL => (p, F, F)
|
||
| CONS (k, d, bal, left, right) =>
|
||
case+ avl_t$compare<key_t> (key, k) of
|
||
| cmp when cmp < 0 =>
|
||
(* Recursive search down the left branch. *)
|
||
let
|
||
val (q, fixbal, found) = search (left, fixbal)
|
||
val (q1, fixbal) =
|
||
balance_L (CONS (k, d, bal, q, right), fixbal)
|
||
in
|
||
(q1, fixbal, found)
|
||
end
|
||
| cmp when cmp > 0 =>
|
||
(* Recursive search down the right branch. *)
|
||
let
|
||
val (q, fixbal, found) = search (right, fixbal)
|
||
val (q1, fixbal) =
|
||
balance_R (CONS (k, d, bal, left, q), fixbal)
|
||
in
|
||
(q1, fixbal, found)
|
||
end
|
||
| _ =>
|
||
if avl_t_is_empty right then
|
||
(* Delete p, replace it with its left branch, then
|
||
rebalance. *)
|
||
(left, T, T)
|
||
else if avl_t_is_empty left then
|
||
(* Delete p, replace it with its right branch, then
|
||
rebalance. *)
|
||
(right, T, T)
|
||
else
|
||
(* Delete p, but it has both left and right branches, and
|
||
therefore may have complicated branch structure. *)
|
||
let
|
||
val (q, fixbal, k1, d1) = del (left, fixbal)
|
||
val (q1, fixbal) =
|
||
balance_L (CONS (k1, d1, bal, q, right), fixbal)
|
||
in
|
||
(q1, fixbal, T)
|
||
end
|
||
in
|
||
if avl_t_is_empty avl then
|
||
(avl, F)
|
||
else
|
||
let
|
||
prval _ = lemma_avl_t_param avl
|
||
val (avl1, _, found) = $effmask_ntm search (avl, F)
|
||
in
|
||
(avl1, found)
|
||
end
|
||
end
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_pairs (avl) =
|
||
let
|
||
fun
|
||
traverse {size : pos}
|
||
{n : nat}
|
||
(p : avl_t (key_t, data_t, size),
|
||
lst : list ((key_t, data_t), n)) :<!ntm>
|
||
[sz : pos] list ((key_t, data_t), sz) =
|
||
(* Reverse in-order traversal, to make an in-order list by
|
||
consing. *)
|
||
case+ p of
|
||
| CONS (k, d, _, left, right) =>
|
||
if avl_t_is_empty left then
|
||
begin
|
||
if avl_t_is_empty right then
|
||
(k, d) :: lst
|
||
else
|
||
(k, d) :: traverse (right, lst)
|
||
end
|
||
else
|
||
begin
|
||
if avl_t_is_empty right then
|
||
traverse (left, (k, d) :: lst)
|
||
else
|
||
traverse (left, (k, d) :: traverse (right, lst))
|
||
end
|
||
in
|
||
case+ avl of
|
||
| NIL => LNIL
|
||
| CONS _ => $effmask_ntm traverse (avl, LNIL)
|
||
end
|
||
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_keys (avl) =
|
||
let
|
||
fun
|
||
traverse {size : pos}
|
||
{n : nat}
|
||
(p : avl_t (key_t, data_t, size),
|
||
lst : list (key_t, n)) :<!ntm>
|
||
[sz : pos] list (key_t, sz) =
|
||
(* Reverse in-order traversal, to make an in-order list by
|
||
consing. *)
|
||
case+ p of
|
||
| CONS (k, _, _, left, right) =>
|
||
if avl_t_is_empty left then
|
||
begin
|
||
if avl_t_is_empty right then
|
||
k :: lst
|
||
else
|
||
k :: traverse (right, lst)
|
||
end
|
||
else
|
||
begin
|
||
if avl_t_is_empty right then
|
||
traverse (left, k :: lst)
|
||
else
|
||
traverse (left, k :: traverse (right, lst))
|
||
end
|
||
in
|
||
case+ avl of
|
||
| NIL => LNIL
|
||
| CONS _ => $effmask_ntm traverse (avl, LNIL)
|
||
end
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_data (avl) =
|
||
let
|
||
fun
|
||
traverse {size : pos}
|
||
{n : nat}
|
||
(p : avl_t (key_t, data_t, size),
|
||
lst : list (data_t, n)) :<!ntm>
|
||
[sz : pos] list (data_t, sz) =
|
||
(* Reverse in-order traversal, to make an in-order list by
|
||
consing. *)
|
||
case+ p of
|
||
| CONS (_, d, _, left, right) =>
|
||
if avl_t_is_empty left then
|
||
begin
|
||
if avl_t_is_empty right then
|
||
d :: lst
|
||
else
|
||
d :: traverse (right, lst)
|
||
end
|
||
else
|
||
begin
|
||
if avl_t_is_empty right then
|
||
traverse (left, d :: lst)
|
||
else
|
||
traverse (left, d :: traverse (right, lst))
|
||
end
|
||
in
|
||
case+ avl of
|
||
| NIL => LNIL
|
||
| CONS _ => $effmask_ntm traverse (avl, LNIL)
|
||
end
|
||
|
||
implement {key_t} {data_t}
|
||
list2avl_t lst =
|
||
let
|
||
fun
|
||
traverse {n : pos}
|
||
{size : nat} .<n>.
|
||
(lst : list ((key_t, data_t), n),
|
||
p : avl_t (key_t, data_t, size)) :<>
|
||
[sz : pos] avl_t (key_t, data_t, sz) =
|
||
case+ lst of
|
||
| (k, d) :: LNIL => avl_t_insert<key_t><data_t> (p, k, d)
|
||
| (k, d) :: (_ :: _) =>
|
||
let
|
||
val+ _ :: tail = lst
|
||
in
|
||
traverse (tail, avl_t_insert<key_t><data_t> (p, k, d))
|
||
end
|
||
in
|
||
case+ lst of
|
||
| LNIL => NIL
|
||
| (_ :: _) => traverse (lst, NIL)
|
||
end
|
||
|
||
fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
push_all_the_way_left (stack : List (avl_t (key_t, data_t)),
|
||
p : avl_t (key_t, data_t)) :
|
||
List0 (avl_t (key_t, data_t)) =
|
||
let
|
||
prval _ = lemma_list_param stack
|
||
in
|
||
case+ p of
|
||
| NIL => stack
|
||
| CONS (_, _, _, left, _) =>
|
||
push_all_the_way_left (p :: stack, left)
|
||
end
|
||
|
||
fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
push_all_the_way_right (stack : List (avl_t (key_t, data_t)),
|
||
p : avl_t (key_t, data_t)) :
|
||
List0 (avl_t (key_t, data_t)) =
|
||
let
|
||
prval _ = lemma_list_param stack
|
||
in
|
||
case+ p of
|
||
| NIL => stack
|
||
| CONS (_, _, _, _, right) =>
|
||
push_all_the_way_right (p :: stack, right)
|
||
end
|
||
|
||
fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
push_all_the_way (stack : List (avl_t (key_t, data_t)),
|
||
p : avl_t (key_t, data_t),
|
||
direction : int) :
|
||
List0 (avl_t (key_t, data_t)) =
|
||
if direction < 0 then
|
||
push_all_the_way_right<key_t><data_t> (stack, p)
|
||
else
|
||
push_all_the_way_left<key_t><data_t> (stack, p)
|
||
|
||
fun {key_t : t@ype}
|
||
{data_t : t@ype}
|
||
update_generator_stack (stack : List (avl_t (key_t, data_t)),
|
||
left : avl_t (key_t, data_t),
|
||
right : avl_t (key_t, data_t),
|
||
direction : int) :
|
||
List0 (avl_t (key_t, data_t)) =
|
||
let
|
||
prval _ = lemma_list_param stack
|
||
in
|
||
if direction < 0 then
|
||
begin
|
||
if avl_t_is_empty left then
|
||
stack
|
||
else
|
||
push_all_the_way_right<key_t><data_t> (stack, left)
|
||
end
|
||
else
|
||
begin
|
||
if avl_t_is_empty right then
|
||
stack
|
||
else
|
||
push_all_the_way_left<key_t><data_t> (stack, right)
|
||
end
|
||
end
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_make_pairs_generator (avl, direction) =
|
||
let
|
||
typedef avl_t = avl_t (key_t, data_t)
|
||
|
||
val stack = push_all_the_way (LNIL, avl, direction)
|
||
val stack_ref = ref stack
|
||
|
||
(* Cast stack_ref to its (otherwise untyped) pointer, so it can be
|
||
enclosed within ‘generate’. *)
|
||
val p_stack_ref = $UNSAFE.castvwtp0{ptr} stack_ref
|
||
|
||
fun
|
||
generate () :<cloref1> Option @(key_t, data_t) =
|
||
let
|
||
(* Restore the type information for stack_ref. *)
|
||
val stack_ref =
|
||
$UNSAFE.castvwtp0{ref (List avl_t)} p_stack_ref
|
||
|
||
var stack : List0 avl_t = !stack_ref
|
||
var retval : Option @(key_t, data_t)
|
||
in
|
||
begin
|
||
case+ stack of
|
||
| LNIL => retval := None ()
|
||
| p :: tail =>
|
||
let
|
||
val- CONS (k, d, _, left, right) = p
|
||
in
|
||
retval := Some @(k, d);
|
||
stack :=
|
||
update_generator_stack<key_t><data_t>
|
||
(tail, left, right, direction)
|
||
end
|
||
end;
|
||
!stack_ref := stack;
|
||
retval
|
||
end
|
||
in
|
||
generate
|
||
end
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_make_keys_generator (avl, direction) =
|
||
let
|
||
typedef avl_t = avl_t (key_t, data_t)
|
||
|
||
val stack = push_all_the_way (LNIL, avl, direction)
|
||
val stack_ref = ref stack
|
||
|
||
(* Cast stack_ref to its (otherwise untyped) pointer, so it can be
|
||
enclosed within ‘generate’. *)
|
||
val p_stack_ref = $UNSAFE.castvwtp0{ptr} stack_ref
|
||
|
||
fun
|
||
generate () :<cloref1> Option key_t =
|
||
let
|
||
(* Restore the type information for stack_ref. *)
|
||
val stack_ref =
|
||
$UNSAFE.castvwtp0{ref (List avl_t)} p_stack_ref
|
||
|
||
var stack : List0 avl_t = !stack_ref
|
||
var retval : Option key_t
|
||
in
|
||
begin
|
||
case+ stack of
|
||
| LNIL => retval := None ()
|
||
| p :: tail =>
|
||
let
|
||
val- CONS (k, _, _, left, right) = p
|
||
in
|
||
retval := Some k;
|
||
stack :=
|
||
update_generator_stack<key_t><data_t>
|
||
(tail, left, right, direction)
|
||
end
|
||
end;
|
||
!stack_ref := stack;
|
||
retval
|
||
end
|
||
in
|
||
generate
|
||
end
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_make_data_generator (avl, direction) =
|
||
let
|
||
typedef avl_t = avl_t (key_t, data_t)
|
||
|
||
val stack = push_all_the_way (LNIL, avl, direction)
|
||
val stack_ref = ref stack
|
||
|
||
(* Cast stack_ref to its (otherwise untyped) pointer, so it can be
|
||
enclosed within ‘generate’. *)
|
||
val p_stack_ref = $UNSAFE.castvwtp0{ptr} stack_ref
|
||
|
||
fun
|
||
generate () :<cloref1> Option data_t =
|
||
let
|
||
(* Restore the type information for stack_ref. *)
|
||
val stack_ref =
|
||
$UNSAFE.castvwtp0{ref (List avl_t)} p_stack_ref
|
||
|
||
var stack : List0 avl_t = !stack_ref
|
||
var retval : Option data_t
|
||
in
|
||
begin
|
||
case+ stack of
|
||
| LNIL => retval := None ()
|
||
| p :: tail =>
|
||
let
|
||
val- CONS (_, d, _, left, right) = p
|
||
in
|
||
retval := Some d;
|
||
stack :=
|
||
update_generator_stack<key_t><data_t>
|
||
(tail, left, right, direction)
|
||
end
|
||
end;
|
||
!stack_ref := stack;
|
||
retval
|
||
end
|
||
in
|
||
generate
|
||
end
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_check_avl_condition (avl) =
|
||
(* If any of the assertions here is triggered, there is a bug. *)
|
||
let
|
||
fun
|
||
get_heights (p : avl_t (key_t, data_t)) : (int, int) =
|
||
case+ p of
|
||
| NIL => (0, 0)
|
||
| CONS (k, d, bal, left, right) =>
|
||
let
|
||
val (height_LL, height_LR) = get_heights left
|
||
val (height_RL, height_RR) = get_heights right
|
||
in
|
||
assertloc (abs (height_LL - height_LR) <= 1);
|
||
assertloc (abs (height_RL - height_RR) <= 1);
|
||
(height_LL + height_LR, height_RL + height_RR)
|
||
end
|
||
in
|
||
if avl_t_isnot_empty avl then
|
||
let
|
||
val (height_L, height_R) = get_heights avl
|
||
in
|
||
assertloc (abs (height_L - height_R) <= 1)
|
||
end
|
||
end
|
||
|
||
implement {key_t} {data_t}
|
||
avl_t_pretty_print (avl) =
|
||
let
|
||
fun
|
||
pad {depth : nat} .<depth>.
|
||
(depth : int depth) : void =
|
||
if depth <> 0 then
|
||
begin
|
||
print! (" ");
|
||
pad (pred depth)
|
||
end
|
||
|
||
fun
|
||
traverse {size : nat}
|
||
{depth : nat}
|
||
(p : avl_t (key_t, data_t, size),
|
||
depth : int depth) : void =
|
||
if avl_t_isnot_empty p then
|
||
let
|
||
val+ CONS (k, d, bal, left, right) = p
|
||
in
|
||
traverse (left, succ depth);
|
||
pad depth;
|
||
avl_t_pretty_print$key_and_data<key_t><data_t> (k, d);
|
||
println! ("\t\tdepth = ", depth, " bal = ", bal2int bal);
|
||
traverse (right, succ depth)
|
||
end
|
||
in
|
||
if avl_t_isnot_empty avl then
|
||
let
|
||
val+ CONS (k, d, bal, left, right) = avl
|
||
in
|
||
traverse (left, 1);
|
||
avl_t_pretty_print$key_and_data<key_t><data_t> (k, d);
|
||
println! ("\t\tdepth = 0 bal = ", bal2int bal);
|
||
traverse (right, 1)
|
||
end
|
||
end
|
||
|
||
(*------------------------------------------------------------------*)
|
||
|
||
(*
|
||
|
||
Here is a little demonstration program.
|
||
|
||
Assuming you are using Boehm GC, compile this source file with
|
||
|
||
patscc -O2 -DATS_MEMALLOC_GCBDW avl_trees-postiats.dats -lgc
|
||
|
||
and run it with
|
||
|
||
./a.out
|
||
|
||
*)
|
||
|
||
%{^
|
||
#include <time.h>
|
||
|
||
ATSinline() atstype_uint64
|
||
get_the_time (void)
|
||
{
|
||
return (atstype_uint64) time (NULL);
|
||
}
|
||
%}
|
||
|
||
(* An implementation of avl_t$compare for keys of type ‘int’. *)
|
||
implement
|
||
avl_t$compare<int> (u, v) =
|
||
if u < v then
|
||
~1
|
||
else if u > v then
|
||
1
|
||
else
|
||
0
|
||
|
||
(* An implementation of avl_t_pretty_print$key_and_data for keys of
|
||
type ‘int’ and values of type ‘double’. *)
|
||
implement
|
||
avl_t_pretty_print$key_and_data<int><double> (key, data) =
|
||
print! ("(", key, ", ", data, ")")
|
||
|
||
implement
|
||
main0 () =
|
||
let
|
||
(* A linear congruential random number generator attributed
|
||
to Donald Knuth. *)
|
||
fn
|
||
next_random (seed : &uint64) : uint64 =
|
||
let
|
||
val a : uint64 = $UNSAFE.cast 6364136223846793005ULL
|
||
val c : uint64 = $UNSAFE.cast 1442695040888963407ULL
|
||
val retval = seed
|
||
in
|
||
seed := (a * seed) + c;
|
||
retval
|
||
end
|
||
|
||
fn {t : t@ype}
|
||
fisher_yates_shuffle
|
||
{n : nat}
|
||
(a : &(@[t][n]),
|
||
n : size_t n,
|
||
seed : &uint64) : void =
|
||
let
|
||
var i : [i : nat | i <= n] size_t i
|
||
in
|
||
for (i := i2sz 0; i < n; i := succ i)
|
||
let
|
||
val randnum = $UNSAFE.cast{Size_t} (next_random seed)
|
||
val j = randnum mod n (* This is good enough for us. *)
|
||
val xi = a[i]
|
||
val xj = a[j]
|
||
in
|
||
a[i] := xj;
|
||
a[j] := xi
|
||
end
|
||
end
|
||
|
||
var seed : uint64 = $extfcall (uint64, "get_the_time")
|
||
|
||
#define N 20
|
||
var keys : @[int][N] = @[int][N] (0)
|
||
|
||
var a : avl_t (int, double)
|
||
var a_saved : avl_t (int, double)
|
||
var a1 : (avl_t (int, double), bool)
|
||
|
||
var i : [i : nat] int i
|
||
|
||
val dflt = ~99999999.0
|
||
val not_dflt = 123456789.0
|
||
in
|
||
println! ("----------------------------------------------------");
|
||
print! ("\n");
|
||
|
||
(* Initialize a shuffled array of keys. *)
|
||
for (i := 0; i < N; i := succ i)
|
||
keys[i] := succ i;
|
||
fisher_yates_shuffle<int> {N} (keys, i2sz N, seed);
|
||
|
||
print! ("The keys\n ");
|
||
for (i := 0; i < N; i := succ i)
|
||
print! (" ", keys[i]);
|
||
print! ("\n");
|
||
|
||
print! ("\nRunning some tests... ");
|
||
|
||
(* Insert key-data pairs in the shuffled order, checking aspects
|
||
of the implementation while doing so. *)
|
||
a := avl_t_nil ();
|
||
for (i := 0; i < N; i := succ i)
|
||
let
|
||
var j : [j : nat] int j
|
||
in
|
||
a := avl_t_insert<int> (a, keys[i], g0i2f keys[i]);
|
||
avl_t_check_avl_condition (a);
|
||
assertloc (avl_t_size a = succ i);
|
||
assertloc (avl_t_is_empty a = iseqz (avl_t_size a));
|
||
assertloc (avl_t_isnot_empty a = isneqz (avl_t_size a));
|
||
a := avl_t_insert<int> (a, keys[i], not_dflt);
|
||
avl_t_check_avl_condition (a);
|
||
assertloc (avl_t_search<int><double> (a, keys[i], dflt)
|
||
= not_dflt);
|
||
assertloc (avl_t_size a = succ i);
|
||
assertloc (avl_t_is_empty a = iseqz (avl_t_size a));
|
||
assertloc (avl_t_isnot_empty a = isneqz (avl_t_size a));
|
||
a := avl_t_insert<int> (a, keys[i], g0i2f keys[i]);
|
||
avl_t_check_avl_condition (a);
|
||
assertloc (avl_t_size a = succ i);
|
||
assertloc (avl_t_is_empty a = iseqz (avl_t_size a));
|
||
assertloc (avl_t_isnot_empty a = isneqz (avl_t_size a));
|
||
for (j := 0; j < N; j := succ j)
|
||
let
|
||
val k = keys[j]
|
||
val has_key = avl_t_has_key<int> (a, k)
|
||
val data_opt = avl_t_search<int><double> (a, k)
|
||
val data_dflt = avl_t_search<int><double> (a, k, dflt)
|
||
in
|
||
assertloc (has_key = (j <= i));
|
||
assertloc (option_is_some data_opt = (j <= i));
|
||
if (j <= i) then
|
||
let
|
||
val- Some data = data_opt
|
||
in
|
||
assertloc (data = g0i2f k);
|
||
assertloc (data_dflt = g0i2f k);
|
||
end
|
||
else
|
||
let
|
||
val- None () = data_opt
|
||
in
|
||
assertloc (data_dflt = dflt);
|
||
end
|
||
end
|
||
end;
|
||
|
||
(* Do it again, but using avl_t_insert_or_replace and checking its
|
||
second return value. *)
|
||
a1 := (avl_t_nil (), false);
|
||
for (i := 0; i < N; i := succ i)
|
||
let
|
||
var j : [j : nat] int j
|
||
in
|
||
a1 :=
|
||
avl_t_insert_or_replace<int> (a1.0, keys[i], g0i2f keys[i]);
|
||
avl_t_check_avl_condition (a1.0);
|
||
assertloc (~(a1.1));
|
||
assertloc (avl_t_size (a1.0) = succ i);
|
||
assertloc (avl_t_is_empty a1.0 = iseqz (avl_t_size a1.0));
|
||
assertloc (avl_t_isnot_empty a1.0 = isneqz (avl_t_size a1.0));
|
||
a1 := avl_t_insert_or_replace<int> (a1.0, keys[i], not_dflt);
|
||
avl_t_check_avl_condition (a1.0);
|
||
assertloc (avl_t_search<int><double> (a1.0, keys[i], dflt)
|
||
= not_dflt);
|
||
assertloc (avl_t_size (a1.0) = succ i);
|
||
assertloc (avl_t_is_empty a1.0 = iseqz (avl_t_size a1.0));
|
||
assertloc (avl_t_isnot_empty a1.0 = isneqz (avl_t_size a1.0));
|
||
a1 :=
|
||
avl_t_insert_or_replace<int> (a1.0, keys[i], g0i2f keys[i]);
|
||
avl_t_check_avl_condition (a1.0);
|
||
assertloc (a1.1);
|
||
assertloc (avl_t_size (a1.0) = succ i);
|
||
assertloc (avl_t_is_empty a1.0 = iseqz (avl_t_size a1.0));
|
||
assertloc (avl_t_isnot_empty a1.0 = isneqz (avl_t_size a1.0));
|
||
for (j := 0; j < N; j := succ j)
|
||
let
|
||
val k = keys[j]
|
||
val has_key = avl_t_has_key<int> (a1.0, k)
|
||
val data_opt = avl_t_search<int><double> (a1.0, k)
|
||
val data_dflt = avl_t_search<int><double> (a1.0, k, dflt)
|
||
in
|
||
assertloc (has_key = (j <= i));
|
||
assertloc (option_is_some data_opt = (j <= i));
|
||
if (j <= i) then
|
||
let
|
||
val- Some data = data_opt
|
||
in
|
||
assertloc (data = g0i2f k);
|
||
assertloc (data_dflt = g0i2f k);
|
||
end
|
||
else
|
||
let
|
||
val- None () = data_opt
|
||
in
|
||
assertloc (data_dflt = dflt);
|
||
end
|
||
end
|
||
end;
|
||
a := a1.0;
|
||
|
||
(* The trees are PERSISTENT, so SAVE THE CURRENT VALUE! *)
|
||
a_saved := a;
|
||
|
||
(* Reshuffle the keys, and test deletion, using the reshuffled
|
||
keys. *)
|
||
fisher_yates_shuffle<int> {N} (keys, i2sz N, seed);
|
||
for (i := 0; i < N; i := succ i)
|
||
let
|
||
val ix = keys[i]
|
||
var j : [j : nat] int j
|
||
in
|
||
a := avl_t_delete<int> (a, ix);
|
||
avl_t_check_avl_condition (a);
|
||
assertloc (avl_t_size a = N - succ i);
|
||
assertloc (avl_t_is_empty a = iseqz (avl_t_size a));
|
||
assertloc (avl_t_isnot_empty a = isneqz (avl_t_size a));
|
||
a := avl_t_delete<int> (a, ix);
|
||
avl_t_check_avl_condition (a);
|
||
assertloc (avl_t_size a = N - succ i);
|
||
assertloc (avl_t_is_empty a = iseqz (avl_t_size a));
|
||
assertloc (avl_t_isnot_empty a = isneqz (avl_t_size a));
|
||
for (j := 0; j < N; j := succ j)
|
||
let
|
||
val k = keys[j]
|
||
val has_key = avl_t_has_key<int> (a, k)
|
||
val data_opt = avl_t_search<int><double> (a, k)
|
||
val data_dflt = avl_t_search<int><double> (a, k, dflt)
|
||
in
|
||
assertloc (has_key = (i < j));
|
||
assertloc (option_is_some data_opt = (i < j));
|
||
if (i < j) then
|
||
let
|
||
val- Some data = data_opt
|
||
in
|
||
assertloc (data = g0i2f k);
|
||
assertloc (data_dflt = g0i2f k);
|
||
end
|
||
else
|
||
let
|
||
val- None () = data_opt
|
||
in
|
||
assertloc (data_dflt = dflt);
|
||
end
|
||
end
|
||
end;
|
||
|
||
(* Get back the PERSISTENT VALUE from before the deletions. *)
|
||
a := a_saved;
|
||
|
||
(* Reshuffle the keys, and test deletion again, this time using
|
||
avl_t_delete_if_found. *)
|
||
fisher_yates_shuffle<int> {N} (keys, i2sz N, seed);
|
||
for (i := 0; i < N; i := succ i)
|
||
let
|
||
val ix = keys[i]
|
||
var j : [j : nat] int j
|
||
in
|
||
a1 := avl_t_delete_if_found<int> (a, ix);
|
||
a := a1.0;
|
||
avl_t_check_avl_condition (a);
|
||
assertloc (a1.1);
|
||
assertloc (avl_t_size a = N - succ i);
|
||
assertloc (avl_t_is_empty a = iseqz (avl_t_size a));
|
||
assertloc (avl_t_isnot_empty a = isneqz (avl_t_size a));
|
||
a1 := avl_t_delete_if_found<int> (a, ix);
|
||
a := a1.0;
|
||
avl_t_check_avl_condition (a);
|
||
assertloc (~(a1.1));
|
||
assertloc (avl_t_size a = N - succ i);
|
||
assertloc (avl_t_is_empty a = iseqz (avl_t_size a));
|
||
assertloc (avl_t_isnot_empty a = isneqz (avl_t_size a));
|
||
for (j := 0; j < N; j := succ j)
|
||
let
|
||
val k = keys[j]
|
||
val has_key = avl_t_has_key<int> (a, k)
|
||
val data_opt = avl_t_search<int><double> (a, k)
|
||
val data_dflt = avl_t_search<int><double> (a, k, dflt)
|
||
in
|
||
assertloc (has_key = (i < j));
|
||
assertloc (option_is_some data_opt = (i < j));
|
||
if (i < j) then
|
||
let
|
||
val- Some data = data_opt
|
||
in
|
||
assertloc (data = g0i2f k);
|
||
assertloc (data_dflt = g0i2f k);
|
||
end
|
||
else
|
||
let
|
||
val- None () = data_opt
|
||
in
|
||
assertloc (data_dflt = dflt);
|
||
end
|
||
end
|
||
end;
|
||
|
||
print! ("passed\n");
|
||
|
||
(* Get back the PERSISTENT VALUE from before the deletions. *)
|
||
a := a_saved;
|
||
|
||
print! ("\n");
|
||
println! ("----------------------------------------------------");
|
||
print! ("\n");
|
||
print! ("*** PRETTY-PRINTING OF THE TREE ***\n\n");
|
||
|
||
avl_t_pretty_print<int><double> a;
|
||
|
||
print! ("\n");
|
||
println! ("----------------------------------------------------");
|
||
print! ("\n");
|
||
print! ("*** GENERATORS ***\n\n");
|
||
|
||
let
|
||
val gen = avl_t_make_pairs_generator (a, 1)
|
||
var x : Option @(int, double)
|
||
in
|
||
print! ("Association pairs in order\n ");
|
||
for (x := gen (); option_is_some (x); x := gen ())
|
||
let
|
||
val @(k, d) = option_unsome x
|
||
in
|
||
print! (" (", k : int, ", ", d : double, ")")
|
||
end
|
||
end;
|
||
|
||
print! ("\n\n");
|
||
|
||
let
|
||
val gen = avl_t_make_pairs_generator (a, ~1)
|
||
var x : Option @(int, double)
|
||
in
|
||
print! ("Association pairs in reverse order\n ");
|
||
for (x := gen (); option_is_some (x); x := gen ())
|
||
let
|
||
val @(k, d) = option_unsome x
|
||
in
|
||
print! (" (", k : int, ", ", d : double, ")")
|
||
end
|
||
end;
|
||
|
||
print! ("\n\n");
|
||
|
||
let
|
||
val gen = avl_t_make_keys_generator (a, 1)
|
||
var x : Option int
|
||
in
|
||
print! ("Keys in order\n ");
|
||
for (x := gen (); option_is_some (x); x := gen ())
|
||
print! (" ", (option_unsome x) : int)
|
||
end;
|
||
|
||
print! ("\n\n");
|
||
|
||
let
|
||
val gen = avl_t_make_keys_generator (a, ~1)
|
||
var x : Option int
|
||
in
|
||
print! ("Keys in reverse order\n ");
|
||
for (x := gen (); option_is_some (x); x := gen ())
|
||
print! (" ", (option_unsome x) : int)
|
||
end;
|
||
|
||
print! ("\n\n");
|
||
|
||
let
|
||
val gen = avl_t_make_data_generator (a, 1)
|
||
var x : Option double
|
||
in
|
||
print! ("Data values in order of their keys\n ");
|
||
for (x := gen (); option_is_some (x); x := gen ())
|
||
print! (" ", (option_unsome x) : double)
|
||
end;
|
||
|
||
print! ("\n\n");
|
||
|
||
let
|
||
val gen = avl_t_make_data_generator (a, ~1)
|
||
var x : Option double
|
||
in
|
||
print! ("Data values in reverse order of their keys\n ");
|
||
for (x := gen (); option_is_some (x); x := gen ())
|
||
print! (" ", (option_unsome x) : double)
|
||
end;
|
||
|
||
print! ("\n");
|
||
|
||
print! ("\n");
|
||
println! ("----------------------------------------------------");
|
||
print! ("\n");
|
||
print! ("*** AVL TREES TO LISTS ***\n\n");
|
||
|
||
print! ("Association pairs in order\n ");
|
||
print! (avl_t_pairs<int><double> a);
|
||
|
||
print! ("\n\n");
|
||
|
||
print! ("Keys in order\n ");
|
||
print! (avl_t_keys<int> a);
|
||
print! ("\n\n");
|
||
|
||
print! ("Data values in order of their keys\n ");
|
||
print! (avl_t_data<int><double> a);
|
||
print! ("\n");
|
||
|
||
print! ("\n");
|
||
println! ("----------------------------------------------------");
|
||
print! ("\n");
|
||
print! ("*** LISTS TO AVL TREES ***\n\n");
|
||
|
||
let
|
||
val lst = (3, 3.0) :: (1, 1.0) :: (4, 4.0) :: (2, 2.0) :: LNIL
|
||
val avl = list2avl_t<int><double> lst
|
||
in
|
||
print! (lst : List @(int, double));
|
||
print! ("\n\n =>\n\n");
|
||
avl_t_pretty_print<int><double> avl
|
||
end;
|
||
|
||
print! ("\n");
|
||
println! ("----------------------------------------------------")
|
||
end
|
||
|
||
(*------------------------------------------------------------------*)
|