From cb515a8cb126f1bcd96b6a7103e90d20767cd484 Mon Sep 17 00:00:00 2001 From: Derenash Date: Tue, 20 Feb 2024 13:32:14 -0300 Subject: [PATCH 01/12] Add working BBT, still optimizing it --- book/BBT.balance.kind2 | 103 ++++++++++++ book/BBT.bin.kind2 | 14 ++ book/BBT.get.kind2 | 17 ++ book/BBT.got_size.kind2 | 14 ++ book/BBT.kind2 | 10 ++ book/BBT.lft_rotate.kind2 | 23 +++ book/BBT.new_node.kind2 | 52 ++++++ book/BBT.rgt_rotate.kind2 | 23 +++ book/BBT.set.kind2 | 28 ++++ book/BBT.singleton.kind2 | 8 + book/BBT.tip.kind2 | 8 + book/Cmp.eql.kind2 | 4 + book/Cmp.gtn.kind2 | 4 + book/Cmp.is_gtn.kind2 | 9 + book/Cmp.kind2 | 8 + book/Cmp.ltn.kind2 | 4 + book/String.newline.kind2 | 3 + book/U60.abs_diff.kind2 | 9 + book/U60.max.kind2 | 6 + book/U60.min.kind2 | 6 + book/U60.test.kind2 | 5 + book/test6.kind2 | 340 +++++++++++++++++++++++++++++++++++++- 22 files changed, 696 insertions(+), 2 deletions(-) create mode 100644 book/BBT.balance.kind2 create mode 100644 book/BBT.bin.kind2 create mode 100644 book/BBT.get.kind2 create mode 100644 book/BBT.got_size.kind2 create mode 100644 book/BBT.kind2 create mode 100644 book/BBT.lft_rotate.kind2 create mode 100644 book/BBT.new_node.kind2 create mode 100644 book/BBT.rgt_rotate.kind2 create mode 100644 book/BBT.set.kind2 create mode 100644 book/BBT.singleton.kind2 create mode 100644 book/BBT.tip.kind2 create mode 100644 book/Cmp.eql.kind2 create mode 100644 book/Cmp.gtn.kind2 create mode 100644 book/Cmp.is_gtn.kind2 create mode 100644 book/Cmp.kind2 create mode 100644 book/Cmp.ltn.kind2 create mode 100644 book/String.newline.kind2 create mode 100644 book/U60.abs_diff.kind2 create mode 100644 book/U60.max.kind2 create mode 100644 book/U60.min.kind2 create mode 100644 book/U60.test.kind2 diff --git a/book/BBT.balance.kind2 b/book/BBT.balance.kind2 new file mode 100644 index 00000000..331a8b16 --- /dev/null +++ b/book/BBT.balance.kind2 @@ -0,0 +1,103 @@ +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 + let P = λx(BBT K V) + let new = λlft.size λlft + let P = λx(BBT K V) + let new = λrgt.size λrgt + let new_size = #(+ #1 (U60.max lft.size rgt.size)) + let balance = (U60.abs_diff lft.size rgt.size) + let P = λx ∀(new_size: #U60) ∀(node_key: K) ∀(val: V) ∀(lft: (BBT K V)) ∀(rgt: (BBT K V)) (BBT K V) + + // Unbalanced Trees + let true = λnew_size λnode_key λval λlft λrgt + let 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) + let true = BBT.balance.lft_heavier + let 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) + + // Balanced Trees + let 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) + + + +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 + let P = λx(BBT K V) + let bin = λlft.size λlft.key λlft.val λlft.lft λlft.rgt + 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 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 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) + + // unreachable case + // Left can't be a tip and greater than right at the same time + let tip = (BBT.tip K V) + (~lft P bin tip) + +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 // Parent Lambdas + 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 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 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) + + // Unreachable case + // Right can't be a tip and greater than left at the same time + let tip = (BBT.tip K V) + (~rgt P bin tip) \ No newline at end of file diff --git a/book/BBT.bin.kind2 b/book/BBT.bin.kind2 new file mode 100644 index 00000000..88802c7b --- /dev/null +++ b/book/BBT.bin.kind2 @@ -0,0 +1,14 @@ +BBT.bin +: ∀(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 + ~λP λbin λtip + (bin size key val lft rgt) + + diff --git a/book/BBT.get.kind2 b/book/BBT.get.kind2 new file mode 100644 index 00000000..accc8d14 --- /dev/null +++ b/book/BBT.get.kind2 @@ -0,0 +1,17 @@ +BBT.get +: ∀(K: *) + ∀(V: *) + ∀(cmp: ∀(a: K) ∀(b: K) Cmp) + ∀(key: K) + ∀(map: (BBT K V)) + (Maybe V) += λ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 tip = (Maybe.none V) + (~map P bin tip) \ No newline at end of file diff --git a/book/BBT.got_size.kind2 b/book/BBT.got_size.kind2 new file mode 100644 index 00000000..68aee12c --- /dev/null +++ b/book/BBT.got_size.kind2 @@ -0,0 +1,14 @@ +// Returns a pair with the size of the map and the reconstructed map +BBT.got_size +: ∀(K: *) + ∀(V: *) + ∀(map: (BBT K V)) + (Pair #U60 (BBT K V)) += λK λV λmap + let P = λx(Pair #U60 (BBT K V)) + let bin = λsize λnext.key λnext.val λnext.lft λnext.rgt + let map = (BBT.bin K V size next.key next.val next.lft next.rgt) + (Pair.new #U60 (BBT K V) size map) + let tip = (Pair.new #U60 (BBT K V) #0 (BBT.tip K V)) + (~map P bin tip) + diff --git a/book/BBT.kind2 b/book/BBT.kind2 new file mode 100644 index 00000000..51efecad --- /dev/null +++ b/book/BBT.kind2 @@ -0,0 +1,10 @@ +BBT +: ∀(K: *) // Key type + ∀(V: *) // Value type + * += λK λV + $self + ∀(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) diff --git a/book/BBT.lft_rotate.kind2 b/book/BBT.lft_rotate.kind2 new file mode 100644 index 00000000..c5acc04c --- /dev/null +++ b/book/BBT.lft_rotate.kind2 @@ -0,0 +1,23 @@ +// b = (left ~ right.left) +// a = (b ~ right.right) +// return a +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 + 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 + 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 + (BBT.bin K V size key val lft (BBT.tip K V)) + ((~rgt P bin tip) key val lft) diff --git a/book/BBT.new_node.kind2 b/book/BBT.new_node.kind2 new file mode 100644 index 00000000..4f1ab4b5 --- /dev/null +++ b/book/BBT.new_node.kind2 @@ -0,0 +1,52 @@ +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 + let P = λx ∀(rgt: (BBT K V)) (BBT K V) + let bin = λlft.size λlft.key λlft.val λlft.lft λlft.rgt λrgt + let P = λx ∀(lft.size: #U60) ∀(lft.key: K) ∀(lft.val: V) ∀(lft.lft: (BBT K V)) ∀(lft.rgt: (BBT K V)) (BBT K V) + let bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt λlft.size λlft.key λlft.val λlft.lft λlft.rgt + let new_size = #(+ #1 (U60.max rgt.size lft.size)) + let lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt) + let rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt) + (BBT.bin K V new_size key val lft rgt) + let tip = λlft.size λlft.key λlft.val λlft.lft λlft.rgt + let new_size = #(+ #1 lft.size) + let lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt) + let rgt = (BBT.tip K V) + (BBT.bin K V new_size key val lft rgt) + ((~rgt P bin tip) lft.size lft.key lft.val lft.lft lft.rgt) + let tip = λrgt + let P = λx(BBT K V) + let bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt + let new_size = #(+ #1 rgt.size) + let lft = (BBT.tip K V) + let rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt) + (BBT.bin K V new_size key val lft rgt) + let tip = (BBT.singleton K V key val) + (~rgt P bin tip) + ((~lft P bin tip) 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 +// let P = λx(BBT K V) +// let new = λlft.size λlft +// let P = λx(BBT K V) +// let new = λrgt.size λrgt +// let 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) \ No newline at end of file diff --git a/book/BBT.rgt_rotate.kind2 b/book/BBT.rgt_rotate.kind2 new file mode 100644 index 00000000..1ea0e83f --- /dev/null +++ b/book/BBT.rgt_rotate.kind2 @@ -0,0 +1,23 @@ +// b = (left.right ~ right) +// a = (left.left ~ b) +// return a +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 + 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 + 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 + (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 new file mode 100644 index 00000000..984681d9 --- /dev/null +++ b/book/BBT.set.kind2 @@ -0,0 +1,28 @@ +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 + 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 P = λx ∀(key: K) ∀(next.key: K) ∀(next.val: V) ∀(next.lft: (BBT K V)) ∀(next.rgt: (BBT K V)) (BBT K V) + 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) + + let eql = λkey λnext.key λnext.val λnext.lft λnext.rgt + (BBT.bin K V size next.key 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) + (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 + (BBT.singleton K V key val) + ((~map P bin tip) key val) + diff --git a/book/BBT.singleton.kind2 b/book/BBT.singleton.kind2 new file mode 100644 index 00000000..60ae49bb --- /dev/null +++ b/book/BBT.singleton.kind2 @@ -0,0 +1,8 @@ +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)) \ No newline at end of file diff --git a/book/BBT.tip.kind2 b/book/BBT.tip.kind2 new file mode 100644 index 00000000..a8a2737d --- /dev/null +++ b/book/BBT.tip.kind2 @@ -0,0 +1,8 @@ +BBT.tip +: ∀(K: *) + ∀(V: *) + (BBT K V) += λK λV + ~λP λbin λtip + tip + diff --git a/book/Cmp.eql.kind2 b/book/Cmp.eql.kind2 new file mode 100644 index 00000000..b478903d --- /dev/null +++ b/book/Cmp.eql.kind2 @@ -0,0 +1,4 @@ +Cmp.eql +: Cmp += ~λP λltn λeql λgtn + eql \ No newline at end of file diff --git a/book/Cmp.gtn.kind2 b/book/Cmp.gtn.kind2 new file mode 100644 index 00000000..cd359d8e --- /dev/null +++ b/book/Cmp.gtn.kind2 @@ -0,0 +1,4 @@ +Cmp.gtn +: Cmp += ~λP λltn λeql λgtn + gtn \ No newline at end of file diff --git a/book/Cmp.is_gtn.kind2 b/book/Cmp.is_gtn.kind2 new file mode 100644 index 00000000..a8bc5c8b --- /dev/null +++ b/book/Cmp.is_gtn.kind2 @@ -0,0 +1,9 @@ +Cmp.is_gtn +: ∀(cmp: Cmp) + Bool += λcmp + let P = λx(Bool) + let ltn = Bool.false + let eql = Bool.false + let gtn = Bool.true + (~cmp P ltn eql gtn) \ No newline at end of file diff --git a/book/Cmp.kind2 b/book/Cmp.kind2 new file mode 100644 index 00000000..d1b99af1 --- /dev/null +++ b/book/Cmp.kind2 @@ -0,0 +1,8 @@ +Cmp +: * += $self + ∀(P: ∀(cmp: Cmp) *) + ∀(ltn: (P Cmp.ltn)) + ∀(eql: (P Cmp.eql)) + ∀(gtn: (P Cmp.gtn)) + (P self) \ No newline at end of file diff --git a/book/Cmp.ltn.kind2 b/book/Cmp.ltn.kind2 new file mode 100644 index 00000000..6e9655d6 --- /dev/null +++ b/book/Cmp.ltn.kind2 @@ -0,0 +1,4 @@ +Cmp.ltn +: Cmp += ~λP λltn λeql λgtn + ltn diff --git a/book/String.newline.kind2 b/book/String.newline.kind2 new file mode 100644 index 00000000..4ae0e9a3 --- /dev/null +++ b/book/String.newline.kind2 @@ -0,0 +1,3 @@ +String.newline +: String += (String.cons #10 String.nil) diff --git a/book/U60.abs_diff.kind2 b/book/U60.abs_diff.kind2 new file mode 100644 index 00000000..92699566 --- /dev/null +++ b/book/U60.abs_diff.kind2 @@ -0,0 +1,9 @@ +U60.abs_diff +: ∀(a: #U60) + ∀(b: #U60) + #U60 += λa λb + let P = λx(#U60) + let true = #(- b a) + let false = #(- a b) + (~(U60.to_bool #(< a b)) P true false) \ No newline at end of file diff --git a/book/U60.max.kind2 b/book/U60.max.kind2 new file mode 100644 index 00000000..7d289348 --- /dev/null +++ b/book/U60.max.kind2 @@ -0,0 +1,6 @@ +U60.max +: ∀(a: #U60) + ∀(b: #U60) + #U60 += λa λb + (~(U60.to_bool #(> a b)) λx(#U60) a b) diff --git a/book/U60.min.kind2 b/book/U60.min.kind2 new file mode 100644 index 00000000..a1515e7b --- /dev/null +++ b/book/U60.min.kind2 @@ -0,0 +1,6 @@ +U60.min +: ∀(a: #U60) + ∀(b: #U60) + #U60 += λa λb + (~(U60.to_bool #(< a b)) λx(#U60) a b) \ No newline at end of file diff --git a/book/U60.test.kind2 b/book/U60.test.kind2 new file mode 100644 index 00000000..be5324df --- /dev/null +++ b/book/U60.test.kind2 @@ -0,0 +1,5 @@ +U60.test +: ∀(a: #U60) + (#U60) += λa + U60.if diff --git a/book/test6.kind2 b/book/test6.kind2 index 11f74006..ee8774fd 100644 --- a/book/test6.kind2 +++ b/book/test6.kind2 @@ -1,5 +1,341 @@ +List.Map.gen +: ∀(n: #U60) + (List.Map #U60 String) += λn + (List.Map.gen.go n (List.Map.new #U60 String)) + +List.Map.gen.go +: ∀(n: #U60) + ∀(map: (List.Map #U60 String)) + (List.Map #U60 String) += λn λmap + let P = λx ∀(map: (List.Map #U60 String)) (List.Map #U60 String) + let true = λmap (List.Map.set #U60 String n (U60.show n) map) + let false = λmap (List.Map.set #U60 String n (U60.show n) (List.Map.gen.go #(- n #1) map)) + ((~(U60.to_bool #(== n #0)) P true false) map) + +List.Map.sum +: ∀(map: (List.Map #U60 String)) + (#U60) += λmap + let P = λx(#U60) + let cons = λhead λtail + let P = λx(#U60) + let new = λkey λval + #(+ key (List.Map.sum tail)) + (~head P new) + let nil = #0 + (~map P cons nil) + +Tests.run +: ∀(tests: (List (Maybe String))) + String += λtests + let folder = (List.fold (Maybe String) tests) + (folder String (λhead λtail (~head λx(String) λsome(some) tail)) (String.cons #10 String.nil)) + + +U60.cmp +: ∀(a: #U60) + ∀(b: #U60) + (Cmp) += λa λb + (U60.if #(== a b) Cmp (U60.if #(< a b) Cmp Cmp.gtn Cmp.ltn) Cmp.eql ) + +U60.get +: ∀(V: *) + ∀(key: #U60) + ∀(map: (BBT #U60 V)) + (Maybe V) += λV λkey λmap + (BBT.get #U60 V U60.cmp key map) + +U60.set +: ∀(V: *) + ∀(key: #U60) + ∀(value: V) + ∀(map: (BBT #U60 V)) + (BBT #U60 V) += λV λkey λvalue λmap + (BBT.set #U60 V U60.cmp key value map) + +U60.add_spaces +: ∀(n: #U60) + (String) += λn + (U60.if #(== n #0) String (String.concat " " (U60.add_spaces #(- n #1))) "") + +U60.map_show +: ∀(map: (BBT #U60 String)) + ∀(depth: #U60) + (String) += λmap λdepth + let P = λx(String) + let bin = λsize λkey λval λlft λrgt + let cct = λa λb (String.concat a b) + let spc = λx (cct (U60.add_spaces depth) x) + let nnl = λx (cct String.newline x) + let key = (U60.show key) + let size = (U60.show size) + let a = (nnl (spc (cct "key: " key))) + let b = (cct ", size: " size) + let c = (cct ", value: " val) + let d = (nnl (spc (cct "left: " (U60.map_show lft #(+ #1 depth))))) + let e = (nnl (spc (cct "right: " (U60.map_show rgt #(+ #1 depth))))) + (cct a (cct b (cct c (cct d e )))) + let tip = "" + (~map P bin tip) + +U60.map_gen +: ∀(n: #U60) + (BBT #U60 String) += λn + (U60.map_gen.go n (BBT.tip #U60 String)) + +U60.map_gen.go +: ∀(n: #U60) + ∀(map: (BBT #U60 String)) + (BBT #U60 String) += λn λmap + let P = λx ∀(map: (BBT #U60 String)) (BBT #U60 String) + let true = λmap (U60.set String n (U60.show n) map) + let false = λmap (U60.map_gen.go #(- n #1) (U60.set String n (U60.show n) map)) + ((~(U60.to_bool #(== n #0)) P true false) map) + +U60.map_gen_u60 +: ∀(n: #U60) + (BBT #U60 #U60) += λn + (U60.map_gen_u60.go n (BBT.tip #U60 #U60)) + +U60.map_gen_u60.go +: ∀(n: #U60) + ∀(map: (BBT #U60 #U60)) + (BBT #U60 #U60) += λn λmap + let P = λx ∀(map: (BBT #U60 #U60)) (BBT #U60 #U60) + let true = λmap (U60.set #U60 n n map) + let false = λmap (U60.map_gen_u60.go #(- n #1) (U60.set #U60 n n map)) + ((~(U60.to_bool #(== n #0)) P true false) map) + +Cmp.show +: ∀(cmp: Cmp) + (String) += λcmp + let P = λx(String) + let ltn = "ltn" + let eql = "eql" + let gtn = "gtn" + (~cmp P ltn eql gtn) + + +Test1 +: (Maybe String) += + let emptyMap = (BBT.tip #U60 String) + let updatedMap = (U60.set String #5 "value5" emptyMap) + let value = (U60.get String #5 updatedMap) + let is_equal = (String.equal (~value λx(String) λsome(some) "none") "value5") + (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 1 Failed!")) + +// Update an existing key +Test2 +: (Maybe String) += + let initialMap = (U60.set String #10 "initialValue" (BBT.tip #U60 String)) + let updatedMap = (U60.set String #10 "updatedValue" initialMap) + let value = (U60.get String #10 updatedMap) + let is_equal = (String.equal (~value λx(String) λsome(some) "none") "updatedValue") + (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 2 Failed!")) + +// Getting on a full map +Test3 +: (Maybe String) += + let map = (U60.map_gen #24) + let value = (U60.get String #7 map) + let is_equal = (String.equal (~value λx(String) λsome(some) "none") "7") + (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 3 Failed!")) + + +U60.fold +: ∀(A: *) + ∀(f: ∀(n: #U60) ∀(acc: A) A) + ∀(nil: A) + ∀(n: #U60) + A += λA λf λnil λn + (U60.fold.go A f nil n) + +U60.fold.go +: ∀(A: *) + ∀(f: ∀(n: #U60) ∀(acc: A) A) + ∀(acc: A) + ∀(n: #U60) + A += λA λf λacc λn + (~(U60.to_bool n) λx(A) (U60.fold.go A f (f n acc) #(- n #1)) acc) + + +AscendingMap +: (BBT #U60 #U60) += + let nil = (BBT.tip #U60 String) + let f = λn λacc (U60.set String #(- #10 n) #(- #10 n) acc) + (U60.fold (BBT #U60 String) f nil #10) + +DescendingMap +: (BBT #U60 #U60) += + let nil = (BBT.tip #U60 String) + let f = λn λacc (U60.set String #(+ n #0) n acc) + (U60.fold (BBT #U60 String) f nil #10) + +// Adds all the numbers in a map +U60.add_all +: ∀(map: (BBT #U60 #U60)) + (#U60) += λmap + let P = λx(#U60) + let bin = λsize λkey λval λlft λrgt + let sum = #(+ #(+ key (U60.add_all lft)) (U60.add_all rgt)) + sum + let tip = #0 + (~map P bin tip) + +RunTests +: (String) += + let tests = (List.nil (Maybe String)) + let tests = (List.cons (Maybe String) Test1 tests) + let tests = (List.cons (Maybe String) Test2 tests) + let tests = (List.cons (Maybe String) Test3 tests) + let solution = (Tests.run tests) + solution + test6 -: Nat -= (Nat.succ (Nat.succ (Nat.succ Nat.zero))) +// : (Maybe String) +: String +// : (List.Map #U60 String) +// : (#U60) += + // RunTests + // (Maybe.none String) + // let map = (List.Map.gen #1024) + // map + // let sum = (List.Map.sum map) + // sum + // let val = (List.Map.get #U60 String U60.equal #0 map) + // 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) + // val1 + // 75225975 + // 35973695 - Removed 1 duplicate map on set + // 35973695 - Removed 2 duplicate values + // 35894135 - Removed 2 duplicate keys + // 9827059 + // let map = (U60.map_gen_u60 #2) + // let map = (BBT.tip #U60 #U60) + // let map = (U60.set #U60 #0 #0 map) // 299 +299 1set + // let map = (U60.set #U60 #1 #1 map) // 1293 +994 2set 1bal + // let map = (U60.set #U60 #2 #2 map) // 3958 +2665 3set 2bal 1rot_lft + // let map = (U60.set #U60 #3 #3 map) // 5811 +1853 3set 2bal + // let map = (U60.set #U60 #4 #4 map) // 9342 +3431 4set 3bal 1rot_lft + // let map = (U60.set #U60 #5 #5 map) // 12952 +3610 4set 3bal 1rot_lft + // let map = (U60.set #U60 #6 #6 map) // 16553 +3601 4set 3bal 1rot_lft + // let map = (U60.set #U60 #7 #7 map) // 19141 +2588 4set 3bal + // 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 map = (BBT.tip #U60 #U60) + let map = (U60.set #U60 #0 #0 map) // 299 +299 1set + let map = (U60.set #U60 #1 #1 map) // 1293 +994 2set 1bal + let map = (U60.set #U60 #2 #2 map) // 3958 +2665 3set 2bal 1rot_lft + let map = (U60.set #U60 #3 #3 map) // 5811 +1853 3set 2bal + let map = (U60.set #U60 #4 #4 map) // 9342 +3431 4set 3bal 1rot_lft + let map = (U60.set #U60 #5 #5 map) // 12952 +3610 4set 3bal 1rot_lft + let map = (U60.set #U60 #6 #6 map) // 16553 +3601 4set 3bal 1rot_lft + let map = (U60.set #U60 #7 #7 map) // 19141 +2588 4set 3bal + 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 map = (U60.map_gen_u60 #1023) + // let map = (U60.set #U60 #3 #3 map) + // let sum = (U60.add_all map) + // sum + + // let map = (BBT.bin #U60 #U60 #1 #0 #0 (BBT.tip #U60 #U60) (BBT.tip #U60 #U60)) + // let map = (BBT.singleton #U60 #U60 #0 #0) + // let sum = (U60.add_all map) + // let val = (BBT.get #U60 #U60 U60.cmp #0 map) + // let val = (U60.get #U60 #0 map) + // map + // val + // sum + // let map = (BBT.tip #U60 #U60) + // let map = (U60.set #U60 #0 #0 map) + // let map = (U60.set #U60 #1 #1 map) + // let map = (U60.set #U60 #2 #2 map) + // let map = (U60.set #U60 #3 #3 map) + // let map = (U60.set #U60 #4 #4 map) + // let map = (AscendingMap) // 27990 + // let map = (DescendingMap) // 26901 + // let map = (U60.map_gen #1024) + // let map = (U60.set #U60 #0 #15 map) + // (U60.get String #10 map) + // let sum = (U60.add_all map) + // sum + // let map = (U60.set #U60 #2000 "test" map) + + // // test u60 fold + // let u60test = (U60.fold String (λn λacc (String.concat (String.concat (U60.show n) String.newline) acc) ) "" #10) + // // u60test + + // let ascMap = AscendingMap + // let descMap = DescendingMap + // // [0, 3, 7] + // let asc0 = (U60.get String #0 ascMap) + // let asc1 = (U60.get String #3 ascMap) + // let asc2 = (U60.get String #7 ascMap) + // let desc0 = (U60.get String #0 descMap) + // let desc1 = (U60.get String #3 descMap) + // let desc2 = (U60.get String #7 descMap) + // (U60.map_show map #0) + + + // (~asc1 λx(String) λsome(some) "VAZIOO") + + // let map = (BBT.tip #U60 String) + // let map = (U60.set String #0 "hello" map) + // // let map = (U60.set String #1 "world" map) + // let map = (U60.set String #2 "!" map) + // // (U60.get String #0 map) + // (U60.map_show map #0) + // let cct = λa λb (String.concat a b) + // let map = (U60.map_gen #24) + // let func = λx (~x λx(String) λsome(some) "none") + // let a = (func (U60.get String #0 map)) + // let b = (func (U60.get String #1 map)) + // let c = (func (U60.get String #2 map)) + // let d = (func (U60.get String #4 map)) + // let e = (func (U60.get String #8 map)) + // let f = (func (U60.get String #16 map)) + // let g = (func (U60.get String #32 map)) + // let h = (func (U60.get String #64 map)) + // (U60.map_show map #0) + // (cct a (cct b (cct c (cct d (cct e (cct f (cct g h))))))) + // a + + + // (Cmp.show (U60.cmp #2 #0)) + // (Tests.run (List.cons (Maybe String) (Maybe.none String) (List.cons (Maybe String) (Maybe.some String "error!") (List.nil (Maybe String))))) From 6bf27d1d22543af4c9e7eb4eefad65657ce2dee0 Mon Sep 17 00:00:00 2001 From: Derenash Date: Tue, 20 Feb 2024 14:55:49 -0300 Subject: [PATCH 02/12] small improvements to BBT --- book/BBT.got_size.kind2 | 14 ++ book/BBT.new_node.kind2 | 61 +++---- book/test6.kind2 | 342 +-------------------------------------- book/testbbt.kind2 | 349 ++++++++++++++++++++++++++++++++++++++++ 4 files changed, 396 insertions(+), 370 deletions(-) create mode 100644 book/testbbt.kind2 diff --git a/book/BBT.got_size.kind2 b/book/BBT.got_size.kind2 index 68aee12c..9a67b72f 100644 --- a/book/BBT.got_size.kind2 +++ b/book/BBT.got_size.kind2 @@ -12,3 +12,17 @@ BBT.got_size let tip = (Pair.new #U60 (BBT K V) #0 (BBT.tip K V)) (~map P bin tip) +// BBT.got_size +// : ∀(K: *) +// ∀(V: *) +// ∀(map: (BBT K V)) +// (Pair #U60 (BBT K V)) +// = λK λV λmap +// let P = λx(Pair #U60 (BBT K V)) +// let bin = λsize λnext.key λnext.val λnext.lft λnext.rgt +// let map = ~λP λbin λtip (bin size next.key next.val next.lft next.rgt) +// ~λP λnew (new size map) +// let tip = ~λP λnew (new #0 ~λP λbin λtip tip) +// (~map P bin tip) + + diff --git a/book/BBT.new_node.kind2 b/book/BBT.new_node.kind2 index 4f1ab4b5..62f4dd7e 100644 --- a/book/BBT.new_node.kind2 +++ b/book/BBT.new_node.kind2 @@ -1,4 +1,5 @@ -BBT.new_node +// Creates a new node with size = 1 + (max lft.size rgt.size) + BBT.new_node : ∀(K: *) ∀(V: *) ∀(key: K) @@ -7,32 +8,15 @@ BBT.new_node ∀(rgt: (BBT K V)) (BBT K V) = λK λV λkey λval λlft λrgt - let P = λx ∀(rgt: (BBT K V)) (BBT K V) - let bin = λlft.size λlft.key λlft.val λlft.lft λlft.rgt λrgt - let P = λx ∀(lft.size: #U60) ∀(lft.key: K) ∀(lft.val: V) ∀(lft.lft: (BBT K V)) ∀(lft.rgt: (BBT K V)) (BBT K V) - let bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt λlft.size λlft.key λlft.val λlft.lft λlft.rgt - let new_size = #(+ #1 (U60.max rgt.size lft.size)) - let lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt) - let rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt) - (BBT.bin K V new_size key val lft rgt) - let tip = λlft.size λlft.key λlft.val λlft.lft λlft.rgt - let new_size = #(+ #1 lft.size) - let lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt) - let rgt = (BBT.tip K V) - (BBT.bin K V new_size key val lft rgt) - ((~rgt P bin tip) lft.size lft.key lft.val lft.lft lft.rgt) - let tip = λrgt + let P = λx(BBT K V) + let new = λlft.size λlft let P = λx(BBT K V) - let bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt - let new_size = #(+ #1 rgt.size) - let lft = (BBT.tip K V) - let rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt) + let new = λrgt.size λrgt + let new_size = #(+ #1 (U60.max rgt.size lft.size)) (BBT.bin K V new_size key val lft rgt) - let tip = (BBT.singleton K V key val) - (~rgt P bin tip) - ((~lft P bin tip) rgt) + (~(BBT.got_size K V rgt) P new) + (~(BBT.got_size K V lft) P new) - // BBT.new_node // : ∀(K: *) // ∀(V: *) @@ -42,11 +26,28 @@ BBT.new_node // ∀(rgt: (BBT K V)) // (BBT K V) // = λK λV λkey λval λlft λrgt -// let P = λx(BBT K V) -// let new = λlft.size λlft -// let P = λx(BBT K V) -// let new = λrgt.size λrgt +// let P = λx ∀(rgt: (BBT K V)) (BBT K V) +// let bin = λlft.size λlft.key λlft.val λlft.lft λlft.rgt λrgt +// let P = λx ∀(lft.size: #U60) ∀(lft.key: K) ∀(lft.val: V) ∀(lft.lft: (BBT K V)) ∀(lft.rgt: (BBT K V)) (BBT K V) +// let bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt λlft.size λlft.key λlft.val λlft.lft λlft.rgt // let new_size = #(+ #1 (U60.max rgt.size lft.size)) +// let lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt) +// let rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt) // (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) \ No newline at end of file +// let tip = λlft.size λlft.key λlft.val λlft.lft λlft.rgt +// let new_size = #(+ #1 lft.size) +// let lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt) +// let rgt = (BBT.tip K V) +// (BBT.bin K V new_size key val lft rgt) +// ((~rgt P bin tip) lft.size lft.key lft.val lft.lft lft.rgt) +// let tip = λrgt +// let P = λx(BBT K V) +// let bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt +// let new_size = #(+ #1 rgt.size) +// let lft = (BBT.tip K V) +// let rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt) +// (BBT.bin K V new_size key val lft rgt) +// let tip = (BBT.singleton K V key val) +// (~rgt P bin tip) +// ((~lft P bin tip) rgt) + diff --git a/book/test6.kind2 b/book/test6.kind2 index ee8774fd..bd30aa9f 100644 --- a/book/test6.kind2 +++ b/book/test6.kind2 @@ -1,341 +1,3 @@ -List.Map.gen -: ∀(n: #U60) - (List.Map #U60 String) -= λn - (List.Map.gen.go n (List.Map.new #U60 String)) - -List.Map.gen.go -: ∀(n: #U60) - ∀(map: (List.Map #U60 String)) - (List.Map #U60 String) -= λn λmap - let P = λx ∀(map: (List.Map #U60 String)) (List.Map #U60 String) - let true = λmap (List.Map.set #U60 String n (U60.show n) map) - let false = λmap (List.Map.set #U60 String n (U60.show n) (List.Map.gen.go #(- n #1) map)) - ((~(U60.to_bool #(== n #0)) P true false) map) - -List.Map.sum -: ∀(map: (List.Map #U60 String)) - (#U60) -= λmap - let P = λx(#U60) - let cons = λhead λtail - let P = λx(#U60) - let new = λkey λval - #(+ key (List.Map.sum tail)) - (~head P new) - let nil = #0 - (~map P cons nil) - -Tests.run -: ∀(tests: (List (Maybe String))) - String -= λtests - let folder = (List.fold (Maybe String) tests) - (folder String (λhead λtail (~head λx(String) λsome(some) tail)) (String.cons #10 String.nil)) - - -U60.cmp -: ∀(a: #U60) - ∀(b: #U60) - (Cmp) -= λa λb - (U60.if #(== a b) Cmp (U60.if #(< a b) Cmp Cmp.gtn Cmp.ltn) Cmp.eql ) - -U60.get -: ∀(V: *) - ∀(key: #U60) - ∀(map: (BBT #U60 V)) - (Maybe V) -= λV λkey λmap - (BBT.get #U60 V U60.cmp key map) - -U60.set -: ∀(V: *) - ∀(key: #U60) - ∀(value: V) - ∀(map: (BBT #U60 V)) - (BBT #U60 V) -= λV λkey λvalue λmap - (BBT.set #U60 V U60.cmp key value map) - -U60.add_spaces -: ∀(n: #U60) - (String) -= λn - (U60.if #(== n #0) String (String.concat " " (U60.add_spaces #(- n #1))) "") - -U60.map_show -: ∀(map: (BBT #U60 String)) - ∀(depth: #U60) - (String) -= λmap λdepth - let P = λx(String) - let bin = λsize λkey λval λlft λrgt - let cct = λa λb (String.concat a b) - let spc = λx (cct (U60.add_spaces depth) x) - let nnl = λx (cct String.newline x) - let key = (U60.show key) - let size = (U60.show size) - let a = (nnl (spc (cct "key: " key))) - let b = (cct ", size: " size) - let c = (cct ", value: " val) - let d = (nnl (spc (cct "left: " (U60.map_show lft #(+ #1 depth))))) - let e = (nnl (spc (cct "right: " (U60.map_show rgt #(+ #1 depth))))) - (cct a (cct b (cct c (cct d e )))) - let tip = "" - (~map P bin tip) - -U60.map_gen -: ∀(n: #U60) - (BBT #U60 String) -= λn - (U60.map_gen.go n (BBT.tip #U60 String)) - -U60.map_gen.go -: ∀(n: #U60) - ∀(map: (BBT #U60 String)) - (BBT #U60 String) -= λn λmap - let P = λx ∀(map: (BBT #U60 String)) (BBT #U60 String) - let true = λmap (U60.set String n (U60.show n) map) - let false = λmap (U60.map_gen.go #(- n #1) (U60.set String n (U60.show n) map)) - ((~(U60.to_bool #(== n #0)) P true false) map) - -U60.map_gen_u60 -: ∀(n: #U60) - (BBT #U60 #U60) -= λn - (U60.map_gen_u60.go n (BBT.tip #U60 #U60)) - -U60.map_gen_u60.go -: ∀(n: #U60) - ∀(map: (BBT #U60 #U60)) - (BBT #U60 #U60) -= λn λmap - let P = λx ∀(map: (BBT #U60 #U60)) (BBT #U60 #U60) - let true = λmap (U60.set #U60 n n map) - let false = λmap (U60.map_gen_u60.go #(- n #1) (U60.set #U60 n n map)) - ((~(U60.to_bool #(== n #0)) P true false) map) - -Cmp.show -: ∀(cmp: Cmp) - (String) -= λcmp - let P = λx(String) - let ltn = "ltn" - let eql = "eql" - let gtn = "gtn" - (~cmp P ltn eql gtn) - - -Test1 -: (Maybe String) -= - let emptyMap = (BBT.tip #U60 String) - let updatedMap = (U60.set String #5 "value5" emptyMap) - let value = (U60.get String #5 updatedMap) - let is_equal = (String.equal (~value λx(String) λsome(some) "none") "value5") - (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 1 Failed!")) - -// Update an existing key -Test2 -: (Maybe String) -= - let initialMap = (U60.set String #10 "initialValue" (BBT.tip #U60 String)) - let updatedMap = (U60.set String #10 "updatedValue" initialMap) - let value = (U60.get String #10 updatedMap) - let is_equal = (String.equal (~value λx(String) λsome(some) "none") "updatedValue") - (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 2 Failed!")) - -// Getting on a full map -Test3 -: (Maybe String) -= - let map = (U60.map_gen #24) - let value = (U60.get String #7 map) - let is_equal = (String.equal (~value λx(String) λsome(some) "none") "7") - (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 3 Failed!")) - - -U60.fold -: ∀(A: *) - ∀(f: ∀(n: #U60) ∀(acc: A) A) - ∀(nil: A) - ∀(n: #U60) - A -= λA λf λnil λn - (U60.fold.go A f nil n) - -U60.fold.go -: ∀(A: *) - ∀(f: ∀(n: #U60) ∀(acc: A) A) - ∀(acc: A) - ∀(n: #U60) - A -= λA λf λacc λn - (~(U60.to_bool n) λx(A) (U60.fold.go A f (f n acc) #(- n #1)) acc) - - -AscendingMap -: (BBT #U60 #U60) -= - let nil = (BBT.tip #U60 String) - let f = λn λacc (U60.set String #(- #10 n) #(- #10 n) acc) - (U60.fold (BBT #U60 String) f nil #10) - -DescendingMap -: (BBT #U60 #U60) -= - let nil = (BBT.tip #U60 String) - let f = λn λacc (U60.set String #(+ n #0) n acc) - (U60.fold (BBT #U60 String) f nil #10) - -// Adds all the numbers in a map -U60.add_all -: ∀(map: (BBT #U60 #U60)) - (#U60) -= λmap - let P = λx(#U60) - let bin = λsize λkey λval λlft λrgt - let sum = #(+ #(+ key (U60.add_all lft)) (U60.add_all rgt)) - sum - let tip = #0 - (~map P bin tip) - -RunTests -: (String) -= - let tests = (List.nil (Maybe String)) - let tests = (List.cons (Maybe String) Test1 tests) - let tests = (List.cons (Maybe String) Test2 tests) - let tests = (List.cons (Maybe String) Test3 tests) - let solution = (Tests.run tests) - solution - test6 -// : (Maybe String) -: String -// : (List.Map #U60 String) -// : (#U60) -= - // RunTests - // (Maybe.none String) - // let map = (List.Map.gen #1024) - // map - // let sum = (List.Map.sum map) - // sum - // let val = (List.Map.get #U60 String U60.equal #0 map) - // 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) - // val1 - // 75225975 - // 35973695 - Removed 1 duplicate map on set - // 35973695 - Removed 2 duplicate values - // 35894135 - Removed 2 duplicate keys - // 9827059 - // let map = (U60.map_gen_u60 #2) - // let map = (BBT.tip #U60 #U60) - // let map = (U60.set #U60 #0 #0 map) // 299 +299 1set - // let map = (U60.set #U60 #1 #1 map) // 1293 +994 2set 1bal - // let map = (U60.set #U60 #2 #2 map) // 3958 +2665 3set 2bal 1rot_lft - // let map = (U60.set #U60 #3 #3 map) // 5811 +1853 3set 2bal - // let map = (U60.set #U60 #4 #4 map) // 9342 +3431 4set 3bal 1rot_lft - // let map = (U60.set #U60 #5 #5 map) // 12952 +3610 4set 3bal 1rot_lft - // let map = (U60.set #U60 #6 #6 map) // 16553 +3601 4set 3bal 1rot_lft - // let map = (U60.set #U60 #7 #7 map) // 19141 +2588 4set 3bal - // 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 map = (BBT.tip #U60 #U60) - let map = (U60.set #U60 #0 #0 map) // 299 +299 1set - let map = (U60.set #U60 #1 #1 map) // 1293 +994 2set 1bal - let map = (U60.set #U60 #2 #2 map) // 3958 +2665 3set 2bal 1rot_lft - let map = (U60.set #U60 #3 #3 map) // 5811 +1853 3set 2bal - let map = (U60.set #U60 #4 #4 map) // 9342 +3431 4set 3bal 1rot_lft - let map = (U60.set #U60 #5 #5 map) // 12952 +3610 4set 3bal 1rot_lft - let map = (U60.set #U60 #6 #6 map) // 16553 +3601 4set 3bal 1rot_lft - let map = (U60.set #U60 #7 #7 map) // 19141 +2588 4set 3bal - 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 map = (U60.map_gen_u60 #1023) - // let map = (U60.set #U60 #3 #3 map) - // let sum = (U60.add_all map) - // sum - - // let map = (BBT.bin #U60 #U60 #1 #0 #0 (BBT.tip #U60 #U60) (BBT.tip #U60 #U60)) - // let map = (BBT.singleton #U60 #U60 #0 #0) - // let sum = (U60.add_all map) - // let val = (BBT.get #U60 #U60 U60.cmp #0 map) - // let val = (U60.get #U60 #0 map) - // map - // val - // sum - // let map = (BBT.tip #U60 #U60) - // let map = (U60.set #U60 #0 #0 map) - // let map = (U60.set #U60 #1 #1 map) - // let map = (U60.set #U60 #2 #2 map) - // let map = (U60.set #U60 #3 #3 map) - // let map = (U60.set #U60 #4 #4 map) - // let map = (AscendingMap) // 27990 - // let map = (DescendingMap) // 26901 - // let map = (U60.map_gen #1024) - // let map = (U60.set #U60 #0 #15 map) - // (U60.get String #10 map) - // let sum = (U60.add_all map) - // sum - // let map = (U60.set #U60 #2000 "test" map) - - // // test u60 fold - // let u60test = (U60.fold String (λn λacc (String.concat (String.concat (U60.show n) String.newline) acc) ) "" #10) - // // u60test - - // let ascMap = AscendingMap - // let descMap = DescendingMap - // // [0, 3, 7] - // let asc0 = (U60.get String #0 ascMap) - // let asc1 = (U60.get String #3 ascMap) - // let asc2 = (U60.get String #7 ascMap) - // let desc0 = (U60.get String #0 descMap) - // let desc1 = (U60.get String #3 descMap) - // let desc2 = (U60.get String #7 descMap) - // (U60.map_show map #0) - - - // (~asc1 λx(String) λsome(some) "VAZIOO") - - // let map = (BBT.tip #U60 String) - // let map = (U60.set String #0 "hello" map) - // // let map = (U60.set String #1 "world" map) - // let map = (U60.set String #2 "!" map) - // // (U60.get String #0 map) - // (U60.map_show map #0) - // let cct = λa λb (String.concat a b) - // let map = (U60.map_gen #24) - // let func = λx (~x λx(String) λsome(some) "none") - // let a = (func (U60.get String #0 map)) - // let b = (func (U60.get String #1 map)) - // let c = (func (U60.get String #2 map)) - // let d = (func (U60.get String #4 map)) - // let e = (func (U60.get String #8 map)) - // let f = (func (U60.get String #16 map)) - // let g = (func (U60.get String #32 map)) - // let h = (func (U60.get String #64 map)) - // (U60.map_show map #0) - // (cct a (cct b (cct c (cct d (cct e (cct f (cct g h))))))) - // a - - - // (Cmp.show (U60.cmp #2 #0)) - // (Tests.run (List.cons (Maybe String) (Maybe.none String) (List.cons (Maybe String) (Maybe.some String "error!") (List.nil (Maybe String))))) - - +: Nat += (Nat.succ (Nat.succ (Nat.succ Nat.zero))) \ No newline at end of file diff --git a/book/testbbt.kind2 b/book/testbbt.kind2 new file mode 100644 index 00000000..d93795b5 --- /dev/null +++ b/book/testbbt.kind2 @@ -0,0 +1,349 @@ +List.Map.gen +: ∀(n: #U60) + (List.Map #U60 String) += λn + (List.Map.gen.go n (List.Map.new #U60 String)) + +List.Map.gen.go +: ∀(n: #U60) + ∀(map: (List.Map #U60 String)) + (List.Map #U60 String) += λn λmap + let P = λx ∀(map: (List.Map #U60 String)) (List.Map #U60 String) + let true = λmap (List.Map.set #U60 String n (U60.show n) map) + let false = λmap (List.Map.set #U60 String n (U60.show n) (List.Map.gen.go #(- n #1) map)) + ((~(U60.to_bool #(== n #0)) P true false) map) + +List.Map.sum +: ∀(map: (List.Map #U60 String)) + (#U60) += λmap + let P = λx(#U60) + let cons = λhead λtail + let P = λx(#U60) + let new = λkey λval + #(+ key (List.Map.sum tail)) + (~head P new) + let nil = #0 + (~map P cons nil) + +Tests.run +: ∀(tests: (List (Maybe String))) + String += λtests + let folder = (List.fold (Maybe String) tests) + (folder String (λhead λtail (~head λx(String) λsome(some) tail)) (String.cons #10 String.nil)) + + +U60.cmp +: ∀(a: #U60) + ∀(b: #U60) + (Cmp) += λa λb + (U60.if #(== a b) Cmp (U60.if #(< a b) Cmp Cmp.gtn Cmp.ltn) Cmp.eql ) + +U60.get +: ∀(V: *) + ∀(key: #U60) + ∀(map: (BBT #U60 V)) + (Maybe V) += λV λkey λmap + (BBT.get #U60 V U60.cmp key map) + +U60.set +: ∀(V: *) + ∀(key: #U60) + ∀(value: V) + ∀(map: (BBT #U60 V)) + (BBT #U60 V) += λV λkey λvalue λmap + (BBT.set #U60 V U60.cmp key value map) + +U60.add_spaces +: ∀(n: #U60) + (String) += λn + (U60.if #(== n #0) String (String.concat " " (U60.add_spaces #(- n #1))) "") + +U60.map_show +: ∀(map: (BBT #U60 String)) + ∀(depth: #U60) + (String) += λmap λdepth + let P = λx(String) + let bin = λsize λkey λval λlft λrgt + let cct = λa λb (String.concat a b) + let spc = λx (cct (U60.add_spaces depth) x) + let nnl = λx (cct String.newline x) + let key = (U60.show key) + let size = (U60.show size) + let a = (nnl (spc (cct "key: " key))) + let b = (cct ", size: " size) + let c = (cct ", value: " val) + let d = (nnl (spc (cct "left: " (U60.map_show lft #(+ #1 depth))))) + let e = (nnl (spc (cct "right: " (U60.map_show rgt #(+ #1 depth))))) + (cct a (cct b (cct c (cct d e )))) + let tip = "" + (~map P bin tip) + +U60.map_gen +: ∀(n: #U60) + (BBT #U60 String) += λn + (U60.map_gen.go n (BBT.tip #U60 String)) + +U60.map_gen.go +: ∀(n: #U60) + ∀(map: (BBT #U60 String)) + (BBT #U60 String) += λn λmap + let P = λx ∀(map: (BBT #U60 String)) (BBT #U60 String) + let true = λmap (U60.set String n (U60.show n) map) + let false = λmap (U60.map_gen.go #(- n #1) (U60.set String n (U60.show n) map)) + ((~(U60.to_bool #(== n #0)) P true false) map) + +U60.map_gen_u60 +: ∀(n: #U60) + (BBT #U60 #U60) += λn + (U60.map_gen_u60.go n (BBT.tip #U60 #U60)) + +U60.map_gen_u60.go +: ∀(n: #U60) + ∀(map: (BBT #U60 #U60)) + (BBT #U60 #U60) += λn λmap + let P = λx ∀(map: (BBT #U60 #U60)) (BBT #U60 #U60) + let true = λmap (U60.set #U60 n n map) + let false = λmap (U60.map_gen_u60.go #(- n #1) (U60.set #U60 n n map)) + ((~(U60.to_bool #(== n #0)) P true false) map) + +Cmp.show +: ∀(cmp: Cmp) + (String) += λcmp + let P = λx(String) + let ltn = "ltn" + let eql = "eql" + let gtn = "gtn" + (~cmp P ltn eql gtn) + + +Test1 +: (Maybe String) += + let emptyMap = (BBT.tip #U60 String) + let updatedMap = (U60.set String #5 "value5" emptyMap) + let value = (U60.get String #5 updatedMap) + let is_equal = (String.equal (~value λx(String) λsome(some) "none") "value5") + (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 1 Failed!")) + +// Update an existing key +Test2 +: (Maybe String) += + let initialMap = (U60.set String #10 "initialValue" (BBT.tip #U60 String)) + let updatedMap = (U60.set String #10 "updatedValue" initialMap) + let value = (U60.get String #10 updatedMap) + let is_equal = (String.equal (~value λx(String) λsome(some) "none") "updatedValue") + (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 2 Failed!")) + +// Getting on a full map +Test3 +: (Maybe String) += + let map = (U60.map_gen #24) + let value = (U60.get String #7 map) + let is_equal = (String.equal (~value λx(String) λsome(some) "none") "7") + (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 3 Failed!")) + + +U60.fold +: ∀(A: *) + ∀(f: ∀(n: #U60) ∀(acc: A) A) + ∀(nil: A) + ∀(n: #U60) + A += λA λf λnil λn + (U60.fold.go A f nil n) + +U60.fold.go +: ∀(A: *) + ∀(f: ∀(n: #U60) ∀(acc: A) A) + ∀(acc: A) + ∀(n: #U60) + A += λA λf λacc λn + (~(U60.to_bool n) λx(A) (U60.fold.go A f (f n acc) #(- n #1)) acc) + + +AscendingMap +: (BBT #U60 #U60) += + let nil = (BBT.tip #U60 String) + let f = λn λacc (U60.set String #(- #10 n) #(- #10 n) acc) + (U60.fold (BBT #U60 String) f nil #10) + +DescendingMap +: (BBT #U60 #U60) += + let nil = (BBT.tip #U60 String) + let f = λn λacc (U60.set String #(+ n #0) n acc) + (U60.fold (BBT #U60 String) f nil #10) + +// Adds all the numbers in a map +U60.add_all +: ∀(map: (BBT #U60 #U60)) + (#U60) += λmap + let P = λx(#U60) + let bin = λsize λkey λval λlft λrgt + let sum = #(+ #(+ key (U60.add_all lft)) (U60.add_all rgt)) + sum + let tip = #0 + (~map P bin tip) + +RunTests +: (String) += + let tests = (List.nil (Maybe String)) + let tests = (List.cons (Maybe String) Test1 tests) + let tests = (List.cons (Maybe String) Test2 tests) + let tests = (List.cons (Maybe String) Test3 tests) + let solution = (Tests.run tests) + solution + +testbbt +// : (Maybe String) +// : String +// : (List.Map #U60 String) +// : (BBT #U60 String) +: (#U60) += + // let map = (BBT.tip #U60 String) + // let map = ~λP λbin λtip (tip) + // let map = (BBT.singleton #U60 String #0 "0") + // let map = (U60.set String #0 "0" map) + // let map = (U60.set String #1 "1" map) + // map + + // RunTests + // (Maybe.none String) + // let map = (List.Map.gen #1024) + // map + // let sum = (List.Map.sum map) + // sum + // let val = (List.Map.get #U60 String U60.equal #0 map) + // 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) + // val1 + // 75225975 + // 35973695 - Removed 1 duplicate map on set + // 35973695 - Removed 2 duplicate values + // 35894135 - Removed 2 duplicate keys + // 9827059 + // let map = (U60.map_gen_u60 #2) + // let map = (BBT.tip #U60 #U60) + // let map = (U60.set #U60 #0 #0 map) // 299 +299 1set + // let map = (U60.set #U60 #1 #1 map) // 1293 +994 2set 1bal + // let map = (U60.set #U60 #2 #2 map) // 3958 +2665 3set 2bal 1rot_lft + // let map = (U60.set #U60 #3 #3 map) // 5811 +1853 3set 2bal + // let map = (U60.set #U60 #4 #4 map) // 9342 +3431 4set 3bal 1rot_lft + // let map = (U60.set #U60 #5 #5 map) // 12952 +3610 4set 3bal 1rot_lft + // let map = (U60.set #U60 #6 #6 map) // 16553 +3601 4set 3bal 1rot_lft + // let map = (U60.set #U60 #7 #7 map) // 19141 +2588 4set 3bal + // 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 map = (BBT.tip #U60 #U60) + let map = (U60.set #U60 #0 #0 map) // 299 +299 1set + let map = (U60.set #U60 #1 #1 map) // 1293 +994 2set 1bal + let map = (U60.set #U60 #2 #2 map) // 3958 +2665 3set 2bal 1rot_lft + let map = (U60.set #U60 #3 #3 map) // 5811 +1853 3set 2bal + let map = (U60.set #U60 #4 #4 map) // 9342 +3431 4set 3bal 1rot_lft + let map = (U60.set #U60 #5 #5 map) // 12952 +3610 4set 3bal 1rot_lft + let map = (U60.set #U60 #6 #6 map) // 16553 +3601 4set 3bal 1rot_lft + let map = (U60.set #U60 #7 #7 map) // 19141 +2588 4set 3bal + 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 map = (U60.map_gen_u60 #1023) + // let map = (U60.set #U60 #3 #3 map) + // let sum = (U60.add_all map) + // sum + + // let map = (BBT.bin #U60 #U60 #1 #0 #0 (BBT.tip #U60 #U60) (BBT.tip #U60 #U60)) + // let map = (BBT.singleton #U60 #U60 #0 #0) + // let sum = (U60.add_all map) + // let val = (BBT.get #U60 #U60 U60.cmp #0 map) + // let val = (U60.get #U60 #0 map) + // map + // val + // sum + // let map = (BBT.tip #U60 #U60) + // let map = (U60.set #U60 #0 #0 map) + // let map = (U60.set #U60 #1 #1 map) + // let map = (U60.set #U60 #2 #2 map) + // let map = (U60.set #U60 #3 #3 map) + // let map = (U60.set #U60 #4 #4 map) + // let map = (AscendingMap) // 27990 + // let map = (DescendingMap) // 26901 + // let map = (U60.map_gen #1024) + // let map = (U60.set #U60 #0 #15 map) + // (U60.get String #10 map) + // let sum = (U60.add_all map) + // sum + // let map = (U60.set #U60 #2000 "test" map) + + // // test u60 fold + // let u60test = (U60.fold String (λn λacc (String.concat (String.concat (U60.show n) String.newline) acc) ) "" #10) + // // u60test + + // let ascMap = AscendingMap + // let descMap = DescendingMap + // // [0, 3, 7] + // let asc0 = (U60.get String #0 ascMap) + // let asc1 = (U60.get String #3 ascMap) + // let asc2 = (U60.get String #7 ascMap) + // let desc0 = (U60.get String #0 descMap) + // let desc1 = (U60.get String #3 descMap) + // let desc2 = (U60.get String #7 descMap) + // (U60.map_show map #0) + + + // (~asc1 λx(String) λsome(some) "VAZIOO") + + // let map = (BBT.tip #U60 String) + // let map = (U60.set String #0 "hello" map) + // // let map = (U60.set String #1 "world" map) + // let map = (U60.set String #2 "!" map) + // // (U60.get String #0 map) + // (U60.map_show map #0) + // let cct = λa λb (String.concat a b) + // let map = (U60.map_gen #24) + // let func = λx (~x λx(String) λsome(some) "none") + // let a = (func (U60.get String #0 map)) + // let b = (func (U60.get String #1 map)) + // let c = (func (U60.get String #2 map)) + // let d = (func (U60.get String #4 map)) + // let e = (func (U60.get String #8 map)) + // let f = (func (U60.get String #16 map)) + // let g = (func (U60.get String #32 map)) + // let h = (func (U60.get String #64 map)) + // (U60.map_show map #0) + // (cct a (cct b (cct c (cct d (cct e (cct f (cct g h))))))) + // a + + + // (Cmp.show (U60.cmp #2 #0)) + // (Tests.run (List.cons (Maybe String) (Maybe.none String) (List.cons (Maybe String) (Maybe.some String "error!") (List.nil (Maybe String))))) + + From 95e65c55a629f484c98dc31d6f9098187e34db31 Mon Sep 17 00:00:00 2001 From: Derenash Date: Tue, 20 Feb 2024 17:08:37 -0300 Subject: [PATCH 03/12] 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) From 5898cf5e706ff25759bc5ec13a7701e471f0847d Mon Sep 17 00:00:00 2001 From: Derenash Date: Tue, 20 Feb 2024 17:09:22 -0300 Subject: [PATCH 04/12] renamed testBBT --- book/{testbbt.kind2 => testBBT.kind2} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename book/{testbbt.kind2 => testBBT.kind2} (100%) diff --git a/book/testbbt.kind2 b/book/testBBT.kind2 similarity index 100% rename from book/testbbt.kind2 rename to book/testBBT.kind2 From aa3de2bf64ed4544ec465315cb219b848c560b36 Mon Sep 17 00:00:00 2001 From: Derenash Date: Tue, 20 Feb 2024 18:18:24 -0300 Subject: [PATCH 05/12] renamed testBBT function --- book/testBBT.kind2 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/book/testBBT.kind2 b/book/testBBT.kind2 index 93b8b3c7..01be53b4 100644 --- a/book/testBBT.kind2 +++ b/book/testBBT.kind2 @@ -221,7 +221,7 @@ RunTests let solution = (Tests.run tests) solution -testbbt +testBBT // : (Maybe String) // : String // : (List.Map #U60 String) From 7124036c94732b904c2e30d02e09af81466129d8 Mon Sep 17 00:00:00 2001 From: Derenash Date: Wed, 21 Feb 2024 12:10:30 -0300 Subject: [PATCH 06/12] Update comments on BBT files --- book/BBT.balance.kind2 | 3 --- book/BBT.got.kind2 | 1 + book/BBT.got_size.kind2 | 15 --------------- book/BBT.new_node.kind2 | 37 +------------------------------------ book/BBT.set.kind2 | 1 + 5 files changed, 3 insertions(+), 54 deletions(-) diff --git a/book/BBT.balance.kind2 b/book/BBT.balance.kind2 index 8120197c..f462453a 100644 --- a/book/BBT.balance.kind2 +++ b/book/BBT.balance.kind2 @@ -84,14 +84,11 @@ BBT.balance_rgt_heavier 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 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 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) diff --git a/book/BBT.got.kind2 b/book/BBT.got.kind2 index 425998d2..bc12bcf9 100644 --- a/book/BBT.got.kind2 +++ b/book/BBT.got.kind2 @@ -1,3 +1,4 @@ +// Returns a pair with the value and the new map BBT.got : ∀(K: *) ∀(V: *) diff --git a/book/BBT.got_size.kind2 b/book/BBT.got_size.kind2 index 9a67b72f..13eb3aea 100644 --- a/book/BBT.got_size.kind2 +++ b/book/BBT.got_size.kind2 @@ -11,18 +11,3 @@ BBT.got_size (Pair.new #U60 (BBT K V) size map) let tip = (Pair.new #U60 (BBT K V) #0 (BBT.tip K V)) (~map P bin tip) - -// BBT.got_size -// : ∀(K: *) -// ∀(V: *) -// ∀(map: (BBT K V)) -// (Pair #U60 (BBT K V)) -// = λK λV λmap -// let P = λx(Pair #U60 (BBT K V)) -// let bin = λsize λnext.key λnext.val λnext.lft λnext.rgt -// let map = ~λP λbin λtip (bin size next.key next.val next.lft next.rgt) -// ~λP λnew (new size map) -// let tip = ~λP λnew (new #0 ~λP λbin λtip tip) -// (~map P bin tip) - - diff --git a/book/BBT.new_node.kind2 b/book/BBT.new_node.kind2 index 62f4dd7e..07c958c9 100644 --- a/book/BBT.new_node.kind2 +++ b/book/BBT.new_node.kind2 @@ -15,39 +15,4 @@ let 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) - -// 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 -// let P = λx ∀(rgt: (BBT K V)) (BBT K V) -// let bin = λlft.size λlft.key λlft.val λlft.lft λlft.rgt λrgt -// let P = λx ∀(lft.size: #U60) ∀(lft.key: K) ∀(lft.val: V) ∀(lft.lft: (BBT K V)) ∀(lft.rgt: (BBT K V)) (BBT K V) -// let bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt λlft.size λlft.key λlft.val λlft.lft λlft.rgt -// let new_size = #(+ #1 (U60.max rgt.size lft.size)) -// let lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt) -// let rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt) -// (BBT.bin K V new_size key val lft rgt) -// let tip = λlft.size λlft.key λlft.val λlft.lft λlft.rgt -// let new_size = #(+ #1 lft.size) -// let lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt) -// let rgt = (BBT.tip K V) -// (BBT.bin K V new_size key val lft rgt) -// ((~rgt P bin tip) lft.size lft.key lft.val lft.lft lft.rgt) -// let tip = λrgt -// let P = λx(BBT K V) -// let bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt -// let new_size = #(+ #1 rgt.size) -// let lft = (BBT.tip K V) -// let rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt) -// (BBT.bin K V new_size key val lft rgt) -// let tip = (BBT.singleton K V key val) -// (~rgt P bin tip) -// ((~lft P bin tip) rgt) - + (~(BBT.got_size K V lft) P new) \ No newline at end of file diff --git a/book/BBT.set.kind2 b/book/BBT.set.kind2 index 4e8e3c7a..268bf815 100644 --- a/book/BBT.set.kind2 +++ b/book/BBT.set.kind2 @@ -17,6 +17,7 @@ BBT.set (BBT.balance K V cmp key next.key next.val new_lft next.rgt) // Same key, update value + // Should we update the value or return the same tree? let eql = λkey λnext.key λnext.val λnext.lft λnext.rgt (BBT.bin K V size next.key val next.lft next.rgt) From 0e97867813954b02bd0fcff4610978e1b27a93f5 Mon Sep 17 00:00:00 2001 From: Derenash Date: Wed, 21 Feb 2024 12:10:56 -0300 Subject: [PATCH 07/12] add Cmp files for String and U60 --- book/String.cmp.kind2 | 22 ++++++++++++++++++++++ book/U60.cmp.kind2 | 7 +++++++ 2 files changed, 29 insertions(+) create mode 100644 book/String.cmp.kind2 create mode 100644 book/U60.cmp.kind2 diff --git a/book/String.cmp.kind2 b/book/String.cmp.kind2 new file mode 100644 index 00000000..1f33e9d3 --- /dev/null +++ b/book/String.cmp.kind2 @@ -0,0 +1,22 @@ +String.cmp +: ∀(a: String) + ∀(b: String) + Cmp += λa λb + let P = λx ∀(b: String) (Cmp) + let cons = λa.head λa.tail λb + let P = λx ∀(a.head: Char) ∀(a.tail: String) (Cmp) + let cons = λb.head λb.tail λa.head λa.tail + let P = λx Cmp + let ltn = Cmp.ltn + let eql = (String.cmp a.tail b.tail) + let gtn = Cmp.gtn + (~(U60.cmp a.head b.head) P ltn eql gtn) + let nil = λa.head λa.tail Cmp.gtn + ((~b P cons nil) a.head a.tail) + let nil = λb + let P = λx Cmp + let cons = λb.head λb.tail Cmp.ltn + let nil = Cmp.eql + (~b P cons nil) + (~a P cons nil b) \ No newline at end of file diff --git a/book/U60.cmp.kind2 b/book/U60.cmp.kind2 new file mode 100644 index 00000000..530f233f --- /dev/null +++ b/book/U60.cmp.kind2 @@ -0,0 +1,7 @@ +U60.cmp +: ∀(a: #U60) + ∀(b: #U60) + (Cmp) += λa λb + (U60.if #(== a b) Cmp (U60.if #(< a b) Cmp Cmp.gtn Cmp.ltn) Cmp.eql) + \ No newline at end of file From 627cc96777324d09d3ec08c879cdb1722d236f6e Mon Sep 17 00:00:00 2001 From: Derenash Date: Wed, 21 Feb 2024 12:11:42 -0300 Subject: [PATCH 08/12] Add commented version of BBT maps to String and U60 --- book/String.Map.kind2 | 38 ++++++++++++++++++++++++++++++++++++++ book/U60.Map.kind2 | 39 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 77 insertions(+) diff --git a/book/String.Map.kind2 b/book/String.Map.kind2 index b465499e..577087a9 100644 --- a/book/String.Map.kind2 +++ b/book/String.Map.kind2 @@ -25,3 +25,41 @@ String.Map.new : ∀(V: *) (String.Map V) = λV (List.Map.new String V) + +// BBT Version + +// String.Map +// : ∀(V: *) +// * +// = λV (BBT String V) + +// String.Map.get +// : ∀(V: *) +// ∀(key: String) +// ∀(map: (String.Map V)) +// (Maybe V) +// = λV λkey λmap +// (BBT.get String V String.cmp key map) + +// String.Map.got +// : ∀(V: *) +// ∀(key: String) +// ∀(map: (String.Map V)) +// (Pair (Maybe V) (String.Map V)) +// = λV λkey λmap +// (BBT.got String V String.cmp key map) + +// String.Map.set +// : ∀(V: *) +// ∀(key: String) +// ∀(val: V) +// ∀(map: (String.Map V)) +// (String.Map V) +// = λV λkey λval λmap +// (BBT.set String V String.cmp key val map) + +// String.Map.new +// : ∀(V: *) +// (String.Map V) +// = λV (BBT.tip String V) + diff --git a/book/U60.Map.kind2 b/book/U60.Map.kind2 index ee14a2a3..5503d47f 100644 --- a/book/U60.Map.kind2 +++ b/book/U60.Map.kind2 @@ -1,3 +1,4 @@ + // Temporarily just a list of key/val U60.Map @@ -25,3 +26,41 @@ U60.Map.new : ∀(V: *) (U60.Map V) = λV (List.Map.new #U60 V) + + +// BBT Version + +// U60.Map +// : ∀(V: *) +// * +// = λV (BBT #U60 V) + +// U60.Map.get +// : ∀(V: *) +// ∀(key: #U60) +// ∀(map: (U60.Map V)) +// (Maybe V) +// = λV λkey λmap +// (BBT.get #U60 V U60.cmp key map) + +// U60.Map.got +// : ∀(V: *) +// ∀(key: #U60) +// ∀(map: (U60.Map V)) +// (Pair (Maybe V) (U60.Map V)) +// = λV λkey λmap +// (BBT.got #U60 V U60.cmp key map) + +// U60.Map.set +// : ∀(V: *) +// ∀(key: #U60) +// ∀(val: V) +// ∀(map: (U60.Map V)) +// (U60.Map V) +// = λV λkey λval λmap +// (BBT.set #U60 V U60.cmp key val map) + +// U60.Map.new +// : ∀(V: *) +// (U60.Map V) +// = λV (BBT.tip #U60 V) From 658bade510f22ab74f2c81fc64034f81cb974292 Mon Sep 17 00:00:00 2001 From: Derenash Date: Wed, 21 Feb 2024 12:12:11 -0300 Subject: [PATCH 09/12] Update BBT tests file --- book/testBBT.kind2 | 527 ++++++++++++++------------------------------- 1 file changed, 157 insertions(+), 370 deletions(-) diff --git a/book/testBBT.kind2 b/book/testBBT.kind2 index 01be53b4..3775c8c5 100644 --- a/book/testBBT.kind2 +++ b/book/testBBT.kind2 @@ -1,386 +1,173 @@ -List.Map.gen -: ∀(n: #U60) - (List.Map #U60 String) -= λn - (List.Map.gen.go n (List.Map.new #U60 String)) +// Add_spaces +// : ∀(n: #U60) +// (String) +// = λn +// (U60.if #(== n #0) String (String.concat " " (Add_spaces #(- n #1))) "") -List.Map.gen.go -: ∀(n: #U60) - ∀(map: (List.Map #U60 String)) - (List.Map #U60 String) -= λn λmap - let P = λx ∀(map: (List.Map #U60 String)) (List.Map #U60 String) - let true = λmap (List.Map.set #U60 String n (U60.show n) map) - let false = λmap (List.Map.set #U60 String n (U60.show n) (List.Map.gen.go #(- n #1) map)) - ((~(U60.to_bool #(== n #0)) P true false) map) +// U60.Map_show +// : ∀(map: (U60.Map String)) +// ∀(depth: #U60) +// (String) +// = λmap λdepth +// let P = λx(String) +// let bin = λsize λkey λval λlft λrgt +// let cct = λa λb (String.concat a b) +// let spc = λx (cct (Add_spaces depth) x) +// let nnl = λx (cct String.newline x) +// let key = (U60.show key) +// let size = (U60.show size) +// let a = (nnl (spc (cct "key: " key))) +// let b = (cct ", size: " size) +// let c = (cct ", value: " val) +// let d = (nnl (spc (cct "left: " (U60.Map_show lft #(+ #1 depth))))) +// let e = (nnl (spc (cct "right: " (U60.Map_show rgt #(+ #1 depth))))) +// (cct a (cct b (cct c (cct d e )))) +// let tip = "" +// (~map P bin tip) -List.Map.sum -: ∀(map: (List.Map #U60 String)) - (#U60) -= λmap - let P = λx(#U60) - let cons = λhead λtail - let P = λx(#U60) - let new = λkey λval - #(+ key (List.Map.sum tail)) - (~head P new) - let nil = #0 - (~map P cons nil) +// U60.Map.gen +// : ∀(V: *) +// ∀(to_val: ∀(n: #U60) V) +// ∀(n: #U60) +// (U60.Map V) +// = λV λto_val λn +// (U60.Map.gen.go V to_val n (U60.Map.new V)) -Tests.run -: ∀(tests: (List (Maybe String))) - String -= λtests - let folder = (List.fold (Maybe String) tests) - (folder String (λhead λtail (~head λx(String) λsome(some) tail)) (String.cons #10 String.nil)) +// U60.Map.gen.go +// : ∀(V: *) +// ∀(to_val: ∀(n: #U60) V) +// ∀(n: #U60) +// ∀(map: (U60.Map V)) +// (U60.Map V) +// = λV λto_val λn λmap +// let P = λx ∀(map: (U60.Map String)) (U60.Map String) +// let true = λmap (U60.Map.set String n (to_val n) map) +// let false = λmap (U60.Map.gen.go V to_val #(- n #1) (U60.Map.set String n (to_val n) map)) +// ((~(U60.to_bool #(== n #0)) P true false) map) -U60.cmp -: ∀(a: #U60) - ∀(b: #U60) - (Cmp) -= λa λb - (U60.if #(== a b) Cmp (U60.if #(< a b) Cmp Cmp.gtn Cmp.ltn) Cmp.eql ) +// U60.fold +// : ∀(A: *) +// ∀(f: ∀(n: #U60) ∀(acc: A) A) +// ∀(nil: A) +// ∀(n: #U60) +// A +// = λA λf λnil λn +// (U60.fold.go A f nil n) -U60.get -: ∀(V: *) - ∀(key: #U60) - ∀(map: (BBT #U60 V)) - (Maybe V) -= λ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) - ∀(value: V) - ∀(map: (BBT #U60 V)) - (BBT #U60 V) -= λV λkey λvalue λmap - (BBT.set #U60 V U60.cmp key value map) - -U60.add_spaces -: ∀(n: #U60) - (String) -= λn - (U60.if #(== n #0) String (String.concat " " (U60.add_spaces #(- n #1))) "") - -U60.map_show -: ∀(map: (BBT #U60 String)) - ∀(depth: #U60) - (String) -= λmap λdepth - let P = λx(String) - let bin = λsize λkey λval λlft λrgt - let cct = λa λb (String.concat a b) - let spc = λx (cct (U60.add_spaces depth) x) - let nnl = λx (cct String.newline x) - let key = (U60.show key) - let size = (U60.show size) - let a = (nnl (spc (cct "key: " key))) - let b = (cct ", size: " size) - let c = (cct ", value: " val) - let d = (nnl (spc (cct "left: " (U60.map_show lft #(+ #1 depth))))) - let e = (nnl (spc (cct "right: " (U60.map_show rgt #(+ #1 depth))))) - (cct a (cct b (cct c (cct d e )))) - let tip = "" - (~map P bin tip) - -U60.map_gen -: ∀(n: #U60) - (BBT #U60 String) -= λn - (U60.map_gen.go n (BBT.tip #U60 String)) - -U60.map_gen.go -: ∀(n: #U60) - ∀(map: (BBT #U60 String)) - (BBT #U60 String) -= λn λmap - let P = λx ∀(map: (BBT #U60 String)) (BBT #U60 String) - let true = λmap (U60.set String n (U60.show n) map) - let false = λmap (U60.map_gen.go #(- n #1) (U60.set String n (U60.show n) map)) - ((~(U60.to_bool #(== n #0)) P true false) map) - -U60.map_gen_u60 -: ∀(n: #U60) - (BBT #U60 #U60) -= λn - (U60.map_gen_u60.go n (BBT.tip #U60 #U60)) - -U60.map_gen_u60.go -: ∀(n: #U60) - ∀(map: (BBT #U60 #U60)) - (BBT #U60 #U60) -= λn λmap - let P = λx ∀(map: (BBT #U60 #U60)) (BBT #U60 #U60) - let true = λmap (U60.set #U60 n n map) - let false = λmap (U60.map_gen_u60.go #(- n #1) (U60.set #U60 n n map)) - ((~(U60.to_bool #(== n #0)) P true false) map) - -Cmp.show -: ∀(cmp: Cmp) - (String) -= λcmp - let P = λx(String) - let ltn = "ltn" - let eql = "eql" - let gtn = "gtn" - (~cmp P ltn eql gtn) +// U60.fold.go +// : ∀(A: *) +// ∀(f: ∀(n: #U60) ∀(acc: A) A) +// ∀(acc: A) +// ∀(n: #U60) +// A +// = λA λf λacc λn +// (~(U60.to_bool n) λx(A) (U60.fold.go A f (f n acc) #(- n #1)) acc) -Test1 -: (Maybe String) -= - let emptyMap = (BBT.tip #U60 String) - let updatedMap = (U60.set String #5 "value5" emptyMap) - let value = (U60.get String #5 updatedMap) - let is_equal = (String.equal (~value λx(String) λsome(some) "none") "value5") - (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 1 Failed!")) +// AscendingMap +// : (U60.Map #U60) +// = +// let nil = (U60.Map.new #U60) +// let f = λn λacc (U60.Map.set #U60 #(- #11 n) #(- #11 n) acc) +// (U60.fold (U60.Map #U60) f nil #10) -// Update an existing key -Test2 -: (Maybe String) -= - let initialMap = (U60.set String #10 "initialValue" (BBT.tip #U60 String)) - let updatedMap = (U60.set String #10 "updatedValue" initialMap) - let value = (U60.get String #10 updatedMap) - let is_equal = (String.equal (~value λx(String) λsome(some) "none") "updatedValue") - (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 2 Failed!")) +// DescendingMap +// : (U60.Map #U60) +// = +// let nil = (U60.Map.new #U60) +// let f = λn λacc (U60.Map.set #U60 #(+ n #0) n acc) +// (U60.fold (U60.Map #U60) f nil #10) -// Getting on a full map -Test3 -: (Maybe String) -= - let map = (U60.map_gen #24) - let value = (U60.get String #7 map) - let is_equal = (String.equal (~value λx(String) λsome(some) "none") "7") - (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 3 Failed!")) +// U60.Map.sum +// : ∀(map: (U60.Map #U60)) +// (#U60) +// = λmap +// let P = λx(#U60) +// let bin = λsize λkey λval λlft λrgt +// let sum = #(+ #(+ key (U60.Map.sum lft)) (U60.Map.sum rgt)) +// sum +// let tip = #0 +// (~map P bin tip) + +// Test1 +// : (Maybe String) +// = +// let emptyMap = (BBT.tip #U60 String) +// let updatedMap = (U60.Map.set String #5 "value5" emptyMap) +// let value = (U60.Map.get String #5 updatedMap) +// let is_equal = (String.equal (~value λx(String) λsome(some) "none") "value5") +// (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 1 Failed!")) + +// Test2 +// : (Maybe String) +// = +// let initialMap = (U60.Map.set String #10 "initialValue" (U60.Map.new String)) +// let updatedMap = (U60.Map.set String #10 "updatedValue" initialMap) +// let value = (U60.Map.get String #10 updatedMap) +// let is_equal = (String.equal (~value λx(String) λsome(some) "none") "updatedValue") +// (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 2 Failed!")) + +// Test3 +// : (Maybe String) +// = +// let map = (U60.Map.gen String U60.show #24) +// let value = (U60.Map.get String #7 map) +// let is_equal = (String.equal (~value λx(String) λsome(some) "none") "7") +// (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 3 Failed!")) + +// Test4 +// : (Maybe String) +// = +// let map = (U60.Map.gen String U60.show #5) +// let value = (U60.Map.get String #6 map) +// let is_none = (~value λx(Bool) λval(Bool.false) Bool.true) +// (~is_none λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 4 Failed!")) + +// Test5 +// : (Maybe String) +// = +// let map = AscendingMap +// let sum = (U60.Map.sum map) +// let expected_sum = #55 +// let is_equal = (U60.equal sum expected_sum) +// (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 5 Failed!")) + +// Test6 +// : (Maybe String) +// = +// let map = (U60.Map.gen #U60 λx(x) #20) +// let new = λfirst_value λmap +// let new = λlast_value λmap +// let is_first_correct = (U60.equal (~first_value λx(#U60) λsome(some) #0) #3) +// let is_last_correct = (U60.equal (~last_value λx(#U60) λsome(some) #0) #10) +// let are_both_correct = (Bool.and is_first_correct is_last_correct) +// (~are_both_correct λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 6 Failed!")) +// (~(U60.Map.got #U60 #10 map) λx(Maybe String) new) +// (~(U60.Map.got #U60 #3 map) λx(Maybe String) new) -U60.fold -: ∀(A: *) - ∀(f: ∀(n: #U60) ∀(acc: A) A) - ∀(nil: A) - ∀(n: #U60) - A -= λA λf λnil λn - (U60.fold.go A f nil n) +// Tests.run +// : ∀(tests: (List (Maybe String))) +// String +// = λtests +// let folder = (List.fold (Maybe String) tests) +// (folder String (λhead λtail (~head λx(String) λsome(some) tail)) "All tests passed!") -U60.fold.go -: ∀(A: *) - ∀(f: ∀(n: #U60) ∀(acc: A) A) - ∀(acc: A) - ∀(n: #U60) - A -= λA λf λacc λn - (~(U60.to_bool n) λx(A) (U60.fold.go A f (f n acc) #(- n #1)) acc) - - -AscendingMap -: (BBT #U60 #U60) -= - let nil = (BBT.tip #U60 String) - let f = λn λacc (U60.set String #(- #10 n) #(- #10 n) acc) - (U60.fold (BBT #U60 String) f nil #10) - -DescendingMap -: (BBT #U60 #U60) -= - let nil = (BBT.tip #U60 String) - let f = λn λacc (U60.set String #(+ n #0) n acc) - (U60.fold (BBT #U60 String) f nil #10) - -// Adds all the numbers in a map -U60.add_all -: ∀(map: (BBT #U60 #U60)) - (#U60) -= λmap - let P = λx(#U60) - let bin = λsize λkey λval λlft λrgt - let sum = #(+ #(+ key (U60.add_all lft)) (U60.add_all rgt)) - sum - let tip = #0 - (~map P bin tip) - -RunTests -: (String) -= - let tests = (List.nil (Maybe String)) - let tests = (List.cons (Maybe String) Test1 tests) - let tests = (List.cons (Maybe String) Test2 tests) - let tests = (List.cons (Maybe String) Test3 tests) - let solution = (Tests.run tests) - solution +// RunTests +// : (String) +// = +// let tests = (List.nil (Maybe String)) +// let tests = (List.cons (Maybe String) Test1 tests) +// let tests = (List.cons (Maybe String) Test2 tests) +// let tests = (List.cons (Maybe String) Test3 tests) +// let tests = (List.cons (Maybe String) Test4 tests) +// let tests = (List.cons (Maybe String) Test5 tests) +// let tests = (List.cons (Maybe String) Test6 tests) +// let solution = (Tests.run tests) +// solution testBBT -// : (Maybe String) -// : String -// : (List.Map #U60 String) -// : (BBT #U60 String) -: (#U60) -// : (Maybe #U60) -= - // let map = (BBT.tip #U60 String) - // let map = ~λP λbin λtip (tip) - // let map = (BBT.singleton #U60 String #0 "0") - // let map = (U60.set String #0 "0" map) - // let map = (U60.set String #1 "1" map) - // map - +: String += "File commented for backward compatibility." // RunTests - // (Maybe.none String) - // let map = (List.Map.gen #1024) - // map - // let sum = (List.Map.sum map) - // sum - // let val = (List.Map.get #U60 String U60.equal #0 map) - // val - // map - // let map = (U60.map_gen #1024) - // let val1 = (U60.get String #5 map) - // let val2 = (U60.get String #10 map) - // #(+ val1 val2) - // val1 - // 75225975 - // 35973695 - Removed 1 duplicate map on set - // 35973695 - Removed 2 duplicate values - // 35894135 - Removed 2 duplicate keys - // 9827059 - // let map = (U60.map_gen_u60 #2) - // let map = (BBT.tip #U60 #U60) - // let map = (U60.set #U60 #0 #0 map) // 299 +299 1set - // let map = (U60.set #U60 #1 #1 map) // 1293 +994 2set 1bal - // let map = (U60.set #U60 #2 #2 map) // 3958 +2665 3set 2bal 1rot_lft - // let map = (U60.set #U60 #3 #3 map) // 5811 +1853 3set 2bal - // let map = (U60.set #U60 #4 #4 map) // 9342 +3431 4set 3bal 1rot_lft - // let map = (U60.set #U60 #5 #5 map) // 12952 +3610 4set 3bal 1rot_lft - // let map = (U60.set #U60 #6 #6 map) // 16553 +3601 4set 3bal 1rot_lft - // let map = (U60.set #U60 #7 #7 map) // 19141 +2588 4set 3bal - // 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 map = (BBT.tip #U60 #U60) - let map = (U60.set #U60 #0 #0 map) // 299 +299 1set - let map = (U60.set #U60 #1 #1 map) // 1293 +994 2set 1bal - let map = (U60.set #U60 #2 #2 map) // 3958 +2665 3set 2bal 1rot_lft - let map = (U60.set #U60 #3 #3 map) // 5811 +1853 3set 2bal - let map = (U60.set #U60 #4 #4 map) // 9342 +3431 4set 3bal 1rot_lft - let map = (U60.set #U60 #5 #5 map) // 12952 +3610 4set 3bal 1rot_lft - let map = (U60.set #U60 #6 #6 map) // 16553 +3601 4set 3bal 1rot_lft - let map = (U60.set #U60 #7 #7 map) // 19141 +2588 4set 3bal - 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 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) - // sum - - // let map = (BBT.bin #U60 #U60 #1 #0 #0 (BBT.tip #U60 #U60) (BBT.tip #U60 #U60)) - // let map = (BBT.singleton #U60 #U60 #0 #0) - // let sum = (U60.add_all map) - // let val = (BBT.get #U60 #U60 U60.cmp #0 map) - // let val = (U60.get #U60 #0 map) - // map - // val - // sum - // let map = (BBT.tip #U60 #U60) - // let map = (U60.set #U60 #0 #0 map) - // let map = (U60.set #U60 #1 #1 map) - // let map = (U60.set #U60 #2 #2 map) - // let map = (U60.set #U60 #3 #3 map) - // let map = (U60.set #U60 #4 #4 map) - // let map = (AscendingMap) // 27990 - // let map = (DescendingMap) // 26901 - // let map = (U60.map_gen #1024) - // let map = (U60.set #U60 #0 #15 map) - // (U60.get String #10 map) - // let sum = (U60.add_all map) - // sum - // let map = (U60.set #U60 #2000 "test" map) - - // // test u60 fold - // let u60test = (U60.fold String (λn λacc (String.concat (String.concat (U60.show n) String.newline) acc) ) "" #10) - // // u60test - - // let ascMap = AscendingMap - // let descMap = DescendingMap - // // [0, 3, 7] - // let asc0 = (U60.get String #0 ascMap) - // let asc1 = (U60.get String #3 ascMap) - // let asc2 = (U60.get String #7 ascMap) - // let desc0 = (U60.get String #0 descMap) - // let desc1 = (U60.get String #3 descMap) - // let desc2 = (U60.get String #7 descMap) - // (U60.map_show map #0) - - - // (~asc1 λx(String) λsome(some) "VAZIOO") - - // let map = (BBT.tip #U60 String) - // let map = (U60.set String #0 "hello" map) - // // let map = (U60.set String #1 "world" map) - // let map = (U60.set String #2 "!" map) - // // (U60.get String #0 map) - // (U60.map_show map #0) - // let cct = λa λb (String.concat a b) - // let map = (U60.map_gen #24) - // let func = λx (~x λx(String) λsome(some) "none") - // let a = (func (U60.get String #0 map)) - // let b = (func (U60.get String #1 map)) - // let c = (func (U60.get String #2 map)) - // let d = (func (U60.get String #4 map)) - // let e = (func (U60.get String #8 map)) - // let f = (func (U60.get String #16 map)) - // let g = (func (U60.get String #32 map)) - // let h = (func (U60.get String #64 map)) - // (U60.map_show map #0) - // (cct a (cct b (cct c (cct d (cct e (cct f (cct g h))))))) - // a - - - // (Cmp.show (U60.cmp #2 #0)) - // (Tests.run (List.cons (Maybe String) (Maybe.none String) (List.cons (Maybe String) (Maybe.some String "error!") (List.nil (Maybe String))))) - - From 1336cd89a0e20ab7e6f08b8bb9815a410d8401f3 Mon Sep 17 00:00:00 2001 From: Derenash Date: Wed, 21 Feb 2024 12:14:16 -0300 Subject: [PATCH 10/12] add comment to testBBT --- book/testBBT.kind2 | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/book/testBBT.kind2 b/book/testBBT.kind2 index 3775c8c5..93ccef0f 100644 --- a/book/testBBT.kind2 +++ b/book/testBBT.kind2 @@ -169,5 +169,11 @@ testBBT : String -= "File commented for backward compatibility." += +" +File commented for backward compatibility. +To run the tests, uncomment the code on: + testBBT.kind2 + U60.Map +" // RunTests From 0f7ebfe06dab59553d3a4c727ea219b6e986acba Mon Sep 17 00:00:00 2001 From: Derenash Date: Wed, 21 Feb 2024 12:18:31 -0300 Subject: [PATCH 11/12] deleting and commenting few U60 files --- book/U60.abs_diff.kind2 | 1 + book/U60.test.kind2 | 5 ----- 2 files changed, 1 insertion(+), 5 deletions(-) delete mode 100644 book/U60.test.kind2 diff --git a/book/U60.abs_diff.kind2 b/book/U60.abs_diff.kind2 index 92699566..0380546a 100644 --- a/book/U60.abs_diff.kind2 +++ b/book/U60.abs_diff.kind2 @@ -1,3 +1,4 @@ +// Returns the absolute difference between two U60s U60.abs_diff : ∀(a: #U60) ∀(b: #U60) diff --git a/book/U60.test.kind2 b/book/U60.test.kind2 deleted file mode 100644 index be5324df..00000000 --- a/book/U60.test.kind2 +++ /dev/null @@ -1,5 +0,0 @@ -U60.test -: ∀(a: #U60) - (#U60) -= λa - U60.if From 3f1828cb0a93f9f6cc13170bb1375e5b00d0f2c6 Mon Sep 17 00:00:00 2001 From: Derenash Date: Wed, 21 Feb 2024 12:21:03 -0300 Subject: [PATCH 12/12] add extra lines to test6 for merge facility --- book/test6.kind2 | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/book/test6.kind2 b/book/test6.kind2 index bd30aa9f..fa05fb37 100644 --- a/book/test6.kind2 +++ b/book/test6.kind2 @@ -1,3 +1,4 @@ test6 : Nat -= (Nat.succ (Nat.succ (Nat.succ Nat.zero))) \ No newline at end of file += (Nat.succ (Nat.succ (Nat.succ Nat.zero))) +