mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-10-03 18:27:13 +03:00
refactor BBT to new syntax
This commit is contained in:
imaqtkatt
parent
de14d56d3d
commit
af0ed6bb8d
@ -1,15 +1,19 @@
|
||||
BBT
|
||||
: ∀(K: *) ∀(V: *) *
|
||||
= λK λV
|
||||
$(self: (BBT K V))
|
||||
∀(P: ∀(bbt: (BBT K V)) *)
|
||||
∀(bin:
|
||||
∀(size: U60)
|
||||
∀(key: K)
|
||||
∀(val: V)
|
||||
∀(lft: (BBT K V))
|
||||
∀(rgt: (BBT K V))
|
||||
(P (BBT.bin K V size key val lft rgt))
|
||||
)
|
||||
∀(tip: (P (BBT.tip K V)))
|
||||
(P self)
|
||||
//BBT
|
||||
//: ∀(K: *) ∀(V: *) *
|
||||
//= λK λV
|
||||
//$(self: (BBT K V))
|
||||
//∀(P: ∀(bbt: (BBT K V)) *)
|
||||
//∀(bin:
|
||||
//∀(size: U60)
|
||||
//∀(key: K)
|
||||
//∀(val: V)
|
||||
//∀(lft: (BBT K V))
|
||||
//∀(rgt: (BBT K V))
|
||||
//(P (BBT.bin K V size key val lft rgt))
|
||||
//)
|
||||
//∀(tip: (P (BBT.tip K V)))
|
||||
//(P self)
|
||||
|
||||
data BBT K V
|
||||
| bin (size: U60) (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V))
|
||||
| tip
|
||||
|
||||
@ -1,66 +1,97 @@
|
||||
BBT.balance
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
∀(set_key: K)
|
||||
∀(node_key: K)
|
||||
∀(val: V)
|
||||
∀(lft: (BBT K V))
|
||||
∀(rgt: (BBT K V))
|
||||
(BBT K V)
|
||||
= λK λV λcmp λset_key λnode_key λval λlft λrgt
|
||||
use P = λx (BBT K V)
|
||||
use new = λlft.size λlft
|
||||
use P = λx (BBT K V)
|
||||
use new = λrgt.size λrgt
|
||||
use new_size = (+ 1 (U60.max lft.size rgt.size))
|
||||
use balance = (U60.abs_diff lft.size rgt.size)
|
||||
use P = λx
|
||||
∀(new_size: U60)
|
||||
∀(node_key: K)
|
||||
∀(val: V)
|
||||
∀(lft: (BBT K V))
|
||||
∀(rgt: (BBT K V))
|
||||
(BBT K V)
|
||||
use true = λnew_size λnode_key λval λlft λrgt
|
||||
use P = λx
|
||||
∀(K: *)
|
||||
∀(V: *)
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
∀(new_size: U60)
|
||||
∀(node_key: K)
|
||||
∀(set_key: K)
|
||||
∀(val: V)
|
||||
∀(lft: (BBT K V))
|
||||
∀(rgt: (BBT K V))
|
||||
(BBT K V)
|
||||
use true = BBT.balance.lft_heavier
|
||||
use false = BBT.balance.rgt_heavier
|
||||
(~(U60.to_bool (< rgt.size lft.size))
|
||||
P
|
||||
true
|
||||
false
|
||||
K
|
||||
V
|
||||
cmp
|
||||
new_size
|
||||
node_key
|
||||
set_key
|
||||
val
|
||||
lft
|
||||
rgt
|
||||
)
|
||||
use false = λnew_size λnode_key λval λlft λrgt
|
||||
(BBT.bin K V new_size node_key val lft rgt)
|
||||
(~(U60.to_bool (> balance 1))
|
||||
P
|
||||
true
|
||||
false
|
||||
new_size
|
||||
node_key
|
||||
val
|
||||
lft
|
||||
rgt
|
||||
)
|
||||
(~(BBT.got_size K V rgt) P new)
|
||||
(~(BBT.got_size K V lft) P new)
|
||||
use BBT/{bin,tip}
|
||||
use Bool/{true,false}
|
||||
|
||||
balance <K> <V>
|
||||
(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
(set_key: K)
|
||||
(node_key: K)
|
||||
(val: V)
|
||||
(lft: (BBT K V))
|
||||
(rgt: (BBT K V))
|
||||
: (BBT K V) =
|
||||
match got_lft = (BBT/got_size lft) {
|
||||
Pair/new:
|
||||
match got_rgt = (BBT/got_size rgt) {
|
||||
Pair/new:
|
||||
use new_size = (+ got_lft.fst got_rgt.fst)
|
||||
use balance = (U60/abs_diff got_lft.fst got_rgt.fst)
|
||||
|
||||
match _ = (U60/to_bool (> balance 1)) {
|
||||
true:
|
||||
match _ = (U60/to_bool (< got_lft.fst got_rgt.fst)) {
|
||||
true: (BBT/balance/lft_heavier cmp new_size node_key set_key val lft rgt)
|
||||
false: (BBT/balance/rgt_heavier cmp new_size node_key set_key val lft rgt)
|
||||
}
|
||||
false: (bin K V new_size node_key val lft rgt)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
//BBT.balance
|
||||
//: ∀(K: *)
|
||||
//∀(V: *)
|
||||
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
//∀(set_key: K)
|
||||
//∀(node_key: K)
|
||||
//∀(val: V)
|
||||
//∀(lft: (BBT K V))
|
||||
//∀(rgt: (BBT K V))
|
||||
//(BBT K V)
|
||||
//= λK λV λcmp λset_key λnode_key λval λlft λrgt
|
||||
//use P = λx (BBT K V)
|
||||
//use new = λlft.size λlft
|
||||
//use P = λx (BBT K V)
|
||||
//use new = λrgt.size λrgt
|
||||
//use new_size = (+ 1 (U60.max lft.size rgt.size))
|
||||
//use balance = (U60.abs_diff lft.size rgt.size)
|
||||
//use P = λx
|
||||
//∀(new_size: U60)
|
||||
//∀(node_key: K)
|
||||
//∀(val: V)
|
||||
//∀(lft: (BBT K V))
|
||||
//∀(rgt: (BBT K V))
|
||||
//(BBT K V)
|
||||
//use true = λnew_size λnode_key λval λlft λrgt
|
||||
//use P = λx
|
||||
//∀(K: *)
|
||||
//∀(V: *)
|
||||
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
//∀(new_size: U60)
|
||||
//∀(node_key: K)
|
||||
//∀(set_key: K)
|
||||
//∀(val: V)
|
||||
//∀(lft: (BBT K V))
|
||||
//∀(rgt: (BBT K V))
|
||||
//(BBT K V)
|
||||
//use true = BBT.balance.lft_heavier
|
||||
//use false = BBT.balance.rgt_heavier
|
||||
//(~(U60.to_bool (< rgt.size lft.size))
|
||||
//P
|
||||
//true
|
||||
//false
|
||||
//K
|
||||
//V
|
||||
//cmp
|
||||
//new_size
|
||||
//node_key
|
||||
//set_key
|
||||
//val
|
||||
//lft
|
||||
//rgt
|
||||
//)
|
||||
//use false = λnew_size λnode_key λval λlft λrgt
|
||||
//(BBT.bin K V new_size node_key val lft rgt)
|
||||
//(~(U60.to_bool (> balance 1))
|
||||
//P
|
||||
//true
|
||||
//false
|
||||
//new_size
|
||||
//node_key
|
||||
//val
|
||||
//lft
|
||||
//rgt
|
||||
//)
|
||||
//(~(BBT.got_size K V rgt) P new)
|
||||
//(~(BBT.got_size K V lft) P new)
|
||||
|
||||
@ -1,53 +1,80 @@
|
||||
BBT.balance.lft_heavier
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
∀(new_size: U60)
|
||||
∀(node_key: K)
|
||||
∀(set_key: K)
|
||||
∀(val: V)
|
||||
∀(lft: (BBT K V))
|
||||
∀(rgt: (BBT K V))
|
||||
(BBT K V)
|
||||
= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt
|
||||
use P = λx (BBT K V)
|
||||
use bin = λlft.size λlft.key λlft.val λlft.lft λlft.rgt
|
||||
use P = λx
|
||||
∀(new_size: U60)
|
||||
∀(key: K)
|
||||
∀(val: V)
|
||||
∀(lft.key: K)
|
||||
∀(lft.val: V)
|
||||
∀(lft.lft: (BBT K V))
|
||||
∀(lft.rgt: (BBT K V))
|
||||
∀(rgt: (BBT K V))
|
||||
(BBT K V)
|
||||
use true = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt
|
||||
use lft = (BBT.lft_rotate
|
||||
K
|
||||
V
|
||||
lft.size
|
||||
lft.key
|
||||
lft.val
|
||||
lft.lft
|
||||
lft.rgt
|
||||
)
|
||||
(BBT.rgt_rotate K V new_size key val lft rgt)
|
||||
use false = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt
|
||||
use lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt)
|
||||
(BBT.rgt_rotate K V new_size key val lft rgt)
|
||||
(~(Cmp.is_gtn (cmp set_key lft.key))
|
||||
P
|
||||
true
|
||||
false
|
||||
new_size
|
||||
node_key
|
||||
val
|
||||
lft.key
|
||||
lft.val
|
||||
lft.lft
|
||||
lft.rgt
|
||||
rgt
|
||||
)
|
||||
use tip = (BBT.tip K V)
|
||||
(~lft P bin tip)
|
||||
use BBT/{bin,tip,lft_rotate,rgt_rotate}
|
||||
use Bool/{true,false}
|
||||
|
||||
lft_heavier <K> <V>
|
||||
(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
(new_size: U60)
|
||||
(node_key: K)
|
||||
(set_key: K)
|
||||
(val: V)
|
||||
(lft: (BBT K V))
|
||||
(rgt: (BBT K V))
|
||||
: (BBT K V) =
|
||||
match lft {
|
||||
bin:
|
||||
match _ = (Cmp/is_gtn (cmp set_key lft.key)) {
|
||||
true:
|
||||
use lft = (lft_rotate lft.size lft.key lft.val lft.lft lft.rgt)
|
||||
(rgt_rotate new_size lft.key val lft rgt)
|
||||
false:
|
||||
use lft = (bin K V lft.size lft.key lft.val lft.lft lft.rgt)
|
||||
(rgt_rotate new_size lft.key val lft rgt)
|
||||
}
|
||||
tip: (tip K V)
|
||||
}
|
||||
|
||||
|
||||
|
||||
//BBT.balance.lft_heavier
|
||||
//: ∀(K: *)
|
||||
//∀(V: *)
|
||||
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
//∀(new_size: U60)
|
||||
//∀(node_key: K)
|
||||
//∀(set_key: K)
|
||||
//∀(val: V)
|
||||
//∀(lft: (BBT K V))
|
||||
//∀(rgt: (BBT K V))
|
||||
//(BBT K V)
|
||||
//= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt
|
||||
//use P = λx (BBT K V)
|
||||
//use bin = λlft.size λlft.key λlft.val λlft.lft λlft.rgt
|
||||
//use P = λx
|
||||
//∀(new_size: U60)
|
||||
//∀(key: K)
|
||||
//∀(val: V)
|
||||
//∀(lft.key: K)
|
||||
//∀(lft.val: V)
|
||||
//∀(lft.lft: (BBT K V))
|
||||
//∀(lft.rgt: (BBT K V))
|
||||
//∀(rgt: (BBT K V))
|
||||
//(BBT K V)
|
||||
//use true = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt
|
||||
//use lft = (BBT.lft_rotate
|
||||
//K
|
||||
//V
|
||||
//lft.size
|
||||
//lft.key
|
||||
//lft.val
|
||||
//lft.lft
|
||||
//lft.rgt
|
||||
//)
|
||||
//(BBT.rgt_rotate K V new_size key val lft rgt)
|
||||
//use false = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt
|
||||
//use lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt)
|
||||
//(BBT.rgt_rotate K V new_size key val lft rgt)
|
||||
//(~(Cmp.is_gtn (cmp set_key lft.key))
|
||||
//P
|
||||
//true
|
||||
//false
|
||||
//new_size
|
||||
//node_key
|
||||
//val
|
||||
//lft.key
|
||||
//lft.val
|
||||
//lft.lft
|
||||
//lft.rgt
|
||||
//rgt
|
||||
//)
|
||||
//use tip = (BBT.tip K V)
|
||||
//(~lft P bin tip)
|
||||
|
||||
@ -1,53 +1,80 @@
|
||||
BBT.balance.rgt_heavier
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
∀(new_size: U60)
|
||||
∀(node_key: K)
|
||||
∀(set_key: K)
|
||||
∀(val: V)
|
||||
∀(lft: (BBT K V))
|
||||
∀(rgt: (BBT K V))
|
||||
(BBT K V)
|
||||
= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt
|
||||
use P = λx (BBT K V)
|
||||
use bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt
|
||||
use P = λx
|
||||
∀(new_size: U60)
|
||||
∀(key: K)
|
||||
∀(val: V)
|
||||
∀(lft: (BBT K V))
|
||||
∀(rgt.key: K)
|
||||
∀(rgt.val: V)
|
||||
∀(rgt.lft: (BBT K V))
|
||||
∀(rgt.rgt: (BBT K V))
|
||||
(BBT K V)
|
||||
use true = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt
|
||||
use rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt)
|
||||
(BBT.lft_rotate K V new_size key val lft rgt)
|
||||
use false = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt
|
||||
use rgt = (BBT.rgt_rotate
|
||||
K
|
||||
V
|
||||
rgt.size
|
||||
rgt.key
|
||||
rgt.val
|
||||
rgt.lft
|
||||
rgt.rgt
|
||||
)
|
||||
(BBT.lft_rotate K V new_size key val lft rgt)
|
||||
(~(Cmp.is_gtn (cmp set_key rgt.key))
|
||||
P
|
||||
true
|
||||
false
|
||||
new_size
|
||||
node_key
|
||||
val
|
||||
lft
|
||||
rgt.key
|
||||
rgt.val
|
||||
rgt.lft
|
||||
rgt.rgt
|
||||
)
|
||||
use tip = (BBT.tip K V)
|
||||
(~rgt P bin tip)
|
||||
use BBT/{bin,tip,lft_rotate,rgt_rotate}
|
||||
use Bool/{true,false}
|
||||
|
||||
rgt_heavier <K> <V>
|
||||
(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
(new_size: U60)
|
||||
(node_key: K)
|
||||
(set_key: K)
|
||||
(val: V)
|
||||
(lft: (BBT K V))
|
||||
(rgt: (BBT K V))
|
||||
: (BBT K V) =
|
||||
match rgt {
|
||||
bin:
|
||||
match _ = (Cmp/is_gtn (cmp set_key rgt.key)) {
|
||||
true:
|
||||
use rgt = (bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt)
|
||||
(lft_rotate new_size rgt.key val lft rgt)
|
||||
false:
|
||||
use rgt = (rgt_rotate rgt.size rgt.key rgt.val rgt.lft rgt.rgt)
|
||||
(lft_rotate new_size rgt.key val lft rgt)
|
||||
}
|
||||
tip: (tip K V)
|
||||
}
|
||||
|
||||
|
||||
|
||||
//BBT.balance.rgt_heavier
|
||||
//: ∀(K: *)
|
||||
//∀(V: *)
|
||||
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
//∀(new_size: U60)
|
||||
//∀(node_key: K)
|
||||
//∀(set_key: K)
|
||||
//∀(val: V)
|
||||
//∀(lft: (BBT K V))
|
||||
//∀(rgt: (BBT K V))
|
||||
//(BBT K V)
|
||||
//= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt
|
||||
//use P = λx (BBT K V)
|
||||
//use bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt
|
||||
//use P = λx
|
||||
//∀(new_size: U60)
|
||||
//∀(key: K)
|
||||
//∀(val: V)
|
||||
//∀(lft: (BBT K V))
|
||||
//∀(rgt.key: K)
|
||||
//∀(rgt.val: V)
|
||||
//∀(rgt.lft: (BBT K V))
|
||||
//∀(rgt.rgt: (BBT K V))
|
||||
//(BBT K V)
|
||||
//use true = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt
|
||||
//use rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt)
|
||||
//(BBT.lft_rotate K V new_size key val lft rgt)
|
||||
//use false = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt
|
||||
//use rgt = (BBT.rgt_rotate
|
||||
//K
|
||||
//V
|
||||
//rgt.size
|
||||
//rgt.key
|
||||
//rgt.val
|
||||
//rgt.lft
|
||||
//rgt.rgt
|
||||
//)
|
||||
//(BBT.lft_rotate K V new_size key val lft rgt)
|
||||
//(~(Cmp.is_gtn (cmp set_key rgt.key))
|
||||
//P
|
||||
//true
|
||||
//false
|
||||
//new_size
|
||||
//node_key
|
||||
//val
|
||||
//lft
|
||||
//rgt.key
|
||||
//rgt.val
|
||||
//rgt.lft
|
||||
//rgt.rgt
|
||||
//)
|
||||
//use tip = (BBT.tip K V)
|
||||
//(~rgt P bin tip)
|
||||
|
||||
@ -8,4 +8,4 @@ BBT.bin
|
||||
∀(rgt: (BBT K V))
|
||||
(BBT K V)
|
||||
= λK λV λsize λkey λval λlft λrgt
|
||||
~λP λbin λtip (bin size key val lft rgt)
|
||||
~λP λbin λtip (bin size key val lft rgt)
|
||||
|
||||
@ -1,15 +1,28 @@
|
||||
BBT.from_list
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
∀(list: (List (Pair K V)))
|
||||
(BBT K V)
|
||||
= λK λV λcmp λlist
|
||||
use P = λx (BBT K V)
|
||||
use cons = λhead λtail
|
||||
use P = λx (BBT K V)
|
||||
use new = λkey λval
|
||||
(BBT.set K V cmp key val (BBT.from_list K V cmp tail))
|
||||
(~head P new)
|
||||
use nil = (BBT.tip K V)
|
||||
(~list P cons nil)
|
||||
use BBT/{bin,tip,set}
|
||||
|
||||
from_list <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (list: (List (Pair K V))) : (BBT K V) =
|
||||
match list {
|
||||
List/cons:
|
||||
match pair = list.head {
|
||||
Pair/new: (set cmp pair.fst pair.snd (from_list cmp list.tail))
|
||||
}
|
||||
List/nil: (tip K V)
|
||||
}
|
||||
|
||||
|
||||
|
||||
//BBT.from_list
|
||||
//: ∀(K: *)
|
||||
//∀(V: *)
|
||||
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
//∀(list: (List (Pair K V)))
|
||||
//(BBT K V)
|
||||
//= λK λV λcmp λlist
|
||||
//use P = λx (BBT K V)
|
||||
//use cons = λhead λtail
|
||||
//use P = λx (BBT K V)
|
||||
//use new = λkey λval
|
||||
//(BBT.set K V cmp key val (BBT.from_list K V cmp tail))
|
||||
//(~head P new)
|
||||
//use nil = (BBT.tip K V)
|
||||
//(~list P cons nil)
|
||||
|
||||
@ -1,18 +1,34 @@
|
||||
BBT.get
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
∀(key: K)
|
||||
∀(map: (BBT K V))
|
||||
(Maybe V)
|
||||
= λK λV λcmp λkey λmap
|
||||
use P = λx (Maybe V)
|
||||
use bin = λ_size λnext.key λnext.val λnext.lft λnext.rgt
|
||||
use P = λx
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) (Maybe V)
|
||||
use ltn = λcmp λkey (BBT.get K V cmp key next.lft)
|
||||
use eql = λcmp λkey (Maybe.some V next.val)
|
||||
use gtn = λcmp λkey (BBT.get K V cmp key next.rgt)
|
||||
(~(cmp key next.key) P ltn eql gtn cmp key)
|
||||
use tip = (Maybe.none V)
|
||||
(~map P bin tip)
|
||||
use BBT/{bin,tip}
|
||||
use Cmp/{ltn,eql,gtn}
|
||||
|
||||
get <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : (Maybe V) =
|
||||
match map {
|
||||
bin:
|
||||
match _ = (cmp key map.key) {
|
||||
ltn: (get cmp key map.lft)
|
||||
eql: (Maybe/some map.val)
|
||||
gtn: (get cmp key map.rgt)
|
||||
}
|
||||
tip: Maybe/none
|
||||
}
|
||||
|
||||
|
||||
|
||||
//BBT.get
|
||||
//: ∀(K: *)
|
||||
//∀(V: *)
|
||||
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
//∀(key: K)
|
||||
//∀(map: (BBT K V))
|
||||
//(Maybe V)
|
||||
//= λK λV λcmp λkey λmap
|
||||
//use P = λx (Maybe V)
|
||||
//use bin = λ_size λnext.key λnext.val λnext.lft λnext.rgt
|
||||
//use P = λx
|
||||
//∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) (Maybe V)
|
||||
//use ltn = λcmp λkey (BBT.get K V cmp key next.lft)
|
||||
//use eql = λcmp λkey (Maybe.some V next.val)
|
||||
//use gtn = λcmp λkey (BBT.get K V cmp key next.rgt)
|
||||
//(~(cmp key next.key) P ltn eql gtn cmp key)
|
||||
//use tip = (Maybe.none V)
|
||||
//(~map P bin tip)
|
||||
|
||||
@ -1,43 +1,70 @@
|
||||
BBT.got
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
∀(key: K)
|
||||
∀(map: (BBT K V))
|
||||
(Pair (Maybe V) (BBT K V))
|
||||
= λK λV λcmp λkey λmap
|
||||
use P = λx (Pair (Maybe V) (BBT K V))
|
||||
use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
|
||||
use P = λx
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K)
|
||||
(Pair (Maybe V) (BBT K V))
|
||||
use ltn = λcmp λkey
|
||||
use new_pair = (BBT.got K V cmp key next.lft)
|
||||
use P = λx (Pair (Maybe V) (BBT K V))
|
||||
use new = λval λlft
|
||||
use map = (BBT.bin K V size next.key next.val lft next.rgt)
|
||||
(Pair.new (Maybe V) (BBT K V) val map)
|
||||
(~new_pair P new)
|
||||
use eql = λcmp λkey
|
||||
use map = (BBT.bin K V size next.key next.val next.lft next.rgt)
|
||||
(Pair.new
|
||||
(Maybe V)
|
||||
(BBT K V)
|
||||
(Maybe.some V next.val)
|
||||
map
|
||||
)
|
||||
use gtn = λcmp λkey
|
||||
use new_pair = (BBT.got K V cmp key next.rgt)
|
||||
use P = λx (Pair (Maybe V) (BBT K V))
|
||||
use new = λval λrgt
|
||||
use map = (BBT.bin K V size next.key next.val next.lft rgt)
|
||||
(Pair.new (Maybe V) (BBT K V) val map)
|
||||
(~new_pair P new)
|
||||
(~(cmp key next.key) P ltn eql gtn cmp key)
|
||||
use tip = (Pair.new
|
||||
(Maybe V)
|
||||
(BBT K V)
|
||||
(Maybe.none V)
|
||||
(BBT.tip K V)
|
||||
)
|
||||
(~map P bin tip)
|
||||
use BBT/{bin,tip}
|
||||
use Maybe/{some,none}
|
||||
use Cmp/{ltn,eql,gtn}
|
||||
|
||||
got <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : (Pair (Maybe V) (BBT K V)) =
|
||||
match map {
|
||||
bin:
|
||||
match _ = (cmp key map.key) {
|
||||
ltn:
|
||||
match new_pair = (got cmp key map.lft) {
|
||||
Pair/new:
|
||||
let map = (bin K V map.size map.key map.val new_pair.snd map.rgt)
|
||||
(Pair/new new_pair.fst map)
|
||||
}
|
||||
eql: (Pair/new (some map.val) map)
|
||||
gtn:
|
||||
match new_pair = (got cmp key map.rgt) {
|
||||
Pair/new:
|
||||
let map = (bin K V map.size map.key map.val map.lft new_pair.snd)
|
||||
(Pair/new new_pair.fst map)
|
||||
}
|
||||
}
|
||||
tip: (Pair/new none (tip K V))
|
||||
}
|
||||
|
||||
|
||||
|
||||
//BBT.got
|
||||
//: ∀(K: *)
|
||||
//∀(V: *)
|
||||
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
//∀(key: K)
|
||||
//∀(map: (BBT K V))
|
||||
//(Pair (Maybe V) (BBT K V))
|
||||
//= λK λV λcmp λkey λmap
|
||||
//use P = λx (Pair (Maybe V) (BBT K V))
|
||||
//use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
|
||||
//use P = λx
|
||||
//∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K)
|
||||
//(Pair (Maybe V) (BBT K V))
|
||||
//use ltn = λcmp λkey
|
||||
//use new_pair = (BBT.got K V cmp key next.lft)
|
||||
//use P = λx (Pair (Maybe V) (BBT K V))
|
||||
//use new = λval λlft
|
||||
//use map = (BBT.bin K V size next.key next.val lft next.rgt)
|
||||
//(Pair.new (Maybe V) (BBT K V) val map)
|
||||
//(~new_pair P new)
|
||||
//use eql = λcmp λkey
|
||||
//use map = (BBT.bin K V size next.key next.val next.lft next.rgt)
|
||||
//(Pair.new
|
||||
//(Maybe V)
|
||||
//(BBT K V)
|
||||
//(Maybe.some V next.val)
|
||||
//map
|
||||
//)
|
||||
//use gtn = λcmp λkey
|
||||
//use new_pair = (BBT.got K V cmp key next.rgt)
|
||||
//use P = λx (Pair (Maybe V) (BBT K V))
|
||||
//use new = λval λrgt
|
||||
//use map = (BBT.bin K V size next.key next.val next.lft rgt)
|
||||
//(Pair.new (Maybe V) (BBT K V) val map)
|
||||
//(~new_pair P new)
|
||||
//(~(cmp key next.key) P ltn eql gtn cmp key)
|
||||
//use tip = (Pair.new
|
||||
//(Maybe V)
|
||||
//(BBT K V)
|
||||
//(Maybe.none V)
|
||||
//(BBT.tip K V)
|
||||
//)
|
||||
//(~map P bin tip)
|
||||
|
||||
@ -1,10 +1,20 @@
|
||||
BBT.got_size
|
||||
: ∀(K: *) ∀(V: *) ∀(map: (BBT K V))
|
||||
(Pair U60 (BBT K V))
|
||||
= λK λV λmap
|
||||
use P = λx (Pair U60 (BBT K V))
|
||||
use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
|
||||
use map = (BBT.bin K V size next.key next.val next.lft next.rgt)
|
||||
(Pair.new U60 (BBT K V) size map)
|
||||
use tip = (Pair.new U60 (BBT K V) 0 (BBT.tip K V))
|
||||
(~map P bin tip)
|
||||
use BBT/{bin,tip}
|
||||
|
||||
got_size <K> <V> (map: (BBT K V)) : (Pair U60 (BBT K V)) =
|
||||
match map {
|
||||
bin: (Pair/new map.size map)
|
||||
tip: (Pair/new 0 (tip K V))
|
||||
}
|
||||
|
||||
|
||||
|
||||
//BBT.got_size
|
||||
//: ∀(K: *) ∀(V: *) ∀(map: (BBT K V))
|
||||
//(Pair U60 (BBT K V))
|
||||
//= λK λV λmap
|
||||
//use P = λx (Pair U60 (BBT K V))
|
||||
//use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
|
||||
//use map = (BBT.bin K V size next.key next.val next.lft next.rgt)
|
||||
//(Pair.new U60 (BBT K V) size map)
|
||||
//use tip = (Pair.new U60 (BBT K V) 0 (BBT.tip K V))
|
||||
//(~map P bin tip)
|
||||
|
||||
@ -1,17 +1,33 @@
|
||||
BBT.has
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
∀(key: K)
|
||||
∀(map: (BBT K V))
|
||||
Bool
|
||||
= λK λV λcmp λkey λmap
|
||||
use P = λx Bool
|
||||
use bin = λnext.size λnext.key λnext.val λnext.lft λnext.rgt
|
||||
use P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) Bool
|
||||
use ltn = λcmp λkey (BBT.has K V cmp key next.lft)
|
||||
use eql = λcmp λkey Bool.true
|
||||
use gtn = λcmp λkey (BBT.has K V cmp key next.rgt)
|
||||
(~(cmp key next.key) P ltn eql gtn cmp key)
|
||||
use tip = Bool.false
|
||||
(~map P bin tip)
|
||||
use BBT/{bin,tip}
|
||||
use Cmp/{ltn,eql,gtn}
|
||||
|
||||
has <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : Bool =
|
||||
match map {
|
||||
bin:
|
||||
match _ = (cmp key map.key) {
|
||||
ltn: (has cmp key map.lft)
|
||||
eql: Bool/true
|
||||
gtn: (has cmp key map.rgt)
|
||||
}
|
||||
tip: Bool/false
|
||||
}
|
||||
|
||||
|
||||
|
||||
//BBT.has
|
||||
//: ∀(K: *)
|
||||
//∀(V: *)
|
||||
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
//∀(key: K)
|
||||
//∀(map: (BBT K V))
|
||||
//Bool
|
||||
//= λK λV λcmp λkey λmap
|
||||
//use P = λx Bool
|
||||
//use bin = λnext.size λnext.key λnext.val λnext.lft λnext.rgt
|
||||
//use P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) Bool
|
||||
//use ltn = λcmp λkey (BBT.has K V cmp key next.lft)
|
||||
//use eql = λcmp λkey Bool.true
|
||||
//use gtn = λcmp λkey (BBT.has K V cmp key next.rgt)
|
||||
//(~(cmp key next.key) P ltn eql gtn cmp key)
|
||||
//use tip = Bool.false
|
||||
//(~map P bin tip)
|
||||
|
||||
@ -1,51 +1,74 @@
|
||||
BBT.has.linear
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
∀(key: K)
|
||||
∀(map: (BBT K V))
|
||||
(Pair Bool (BBT K V))
|
||||
= λK λV λcmp λhas_key λmap
|
||||
use P = λx (Pair Bool (BBT K V))
|
||||
use bin = λsize λnode_key λval λlft λrgt
|
||||
use P = λx
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
∀(size: U60)
|
||||
∀(node_key: K)
|
||||
∀(val: V)
|
||||
∀(lft: (BBT K V))
|
||||
∀(rgt: (BBT K V))
|
||||
∀(key: K)
|
||||
(Pair Bool (BBT K V))
|
||||
use ltn = λcmp λsize λnode_key λval λlft λrgt λhas_key
|
||||
use P = λx (Pair Bool (BBT K V))
|
||||
use new = λbool λlft
|
||||
use map = (BBT.bin K V size node_key val lft rgt)
|
||||
(Pair.new Bool (BBT K V) bool map)
|
||||
(~(BBT.has.linear K V cmp has_key lft) P new)
|
||||
use eql = λcmp λsize λnode_key λval λlft λrgt λhas_key
|
||||
(Pair.new
|
||||
Bool
|
||||
(BBT K V)
|
||||
Bool.true
|
||||
(BBT.bin K V size node_key val lft rgt)
|
||||
)
|
||||
use gtn = λcmp λsize λnode_key λval λlft λrgt λhas_key
|
||||
use P = λx (Pair Bool (BBT K V))
|
||||
use new = λbool λrgt
|
||||
use map = (BBT.bin K V size node_key val lft rgt)
|
||||
(Pair.new Bool (BBT K V) bool rgt)
|
||||
(~(BBT.has.linear K V cmp has_key rgt) P new)
|
||||
((~(cmp has_key node_key) P ltn eql gtn)
|
||||
cmp
|
||||
size
|
||||
node_key
|
||||
val
|
||||
lft
|
||||
rgt
|
||||
has_key
|
||||
)
|
||||
use tip = (Pair.new Bool (BBT K V) Bool.false (BBT.tip K V))
|
||||
(~map P bin tip)
|
||||
use BBT/{bin,tip}
|
||||
use Bool/{false,true}
|
||||
use Cmp/{ltn,eql,gtn}
|
||||
|
||||
|
||||
linear <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : (Pair Bool (BBT K V)) =
|
||||
match map {
|
||||
bin:
|
||||
match _ = (cmp key map.key) {
|
||||
ltn:
|
||||
match result = (linear cmp key map.lft) {
|
||||
Pair/new:
|
||||
(Pair/new result.fst (bin K V map.size map.key map.val result.snd map.rgt))
|
||||
}
|
||||
eql: (Pair/new true (bin K V map.size map.key map.val map.lft map.rgt))
|
||||
gtn:
|
||||
match result = (linear cmp key map.rgt) {
|
||||
Pair/new:
|
||||
(Pair/new result.fst (bin K V map.size map.key map.val map.lft result.snd))
|
||||
}
|
||||
}
|
||||
tip: (Pair/new false (tip K V))
|
||||
}
|
||||
|
||||
|
||||
|
||||
//BBT.has.linear
|
||||
//: ∀(K: *)
|
||||
//∀(V: *)
|
||||
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
//∀(key: K)
|
||||
//∀(map: (BBT K V))
|
||||
//(Pair Bool (BBT K V))
|
||||
//= λK λV λcmp λhas_key λmap
|
||||
//use P = λx (Pair Bool (BBT K V))
|
||||
//use bin = λsize λnode_key λval λlft λrgt
|
||||
//use P = λx
|
||||
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
//∀(size: U60)
|
||||
//∀(node_key: K)
|
||||
//∀(val: V)
|
||||
//∀(lft: (BBT K V))
|
||||
//∀(rgt: (BBT K V))
|
||||
//∀(key: K)
|
||||
//(Pair Bool (BBT K V))
|
||||
//use ltn = λcmp λsize λnode_key λval λlft λrgt λhas_key
|
||||
//use P = λx (Pair Bool (BBT K V))
|
||||
//use new = λbool λlft
|
||||
//use map = (BBT.bin K V size node_key val lft rgt)
|
||||
//(Pair.new Bool (BBT K V) bool map)
|
||||
//(~(BBT.has.linear K V cmp has_key lft) P new)
|
||||
//use eql = λcmp λsize λnode_key λval λlft λrgt λhas_key
|
||||
//(Pair.new
|
||||
//Bool
|
||||
//(BBT K V)
|
||||
//Bool.true
|
||||
//(BBT.bin K V size node_key val lft rgt)
|
||||
//)
|
||||
//use gtn = λcmp λsize λnode_key λval λlft λrgt λhas_key
|
||||
//use P = λx (Pair Bool (BBT K V))
|
||||
//use new = λbool λrgt
|
||||
//use map = (BBT.bin K V size node_key val lft rgt)
|
||||
//(Pair.new Bool (BBT K V) bool rgt)
|
||||
//(~(BBT.has.linear K V cmp has_key rgt) P new)
|
||||
//((~(cmp has_key node_key) P ltn eql gtn)
|
||||
//cmp
|
||||
//size
|
||||
//node_key
|
||||
//val
|
||||
//lft
|
||||
//rgt
|
||||
//has_key
|
||||
//)
|
||||
//use tip = (Pair.new Bool (BBT K V) Bool.false (BBT.tip K V))
|
||||
//(~map P bin tip)
|
||||
|
||||
@ -1,18 +1,31 @@
|
||||
BBT.lft_rotate
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(size: U60)
|
||||
∀(key: K)
|
||||
∀(val: V)
|
||||
∀(lft: (BBT K V))
|
||||
∀(rgt: (BBT K V))
|
||||
(BBT K V)
|
||||
= λK λV λsize λkey λval λlft λrgt
|
||||
use P = λx ∀(key: K) ∀(val: V) ∀(lft: (BBT K V)) (BBT K V)
|
||||
use bin = λ_size λrgt.key λrgt.val λrgt.lft λrgt.rgt λkey λval λlft
|
||||
use b = (BBT.new_node K V key val lft rgt.lft)
|
||||
use a = (BBT.new_node K V rgt.key rgt.val b rgt.rgt)
|
||||
a
|
||||
use tip = λkey λval λlft
|
||||
(BBT.bin K V size key val lft (BBT.tip K V))
|
||||
(~rgt P bin tip key val lft)
|
||||
use BBT/{bin,tip}
|
||||
|
||||
lft_rotate <K> <V> (size: U60) (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V)) : (BBT K V) =
|
||||
match rgt {
|
||||
bin:
|
||||
use b = (BBT/new_node key val lft rgt.lft)
|
||||
use a = (BBT/new_node rgt.key rgt.val b rgt.rgt)
|
||||
a
|
||||
tip: (bin K V size key val lft (tip K V))
|
||||
}
|
||||
|
||||
|
||||
|
||||
//BBT.lft_rotate
|
||||
//: ∀(K: *)
|
||||
//∀(V: *)
|
||||
//∀(size: U60)
|
||||
//∀(key: K)
|
||||
//∀(val: V)
|
||||
//∀(lft: (BBT K V))
|
||||
//∀(rgt: (BBT K V))
|
||||
//(BBT K V)
|
||||
//= λK λV λsize λkey λval λlft λrgt
|
||||
//use P = λx ∀(key: K) ∀(val: V) ∀(lft: (BBT K V)) (BBT K V)
|
||||
//use bin = λ_size λrgt.key λrgt.val λrgt.lft λrgt.rgt λkey λval λlft
|
||||
//use b = (BBT.new_node K V key val lft rgt.lft)
|
||||
//use a = (BBT.new_node K V rgt.key rgt.val b rgt.rgt)
|
||||
//a
|
||||
//use tip = λkey λval λlft
|
||||
//(BBT.bin K V size key val lft (BBT.tip K V))
|
||||
//(~rgt P bin tip key val lft)
|
||||
|
||||
@ -1,17 +1,30 @@
|
||||
BBT.new_node
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(key: K)
|
||||
∀(val: V)
|
||||
∀(lft: (BBT K V))
|
||||
∀(rgt: (BBT K V))
|
||||
(BBT K V)
|
||||
= λK λV λkey λval λlft λrgt
|
||||
use P = λx (BBT K V)
|
||||
use new = λlft.size λlft
|
||||
use P = λx (BBT K V)
|
||||
use new = λrgt.size λrgt
|
||||
use new_size = (+ 1 (U60.max rgt.size lft.size))
|
||||
(BBT.bin K V new_size key val lft rgt)
|
||||
(~(BBT.got_size K V rgt) P new)
|
||||
(~(BBT.got_size K V lft) P new)
|
||||
use BBT/{bin}
|
||||
|
||||
new_node <K> <V> (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V)) : (BBT K V) =
|
||||
match lft_size = (BBT/got_size lft) {
|
||||
Pair/new: match rgt_size = (BBT/got_size rgt) {
|
||||
Pair/new:
|
||||
use new_size = (+ 1 (U60/max lft_size.fst rgt_size.fst))
|
||||
(bin K V new_size key val lft rgt)
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
//BBT.new_node
|
||||
//: ∀(K: *)
|
||||
//∀(V: *)
|
||||
//∀(key: K)
|
||||
//∀(val: V)
|
||||
//∀(lft: (BBT K V))
|
||||
//∀(rgt: (BBT K V))
|
||||
//(BBT K V)
|
||||
//= λK λV λkey λval λlft λrgt
|
||||
//use P = λx (BBT K V)
|
||||
//use new = λlft.size λlft
|
||||
//use P = λx (BBT K V)
|
||||
//use new = λrgt.size λrgt
|
||||
//use new_size = (+ 1 (U60.max rgt.size lft.size))
|
||||
//(BBT.bin K V new_size key val lft rgt)
|
||||
//(~(BBT.got_size K V rgt) P new)
|
||||
//(~(BBT.got_size K V lft) P new)
|
||||
|
||||
@ -1,18 +1,31 @@
|
||||
BBT.rgt_rotate
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(size: U60)
|
||||
∀(key: K)
|
||||
∀(val: V)
|
||||
∀(lft: (BBT K V))
|
||||
∀(rgt: (BBT K V))
|
||||
(BBT K V)
|
||||
= λK λV λsize λkey λval λlft λrgt
|
||||
use P = λx ∀(key: K) ∀(val: V) ∀(rgt: (BBT K V)) (BBT K V)
|
||||
use bin = λ_size λlft.key λlft.val λlft.lft λlft.rgt λkey λval λrgt
|
||||
use b = (BBT.new_node K V key val lft.rgt rgt)
|
||||
use a = (BBT.new_node K V lft.key lft.val lft.lft b)
|
||||
a
|
||||
use tip = λkey λval λrgt
|
||||
(BBT.bin K V size key val (BBT.tip K V) rgt)
|
||||
(~lft P bin tip key val rgt)
|
||||
use BBT/{bin,tip}
|
||||
|
||||
rgt_rotate <K> <V> (size: U60) (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V)) : (BBT K V) =
|
||||
match lft {
|
||||
bin:
|
||||
use b = (BBT/new_node key val lft.rgt rgt)
|
||||
use a = (BBT/new_node lft.key lft.val lft.lft b)
|
||||
a
|
||||
tip: (bin K V size key val (tip K V) rgt)
|
||||
}
|
||||
|
||||
|
||||
|
||||
//BBT.rgt_rotate
|
||||
//: ∀(K: *)
|
||||
//∀(V: *)
|
||||
//∀(size: U60)
|
||||
//∀(key: K)
|
||||
//∀(val: V)
|
||||
//∀(lft: (BBT K V))
|
||||
//∀(rgt: (BBT K V))
|
||||
//(BBT K V)
|
||||
//= λK λV λsize λkey λval λlft λrgt
|
||||
//use P = λx ∀(key: K) ∀(val: V) ∀(rgt: (BBT K V)) (BBT K V)
|
||||
//use bin = λ_size λlft.key λlft.val λlft.lft λlft.rgt λkey λval λrgt
|
||||
//use b = (BBT.new_node K V key val lft.rgt rgt)
|
||||
//use a = (BBT.new_node K V lft.key lft.val lft.lft b)
|
||||
//a
|
||||
//use tip = λkey λval λrgt
|
||||
//(BBT.bin K V size key val (BBT.tip K V) rgt)
|
||||
//(~lft P bin tip key val rgt)
|
||||
|
||||
@ -1,61 +1,81 @@
|
||||
BBT.set
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
∀(key: K)
|
||||
∀(val: V)
|
||||
∀(map: (BBT K V))
|
||||
(BBT K V)
|
||||
= λK λV λcmp λkey λval λmap
|
||||
use P = λx ∀(key: K) ∀(val: V) (BBT K V)
|
||||
use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt λkey λval
|
||||
use P = λx
|
||||
∀(key: K)
|
||||
∀(next.key: K)
|
||||
∀(next.val: V)
|
||||
∀(next.lft: (BBT K V))
|
||||
∀(next.rgt: (BBT K V))
|
||||
∀(key: K)
|
||||
∀(val: V)
|
||||
(BBT K V)
|
||||
use ltn = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
|
||||
use new_lft = (BBT.set K V cmp key val next.lft)
|
||||
(BBT.balance
|
||||
K
|
||||
V
|
||||
cmp
|
||||
key
|
||||
next.key
|
||||
next.val
|
||||
new_lft
|
||||
next.rgt
|
||||
)
|
||||
use eql = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
|
||||
(BBT.bin K V size next.key val next.lft next.rgt)
|
||||
use gtn = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
|
||||
use new_rgt = (BBT.set K V cmp key val next.rgt)
|
||||
(BBT.balance
|
||||
K
|
||||
V
|
||||
cmp
|
||||
key
|
||||
next.key
|
||||
next.val
|
||||
next.lft
|
||||
new_rgt
|
||||
)
|
||||
(~(cmp key next.key)
|
||||
P
|
||||
ltn
|
||||
eql
|
||||
gtn
|
||||
key
|
||||
next.key
|
||||
next.val
|
||||
next.lft
|
||||
next.rgt
|
||||
key
|
||||
val
|
||||
)
|
||||
use tip = λkey λval (BBT.singleton K V key val)
|
||||
(~map P bin tip key val)
|
||||
use BBT/{bin,tip}
|
||||
use Cmp/{ltn,eql,gtn}
|
||||
|
||||
set <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (val: V) (map: (BBT K V)) : (BBT K V) =
|
||||
match map {
|
||||
bin:
|
||||
match _ = (cmp key map.key) {
|
||||
ltn:
|
||||
use new_lft = (set cmp key val map.lft)
|
||||
(BBT/balance cmp key map.key map.val new_lft map.rgt)
|
||||
eql: (bin K V map.size map.key val map.lft map.rgt)
|
||||
gtn:
|
||||
use new_rgt = (set cmp key val map.rgt)
|
||||
(BBT/balance cmp key map.key map.val map.lft new_rgt)
|
||||
}
|
||||
tip: (BBT/singleton key val)
|
||||
}
|
||||
|
||||
|
||||
|
||||
//BBT.set
|
||||
//: ∀(K: *)
|
||||
//∀(V: *)
|
||||
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
//∀(key: K)
|
||||
//∀(val: V)
|
||||
//∀(map: (BBT K V))
|
||||
//(BBT K V)
|
||||
//= λK λV λcmp λkey λval λmap
|
||||
//use P = λx ∀(key: K) ∀(val: V) (BBT K V)
|
||||
//use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt λkey λval
|
||||
//use P = λx
|
||||
//∀(key: K)
|
||||
//∀(next.key: K)
|
||||
//∀(next.val: V)
|
||||
//∀(next.lft: (BBT K V))
|
||||
//∀(next.rgt: (BBT K V))
|
||||
//∀(key: K)
|
||||
//∀(val: V)
|
||||
//(BBT K V)
|
||||
//use ltn = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
|
||||
//use new_lft = (BBT.set K V cmp key val next.lft)
|
||||
//(BBT.balance
|
||||
//K
|
||||
//V
|
||||
//cmp
|
||||
//key
|
||||
//next.key
|
||||
//next.val
|
||||
//new_lft
|
||||
//next.rgt
|
||||
//)
|
||||
//use eql = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
|
||||
//(BBT.bin K V size next.key val next.lft next.rgt)
|
||||
//use gtn = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
|
||||
//use new_rgt = (BBT.set K V cmp key val next.rgt)
|
||||
//(BBT.balance
|
||||
//K
|
||||
//V
|
||||
//cmp
|
||||
//key
|
||||
//next.key
|
||||
//next.val
|
||||
//next.lft
|
||||
//new_rgt
|
||||
//)
|
||||
//(~(cmp key next.key)
|
||||
//P
|
||||
//ltn
|
||||
//eql
|
||||
//gtn
|
||||
//key
|
||||
//next.key
|
||||
//next.val
|
||||
//next.lft
|
||||
//next.rgt
|
||||
//key
|
||||
//val
|
||||
//)
|
||||
//use tip = λkey λval (BBT.singleton K V key val)
|
||||
//(~map P bin tip key val)
|
||||
|
||||
@ -1,4 +1,10 @@
|
||||
BBT.singleton
|
||||
: ∀(K: *) ∀(V: *) ∀(key: K) ∀(val: V) (BBT K V)
|
||||
= λK λV λkey λval
|
||||
(BBT.bin K V 1 key val (BBT.tip K V) (BBT.tip K V))
|
||||
singleton <K> <V> (key: K) (val: V) : (BBT K V) =
|
||||
use tip = (BBT/tip K V)
|
||||
(BBT/bin K V 1 key val tip tip)
|
||||
|
||||
|
||||
|
||||
//BBT.singleton
|
||||
//: ∀(K: *) ∀(V: *) ∀(key: K) ∀(val: V) (BBT K V)
|
||||
//= λK λV λkey λval
|
||||
//(BBT.bin K V 1 key val (BBT.tip K V) (BBT.tip K V))
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
BBT.tip
|
||||
: ∀(K: *) ∀(V: *) (BBT K V)
|
||||
= λK λV ~λP λbin λtip tip
|
||||
= λK λV ~λP λbin λtip tip
|
||||
|
||||
@ -1,17 +1,32 @@
|
||||
BBT.to_list
|
||||
: ∀(K: *) ∀(V: *) ∀(map: (BBT K V))
|
||||
(List (Pair K V))
|
||||
= λK λV λmap
|
||||
use P = λx (List (Pair K V))
|
||||
use bin = λsize λkey λval λlft λrgt
|
||||
use lft = (BBT.to_list K V lft)
|
||||
use rgt = (BBT.to_list K V rgt)
|
||||
use pair = (Pair.new K V key val)
|
||||
use list = (List.cons
|
||||
(Pair K V)
|
||||
pair
|
||||
(List.concat (Pair K V) lft rgt)
|
||||
)
|
||||
list
|
||||
use tip = (List.nil (Pair K V))
|
||||
(~map P bin tip)
|
||||
use BBT/{bin,tip}
|
||||
|
||||
to_list <K> <V> (map: (BBT K V)) : (List (Pair K V)) =
|
||||
match map {
|
||||
bin:
|
||||
use lft = (to_list map.lft)
|
||||
use rgt = (to_list map.rgt)
|
||||
use pair = (Pair/new map.key map.val)
|
||||
use list = (List/cons pair (List/concat lft rgt))
|
||||
list
|
||||
tip: List/nil
|
||||
}
|
||||
|
||||
|
||||
|
||||
//BBT.to_list
|
||||
//: ∀(K: *) ∀(V: *) ∀(map: (BBT K V))
|
||||
//(List (Pair K V))
|
||||
//= λK λV λmap
|
||||
//use P = λx (List (Pair K V))
|
||||
//use bin = λsize λkey λval λlft λrgt
|
||||
//use lft = (BBT.to_list K V lft)
|
||||
//use rgt = (BBT.to_list K V rgt)
|
||||
//use pair = (Pair.new K V key val)
|
||||
//use list = (List.cons
|
||||
//(Pair K V)
|
||||
//pair
|
||||
//(List.concat (Pair K V) lft rgt)
|
||||
//)
|
||||
//list
|
||||
//use tip = (List.nil (Pair K V))
|
||||
//(~map P bin tip)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user