HigherOrderCO/Kind
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind.git synced 2024-08-16 16:10:27 +03:00
Code Issues Packages Projects Releases Wiki Activity

WIP

Browse Source
This commit is contained in:
Victor Taelin 2024-07-05 02:03:05 -03:00
parent 89c6a0d155
commit 24510cedbe
75 changed files with 228 additions and 812 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@ -1,4 +1,5 @@
/target
.bkp/
.tmp/
.kind21/
plans.txt

19
book/BBT.kind2
View File

@ -1,19 +0,0 @@
//BBT
//: ∀(K: *) ∀(V: *) *
//= λK λV
//$(self: (BBT K V))
//∀(P: ∀(bbt: (BBT K V)) *)
//∀(bin:
//∀(size: U60)
//∀(key: K)
//∀(val: V)
//∀(lft: (BBT K V))
//∀(rgt: (BBT K V))
//(P (BBT.bin K V size key val lft rgt))
//)
//∀(tip: (P (BBT.tip K V)))
//(P self)
data BBT K V
| bin (size: U60) (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V))
| tip

97
book/BBT/balance.kind2
View File

@ -1,97 +0,0 @@
use BBT/{bin,tip}
use Bool/{true,false}
balance <K> <V>
(cmp: ∀(a: K) ∀(b: K) Cmp)
(set_key: K)
(node_key: K)
(val: V)
(lft: (BBT K V))
(rgt: (BBT K V))
: (BBT K V) =
match got_lft = (BBT/got_size lft) {
Pair/new:
match got_rgt = (BBT/got_size rgt) {
Pair/new:
use new_size = (+ got_lft.fst got_rgt.fst)
use balance = (U60/abs_diff got_lft.fst got_rgt.fst)
match _ = (U60/to_bool (> balance 1)) {
true:
match _ = (U60/to_bool (< got_lft.fst got_rgt.fst)) {
true: (BBT/balance/lft_heavier cmp new_size node_key set_key val lft rgt)
false: (BBT/balance/rgt_heavier cmp new_size node_key set_key val lft rgt)
}
false: (bin K V new_size node_key val lft rgt)
}
}
}
//BBT.balance
//: ∀(K: *)
//∀(V: *)
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
//∀(set_key: K)
//∀(node_key: K)
//∀(val: V)
//∀(lft: (BBT K V))
//∀(rgt: (BBT K V))
//(BBT K V)
//= λK λV λcmp λset_key λnode_key λval λlft λrgt
//use P = λx (BBT K V)
//use new = λlft.size λlft
//use P = λx (BBT K V)
//use new = λrgt.size λrgt
//use new_size = (+ 1 (U60.max lft.size rgt.size))
//use balance = (U60.abs_diff lft.size rgt.size)
//use P = λx
//∀(new_size: U60)
//∀(node_key: K)
//∀(val: V)
//∀(lft: (BBT K V))
//∀(rgt: (BBT K V))
//(BBT K V)
//use true = λnew_size λnode_key λval λlft λrgt
//use P = λx
//∀(K: *)
//∀(V: *)
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
//∀(new_size: U60)
//∀(node_key: K)
//∀(set_key: K)
//∀(val: V)
//∀(lft: (BBT K V))
//∀(rgt: (BBT K V))
//(BBT K V)
//use true = BBT.balance.lft_heavier
//use false = BBT.balance.rgt_heavier
//(~(U60.to_bool (< rgt.size lft.size))
//P
//true
//false
//K
//V
//cmp
//new_size
//node_key
//set_key
//val
//lft
//rgt
//)
//use false = λnew_size λnode_key λval λlft λrgt
//(BBT.bin K V new_size node_key val lft rgt)
//(~(U60.to_bool (> balance 1))
//P
//true
//false
//new_size
//node_key
//val
//lft
//rgt
//)
//(~(BBT.got_size K V rgt) P new)
//(~(BBT.got_size K V lft) P new)

80
book/BBT/balance/lft_heavier.kind2
View File

@ -1,80 +0,0 @@
use BBT/{bin,tip,lft_rotate,rgt_rotate}
use Bool/{true,false}
lft_heavier <K> <V>
(cmp: ∀(a: K) ∀(b: K) Cmp)
(new_size: U60)
(node_key: K)
(set_key: K)
(val: V)
(lft: (BBT K V))
(rgt: (BBT K V))
: (BBT K V) =
match lft {
bin:
match _ = (Cmp/is_gtn (cmp set_key lft.key)) {
true:
use lft = (lft_rotate lft.size lft.key lft.val lft.lft lft.rgt)
(rgt_rotate new_size lft.key val lft rgt)
false:
use lft = (bin K V lft.size lft.key lft.val lft.lft lft.rgt)
(rgt_rotate new_size lft.key val lft rgt)
}
tip: (tip K V)
}
//BBT.balance.lft_heavier
//: ∀(K: *)
//∀(V: *)
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
//∀(new_size: U60)
//∀(node_key: K)
//∀(set_key: K)
//∀(val: V)
//∀(lft: (BBT K V))
//∀(rgt: (BBT K V))
//(BBT K V)
//= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt
//use P = λx (BBT K V)
//use bin = λlft.size λlft.key λlft.val λlft.lft λlft.rgt
//use P = λx
//∀(new_size: U60)
//∀(key: K)
//∀(val: V)
//∀(lft.key: K)
//∀(lft.val: V)
//∀(lft.lft: (BBT K V))
//∀(lft.rgt: (BBT K V))
//∀(rgt: (BBT K V))
//(BBT K V)
//use true = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt
//use lft = (BBT.lft_rotate
//K
//V
//lft.size
//lft.key
//lft.val
//lft.lft
//lft.rgt
//)
//(BBT.rgt_rotate K V new_size key val lft rgt)
//use false = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt
//use lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt)
//(BBT.rgt_rotate K V new_size key val lft rgt)
//(~(Cmp.is_gtn (cmp set_key lft.key))
//P
//true
//false
//new_size
//node_key
//val
//lft.key
//lft.val
//lft.lft
//lft.rgt
//rgt
//)
//use tip = (BBT.tip K V)
//(~lft P bin tip)

80
book/BBT/balance/rgt_heavier.kind2
View File

@ -1,80 +0,0 @@
use BBT/{bin,tip,lft_rotate,rgt_rotate}
use Bool/{true,false}
rgt_heavier <K> <V>
(cmp: ∀(a: K) ∀(b: K) Cmp)
(new_size: U60)
(node_key: K)
(set_key: K)
(val: V)
(lft: (BBT K V))
(rgt: (BBT K V))
: (BBT K V) =
match rgt {
bin:
match _ = (Cmp/is_gtn (cmp set_key rgt.key)) {
true:
use rgt = (bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt)
(lft_rotate new_size rgt.key val lft rgt)
false:
use rgt = (rgt_rotate rgt.size rgt.key rgt.val rgt.lft rgt.rgt)
(lft_rotate new_size rgt.key val lft rgt)
}
tip: (tip K V)
}
//BBT.balance.rgt_heavier
//: ∀(K: *)
//∀(V: *)
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
//∀(new_size: U60)
//∀(node_key: K)
//∀(set_key: K)
//∀(val: V)
//∀(lft: (BBT K V))
//∀(rgt: (BBT K V))
//(BBT K V)
//= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt
//use P = λx (BBT K V)
//use bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt
//use P = λx
//∀(new_size: U60)
//∀(key: K)
//∀(val: V)
//∀(lft: (BBT K V))
//∀(rgt.key: K)
//∀(rgt.val: V)
//∀(rgt.lft: (BBT K V))
//∀(rgt.rgt: (BBT K V))
//(BBT K V)
//use true = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt
//use rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt)
//(BBT.lft_rotate K V new_size key val lft rgt)
//use false = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt
//use rgt = (BBT.rgt_rotate
//K
//V
//rgt.size
//rgt.key
//rgt.val
//rgt.lft
//rgt.rgt
//)
//(BBT.lft_rotate K V new_size key val lft rgt)
//(~(Cmp.is_gtn (cmp set_key rgt.key))
//P
//true
//false
//new_size
//node_key
//val
//lft
//rgt.key
//rgt.val
//rgt.lft
//rgt.rgt
//)
//use tip = (BBT.tip K V)
//(~rgt P bin tip)

11
book/BBT/bin.kind2
View File

@ -1,11 +0,0 @@
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)

28
book/BBT/from_list.kind2
View File

@ -1,28 +0,0 @@
use BBT/{bin,tip,set}
from_list <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (list: (List (Pair K V))) : (BBT K V) =
match list {
List/cons:
match pair = list.head {
Pair/new: (set cmp pair.fst pair.snd (from_list cmp list.tail))
}
List/nil: (tip K V)
}
//BBT.from_list
//: ∀(K: *)
//∀(V: *)
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
//∀(list: (List (Pair K V)))
//(BBT K V)
//= λK λV λcmp λlist
//use P = λx (BBT K V)
//use cons = λhead λtail
//use P = λx (BBT K V)
//use new = λkey λval
//(BBT.set K V cmp key val (BBT.from_list K V cmp tail))
//(~head P new)
//use nil = (BBT.tip K V)
//(~list P cons nil)

34
book/BBT/get.kind2
View File

@ -1,34 +0,0 @@
use BBT/{bin,tip}
use Cmp/{ltn,eql,gtn}
get <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : (Maybe V) =
match map {
bin:
match _ = (cmp key map.key) {
ltn: (get cmp key map.lft)
eql: (Maybe/some map.val)
gtn: (get cmp key map.rgt)
}
tip: Maybe/none
}
//BBT.get
//: ∀(K: *)
//∀(V: *)
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
//∀(key: K)
//∀(map: (BBT K V))
//(Maybe V)
//= λK λV λcmp λkey λmap
//use P = λx (Maybe V)
//use bin = λ_size λnext.key λnext.val λnext.lft λnext.rgt
//use P = λx
//∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) (Maybe V)
//use ltn = λcmp λkey (BBT.get K V cmp key next.lft)
//use eql = λcmp λkey (Maybe.some V next.val)
//use gtn = λcmp λkey (BBT.get K V cmp key next.rgt)
//(~(cmp key next.key) P ltn eql gtn cmp key)
//use tip = (Maybe.none V)
//(~map P bin tip)

70
book/BBT/got.kind2
View File

@ -1,70 +0,0 @@
use BBT/{bin,tip}
use Maybe/{some,none}
use Cmp/{ltn,eql,gtn}
got <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : (Pair (Maybe V) (BBT K V)) =
match map {
bin:
match _ = (cmp key map.key) {
ltn:
match new_pair = (got cmp key map.lft) {
Pair/new:
let map = (bin K V map.size map.key map.val new_pair.snd map.rgt)
(Pair/new new_pair.fst map)
}
eql: (Pair/new (some map.val) map)
gtn:
match new_pair = (got cmp key map.rgt) {
Pair/new:
let map = (bin K V map.size map.key map.val map.lft new_pair.snd)
(Pair/new new_pair.fst map)
}
}
tip: (Pair/new none (tip K V))
}
//BBT.got
//: ∀(K: *)
//∀(V: *)
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
//∀(key: K)
//∀(map: (BBT K V))
//(Pair (Maybe V) (BBT K V))
//= λK λV λcmp λkey λmap
//use P = λx (Pair (Maybe V) (BBT K V))
//use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
//use P = λx
//∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K)
//(Pair (Maybe V) (BBT K V))
//use ltn = λcmp λkey
//use new_pair = (BBT.got K V cmp key next.lft)
//use P = λx (Pair (Maybe V) (BBT K V))
//use new = λval λlft
//use map = (BBT.bin K V size next.key next.val lft next.rgt)
//(Pair.new (Maybe V) (BBT K V) val map)
//(~new_pair P new)
//use eql = λcmp λkey
//use map = (BBT.bin K V size next.key next.val next.lft next.rgt)
//(Pair.new
//(Maybe V)
//(BBT K V)
//(Maybe.some V next.val)
//map
//)
//use gtn = λcmp λkey
//use new_pair = (BBT.got K V cmp key next.rgt)
//use P = λx (Pair (Maybe V) (BBT K V))
//use new = λval λrgt
//use map = (BBT.bin K V size next.key next.val next.lft rgt)
//(Pair.new (Maybe V) (BBT K V) val map)
//(~new_pair P new)
//(~(cmp key next.key) P ltn eql gtn cmp key)
//use tip = (Pair.new
//(Maybe V)
//(BBT K V)
//(Maybe.none V)
//(BBT.tip K V)
//)
//(~map P bin tip)

20
book/BBT/got_size.kind2
View File

@ -1,20 +0,0 @@
use BBT/{bin,tip}
got_size <K> <V> (map: (BBT K V)) : (Pair U60 (BBT K V)) =
match map {
bin: (Pair/new map.size map)
tip: (Pair/new 0 (tip K V))
}
//BBT.got_size
//: ∀(K: *) ∀(V: *) ∀(map: (BBT K V))
//(Pair U60 (BBT K V))
//= λK λV λmap
//use P = λx (Pair U60 (BBT K V))
//use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
//use map = (BBT.bin K V size next.key next.val next.lft next.rgt)
//(Pair.new U60 (BBT K V) size map)
//use tip = (Pair.new U60 (BBT K V) 0 (BBT.tip K V))
//(~map P bin tip)

33
book/BBT/has.kind2
View File

@ -1,33 +0,0 @@
use BBT/{bin,tip}
use Cmp/{ltn,eql,gtn}
has <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : Bool =
match map {
bin:
match _ = (cmp key map.key) {
ltn: (has cmp key map.lft)
eql: Bool/true
gtn: (has cmp key map.rgt)
}
tip: Bool/false
}
//BBT.has
//: ∀(K: *)
//∀(V: *)
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
//∀(key: K)
//∀(map: (BBT K V))
//Bool
//= λK λV λcmp λkey λmap
//use P = λx Bool
//use bin = λnext.size λnext.key λnext.val λnext.lft λnext.rgt
//use P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) Bool
//use ltn = λcmp λkey (BBT.has K V cmp key next.lft)
//use eql = λcmp λkey Bool.true
//use gtn = λcmp λkey (BBT.has K V cmp key next.rgt)
//(~(cmp key next.key) P ltn eql gtn cmp key)
//use tip = Bool.false
//(~map P bin tip)

74
book/BBT/has/linear.kind2
View File

@ -1,74 +0,0 @@
use BBT/{bin,tip}
use Bool/{false,true}
use Cmp/{ltn,eql,gtn}
linear <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : (Pair Bool (BBT K V)) =
match map {
bin:
match _ = (cmp key map.key) {
ltn:
match result = (linear cmp key map.lft) {
Pair/new:
(Pair/new result.fst (bin K V map.size map.key map.val result.snd map.rgt))
}
eql: (Pair/new true (bin K V map.size map.key map.val map.lft map.rgt))
gtn:
match result = (linear cmp key map.rgt) {
Pair/new:
(Pair/new result.fst (bin K V map.size map.key map.val map.lft result.snd))
}
}
tip: (Pair/new false (tip K V))
}
//BBT.has.linear
//: ∀(K: *)
//∀(V: *)
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
//∀(key: K)
//∀(map: (BBT K V))
//(Pair Bool (BBT K V))
//= λK λV λcmp λhas_key λmap
//use P = λx (Pair Bool (BBT K V))
//use bin = λsize λnode_key λval λlft λrgt
//use P = λx
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
//∀(size: U60)
//∀(node_key: K)
//∀(val: V)
//∀(lft: (BBT K V))
//∀(rgt: (BBT K V))
//∀(key: K)
//(Pair Bool (BBT K V))
//use ltn = λcmp λsize λnode_key λval λlft λrgt λhas_key
//use P = λx (Pair Bool (BBT K V))
//use new = λbool λlft
//use map = (BBT.bin K V size node_key val lft rgt)
//(Pair.new Bool (BBT K V) bool map)
//(~(BBT.has.linear K V cmp has_key lft) P new)
//use eql = λcmp λsize λnode_key λval λlft λrgt λhas_key
//(Pair.new
//Bool
//(BBT K V)
//Bool.true
//(BBT.bin K V size node_key val lft rgt)
//)
//use gtn = λcmp λsize λnode_key λval λlft λrgt λhas_key
//use P = λx (Pair Bool (BBT K V))
//use new = λbool λrgt
//use map = (BBT.bin K V size node_key val lft rgt)
//(Pair.new Bool (BBT K V) bool rgt)
//(~(BBT.has.linear K V cmp has_key rgt) P new)
//((~(cmp has_key node_key) P ltn eql gtn)
//cmp
//size
//node_key
//val
//lft
//rgt
//has_key
//)
//use tip = (Pair.new Bool (BBT K V) Bool.false (BBT.tip K V))
//(~map P bin tip)

31
book/BBT/lft_rotate.kind2
View File

@ -1,31 +0,0 @@
use BBT/{bin,tip}
lft_rotate <K> <V> (size: U60) (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V)) : (BBT K V) =
match rgt {
bin:
use b = (BBT/new_node key val lft rgt.lft)
use a = (BBT/new_node rgt.key rgt.val b rgt.rgt)
a
tip: (bin K V size key val lft (tip K V))
}
//BBT.lft_rotate
//: ∀(K: *)
//∀(V: *)
//∀(size: U60)
//∀(key: K)
//∀(val: V)
//∀(lft: (BBT K V))
//∀(rgt: (BBT K V))
//(BBT K V)
//= λK λV λsize λkey λval λlft λrgt
//use P = λx ∀(key: K) ∀(val: V) ∀(lft: (BBT K V)) (BBT K V)
//use bin = λ_size λrgt.key λrgt.val λrgt.lft λrgt.rgt λkey λval λlft
//use b = (BBT.new_node K V key val lft rgt.lft)
//use a = (BBT.new_node K V rgt.key rgt.val b rgt.rgt)
//a
//use tip = λkey λval λlft
//(BBT.bin K V size key val lft (BBT.tip K V))
//(~rgt P bin tip key val lft)

30
book/BBT/new_node.kind2
View File

@ -1,30 +0,0 @@
use BBT/{bin}
new_node <K> <V> (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V)) : (BBT K V) =
match lft_size = (BBT/got_size lft) {
Pair/new: match rgt_size = (BBT/got_size rgt) {
Pair/new:
use new_size = (+ 1 (U60/max lft_size.fst rgt_size.fst))
(bin K V new_size key val lft rgt)
}
}
//BBT.new_node
//: ∀(K: *)
//∀(V: *)
//∀(key: K)
//∀(val: V)
//∀(lft: (BBT K V))
//∀(rgt: (BBT K V))
//(BBT K V)
//= λK λV λkey λval λlft λrgt
//use P = λx (BBT K V)
//use new = λlft.size λlft
//use P = λx (BBT K V)
//use new = λrgt.size λrgt
//use new_size = (+ 1 (U60.max rgt.size lft.size))
//(BBT.bin K V new_size key val lft rgt)
//(~(BBT.got_size K V rgt) P new)
//(~(BBT.got_size K V lft) P new)

31
book/BBT/rgt_rotate.kind2
View File

@ -1,31 +0,0 @@
use BBT/{bin,tip}
rgt_rotate <K> <V> (size: U60) (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V)) : (BBT K V) =
match lft {
bin:
use b = (BBT/new_node key val lft.rgt rgt)
use a = (BBT/new_node lft.key lft.val lft.lft b)
a
tip: (bin K V size key val (tip K V) rgt)
}
//BBT.rgt_rotate
//: ∀(K: *)
//∀(V: *)
//∀(size: U60)
//∀(key: K)
//∀(val: V)
//∀(lft: (BBT K V))
//∀(rgt: (BBT K V))
//(BBT K V)
//= λK λV λsize λkey λval λlft λrgt
//use P = λx ∀(key: K) ∀(val: V) ∀(rgt: (BBT K V)) (BBT K V)
//use bin = λ_size λlft.key λlft.val λlft.lft λlft.rgt λkey λval λrgt
//use b = (BBT.new_node K V key val lft.rgt rgt)
//use a = (BBT.new_node K V lft.key lft.val lft.lft b)
//a
//use tip = λkey λval λrgt
//(BBT.bin K V size key val (BBT.tip K V) rgt)
//(~lft P bin tip key val rgt)

81
book/BBT/set.kind2
View File

@ -1,81 +0,0 @@
use BBT/{bin,tip}
use Cmp/{ltn,eql,gtn}
set <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (val: V) (map: (BBT K V)) : (BBT K V) =
match map {
bin:
match _ = (cmp key map.key) {
ltn:
use new_lft = (set cmp key val map.lft)
(BBT/balance cmp key map.key map.val new_lft map.rgt)
eql: (bin K V map.size map.key val map.lft map.rgt)
gtn:
use new_rgt = (set cmp key val map.rgt)
(BBT/balance cmp key map.key map.val map.lft new_rgt)
}
tip: (BBT/singleton key val)
}
//BBT.set
//: ∀(K: *)
//∀(V: *)
//∀(cmp: ∀(a: K) ∀(b: K) Cmp)
//∀(key: K)
//∀(val: V)
//∀(map: (BBT K V))
//(BBT K V)
//= λK λV λcmp λkey λval λmap
//use P = λx ∀(key: K) ∀(val: V) (BBT K V)
//use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt λkey λval
//use P = λx
//∀(key: K)
//∀(next.key: K)
//∀(next.val: V)
//∀(next.lft: (BBT K V))
//∀(next.rgt: (BBT K V))
//∀(key: K)
//∀(val: V)
//(BBT K V)
//use ltn = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
//use new_lft = (BBT.set K V cmp key val next.lft)
//(BBT.balance
//K
//V
//cmp
//key
//next.key
//next.val
//new_lft
//next.rgt
//)
//use eql = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
//(BBT.bin K V size next.key val next.lft next.rgt)
//use gtn = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
//use new_rgt = (BBT.set K V cmp key val next.rgt)
//(BBT.balance
//K
//V
//cmp
//key
//next.key
//next.val
//next.lft
//new_rgt
//)
//(~(cmp key next.key)
//P
//ltn
//eql
//gtn
//key
//next.key
//next.val
//next.lft
//next.rgt
//key
//val
//)
//use tip = λkey λval (BBT.singleton K V key val)
//(~map P bin tip key val)

10
book/BBT/singleton.kind2
View File

@ -1,10 +0,0 @@
singleton <K> <V> (key: K) (val: V) : (BBT K V) =
use tip = (BBT/tip K V)
(BBT/bin K V 1 key val tip tip)
//BBT.singleton
//: ∀(K: *) ∀(V: *) ∀(key: K) ∀(val: V) (BBT K V)
//= λK λV λkey λval
//(BBT.bin K V 1 key val (BBT.tip K V) (BBT.tip K V))

3
book/BBT/tip.kind2
View File

@ -1,3 +0,0 @@
BBT.tip
: ∀(K: *) ∀(V: *) (BBT K V)
= λK λV ~λP λbin λtip tip

32
book/BBT/to_list.kind2
View File

@ -1,32 +0,0 @@
use BBT/{bin,tip}
to_list <K> <V> (map: (BBT K V)) : (List (Pair K V)) =
match map {
bin:
use lft = (to_list map.lft)
use rgt = (to_list map.rgt)
use pair = (Pair/new map.key map.val)
use list = (List/cons pair (List/concat lft rgt))
list
tip: List/nil
}
//BBT.to_list
//: ∀(K: *) ∀(V: *) ∀(map: (BBT K V))
//(List (Pair K V))
//= λK λV λmap
//use P = λx (List (Pair K V))
//use bin = λsize λkey λval λlft λrgt
//use lft = (BBT.to_list K V lft)
//use rgt = (BBT.to_list K V rgt)
//use pair = (Pair.new K V key val)
//use list = (List.cons
//(Pair K V)
//pair
//(List.concat (Pair K V) lft rgt)
//)
//list
//use tip = (List.nil (Pair K V))
//(~map P bin tip)

2
book/BMap.kind2 → book/BMap/_.kind2
View File

@ -1,3 +1,3 @@
data BMap A
data BMap <A>
| node (lft: (BMap A)) (val: A) (rgt: (BMap A))
| leaf

2
book/BMap/leaf.kind2
View File

@ -1,3 +1,3 @@
BMap.leaf
BMap/leaf
: ∀(A: *) (BMap A)
= λA ~λP λnode λleaf leaf

Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 61 B

After

Width:  |  Height:  |  Size: 61 B

2
book/BMap/node.kind2
View File

@ -1,4 +1,4 @@
BMap.node
BMap/node
: ∀(A: *)
∀(lft: (BMap A))
∀(val: A)

Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 153 B

After

Width:  |  Height:  |  Size: 153 B

0
book/Bool.kind2 → book/Bool/_.kind2
View File

2
book/Bool/and.kind2
View File

@ -2,6 +2,6 @@ use Bool/{true,false,and}
and (a: Bool) (b: Bool) : Bool =
match a {
true: "foo"
true: b
false: false
}

5
book/Bool/lemma/double_negation.kind2
View File

@ -1,4 +1,7 @@
use Bool/{true,false,not}
double_negation (x: Bool) : (Equal Bool (not (not x)) x) =
?a
match x {
true : {=}
false: {=}
}

0
book/Char.kind2 → book/Char/_.kind2
View File

0
book/Cmp.kind2 → book/Cmp/_.kind2
View File

0
book/Empty.kind2 → book/Empty/_.kind2
View File

0
book/Equal.kind2 → book/Equal/_.kind2
View File

12
book/Equal/match.kind2
View File

@ -4,15 +4,3 @@ match <T: *> <a: T> <b: T>
(e: (Equal T a b))
: (P a b e) =
(~e P refl)
can you understand this?
Yes, this appears to be a dependently-typed pattern matching function, likely written in a language similar to Idris, Agda, or Coq. It's implementing the principle of indiscernibility of identicals, also known as Leibniz's law. Here's a brief explanation:
1. It takes two values `a` and `b` of some type `T`.
2. It takes a predicate `P` that depends on two values of type `T` and a proof of their equality.
3. It takes a proof `refl` that the predicate holds for any value `x` when compared to itself.
4. It takes a proof `e` that `a` and `b` are equal.
5. It returns a proof that the predicate `P` holds for `a`, `b`, and the equality proof `e`.
The implementation uses the equality proof `e` to rewrite the goal, effectively turning it into `P a a (Equal/refl/ T a)`, which can be solved by the `refl` argument.

0
book/IO.kind2 → book/IO/_.kind2
View File

0
book/Kind.kind2 → book/Kind/_.kind2
View File

0
book/List.kind2 → book/List/_.kind2
View File

2
book/Maybe.kind2 → book/Maybe/_.kind2
View File

@ -1,3 +1,3 @@
data Maybe T
data Maybe <T: *>
| some (value: T)
| none

0
book/Monad.kind2 → book/Monad/_.kind2
View File

0
book/Nat.kind2 → book/Nat/_.kind2
View File

167
book/Nat/is_zero.kind2 Normal file
View File

@ -0,0 +1,167 @@
// EXAMPLES IN BEND LANG
type Map_:
Free
Used
Both {~a, ~b}
type Arr:
Null
Leaf {~a}
Node {~a, ~b}
def swap(s, a, b):
switch s:
case 0:
return Map_/Both{ a: a, b: b }
case _:
return Map_/Both{ a: b, b: a }
# Sort : Arr -> Arr
def sort(t):
return to_arr(0, to_map(t))
# ToMap : Arr -> Map
def to_map(t):
match t:
case Arr/Null:
return Map_/Free
case Arr/Leaf:
return radix(t.a)
case Arr/Node:
return merge(to_map(t.a), to_map(t.b))
# ToArr : U60 -> Map -> Arr
def to_arr(x, m):
match m:
case Map_/Free:
return Arr/Null
case Map_/Used:
return Arr/Leaf{ a: x }
case Map_/Both:
return Arr/Node{ a: to_arr(x * 2, m.a), b: to_arr(x * 2 + 1, m.b) }
# Merge : Map -> Map -> Map
def merge(a, b):
match a:
case Map_/Free:
return b
case Map_/Used:
return Map_/Used
case Map_/Both:
match b:
case Map_/Free:
return a
case Map_/Used:
return Map_/Used
case Map_/Both:
return Map_/Both{ a: merge(a.a, b.a), b: merge(a.b, b.b) }
# Radix : U60 -> Map
def radix(n):
r = Map_/Used
r = swap(n & 1, r, Map_/Free)
r = swap(n & 2, r, Map_/Free)
r = swap(n & 4, r, Map_/Free)
r = swap(n & 8, r, Map_/Free)
r = swap(n & 16, r, Map_/Free)
r = swap(n & 32, r, Map_/Free)
r = swap(n & 64, r, Map_/Free)
r = swap(n & 128, r, Map_/Free)
r = swap(n & 256, r, Map_/Free)
r = swap(n & 512, r, Map_/Free)
return radix2(n, r)
# At the moment, we need to manually break very large functions into smaller ones
# if we want to run this program on the GPU.
# In a future version of Bend, we will be able to do this automatically.
def radix2(n, r):
r = swap(n & 1024, r, Map_/Free)
r = swap(n & 2048, r, Map_/Free)
r = swap(n & 4096, r, Map_/Free)
r = swap(n & 8192, r, Map_/Free)
r = swap(n & 16384, r, Map_/Free)
r = swap(n & 32768, r, Map_/Free)
r = swap(n & 65536, r, Map_/Free)
r = swap(n & 131072, r, Map_/Free)
r = swap(n & 262144, r, Map_/Free)
r = swap(n & 524288, r, Map_/Free)
return radix3(n, r)
def radix3(n, r):
r = swap(n & 1048576, r, Map_/Free)
r = swap(n & 2097152, r, Map_/Free)
r = swap(n & 4194304, r, Map_/Free)
r = swap(n & 8388608, r, Map_/Free)
return r
def reverse(t):
match t:
case Arr/Null:
return Arr/Null
case Arr/Leaf:
return t
case Arr/Node:
return Arr/Node{ a: reverse(t.b), b: reverse(t.a) }
# Sum : Arr -> U60
def sum(t):
match t:
case Arr/Null:
return 0
case Arr/Leaf:
return t.a
case Arr/Node:
return sum(t.a) + sum(t.b)
# Gen : U60 -> Arr
def gen(n):
return gen_go(n, 0)
def gen_go(n, x):
switch n:
case 0:
return Arr/Leaf{ a: x }
case _:
a = x * 2
b = x * 2 + 1
return Arr/Node{ a: gen_go(n-1, a), b: gen_go(n-1, b) }
Main = (sum (sort(reverse(gen 4))))
// FUNCTION IN KIND LANG
use Nat/{succ,zero}
is_zero (a: Nat) : String =
match a {
zero: "é zero"
succ: "não é zero"
}
// TASK: translate this kind function to bend
def is_zero(a):
match a:
case Nat/zero:
return "é zero"
case Nat/succ:
return "não é zero"

2
book/Pair.kind2 → book/Pair/_.kind2
View File

@ -1,2 +1,2 @@
data Pair A B
data Pair <A: *> <B: *>
| new (fst: A) (snd: B) : (Pair A B)

0
book/Parser.kind2 → book/Parser/_.kind2
View File

0
book/QBool.kind2 → book/QBool/_.kind2
View File

0
book/QBool2.kind2 → book/QBool2/_.kind2
View File

0
book/QUnit.kind2 → book/QUnit/_.kind2
View File

0
book/Sigma.kind2 → book/Sigma/_.kind2
View File

0
book/String.kind2 → book/String/_.kind2
View File

0
book/The.kind2 → book/The/_.kind2
View File

0
book/Tree.kind2 → book/Tree/_.kind2
View File

2
book/U60/abs_diff.kind2
View File

@ -1,7 +1,7 @@
use Bool/{true,false}
abs_diff (a: U60) (b: U60) : U60 =
match x = (U60/to_bool (< a b)) {
match Bool/true {
true: (- b a)
false: (- a b)
}

2
book/U60/name.kind2
View File

@ -1,2 +1,2 @@
U60.name (n: U60) : String =
U60/name (n: U60) : String =
(String/Chunk/build (U60/name/go (+ n 1)))

2
book/U60/show.kind2
View File

@ -1,2 +1,2 @@
U60.show (n: U60) : String =
U60/show (n: U60) : String =
(String/Chunk/build (U60/show/go n))

0
book/Unit.kind2 → book/Unit/_.kind2
View File

0
book/Vector.kind2 → book/Vector/_.kind2
View File

9
book/foo.ts Normal file
View File

@ -0,0 +1,9 @@
// create a function in typescript with
function foo(n: number) : string {
return "foo";
}
let x : any = "bar";
console.log(foo(x));

0
book/_OBLITERATE.kind2 → book/tmp/_OBLITERATE.kind2
View File

0
book/_err.txt → book/tmp/_err.txt
View File

0
book/_main → book/tmp/_main
View File

0
book/_main.hvm2 → book/tmp/_main.hvm2
View File

0
book/_main.hvmc → book/tmp/_main.hvmc
View File

0
book/_main.js → book/tmp/_main.js
View File

0
book/_main.kind2 → book/tmp/_main.kind2
View File

0
book/test0.kind2 → book/tmp/test0.kind2
View File

0
book/test1.kind2 → book/tmp/test1.kind2
View File

0
book/test10.kind2 → book/tmp/test10.kind2
View File

0
book/test11.kind2 → book/tmp/test11.kind2
View File

0
book/test2.kind2 → book/tmp/test2.kind2
View File

0
book/test3.kind2 → book/tmp/test3.kind2
View File

0
book/test4.kind2 → book/tmp/test4.kind2
View File

0
book/test5.kind2 → book/tmp/test5.kind2
View File

0
book/test6.kind2 → book/tmp/test6.kind2
View File

0
book/test7.kind2 → book/tmp/test7.kind2
View File

0
book/test8.kind2 → book/tmp/test8.kind2
View File

0
book/test9.kind2 → book/tmp/test9.kind2
View File

0
book/testBBT.kind2 → book/tmp/testBBT.kind2
View File

8
src/book/mod.rs
View File

@ -64,7 +64,13 @@ impl Book {
if !self.defs.contains_key(name) {
// Parses a file into a new book
let file = format!("{}/{}.kind2", base, name);
let text = std::fs::read_to_string(&file).map_err(|_| format!("Could not read file: {}", file))?;
let text = match std::fs::read_to_string(&file) {
Ok(content) => content,
Err(_) => {
let backup_file = format!("{}/{}/_.kind2", base, name);
std::fs::read_to_string(&backup_file).map_err(|_| format!("Could not read file: {} or {}", file, backup_file))?
}
};
let fid = self.get_file_id(&file);
let defs = KindParser::new(&text).parse_book(name, fid)?;
// Merges new book into book

4
src/info/mod.rs
View File

@ -53,7 +53,9 @@ impl Info {
let det = format!("- detected: \x1b[31m{}\x1b[0m", det.show());
let bad = format!("- bad_term: \x1b[2m{}\x1b[0m", bad.show());
let file = book.get_file_name(src.fid).unwrap_or_else(|| "unknown_file".to_string());
let text = std::fs::read_to_string(&file).unwrap_or_else(|_| "Could not read source file.".to_string());
let text = std::fs::read_to_string(&file)
.or_else(|_| std::fs::read_to_string(format!("{}/_.kind2", file)))
.unwrap_or_else(|_| "Could not read source file.".to_string());
let orig = highlight_error(src.ini as usize, src.end as usize, &text);
let src = format!("\x1b[4m{}\x1b[0m\n{}", file, orig);
format!("\x1b[1mERROR:\x1b[0m\n{}\n{}\n{}\n{}", exp, det, bad, src)

52
src/kindc.hs
View File

@ -200,9 +200,9 @@ bind term = go term [] where
-- ----------
-- Evaluation levels:
-- - 0: reduces refs never
-- - 1: reduces refs on redexes
-- - 2: reduces refs always
-- - 0: reduces refs: never
-- - 1: reduces refs: redexes
-- - 2: reduces refs: always
reduce :: Book -> Fill -> Int -> Term -> Term
reduce book fill lv (App fun arg) = reduceApp book fill lv (reduce book fill lv fun) arg
@ -315,15 +315,16 @@ normal book fill lv term dep = normalGo book fill lv (reduce book fill lv term)
equal :: Term -> Term -> Int -> Env Bool
equal a b dep = do
book <- envGetBook
fill <- envGetFill
let a' = reduce book fill 2 a
let b' = reduce book fill 2 b
same <- tryIdentical a' b' dep
if same then do
return True
else do
similar a' b' dep
-- trace ("= " ++ termStr a dep ++ "\n? " ++ termStr b dep) $ do
book <- envGetBook
fill <- envGetFill
let a' = reduce book fill 2 a
let b' = reduce book fill 2 b
same <- tryIdentical a' b' dep
if same then do
return True
else do
similar a' b' dep
tryIdentical :: Term -> Term -> Int -> Env Bool
tryIdentical a b dep = do
@ -802,7 +803,7 @@ checkDef (Ref nam) = do
Just val -> case val of
Ann chk val typ -> check 0 val typ 0 >> return ()
Ref nm2 -> checkDef (Ref nm2)
_ -> trace ("oxi" ++ termStr val 0) $ infer val 0 >> return ()
_ -> infer val 0 >> return ()
Nothing -> do
envLog (Error 0 (Hol "undefined_reference" []) (Hol "unknown_type" []) (Ref nam) 0)
envFail
@ -901,7 +902,7 @@ contextStrAnn book fill term dep = termStr (normal book fill 0 term
infoStr :: Book -> Fill -> Info -> String
infoStr book fill (Found name typ ctx dep) =
let typ' = termStr (normal book fill 1 typ dep) dep
let typ' = termStr (normal book fill 0 typ dep) dep
ctx' = drop 1 (contextStr book fill ctx dep)
in concat ["#found{", name, " ", typ', " [", ctx', "]}"]
infoStr book fill (Error src expected detected value dep) =
@ -930,6 +931,7 @@ parseTerm :: P.Parsec String () Term
parseTerm = P.choice
[ parseAll
, parseLam
, parseOp2
, parseApp
, parseAnn
, parseSlf
@ -937,9 +939,7 @@ parseTerm = P.choice
, parseUse
, parseLet
, parseSet
, parseU60
, parseNum
, parseOp2
, parseSwi
, parseTxt
, parseNat
@ -1003,7 +1003,11 @@ parseIns = do
val <- parseTerm
return $ Ins val
parseRef = Ref <$> parseName
parseRef = do
name <- parseName
return $ case name of
"U60" -> U60
_ -> Ref name
parseUse = do
P.try (P.string "use ")
@ -1033,13 +1037,13 @@ parseLet = do
parseSet = P.char '*' >> return Set
parseU60 = P.try $ P.string "U60" >> return U60
parseNum = Num . read <$> P.many1 P.digit
parseOp2 = do
P.char '('
opr <- parseOper
opr <- P.try $ do
P.string "("
opr <- parseOper
return opr
P.spaces
fst <- parseTerm
P.spaces
@ -1108,7 +1112,7 @@ parseSrc = do
parseName :: P.Parsec String () String
parseName = do
head <- P.letter
tail <- P.many (P.alphaNum <|> P.char '/' <|> P.char '.' <|> P.char '_')
tail <- P.many (P.alphaNum <|> P.char '/' <|> P.char '.' <|> P.char '_' <|> P.char '-')
return (head : tail)
parseOper = P.choice
@ -1117,12 +1121,12 @@ parseOper = P.choice
, P.string "*" >> return MUL
, P.string "/" >> return DIV
, P.string "%" >> return MOD
, P.string "<" >> return LT
, P.string ">" >> return GT
, P.string "==" >> return EQ
, P.string "!=" >> return NE
, P.string "<=" >> return LTE
, P.string ">=" >> return GTE
, P.string "<" >> return LT
, P.string ">" >> return GT
, P.string "&" >> return AND
, P.string "|" >> return OR
, P.string "^" >> return XOR