From 95e65c55a629f484c98dc31d6f9098187e34db31 Mon Sep 17 00:00:00 2001 From: Derenash Date: Tue, 20 Feb 2024 17:08:37 -0300 Subject: [PATCH] BBT updates --- book/BBT.balance.kind2 | 10 ++++----- book/BBT.get.kind2 | 10 ++++----- book/BBT.got.kind2 | 31 ++++++++++++++++++++++++++++ book/BBT.lft_rotate.kind2 | 4 ++-- book/BBT.rgt_rotate.kind2 | 4 ++-- book/BBT.set.kind2 | 11 +++++++--- book/testbbt.kind2 | 43 ++++++++++++++++++++++++++++++++++++--- 7 files changed, 93 insertions(+), 20 deletions(-) create mode 100644 book/BBT.got.kind2 diff --git a/book/BBT.balance.kind2 b/book/BBT.balance.kind2 index 331a8b16..8120197c 100644 --- a/book/BBT.balance.kind2 +++ b/book/BBT.balance.kind2 @@ -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) // 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) (BBT.rgt_rotate K V new_size key val lft rgt) // 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) (BBT.rgt_rotate K V new_size key val lft rgt) @@ -78,21 +78,21 @@ BBT.balance_rgt_heavier ∀(lft: (BBT K V)) ∀(rgt: (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 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) // key > rgt.key // 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) (BBT.lft_rotate K V new_size key val lft rgt) // key < rgt.key // rotating parent once to the left // 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) (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) diff --git a/book/BBT.get.kind2 b/book/BBT.get.kind2 index accc8d14..08256f3b 100644 --- a/book/BBT.get.kind2 +++ b/book/BBT.get.kind2 @@ -8,10 +8,10 @@ BBT.get = λK λV λcmp λkey λmap let P = λx(Maybe V) let bin = λ_size λnext.key λnext.val λnext.lft λnext.rgt - let P = λx(Maybe V) - let ltn = (BBT.get K V cmp key next.lft) - let eql = (Maybe.some V next.val) - let gtn = (BBT.get K V cmp key next.rgt) - (~(cmp key next.key) P ltn eql gtn) + let P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) (Maybe V) + let ltn = λcmp λkey (BBT.get K V cmp key next.lft) + let eql = λcmp λkey (Maybe.some V next.val) + let gtn = λcmp λkey (BBT.get K V cmp key next.rgt) + ((~(cmp key next.key) P ltn eql gtn) cmp key) let tip = (Maybe.none V) (~map P bin tip) \ No newline at end of file diff --git a/book/BBT.got.kind2 b/book/BBT.got.kind2 new file mode 100644 index 00000000..425998d2 --- /dev/null +++ b/book/BBT.got.kind2 @@ -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) \ No newline at end of file diff --git a/book/BBT.lft_rotate.kind2 b/book/BBT.lft_rotate.kind2 index c5acc04c..145f3a7a 100644 --- a/book/BBT.lft_rotate.kind2 +++ b/book/BBT.lft_rotate.kind2 @@ -13,11 +13,11 @@ BBT.lft_rotate = λK λV λsize λkey λval λlft λrgt 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 - λkey λval λlft // Parent lambdas + λkey λval λ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) a let tip = - λkey λval λlft // Parent lambdas + λkey λval λlft (BBT.bin K V size key val lft (BBT.tip K V)) ((~rgt P bin tip) key val lft) diff --git a/book/BBT.rgt_rotate.kind2 b/book/BBT.rgt_rotate.kind2 index 1ea0e83f..71723b0f 100644 --- a/book/BBT.rgt_rotate.kind2 +++ b/book/BBT.rgt_rotate.kind2 @@ -13,11 +13,11 @@ BBT.rgt_rotate = λK λV λsize λkey λval λlft λrgt 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 - λkey λval λrgt // Parent lambdas + λkey λval λ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 ) a let tip = - λkey λval λrgt // Parent lambdas + λkey λval λrgt (BBT.bin K V size key val (BBT.tip K V) rgt) ((~lft P bin tip) key val rgt) diff --git a/book/BBT.set.kind2 b/book/BBT.set.kind2 index 984681d9..4e8e3c7a 100644 --- a/book/BBT.set.kind2 +++ b/book/BBT.set.kind2 @@ -8,21 +8,26 @@ BBT.set (BBT K V) = λK λV λcmp λkey λval λmap let P = λx ∀(key: K) ∀(val: V) (BBT K V) - let bin = λsize λnext.key λnext.val λnext.lft λnext.rgt - λkey λval // Parent Lambdas + let bin = λsize λnext.key λnext.val λnext.lft λnext.rgt λkey λval 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 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) + // Same key, update value let eql = λkey λnext.key λnext.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 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) - let tip = λkey λval // Parent Lambdas + + // Empty tree, create new node + let tip = λkey λval (BBT.singleton K V key val) ((~map P bin tip) key val) diff --git a/book/testbbt.kind2 b/book/testbbt.kind2 index d93795b5..93b8b3c7 100644 --- a/book/testbbt.kind2 +++ b/book/testbbt.kind2 @@ -50,6 +50,14 @@ U60.get = λV λ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 : ∀(V: *) ∀(key: #U60) @@ -219,6 +227,7 @@ testbbt // : (List.Map #U60 String) // : (BBT #U60 String) : (#U60) +// : (Maybe #U60) = // let map = (BBT.tip #U60 String) // let map = ~λP λbin λtip (tip) @@ -237,7 +246,6 @@ testbbt // val // map // let map = (U60.map_gen #1024) - // let ext = λx (~x λx(#U60) λsome(#2) #0) // let val1 = (U60.get String #5 map) // let val2 = (U60.get String #10 map) // #(+ 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 #9 #9 map) // 27789 +4484 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.set #U60 #3 #3 map) // let sum = (U60.add_all map)