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

auto formatter

Browse Source
This commit is contained in:
Victor Taelin 2024-03-01 20:40:31 -03:00
parent 21dd404798
commit e849d16aee
336 changed files with 4170 additions and 3358 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@ -4,3 +4,4 @@
plans.txt
.check.hvm1
demo/
.fill.tmp

3
book/.fill.tmp
View File

@ -1,3 +0,0 @@
if I take 1 screenshot of my macbook every minute, and store it as a PNG (1920x1080), how much storage will that need, in average, per day? make an educated calculation.
{{FILL_HERE}}

130
book/BBT.balance.kind2
View File

@ -9,90 +9,58 @@ BBT.balance
∀(rgt: (BBT K V))
(BBT K V)
= λK λV λcmp λset_key λnode_key λval λlft λrgt
let P = λx(BBT K V)
let P = λx (BBT K V)
let new = λlft.size λlft
let P = λx(BBT K V)
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 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)
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
)
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)
(~(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
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
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
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
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
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)
// 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)
(~(BBT.got_size K V lft) P new)

53
book/BBT.balance.lft_heavier.kind2 Normal file
View File

@ -0,0 +1,53 @@
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)
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)
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)
(~(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
)
let tip = (BBT.tip K V)
(~lft P bin tip)

53
book/BBT.balance.rgt_heavier.kind2 Normal file
View File

@ -0,0 +1,53 @@
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
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)
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)
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
)
let tip = (BBT.tip K V)
(~rgt P bin tip)

5
book/BBT.bin.kind2
View File

@ -8,7 +8,4 @@ BBT.bin
∀(rgt: (BBT K V))
(BBT K V)
= λK λV λsize λkey λval λlft λrgt
~λP λbin λtip
(bin size key val lft rgt)
~λP λbin λtip (bin size key val lft rgt)

11
book/BBT.from_list.kind2
View File

@ -5,10 +5,11 @@ BBT.from_list
∀(list: (List (Pair K V)))
(BBT K V)
= λK λV λcmp λlist
let P = λx(BBT K V)
let P = λx (BBT K V)
let cons = λhead λtail
let P = λx(BBT K V)
let new = λkey λval (BBT.set K V cmp key val (BBT.from_list K V cmp tail))
let P = λx (BBT K V)
let new = λkey λval
(BBT.set K V cmp key val (BBT.from_list K V cmp tail))
(~head P new)
let nil = (BBT.tip K V)
(~list P cons nil)
let nil = (BBT.tip K V)
(~list P cons nil)

9
book/BBT.get.kind2
View File

@ -6,12 +6,13 @@ BBT.get
∀(map: (BBT K V))
(Maybe V)
= λK λV λcmp λkey λmap
let P = λx(Maybe V)
let P = λx (Maybe V)
let bin = λ_size λnext.key λnext.val λnext.lft λnext.rgt
let P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) (Maybe V)
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)
(~(cmp key next.key) P ltn eql gtn cmp key)
let tip = (Maybe.none V)
(~map P bin tip)
(~map P bin tip)

33
book/BBT.got.kind2
View File

@ -1,4 +1,3 @@
// Returns a pair with the value and the new map
BBT.got
: ∀(K: *)
∀(V: *)
@ -7,26 +6,38 @@ BBT.got
∀(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 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 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 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
(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 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)
(~(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)

9
book/BBT.got_size.kind2
View File

@ -1,13 +1,10 @@
// Returns a pair with the size of the map and the reconstructed map
BBT.got_size
: ∀(K: *)
∀(V: *)
∀(map: (BBT K V))
: ∀(K: *) ∀(V: *) ∀(map: (BBT K V))
(Pair #U60 (BBT K V))
= λK λV λmap
let P = λx(Pair #U60 (BBT K V))
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)
(~map P bin tip)

4
book/BBT.has.kind2
View File

@ -12,6 +12,6 @@ BBT.has
let ltn = λcmp λkey (BBT.has K V cmp key next.lft)
let eql = λcmp λkey Bool.true
let gtn = λcmp λkey (BBT.has K V cmp key next.rgt)
((~(cmp key next.key) P ltn eql gtn) cmp key)
(~(cmp key next.key) P ltn eql gtn cmp key)
let tip = Bool.false
(~map P bin tip)
(~map P bin tip)

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

@ -1,4 +1,3 @@
// Returns a Pair with the boolean (indicating if the key is present) and the original map
BBT.has.linear
: ∀(K: *)
∀(V: *)
@ -7,26 +6,45 @@ BBT.has.linear
∀(map: (BBT K V))
(Pair Bool (BBT K V))
= λK λV λcmp λkey λmap
let P = λx(Pair Bool (BBT K V))
let P = λx (Pair Bool (BBT K V))
let bin = λsize λnode_key λval λlft λrgt
let P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) ∀(lft: (BBT K V)) ∀(rgt: (BBT K V)) (Pair Bool (BBT K V))
let P = λx
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
∀(key: K)
∀(lft: (BBT K V))
∀(rgt: (BBT K V))
(Pair Bool (BBT K V))
let ltn = λcmp λsize λhas_key λval λlft λrgt λhas_key
let P = λx (Pair Bool (BBT K V))
let new = λbool λlft
let new = λbool λlft
let 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)
let eql = λcmp λsize λkey λval λlft λrgt λhas_key
(Pair.new Bool (BBT K V) Bool.true (BBT.bin K V size node_key val lft rgt))
(Pair.new
Bool
(BBT K V)
Bool.true
(BBT.bin K V size node_key val lft rgt)
)
let gtn = λcmp λsize λkey λval λlft λrgt λhas_key
let P = λx (Pair Bool (BBT K V))
let new = λbool λrgt
let new = λbool λrgt
let 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 key node_key) P ltn eql gtn) cmp size node_key val lft rgt key)
(~(cmp key node_key)
P
ltn
eql
gtn
cmp
size
node_key
val
lft
rgt
key
)
let tip = (Pair.new Bool (BBT K V) Bool.false (BBT.tip K V))
(~map P bin tip)
(~map P bin tip)

15
book/BBT.kind2
View File

@ -1,10 +1,15 @@
BBT
: ∀(K: *) // Key type
∀(V: *) // Value type
*
: ∀(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)))
∀(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)
(P self)

17
book/BBT.lft_rotate.kind2
View File

@ -1,6 +1,3 @@
// b = (left ~ right.left)
// a = (b ~ right.right)
// return a
BBT.lft_rotate
: ∀(K: *)
∀(V: *)
@ -11,13 +8,11 @@ BBT.lft_rotate
∀(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
let b = (BBT.new_node K V key val lft rgt.lft)
let a = (BBT.new_node K V rgt.key rgt.val b rgt.rgt)
let 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
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
let tip = λkey λval λlft
(BBT.bin K V size key val lft (BBT.tip K V))
((~rgt P bin tip) key val lft)
(~rgt P bin tip key val lft)

7
book/BBT.new_node.kind2
View File

@ -1,5 +1,4 @@
// Creates a new node with size = 1 + (max lft.size rgt.size)
BBT.new_node
BBT.new_node
: ∀(K: *)
∀(V: *)
∀(key: K)
@ -8,9 +7,9 @@
∀(rgt: (BBT K V))
(BBT K V)
= λK λV λkey λval λlft λrgt
let P = λx(BBT K V)
let P = λx (BBT K V)
let new = λlft.size λlft
let P = λx(BBT K V)
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)

17
book/BBT.rgt_rotate.kind2
View File

@ -1,6 +1,3 @@
// b = (left.right ~ right)
// a = (left.left ~ b)
// return a
BBT.rgt_rotate
: ∀(K: *)
∀(V: *)
@ -11,13 +8,11 @@ BBT.rgt_rotate
∀(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
let b = (BBT.new_node K V key val lft.rgt rgt)
let a = (BBT.new_node K V lft.key lft.val lft.lft b )
let 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
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
let tip = λkey λval λrgt
(BBT.bin K V size key val (BBT.tip K V) rgt)
((~lft P bin tip) key val rgt)
(~lft P bin tip key val rgt)

64
book/BBT.set.kind2
View File

@ -8,26 +8,54 @@ 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
let 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)
// Go left
let ltn = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
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))
∀(key: K)
∀(val: V)
(BBT K V)
let ltn = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
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
// Should we update the value or return the same tree?
(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 λkey λval
(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 λkey λval
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 key val)
// Empty tree, create new node
let tip = λkey λval
(BBT.singleton K V key val)
((~map P bin tip) key val)
(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
)
let tip = λkey λval (BBT.singleton K V key val)
(~map P bin tip key val)

8
book/BBT.singleton.kind2
View File

@ -1,8 +1,4 @@
BBT.singleton
: ∀(K: *)
∀(V: *)
∀(key: K)
∀(val: V)
(BBT K V)
: ∀(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))
(BBT.bin K V #1 key val (BBT.tip K V) (BBT.tip K V))

9
book/BBT.tip.kind2
View File

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

14
book/BBT.to_list.kind2
View File

@ -1,15 +1,17 @@
BBT.to_list
: ∀(K: *)
∀(V: *)
∀(map: (BBT K V))
: ∀(K: *) ∀(V: *) ∀(map: (BBT K V))
(List (Pair K V))
= λK λV λmap
let P = λx(List (Pair K V))
let P = λx (List (Pair K V))
let bin = λsize λkey λval λlft λrgt
let lft = (BBT.to_list K V lft)
let rgt = (BBT.to_list K V rgt)
let pair = (Pair.new K V key val)
let list = (List.cons (Pair K V) pair (List.concat (Pair K V) lft rgt))
let list = (List.cons
(Pair K V)
pair
(List.concat (Pair K V) lft rgt)
)
list
let tip = (List.nil (Pair K V))
(~map P bin tip)
(~map P bin tip)

10
book/Bool.and.kind2
View File

@ -1,9 +1,7 @@
Bool.and
: ∀(a: Bool)
∀(b: Bool)
Bool
: ∀(a: Bool) ∀(b: Bool) Bool
= λa
let P = λa ∀(b:Bool) Bool
let true = λb b
let P = λa ∀(b: Bool) Bool
let true = λb b
let false = λb Bool.false
(~a P true false)
(~a P true false)

2
book/Bool.false.kind2
View File

@ -1,3 +1,3 @@
Bool.false
: Bool
= ~λP λt λf f
= ~λP λt λf f

10
book/Bool.if.kind2
View File

@ -1,9 +1,3 @@
Bool.if
: ∀(b: Bool)
∀(P: *)
∀(t: P)
∀(f: P)
P
= λb λP λt λf
(~b λx(P) t f)
: ∀(b: Bool) ∀(P: *) ∀(t: P) ∀(f: P) P
= λb λP λt λf (~b λx P t f)

2
book/Bool.kind2
View File

@ -4,4 +4,4 @@ Bool
∀(P: ∀(x: Bool) *)
∀(t: (P Bool.true))
∀(f: (P Bool.false))
(P self)
(P self)

9
book/Bool.lemma.notnot.kind2
View File

@ -1,7 +1,8 @@
Bool.lemma.notnot
: ∀(b: Bool)
(Equal Bool (Bool.not (Bool.not b)) b)
: ∀(b: Bool) (Equal Bool (Bool.not (Bool.not b)) b)
= λb
(~b λx(Equal Bool (Bool.not (Bool.not x)) x)
(~b
λx (Equal Bool (Bool.not (Bool.not x)) x)
(Equal.refl Bool Bool.true)
(Equal.refl Bool Bool.false))
(Equal.refl Bool Bool.false)
)

3
book/Bool.match.kind2
View File

@ -4,5 +4,4 @@ Bool.match
∀(t: (P Bool.true))
∀(f: (P Bool.false))
(P b)
= λb λP λt λf
(~b P t f)
= λb λP λt λf (~b P t f)

6
book/Bool.not.kind2
View File

@ -1,7 +1,7 @@
Bool.not
: ∀(x: Bool) Bool
= λx
let P = λx(Bool)
let true = Bool.false
let P = λx Bool
let true = Bool.false
let false = Bool.true
(~x P true false)
(~x P true false)

10
book/Bool.or.kind2
View File

@ -1,9 +1,7 @@
Bool.or
: ∀(a: Bool)
∀(b: Bool)
Bool
: ∀(a: Bool) ∀(b: Bool) Bool
= λa
let P = λa ∀(b:Bool) Bool
let true = λb Bool.true
let P = λa ∀(b: Bool) Bool
let true = λb Bool.true
let false = λb b
(~a P true false)
(~a P true false)

9
book/Bool.show.kind2
View File

@ -1,8 +1,7 @@
Bool.show
: ∀(x: Bool)
String
: ∀(x: Bool) String
= λx
let P = λx(String)
let true = "true"
let P = λx String
let true = "true"
let false = "false"
(~x P true false)
(~x P true false)

2
book/Bool.true.kind2
View File

@ -1,3 +1,3 @@
Bool.true
: Bool
= ~λP λt λf t
= ~λP λt λf t

6
book/Char.equal.kind2
View File

@ -1,5 +1,3 @@
Char.equal
: ∀(a: Char)
∀(b: Char)
Bool
= U60.equal
: ∀(a: Char) ∀(b: Char) Bool
= U60.equal

54
book/Char.escapes.kind2
View File

@ -1,13 +1,43 @@
Char.escapes
Char.escapes
: (List (Pair Char Char))
= (List.cons (Pair Char Char) (Pair.new Char Char #98 #8) // '\b'
(List.cons (Pair Char Char) (Pair.new Char Char #102 #12) // '\f'
(List.cons (Pair Char Char) (Pair.new Char Char #110 #10) // '\n'
(List.cons (Pair Char Char) (Pair.new Char Char #114 #13) // '\r'
(List.cons (Pair Char Char) (Pair.new Char Char #116 #9) // '\t'
(List.cons (Pair Char Char) (Pair.new Char Char #118 #11) // '\v'
(List.cons (Pair Char Char) (Pair.new Char Char #92 #92) // '\\'
(List.cons (Pair Char Char) (Pair.new Char Char #34 #34) // '\"'
(List.cons (Pair Char Char) (Pair.new Char Char #48 #0) // '\0'
(List.cons (Pair Char Char) (Pair.new Char Char #39 #39) // '\''
(List.nil (Pair Char Char))))))))))))
= (List.cons
(Pair Char Char)
(Pair.new Char Char #98 #8)
(List.cons
(Pair Char Char)
(Pair.new Char Char #102 #12)
(List.cons
(Pair Char Char)
(Pair.new Char Char #110 #10)
(List.cons
(Pair Char Char)
(Pair.new Char Char #114 #13)
(List.cons
(Pair Char Char)
(Pair.new Char Char #116 #9)
(List.cons
(Pair Char Char)
(Pair.new Char Char #118 #11)
(List.cons
(Pair Char Char)
(Pair.new Char Char #92 #92)
(List.cons
(Pair Char Char)
(Pair.new Char Char #34 #34)
(List.cons
(Pair Char Char)
(Pair.new Char Char #48 #0)
(List.cons
(Pair Char Char)
(Pair.new Char Char #39 #39)
(List.nil (Pair Char Char))
)
)
)
)
)
)
)
)
)
)

9
book/Char.is_between.kind2
View File

@ -1,10 +1,7 @@
// Checks if a character is within a specified range, inclusive.
Char.is_between
: ∀(min: Char)
∀(max: Char)
∀(chr: Char)
Bool
: ∀(min: Char) ∀(max: Char) ∀(chr: Char) Bool
= λmin λmax λchr
(Bool.and
(U60.to_bool #(>= chr min))
(U60.to_bool #(<= chr max)))
(U60.to_bool #(<= chr max))
)

7
book/Char.is_blank.kind2
View File

@ -1,6 +1,3 @@
Char.is_blank
: ∀(a: Char)
Bool
= λa (Bool.or
(Char.equal a #10) // newline
(Char.equal a #32)) // space
: ∀(a: Char) Bool
= λa (Bool.or (Char.equal a #10) (Char.equal a #32))

6
book/Char.is_decimal.kind2
View File

@ -1,5 +1,3 @@
Char.is_decimal
: ∀(a: Char)
Bool
= λa
(Char.is_between '0' '9' a)
: ∀(a: Char) Bool
= λa (Char.is_between #48 #57 a)

28
book/Char.is_name.kind2
View File

@ -1,11 +1,19 @@
Char.is_name
: ∀(a: Char)
Bool
= λa
(Bool.or (Char.is_between 'a' 'z' a)
(Bool.or (Char.is_between 'A' 'Z' a)
(Bool.or (Char.is_between '0' '9' a)
(Bool.or (Char.equal '_' a)
(Bool.or (Char.equal '.' a)
(Bool.or (Char.equal '-' a)
Bool.false))))))
: ∀(a: Char) Bool
= λa
(Bool.or
(Char.is_between #97 #122 a)
(Bool.or
(Char.is_between #65 #90 a)
(Bool.or
(Char.is_between #48 #57 a)
(Bool.or
(Char.equal #95 a)
(Bool.or
(Char.equal #46 a)
(Bool.or (Char.equal #45 a) Bool.false)
)
)
)
)
)

5
book/Char.is_newline.kind2
View File

@ -1,4 +1,3 @@
Char.is_newline
: ∀(a: Char)
Bool
= λa (Char.equal a #10) // newline
: ∀(a: Char) Bool
= λa (Char.equal a #10)

56
book/Char.is_oper.kind2
View File

@ -1,18 +1,40 @@
Char.is_oper
: ∀(a: Char)
Bool
= λa
(Bool.or (Char.equal '+' a)
(Bool.or (Char.equal '-' a)
(Bool.or (Char.equal '*' a)
(Bool.or (Char.equal '/' a)
(Bool.or (Char.equal '%' a)
(Bool.or (Char.equal '<' a)
(Bool.or (Char.equal '>' a)
(Bool.or (Char.equal '=' a)
(Bool.or (Char.equal '&' a)
(Bool.or (Char.equal '|' a)
(Bool.or (Char.equal '^' a)
(Bool.or (Char.equal '!' a)
(Bool.or (Char.equal '~' a)
Bool.false)))))))))))))
: ∀(a: Char) Bool
= λa
(Bool.or
(Char.equal #43 a)
(Bool.or
(Char.equal #45 a)
(Bool.or
(Char.equal #42 a)
(Bool.or
(Char.equal #47 a)
(Bool.or
(Char.equal #37 a)
(Bool.or
(Char.equal #60 a)
(Bool.or
(Char.equal #62 a)
(Bool.or
(Char.equal #61 a)
(Bool.or
(Char.equal #38 a)
(Bool.or
(Char.equal #124 a)
(Bool.or
(Char.equal #94 a)
(Bool.or
(Char.equal #33 a)
(Bool.or (Char.equal #126 a) Bool.false)
)
)
)
)
)
)
)
)
)
)
)
)

6
book/Char.is_slash.kind2
View File

@ -1,5 +1,3 @@
Char.is_slash
: ∀(a: Char)
Bool
= λa (Char.equal a #47) // slash
: ∀(a: Char) Bool
= λa (Char.equal a #47)

2
book/Char.kind2
View File

@ -1,3 +1,3 @@
Char
: *
= #U60
= #U60

4
book/Char.slash.kind2
View File

@ -1,3 +1,3 @@
Char.slash
Char.slash
: Char
= #47
= #47

3
book/Cmp.eql.kind2
View File

@ -1,4 +1,3 @@
Cmp.eql
: Cmp
= ~λP λltn λeql λgtn
eql
= ~λP λltn λeql λgtn eql

3
book/Cmp.gtn.kind2
View File

@ -1,4 +1,3 @@
Cmp.gtn
: Cmp
= ~λP λltn λeql λgtn
gtn
= ~λP λltn λeql λgtn gtn

5
book/Cmp.is_gtn.kind2
View File

@ -1,8 +1,7 @@
Cmp.is_gtn
: ∀(cmp: Cmp)
Bool
: ∀(cmp: Cmp) Bool
= λcmp
let P = λx(Bool)
let P = λx Bool
let ltn = Bool.false
let eql = Bool.false
let gtn = Bool.true

2
book/Cmp.kind2
View File

@ -5,4 +5,4 @@ Cmp
∀(ltn: (P Cmp.ltn))
∀(eql: (P Cmp.eql))
∀(gtn: (P Cmp.gtn))
(P self)
(P self)

3
book/Cmp.ltn.kind2
View File

@ -1,4 +1,3 @@
Cmp.ltn
: Cmp
= ~λP λltn λeql λgtn
ltn
= ~λP λltn λeql λgtn ltn

6
book/Empty.absurd.kind2
View File

@ -1,5 +1,3 @@
Empty.absurd
: ∀(e: Empty)
∀(P: *)
P
= λe λP (~e λx(P))
: ∀(e: Empty) ∀(P: *) P
= λe λP (~e λx P)

4
book/Empty.kind2
View File

@ -1,5 +1,3 @@
Empty
: *
= $(self: Empty)
∀(P: ∀(x: Empty) *)
(P self)
= $(self: Empty) ∀(P: ∀(x: Empty) *) (P self)

2
book/Equal.apply.kind2
View File

@ -7,4 +7,4 @@ Equal.apply
∀(e: (Equal A a b))
(Equal B (f a) (f b))
= λA λB λf λa λb λe
(e λx(Equal B (f a) (f x)) λP λx x)
(e λx (Equal B (f a) (f x)) λP λx x)

10
book/Equal.kind2
View File

@ -1,9 +1,3 @@
Equal
: ∀(A: *)
∀(a: A)
∀(b: A)
*
= λA λa λb
∀(P: ∀(x: A) *)
∀(p: (P a))
(P b)
: ∀(A: *) ∀(a: A) ∀(b: A) *
= λA λa λb ∀(P: ∀(x: A) *) ∀(p: (P a)) (P b)

7
book/Equal.refl.kind2
View File

@ -1,6 +1,3 @@
Equal.refl
: ∀(A: *)
∀(a: A)
(Equal A a a)
= λA λa
λP λp p
: ∀(A: *) ∀(a: A) (Equal A a a)
= λA λa λP λp p

8
book/HVM.load.kind2
View File

@ -1,7 +1,3 @@
HVM.load
: ∀(A: *)
∀(file: String)
∀(cont: ∀(x: String) A)
A
= λA λfile λcont
(cont String.nil)
: ∀(A: *) ∀(file: String) ∀(cont: ∀(x: String) A) A
= λA λfile λcont (cont String.nil)

9
book/HVM.log.kind2
View File

@ -1,8 +1,3 @@
HVM.log
: ∀(A: *)
∀(B: *)
∀(msg: A)
∀(ret: B)
B
= λA λB λmsg λret
ret
: ∀(A: *) ∀(B: *) ∀(msg: A) ∀(ret: B) B
= λA λB λmsg λret ret

8
book/HVM.print.kind2
View File

@ -1,7 +1,3 @@
HVM.print
: ∀(A: *)
∀(msg: String)
∀(ret: A)
A
= λA λmsg λret
ret
: ∀(A: *) ∀(msg: String) ∀(ret: A) A
= λA λmsg λret ret

14
book/HVM.print.many.kind2
View File

@ -1,10 +1,8 @@
HVM.print.many
: ∀(A: *)
∀(msgs: (List String))
∀(ret: A)
A
: ∀(A: *) ∀(msgs: (List String)) ∀(ret: A) A
= λA λmsgs λret
let P = λx(A)
let cons = λmsg λmsgs (HVM.print A msg (HVM.print.many A msgs ret))
let nil = ret
(~msgs P cons nil)
let P = λx A
let cons = λmsg λmsgs
(HVM.print A msg (HVM.print.many A msgs ret))
let nil = ret
(~msgs P cons nil)

8
book/HVM.save.kind2
View File

@ -1,8 +1,4 @@
HVM.save
: ∀(A: *)
∀(file: String)
∀(data: String)
∀(cont: A)
: ∀(A: *) ∀(file: String) ∀(data: String) ∀(cont: A)
A
= λA λfile λdata λcont
cont
= λA λfile λdata λcont cont

21
book/IO.bind.kind2
View File

@ -5,10 +5,17 @@ IO.bind
∀(b: ∀(x: A) (IO B))
(IO B)
= λA λB λa λb
let P = λx ∀(b: ∀(x: A) (IO B)) (IO B)
let print = λtext λthen λb (IO.print B text λx(IO.bind A B (then x) b))
let load = λfile λthen λb (IO.load B file λs(IO.bind A B (then s) b))
let save = λfile λdata λthen λb (IO.save B file data λx(IO.bind A B (then Unit.one) b))
let done = λterm λb (b term)
((~a P print load save done) b)
let P = λx ∀(b: ∀(x: A) (IO B)) (IO B)
let print = λtext λthen λb
(IO.print B text λx (IO.bind A B (then x) b))
let load = λfile λthen λb
(IO.load B file λs (IO.bind A B (then s) b))
let save = λfile λdata λthen λb
(IO.save
B
file
data
λx (IO.bind A B (then Unit.one) b)
)
let done = λterm λb (b term)
(~a P print load save done b)

9
book/IO.done.kind2
View File

@ -1,8 +1,3 @@
IO.done
: ∀(A: *)
∀(term: A)
(IO A)
= λA λterm
~λP λprint λload λsave λdone
(done term)
: ∀(A: *) ∀(term: A) (IO A)
= λA λterm ~λP λprint λload λsave λdone (done term)

19
book/IO.kind2
View File

@ -3,8 +3,19 @@ IO
= λA
$(self: (IO A))
∀(P: ∀(x: (IO A)) *)
∀(print: ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO.print A text then)))
∀(load: ∀(file: String) ∀(then: ∀(x: String) (IO A)) (P (IO.load A file then)))
∀(save: ∀(file: String) ∀(data: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO.save A file data then)))
∀(print:
∀(text: String) ∀(then: ∀(x: Unit) (IO A))
(P (IO.print A text then))
)
∀(load:
∀(file: String) ∀(then: ∀(x: String) (IO A))
(P (IO.load A file then))
)
∀(save:
∀(file: String)
∀(data: String)
∀(then: ∀(x: Unit) (IO A))
(P (IO.save A file data then))
)
∀(done: ∀(term: A) (P (IO.done A term)))
(P self)
(P self)

8
book/IO.load.do.kind2
View File

@ -1,7 +1,3 @@
IO.load.do
: ∀(file: String)
(IO String)
= λfile
(IO.load String file λx
(IO.done String x))
: ∀(file: String) (IO String)
= λfile (IO.load String file λx (IO.done String x))

4
book/IO.load.kind2
View File

@ -4,6 +4,4 @@ IO.load
∀(then: ∀(x: String) (IO A))
(IO A)
= λA λfile λthen
~λP λprint λload λsave λdone
(load file then)
~λP λprint λload λsave λdone (load file then)

8
book/IO.print.do.kind2
View File

@ -1,7 +1,3 @@
IO.print.do
: ∀(text: String)
(IO Unit)
= λtext
(IO.print Unit text λx
(IO.done Unit x))
: ∀(text: String) (IO Unit)
= λtext (IO.print Unit text λx (IO.done Unit x))

8
book/IO.print.kind2
View File

@ -1,9 +1,5 @@
IO.print
: ∀(A: *)
∀(text: String)
∀(then: ∀(x: Unit) (IO A))
: ∀(A: *) ∀(text: String) ∀(then: ∀(x: Unit) (IO A))
(IO A)
= λA λtext λthen
~λP λprint λload λsave λdone
(print text then)
~λP λprint λload λsave λdone (print text then)

20
book/IO.run.kind2
View File

@ -1,12 +1,12 @@
IO.run
: ∀(A: *)
∀(x: (IO A))
(IO A)
: ∀(A: *) ∀(x: (IO A)) (IO A)
= λA λx
let P = λx(IO A)
let print = λtext λthen (HVM.print (IO A) text (IO.run A (then Unit.one)))
let load = λfile λthen (HVM.load (IO A) file λs(IO.run A (then s)))
let save = λfile λdata λthen (HVM.save (IO A) file data (IO.run A (then Unit.one)))
let done = λterm (IO.done A term)
(~x P print load save done)
let P = λx (IO A)
let print = λtext λthen
(HVM.print (IO A) text (IO.run A (then Unit.one)))
let load = λfile λthen
(HVM.load (IO A) file λs (IO.run A (then s)))
let save = λfile λdata λthen
(HVM.save (IO A) file data (IO.run A (then Unit.one)))
let done = λterm (IO.done A term)
(~x P print load save done)

8
book/IO.save.do.kind2
View File

@ -1,8 +1,4 @@
IO.save.do
: ∀(file: String)
∀(data: String)
(IO Unit)
: ∀(file: String) ∀(data: String) (IO Unit)
= λfile λdata
(IO.save Unit file data λx
(IO.done Unit x))
(IO.save Unit file data λx (IO.done Unit x))

4
book/IO.save.kind2
View File

@ -5,6 +5,4 @@ IO.save
∀(then: ∀(x: Unit) (IO A))
(IO A)
= λA λfile λdata λthen
~λP λprint λload λsave λdone
(save file data then)
~λP λprint λload λsave λdone (save file data then)

7
book/Kind.API.check.done.kind2 Normal file
View File

@ -0,0 +1,7 @@
Kind.API.check.done
: ∀(result: (Maybe Kind.Term)) (IO Unit)
= λresult
let P = λx (IO Unit)
let some = λvalue (IO.print.do "check")
let none = (IO.print.do "error")
(~result P some none)

32
book/Kind.API.check.kind2
View File

@ -1,17 +1,19 @@
Kind.API.check
: ∀(term: Kind.Term)
(IO Unit)
: ∀(term: Kind.Term) (IO Unit)
= λterm
(IO.run Unit
(Kind.if.ref term (IO Unit) λnam λval (Kind.API.check val) λterm
(Kind.if.ann term (IO Unit) λval λtyp (Kind.API.check.done (Kind.check val typ Nat.zero)) λterm
(Kind.API.check.done (Kind.infer term Nat.zero)))))
Kind.API.check.done
: ∀(result: (Maybe Kind.Term))
(IO Unit)
= λresult
let P = λx(IO Unit)
let some = λvalue (IO.print.do "check")
let none = (IO.print.do "error")
(~result P some none)
(IO.run
Unit
(Kind.if.ref
term
(IO Unit)
λnam λval (Kind.API.check val)
λterm
(Kind.if.ann
term
(IO Unit)
λval λtyp
(Kind.API.check.done (Kind.check val typ Nat.zero))
λterm (Kind.API.check.done (Kind.infer term Nat.zero))
)
)
)

25
book/Kind.API.get_refs.kind2
View File

@ -1,9 +1,20 @@
Kind.API.get_refs
: ∀(name: String)
(IO Unit)
: ∀(name: String) (IO Unit)
= λname
(IO.run Unit
(IO.bind Kind.Book Unit (Kind.load.code name) λbook
(IO.bind Unit Unit (IO.print.do (String.join String.newline (Kind.Book.get_refs book))) λx
(IO.done Unit Unit.one))))
(IO.run
Unit
(IO.bind
Kind.Book
Unit
(Kind.load.code name)
λbook
(IO.bind
Unit
Unit
(IO.print.do
(String.join String.newline (Kind.Book.get_refs book))
)
λx (IO.done Unit Unit.one)
)
)
)

34
book/Kind.API.normal.kind2
View File

@ -1,9 +1,29 @@
Kind.API.normal
: ∀(term: Kind.Term)
(IO Unit)
: ∀(term: Kind.Term) (IO Unit)
= λterm
(IO.run Unit
(Kind.if.ref term (IO Unit) λnam λval (Kind.API.normal val) λterm
(Kind.if.ann term (IO Unit) λval λtyp (Kind.API.normal val) λterm
(IO.bind Unit Unit (IO.print.do (Kind.Term.show (Kind.normal Bool.true term Nat.zero) Nat.zero)) λx
(IO.done Unit Unit.one)))))
(IO.run
Unit
(Kind.if.ref
term
(IO Unit)
λnam λval (Kind.API.normal val)
λterm
(Kind.if.ann
term
(IO Unit)
λval λtyp (Kind.API.normal val)
λterm
(IO.bind
Unit
Unit
(IO.print.do
(Kind.Term.show
(Kind.normal Bool.true term Nat.zero)
Nat.zero
)
)
λx (IO.done Unit Unit.one)
)
)
)
)

22
book/Kind.API.to_hvm.kind2
View File

@ -1,8 +1,18 @@
Kind.API.to_hvm
: ∀(name: String)
(IO Unit)
: ∀(name: String) (IO Unit)
= λname
(IO.run Unit
(IO.bind Kind.Book Unit (Kind.load.code name) λbook
(IO.bind Unit Unit (IO.print.do (Kind.Book.to_hvm book)) λx
(IO.done Unit Unit.one))))
(IO.run
Unit
(IO.bind
Kind.Book
Unit
(Kind.load.code name)
λbook
(IO.bind
Unit
Unit
(IO.print.do (Kind.Book.to_hvm book))
λx (IO.done Unit Unit.one)
)
)
)

6
book/Kind.Binder.new.kind2
View File

@ -1,5 +1,3 @@
Kind.Binder.new
: ∀(nam: String) ∀(typ: Kind.Term)
Kind.Binder
= λnam λtyp
(Pair.new String Kind.Term nam typ)
: ∀(nam: String) ∀(typ: Kind.Term) Kind.Binder
= λnam λtyp (Pair.new String Kind.Term nam typ)

2
book/Kind.Book.String.cons.kind2
View File

@ -1,3 +1,3 @@
Kind.Book.String.cons
: Kind.Term
= (Kind.hol "TODO" (List.nil Kind.Term))
= (Kind.hol "TODO" (List.nil Kind.Term))

15
book/Kind.Book.get_refs.go.kind2
View File

@ -2,13 +2,14 @@ Kind.Book.get_refs.go
: ∀(book: (List (Pair String Kind.Term)))
(List.Concatenator String)
= λbook
let P = λx (List.Concatenator String)
let P = λx (List.Concatenator String)
let cons = λhead λtail
let P = λx (List.Concatenator String)
let P = λx (List.Concatenator String)
let new = λhead.fst λhead.snd λnil
((Kind.Term.get_refs.go head.snd)
((Kind.Book.get_refs.go tail)
nil))
(Kind.Term.get_refs.go
head.snd
(Kind.Book.get_refs.go tail nil)
)
(~head P new)
let nil = λnil nil
(~book P cons nil)
let nil = λnil nil
(~book P cons nil)

12
book/Kind.Book.get_refs.kind2
View File

@ -1,7 +1,9 @@
Kind.Book.get_refs
: ∀(book: Kind.Book)
(List String)
: ∀(book: Kind.Book) (List String)
= λbook
(List.Concatenator.build String
(Kind.Book.get_refs.go
(String.Map.to_list Kind.Term book)))
(List.Concatenator.build
String
(Kind.Book.get_refs.go
(String.Map.to_list Kind.Term book)
)
)

2
book/Kind.Book.kind2
View File

@ -1,3 +1,3 @@
Kind.Book
: *
= (String.Map Kind.Term)
= (String.Map Kind.Term)

7
book/Kind.Book.parse.kind2
View File

@ -1,8 +1,7 @@
Kind.Book.parse
: ∀(code: String)
Kind.Book
: ∀(code: String) Kind.Book
= λcode
let P = λx(Kind.Book)
let P = λx Kind.Book
let done = λcode λbook book
let fail = λerror (String.Map.new Kind.Term)
(~(Kind.Book.parser code) P done fail)
(~(Kind.Book.parser code) P done fail)

118
book/Kind.Book.parser.kind2
View File

@ -1,28 +1,94 @@
Kind.Book.parser
: (Parser Kind.Book)
= (Parser.bind Bool Kind.Book Parser.is_eof λis_eof
let P = λx(Parser Kind.Book)
// If EOF, return an empty book
let true =
(Parser.pure Kind.Book (String.Map.new Kind.Term))
// Otherwise, parse a definition
let false =
(Parser.bind String Kind.Book Parser.name λnam
(Parser.bind Bool Kind.Book (Parser.skip Bool (Parser.test ":")) λann
let P = λx(Parser Kind.Book)
// If annotated, parses the annotation
let true =
(Parser.bind Unit Kind.Book (Parser.text ":") λ_
(Parser.bind Kind.PreTerm Kind.Book Kind.Term.parser λtyp
(Parser.bind Unit Kind.Book (Parser.text "=") λ_
(Parser.bind Kind.PreTerm Kind.Book Kind.Term.parser λval
(Parser.bind Kind.Book Kind.Book Kind.Book.parser λbook
(Parser.pure Kind.Book (String.Map.set Kind.Term nam (Kind.ann (val (List.nil Kind.Binder)) (typ (List.nil Kind.Binder))) book)))))))
// Otherwise, parses just the value
let false =
(Parser.bind Unit Kind.Book (Parser.text "=") λ_
(Parser.bind Kind.PreTerm Kind.Book Kind.Term.parser λval
(Parser.bind Kind.Book Kind.Book Kind.Book.parser λbook
(Parser.pure Kind.Book (String.Map.set Kind.Term nam (val (List.nil Kind.Binder)) book)))))
(~ann P true false)))
(~is_eof P true false))
= (Parser.bind
Bool
Kind.Book
Parser.is_eof
λis_eof
let P = λx (Parser Kind.Book)
let true = (Parser.pure Kind.Book (String.Map.new Kind.Term))
let false = (Parser.bind
String
Kind.Book
Parser.name
λnam
(Parser.bind
Bool
Kind.Book
(Parser.skip Bool (Parser.test ":"))
λann
let P = λx (Parser Kind.Book)
let true = (Parser.bind
Unit
Kind.Book
(Parser.text ":")
λ_
(Parser.bind
Kind.PreTerm
Kind.Book
Kind.Term.parser
λtyp
(Parser.bind
Unit
Kind.Book
(Parser.text "=")
λ_
(Parser.bind
Kind.PreTerm
Kind.Book
Kind.Term.parser
λval
(Parser.bind
Kind.Book
Kind.Book
Kind.Book.parser
λbook
(Parser.pure
Kind.Book
(String.Map.set
Kind.Term
nam
(Kind.ann
(val (List.nil Kind.Binder))
(typ (List.nil Kind.Binder))
)
book
)
)
)
)
)
)
)
let false = (Parser.bind
Unit
Kind.Book
(Parser.text "=")
λ_
(Parser.bind
Kind.PreTerm
Kind.Book
Kind.Term.parser
λval
(Parser.bind
Kind.Book
Kind.Book
Kind.Book.parser
λbook
(Parser.pure
Kind.Book
(String.Map.set
Kind.Term
nam
(val (List.nil Kind.Binder))
book
)
)
)
)
)
(~ann P true false)
)
)
(~is_eof P true false)
)

28
book/Kind.Book.show.go.kind2
View File

@ -2,16 +2,24 @@ Kind.Book.show.go
: ∀(book: (List (Pair String Kind.Term)))
String.Concatenator
= λbook
let P = λx String.Concatenator
let P = λx String.Concatenator
let cons = λhead λtail
let P = λx String.Concatenator
let P = λx String.Concatenator
let new = λhead.fst λhead.snd λnil
((Kind.Text.show.go head.fst)
((Kind.Text.show.go " = "
((Kind.Term.show.go head.snd Nat.zero
((Kind.Text.show.go String.newline
((Kind.Book.show.go tail
nil)))))))))
(Kind.Text.show.go
head.fst
(Kind.Text.show.go
" = "
(Kind.Term.show.go
head.snd
Nat.zero
(Kind.Text.show.go
String.newline
(Kind.Book.show.go tail nil)
)
)
)
)
(~head P new)
let nil = λnil nil
(~book P cons nil)
let nil = λnil nil
(~book P cons nil)

7
book/Kind.Book.show.kind2
View File

@ -1,5 +1,6 @@
Kind.Book.show
: ∀(book: Kind.Book)
String
: ∀(book: Kind.Book) String
= λbook
(String.Concatenator.build (Kind.Book.show.go (String.Map.to_list Kind.Term book)))
(String.Concatenator.build
(Kind.Book.show.go (String.Map.to_list Kind.Term book))
)

18
book/Kind.Book.to_hvm.go.kind2
View File

@ -1,18 +0,0 @@
Kind.Book.to_hvm.go
: ∀(book: (List (Pair String Kind.Term)))
String.Concatenator
= λbook
let P = λx String.Concatenator
let cons = λhead λtail
let P = λx String.Concatenator
let new = λhead.fst λhead.snd λnil
((Kind.Text.show.go "F.")
((Kind.Text.show.go head.fst)
((Kind.Text.show.go " = ")
((Kind.Term.to_hvm.go head.snd Nat.zero Bool.true Nat.zero)
((Kind.Text.show.go String.newline)
((Kind.Book.to_hvm.go tail)
nil))))))
(~head P new)
let nil = λnil nil
(~book P cons nil)

7
book/Kind.Book.to_hvm.kind2
View File

@ -1,7 +0,0 @@
Kind.Book.to_hvm
: ∀(book: Kind.Book)
String
= λbook
(String.Concatenator.build
(Kind.Book.to_hvm.go
(String.Map.to_list Kind.Term book)))

18
book/Kind.Book.to_hvm.quoted.go.kind2
View File

@ -1,18 +0,0 @@
Kind.Book.to_hvm.quoted.go
: ∀(book: (List (Pair String Kind.Term)))
String.Concatenator
= λbook
let P = λx String.Concatenator
let cons = λhead λtail
let P = λx String.Concatenator
let new = λhead.fst λhead.snd λnil
((Kind.Text.show.go "Book.")
((Kind.Text.show.go head.fst)
((Kind.Text.show.go " = ")
((Kind.Term.to_hvm.quoted.go head.snd Nat.zero)
((Kind.Text.show.go String.newline)
((Kind.Book.to_hvm.quoted.go tail)
nil))))))
(~head P new)
let nil = λnil nil
(~book P cons nil)

7
book/Kind.Book.to_hvm.quoted.kind2
View File

@ -1,7 +0,0 @@
Kind.Book.to_hvm.quoted
: ∀(book: Kind.Book)
String
= λbook
(String.Concatenator.build
(Kind.Book.to_hvm.quoted.go
(String.Map.to_list Kind.Term book)))

2
book/Kind.Oper.add.kind2
View File

@ -1,4 +1,4 @@
Kind.Oper.add
: Kind.Oper
= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
(add)
add

2
book/Kind.Oper.and.kind2
View File

@ -1,4 +1,4 @@
Kind.Oper.and
: Kind.Oper
= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
(and)
and

2
book/Kind.Oper.div.kind2
View File

@ -1,4 +1,4 @@
Kind.Oper.div
: Kind.Oper
= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
(div)
div

2
book/Kind.Oper.eq.kind2
View File

@ -1,4 +1,4 @@
Kind.Oper.eq
: Kind.Oper
= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
(eq)
eq

2
book/Kind.Oper.gt.kind2
View File

@ -1,4 +1,4 @@
Kind.Oper.gt
: Kind.Oper
= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
(gt)
gt

2
book/Kind.Oper.gte.kind2
View File

@ -1,4 +1,4 @@
Kind.Oper.gte
: Kind.Oper
= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
(gte)
gte

12
book/Kind.Oper.kind2
View File

@ -7,15 +7,15 @@ Kind.Oper
∀(sub: (P Kind.Oper.sub))
∀(div: (P Kind.Oper.div))
∀(mod: (P Kind.Oper.mod))
∀(eq: (P Kind.Oper.eq))
∀(ne: (P Kind.Oper.ne))
∀(lt: (P Kind.Oper.lt))
∀(gt: (P Kind.Oper.gt))
∀(eq: (P Kind.Oper.eq))
∀(ne: (P Kind.Oper.ne))
∀(lt: (P Kind.Oper.lt))
∀(gt: (P Kind.Oper.gt))
∀(lte: (P Kind.Oper.lte))
∀(gte: (P Kind.Oper.gte))
∀(and: (P Kind.Oper.and))
∀(or: (P Kind.Oper.or))
∀(or: (P Kind.Oper.or))
∀(xor: (P Kind.Oper.xor))
∀(lsh: (P Kind.Oper.lsh))
∀(rsh: (P Kind.Oper.rsh))
(P self)
(P self)

2
book/Kind.Oper.lsh.kind2
View File

@ -1,4 +1,4 @@
Kind.Oper.lsh
: Kind.Oper
= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
(lsh)
lsh

2
book/Kind.Oper.lt.kind2
View File

@ -1,4 +1,4 @@
Kind.Oper.lt
: Kind.Oper
= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
(lt)
lt

2
book/Kind.Oper.lte.kind2
View File

@ -1,4 +1,4 @@
Kind.Oper.lte
: Kind.Oper
= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
(lte)
lte

2
book/Kind.Oper.mod.kind2
View File

@ -1,4 +1,4 @@
Kind.Oper.mod
: Kind.Oper
= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
(mod)
mod

2
book/Kind.Oper.mul.kind2
View File

@ -1,4 +1,4 @@
Kind.Oper.mul
: Kind.Oper
= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
(mul)
mul

2
book/Kind.Oper.ne.kind2
View File

@ -1,4 +1,4 @@
Kind.Oper.ne
: Kind.Oper
= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
(ne)
ne

2
book/Kind.Oper.or.kind2
View File

@ -1,4 +1,4 @@
Kind.Oper.or
: Kind.Oper
= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
(or)
or

86
book/Kind.Oper.parser.kind2
View File

@ -2,27 +2,65 @@ Kind.Oper.parser
: (Parser Kind.Oper)
= let TRY = (List.cons (Parser.Guard Kind.Oper))
let END = (List.nil (Parser.Guard Kind.Oper))
let OP2 =
{ λsym λoper
(Parser.Guard.text Kind.Oper sym
(Parser.bind Unit Kind.Oper (Parser.text sym) λx
(Parser.pure Kind.Oper oper)))
: ∀(sym: String) ∀(oper: Kind.Oper) (Parser.Guard Kind.Oper)}
(Parser.variant Kind.Oper
(TRY (OP2 "+" Kind.Oper.add)
(TRY (OP2 "*" Kind.Oper.mul)
(TRY (OP2 "-" Kind.Oper.sub)
(TRY (OP2 "/" Kind.Oper.div)
(TRY (OP2 "%" Kind.Oper.mod)
(TRY (OP2 "==" Kind.Oper.eq)
(TRY (OP2 "!=" Kind.Oper.ne)
(TRY (OP2 "<=" Kind.Oper.lte)
(TRY (OP2 ">=" Kind.Oper.gte)
(TRY (OP2 "<<" Kind.Oper.lsh)
(TRY (OP2 ">>" Kind.Oper.rsh)
(TRY (OP2 "<" Kind.Oper.lt)
(TRY (OP2 ">" Kind.Oper.gt)
(TRY (OP2 "&" Kind.Oper.and)
(TRY (OP2 "|" Kind.Oper.or)
(TRY (OP2 "^" Kind.Oper.xor)
END)))))))))))))))))
let OP2 = {λsym λoper
(Parser.Guard.text
Kind.Oper
sym
(Parser.bind
Unit
Kind.Oper
(Parser.text sym)
λx (Parser.pure Kind.Oper oper)
)
)
:∀(sym: String) ∀(oper: Kind.Oper)
(Parser.Guard Kind.Oper)}
(Parser.variant
Kind.Oper
(TRY
(OP2 "+" Kind.Oper.add)
(TRY
(OP2 "*" Kind.Oper.mul)
(TRY
(OP2 "-" Kind.Oper.sub)
(TRY
(OP2 "/" Kind.Oper.div)
(TRY
(OP2 "%" Kind.Oper.mod)
(TRY
(OP2 "==" Kind.Oper.eq)
(TRY
(OP2 "!=" Kind.Oper.ne)
(TRY
(OP2 "<=" Kind.Oper.lte)
(TRY
(OP2 ">=" Kind.Oper.gte)
(TRY
(OP2 "<<" Kind.Oper.lsh)
(TRY
(OP2 ">>" Kind.Oper.rsh)
(TRY
(OP2 "<" Kind.Oper.lt)
(TRY
(OP2 ">" Kind.Oper.gt)
(TRY
(OP2 "&" Kind.Oper.and)
(TRY
(OP2 "|" Kind.Oper.or)
(TRY (OP2 "^" Kind.Oper.xor) END)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)

2
book/Kind.Oper.rsh.kind2
View File

@ -1,4 +1,4 @@
Kind.Oper.rsh
: Kind.Oper
= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
(rsh)
rsh

Some files were not shown because too many files have changed in this diff Show More