mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-08-16 22:00:46 +03:00
BBT updates
This commit is contained in:
parent
c6be73b582
commit
95e65c55a6
@ -51,12 +51,12 @@ BBT.balance.lft_heavier
|
|||||||
let 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)
|
let 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)
|
||||||
|
|
||||||
// key > lft.key
|
// key > lft.key
|
||||||
let true = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt // Parent Lambdas
|
let true = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt
|
||||||
let lft = (BBT.lft_rotate K V lft.size lft.key lft.val lft.lft lft.rgt)
|
let 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)
|
(BBT.rgt_rotate K V new_size key val lft rgt)
|
||||||
|
|
||||||
// key < lft.key
|
// key < lft.key
|
||||||
let false = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt // Parent Lambdas
|
let false = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt
|
||||||
let lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt)
|
let 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)
|
(BBT.rgt_rotate K V new_size key val lft rgt)
|
||||||
|
|
||||||
@ -78,21 +78,21 @@ BBT.balance_rgt_heavier
|
|||||||
∀(lft: (BBT K V))
|
∀(lft: (BBT K V))
|
||||||
∀(rgt: (BBT K V))
|
∀(rgt: (BBT K V))
|
||||||
(BBT K V)
|
(BBT K V)
|
||||||
= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt // Parent Lambdas
|
= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt
|
||||||
let P = λx(BBT K V)
|
let P = λx(BBT K V)
|
||||||
let bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt
|
let bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt
|
||||||
let 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)
|
let 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)
|
||||||
|
|
||||||
// key > rgt.key
|
// key > rgt.key
|
||||||
// rotating parent once to the left
|
// rotating parent once to the left
|
||||||
let true = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt // Parent Lambdas
|
let true = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt
|
||||||
let rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt)
|
let 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)
|
(BBT.lft_rotate K V new_size key val lft rgt)
|
||||||
|
|
||||||
// key < rgt.key
|
// key < rgt.key
|
||||||
// rotating parent once to the left
|
// rotating parent once to the left
|
||||||
// rotating right child once to the right
|
// rotating right child once to the right
|
||||||
let false = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt // Parent Lambdas
|
let false = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt
|
||||||
let rgt = (BBT.rgt_rotate K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt)
|
let 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)
|
(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)
|
((~(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)
|
||||||
|
@ -8,10 +8,10 @@ BBT.get
|
|||||||
= λK λV λcmp λkey λmap
|
= λK λV λcmp λkey λmap
|
||||||
let P = λx(Maybe V)
|
let P = λx(Maybe V)
|
||||||
let bin = λ_size λnext.key λnext.val λnext.lft λnext.rgt
|
let bin = λ_size λnext.key λnext.val λnext.lft λnext.rgt
|
||||||
let P = λx(Maybe V)
|
let P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) (Maybe V)
|
||||||
let ltn = (BBT.get K V cmp key next.lft)
|
let ltn = λcmp λkey (BBT.get K V cmp key next.lft)
|
||||||
let eql = (Maybe.some V next.val)
|
let eql = λcmp λkey (Maybe.some V next.val)
|
||||||
let gtn = (BBT.get K V cmp key next.rgt)
|
let gtn = λcmp λkey (BBT.get K V cmp key next.rgt)
|
||||||
(~(cmp key next.key) P ltn eql gtn)
|
((~(cmp key next.key) P ltn eql gtn) cmp key)
|
||||||
let tip = (Maybe.none V)
|
let tip = (Maybe.none V)
|
||||||
(~map P bin tip)
|
(~map P bin tip)
|
31
book/BBT.got.kind2
Normal file
31
book/BBT.got.kind2
Normal file
@ -0,0 +1,31 @@
|
|||||||
|
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
|
||||||
|
let P = λx(Pair (Maybe V) (BBT K V))
|
||||||
|
let bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
|
||||||
|
let P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) (Pair (Maybe V) (BBT K V))
|
||||||
|
let ltn = λcmp λkey
|
||||||
|
let new_pair = (BBT.got K V cmp key next.lft)
|
||||||
|
let P = λx(Pair (Maybe V) (BBT K V))
|
||||||
|
let new = λval λlft
|
||||||
|
let 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)
|
||||||
|
let eql = λcmp λkey
|
||||||
|
let 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)
|
||||||
|
let gtn = λcmp λkey
|
||||||
|
let new_pair = (BBT.got K V cmp key next.rgt)
|
||||||
|
let P = λx(Pair (Maybe V) (BBT K V))
|
||||||
|
let new = λval λrgt
|
||||||
|
let 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)
|
||||||
|
let tip = (Pair.new (Maybe V) (BBT K V) (Maybe.none V) (BBT.tip K V))
|
||||||
|
(~map P bin tip)
|
@ -13,11 +13,11 @@ BBT.lft_rotate
|
|||||||
= λK λV λsize λkey λval λlft λrgt
|
= λK λV λsize λkey λval λlft λrgt
|
||||||
let P = λx ∀(key: K) ∀(val: V) ∀(lft: (BBT K V)) (BBT K V)
|
let P = λx ∀(key: K) ∀(val: V) ∀(lft: (BBT K V)) (BBT K V)
|
||||||
let bin = λ_size λrgt.key λrgt.val λrgt.lft λrgt.rgt
|
let bin = λ_size λrgt.key λrgt.val λrgt.lft λrgt.rgt
|
||||||
λkey λval λlft // Parent lambdas
|
λkey λval λlft
|
||||||
let b = (BBT.new_node K V key val lft rgt.lft)
|
let b = (BBT.new_node K V key val lft rgt.lft)
|
||||||
let a = (BBT.new_node K V rgt.key rgt.val b rgt.rgt)
|
let a = (BBT.new_node K V rgt.key rgt.val b rgt.rgt)
|
||||||
a
|
a
|
||||||
let tip =
|
let tip =
|
||||||
λkey λval λlft // Parent lambdas
|
λkey λval λlft
|
||||||
(BBT.bin K V size key val lft (BBT.tip K V))
|
(BBT.bin K V size key val lft (BBT.tip K V))
|
||||||
((~rgt P bin tip) key val lft)
|
((~rgt P bin tip) key val lft)
|
||||||
|
@ -13,11 +13,11 @@ BBT.rgt_rotate
|
|||||||
= λK λV λsize λkey λval λlft λrgt
|
= λK λV λsize λkey λval λlft λrgt
|
||||||
let P = λx ∀(key: K) ∀(val: V) ∀(rgt: (BBT K V)) (BBT K V)
|
let P = λx ∀(key: K) ∀(val: V) ∀(rgt: (BBT K V)) (BBT K V)
|
||||||
let bin = λ_size λlft.key λlft.val λlft.lft λlft.rgt
|
let bin = λ_size λlft.key λlft.val λlft.lft λlft.rgt
|
||||||
λkey λval λrgt // Parent lambdas
|
λkey λval λrgt
|
||||||
let b = (BBT.new_node K V key val lft.rgt rgt)
|
let b = (BBT.new_node K V key val lft.rgt rgt)
|
||||||
let a = (BBT.new_node K V lft.key lft.val lft.lft b )
|
let a = (BBT.new_node K V lft.key lft.val lft.lft b )
|
||||||
a
|
a
|
||||||
let tip =
|
let tip =
|
||||||
λkey λval λrgt // Parent lambdas
|
λkey λval λrgt
|
||||||
(BBT.bin K V size key val (BBT.tip K V) rgt)
|
(BBT.bin K V size key val (BBT.tip K V) rgt)
|
||||||
((~lft P bin tip) key val rgt)
|
((~lft P bin tip) key val rgt)
|
||||||
|
@ -8,21 +8,26 @@ BBT.set
|
|||||||
(BBT K V)
|
(BBT K V)
|
||||||
= λK λV λcmp λkey λval λmap
|
= λK λV λcmp λkey λval λmap
|
||||||
let P = λx ∀(key: K) ∀(val: V) (BBT K V)
|
let P = λx ∀(key: K) ∀(val: V) (BBT K V)
|
||||||
let bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
|
let bin = λsize λnext.key λnext.val λnext.lft λnext.rgt λkey λval
|
||||||
λkey λval // Parent Lambdas
|
|
||||||
let P = λx ∀(key: K) ∀(next.key: K) ∀(next.val: V) ∀(next.lft: (BBT K V)) ∀(next.rgt: (BBT K V)) (BBT K V)
|
let P = λx ∀(key: K) ∀(next.key: K) ∀(next.val: V) ∀(next.lft: (BBT K V)) ∀(next.rgt: (BBT K V)) (BBT K V)
|
||||||
|
|
||||||
|
// Go left
|
||||||
let ltn = λkey λnext.key λnext.val λnext.lft λnext.rgt
|
let ltn = λkey λnext.key λnext.val λnext.lft λnext.rgt
|
||||||
let new_lft = (BBT.set K V cmp key val next.lft)
|
let 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)
|
(BBT.balance K V cmp key next.key next.val new_lft next.rgt)
|
||||||
|
|
||||||
|
// Same key, update value
|
||||||
let eql = λkey λnext.key λnext.val λnext.lft λnext.rgt
|
let eql = λkey λnext.key λnext.val λnext.lft λnext.rgt
|
||||||
(BBT.bin K V size next.key val next.lft next.rgt)
|
(BBT.bin K V size next.key val next.lft next.rgt)
|
||||||
|
|
||||||
|
// Go right
|
||||||
let gtn = λkey λnext.key λnext.val λnext.lft λnext.rgt
|
let gtn = λkey λnext.key λnext.val λnext.lft λnext.rgt
|
||||||
let new_rgt = (BBT.set K V cmp key val next.rgt)
|
let 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)
|
(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)
|
((~(cmp key next.key) P ltn eql gtn) key next.key next.val next.lft next.rgt)
|
||||||
let tip = λkey λval // Parent Lambdas
|
|
||||||
|
// Empty tree, create new node
|
||||||
|
let tip = λkey λval
|
||||||
(BBT.singleton K V key val)
|
(BBT.singleton K V key val)
|
||||||
((~map P bin tip) key val)
|
((~map P bin tip) key val)
|
||||||
|
|
||||||
|
@ -50,6 +50,14 @@ U60.get
|
|||||||
= λV λkey λmap
|
= λV λkey λmap
|
||||||
(BBT.get #U60 V U60.cmp key map)
|
(BBT.get #U60 V U60.cmp key map)
|
||||||
|
|
||||||
|
U60.got
|
||||||
|
: ∀(V: *)
|
||||||
|
∀(key: #U60)
|
||||||
|
∀(map: (BBT #U60 V))
|
||||||
|
(Pair (Maybe V) (BBT #U60 V))
|
||||||
|
= λV λkey λmap
|
||||||
|
(BBT.got #U60 V U60.cmp key map)
|
||||||
|
|
||||||
U60.set
|
U60.set
|
||||||
: ∀(V: *)
|
: ∀(V: *)
|
||||||
∀(key: #U60)
|
∀(key: #U60)
|
||||||
@ -219,6 +227,7 @@ testbbt
|
|||||||
// : (List.Map #U60 String)
|
// : (List.Map #U60 String)
|
||||||
// : (BBT #U60 String)
|
// : (BBT #U60 String)
|
||||||
: (#U60)
|
: (#U60)
|
||||||
|
// : (Maybe #U60)
|
||||||
=
|
=
|
||||||
// let map = (BBT.tip #U60 String)
|
// let map = (BBT.tip #U60 String)
|
||||||
// let map = ~λP λbin λtip (tip)
|
// let map = ~λP λbin λtip (tip)
|
||||||
@ -237,7 +246,6 @@ testbbt
|
|||||||
// val
|
// val
|
||||||
// map
|
// map
|
||||||
// let map = (U60.map_gen #1024)
|
// let map = (U60.map_gen #1024)
|
||||||
// let ext = λx (~x λx(#U60) λsome(#2) #0)
|
|
||||||
// let val1 = (U60.get String #5 map)
|
// let val1 = (U60.get String #5 map)
|
||||||
// let val2 = (U60.get String #10 map)
|
// let val2 = (U60.get String #10 map)
|
||||||
// #(+ val1 val2)
|
// #(+ val1 val2)
|
||||||
@ -273,8 +281,37 @@ testbbt
|
|||||||
let map = (U60.set #U60 #8 #8 map) // 23469 +4320 5set 4bal 1rot_lft
|
let map = (U60.set #U60 #8 #8 map) // 23469 +4320 5set 4bal 1rot_lft
|
||||||
let map = (U60.set #U60 #9 #9 map) // 27789 +4484 5set 4bal 1rot_lft
|
let map = (U60.set #U60 #9 #9 map) // 27789 +4484 5set 4bal 1rot_lft
|
||||||
let map = (U60.set #U60 #10 #10 map) // 32281 +4492 5set 4bal 1rot_lft
|
let map = (U60.set #U60 #10 #10 map) // 32281 +4492 5set 4bal 1rot_lft
|
||||||
let sum = (U60.add_all map)
|
|
||||||
sum
|
let P = λx(#U60)
|
||||||
|
let new = λval1 λmap
|
||||||
|
let val1 =
|
||||||
|
let P = λx(#U60)
|
||||||
|
let some = λval (val)
|
||||||
|
let none = #0
|
||||||
|
(~val1 P some none)
|
||||||
|
let P = λx(#U60)
|
||||||
|
let new = λval2 λmap
|
||||||
|
|
||||||
|
let val2 =
|
||||||
|
let P = λx(#U60)
|
||||||
|
let some = λval (val)
|
||||||
|
let none = #0
|
||||||
|
(~val2 P some none)
|
||||||
|
|
||||||
|
#(+ val1 val2)
|
||||||
|
(~(U60.got #U60 #3 map) P new)
|
||||||
|
|
||||||
|
(~(U60.got #U60 #3 map) P new)
|
||||||
|
|
||||||
|
// #(+ val1 val2)
|
||||||
|
|
||||||
|
// #3
|
||||||
|
// #(+ (ext val1) (ext val1))
|
||||||
|
|
||||||
|
// let mymap = λ_ λx0 λ_ (x0 #4 #3 #3 λ_ λx1 λ_ (x1 #2 #1 #1 λ_ λx2 λ_ (x2 #1 #0 #0 λ_ λ_ λx3 x3 λ_ λ_ λx4 x4) λ_ λx5 λ_ (x5 #1 #2 #2 λ_ λ_ λx6 x6 λ_ λ_ λx7 x7)) λ_ λx8 λ_ (x8 #3 #7 #7 λ_ λx9 λ_ (x9 #2 #5 #5 λ_ λx10 λ_ (x10 #1 #4 #4 λ_ λ_ λx11 x11 λ_ λ_ λx12 x12) λ_ λx13 λ_ (x13 #1 #6 #6 λ_ λ_ λx14 x14 λ_ λ_ λx15 x15)) λ_ λx16 λ_ (x16 #2 #9 #9 λ_ λx17 λ_ (x17 #1 #8 #8 λ_ λ_ λx18 x18 λ_ λ_ λx19 x19) λ_ λx20 λ_ (x20 #1 #10 #10 λ_ λ_ λx21 (x21 λ_ λ_ λx22 x22)))))
|
||||||
|
// mymap
|
||||||
|
// let sum = (U60.add_all map)
|
||||||
|
// sum
|
||||||
// let map = (U60.map_gen_u60 #1023)
|
// let map = (U60.map_gen_u60 #1023)
|
||||||
// let map = (U60.set #U60 #3 #3 map)
|
// let map = (U60.set #U60 #3 #3 map)
|
||||||
// let sum = (U60.add_all map)
|
// let sum = (U60.add_all map)
|
||||||
|
Loading…
Reference in New Issue
Block a user