mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-08-17 11:40:22 +03:00
wip
This commit is contained in:
commit
ab98950f50
100
book/BBT.balance.kind2
Normal file
100
book/BBT.balance.kind2
Normal file
@ -0,0 +1,100 @@
|
||||
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
|
||||
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)
|
14
book/BBT.bin.kind2
Normal file
14
book/BBT.bin.kind2
Normal file
@ -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)
|
||||
|
||||
|
14
book/BBT.from_list.kind2
Normal file
14
book/BBT.from_list.kind2
Normal file
@ -0,0 +1,14 @@
|
||||
BBT.from_list
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
∀(list: (List (Pair K V)))
|
||||
(BBT K V)
|
||||
= λK λV λcmp λlist
|
||||
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))
|
||||
(~head P new)
|
||||
let nil = (BBT.tip K V)
|
||||
(~list P cons nil)
|
17
book/BBT.get.kind2
Normal file
17
book/BBT.get.kind2
Normal file
@ -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 ∀(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)
|
32
book/BBT.got.kind2
Normal file
32
book/BBT.got.kind2
Normal file
@ -0,0 +1,32 @@
|
||||
// Returns a pair with the value and the new map
|
||||
BBT.got
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
∀(key: K)
|
||||
∀(map: (BBT K V))
|
||||
(Pair (Maybe V) (BBT K V))
|
||||
= λK λV λcmp λkey λmap
|
||||
let P = λx(Pair (Maybe V) (BBT K V))
|
||||
let bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
|
||||
let P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) (Pair (Maybe V) (BBT K V))
|
||||
let ltn = λcmp λkey
|
||||
let new_pair = (BBT.got K V cmp key next.lft)
|
||||
let P = λx(Pair (Maybe V) (BBT K V))
|
||||
let new = λval λlft
|
||||
let map = (BBT.bin K V size next.key next.val lft next.rgt)
|
||||
(Pair.new (Maybe V) (BBT K V) val map)
|
||||
(~new_pair P new)
|
||||
let eql = λcmp λkey
|
||||
let map = (BBT.bin K V size next.key next.val next.lft next.rgt)
|
||||
(Pair.new (Maybe V) (BBT K V) (Maybe.some V next.val) map)
|
||||
let gtn = λcmp λkey
|
||||
let new_pair = (BBT.got K V cmp key next.rgt)
|
||||
let P = λx(Pair (Maybe V) (BBT K V))
|
||||
let new = λval λrgt
|
||||
let map = (BBT.bin K V size next.key next.val next.lft rgt)
|
||||
(Pair.new (Maybe V) (BBT K V) val map)
|
||||
(~new_pair P new)
|
||||
((~(cmp key next.key) P ltn eql gtn) cmp key)
|
||||
let tip = (Pair.new (Maybe V) (BBT K V) (Maybe.none V) (BBT.tip K V))
|
||||
(~map P bin tip)
|
13
book/BBT.got_size.kind2
Normal file
13
book/BBT.got_size.kind2
Normal file
@ -0,0 +1,13 @@
|
||||
// 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)
|
17
book/BBT.has.kind2
Normal file
17
book/BBT.has.kind2
Normal file
@ -0,0 +1,17 @@
|
||||
BBT.has
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(cmp: ∀(a: K) ∀(b: K) Cmp)
|
||||
∀(key: K)
|
||||
∀(map: (BBT K V))
|
||||
Bool
|
||||
= λK λV λcmp λkey λmap
|
||||
let P = λx Bool
|
||||
let bin = λnext.size λnext.key λnext.val λnext.lft λnext.rgt
|
||||
let P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) Bool
|
||||
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)
|
||||
let tip = Bool.false
|
||||
(~map P bin tip)
|
32
book/BBT.has.linear.kind2
Normal file
32
book/BBT.has.linear.kind2
Normal file
@ -0,0 +1,32 @@
|
||||
// Returns a Pair with the boolean (indicating if the key is present) and the original map
|
||||
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 λkey λmap
|
||||
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 ltn = λcmp λsize λhas_key λval λlft λrgt λhas_key
|
||||
let P = λx (Pair Bool (BBT K V))
|
||||
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))
|
||||
|
||||
let gtn = λcmp λsize λkey λval λlft λrgt λhas_key
|
||||
let P = λx (Pair Bool (BBT K V))
|
||||
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)
|
||||
|
||||
let tip = (Pair.new Bool (BBT K V) Bool.false (BBT.tip K V))
|
||||
(~map P bin tip)
|
10
book/BBT.kind2
Normal file
10
book/BBT.kind2
Normal file
@ -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)
|
23
book/BBT.lft_rotate.kind2
Normal file
23
book/BBT.lft_rotate.kind2
Normal file
@ -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
|
||||
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
|
||||
(BBT.bin K V size key val lft (BBT.tip K V))
|
||||
((~rgt P bin tip) key val lft)
|
18
book/BBT.new_node.kind2
Normal file
18
book/BBT.new_node.kind2
Normal file
@ -0,0 +1,18 @@
|
||||
// Creates a new node with size = 1 + (max lft.size rgt.size)
|
||||
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)
|
23
book/BBT.rgt_rotate.kind2
Normal file
23
book/BBT.rgt_rotate.kind2
Normal file
@ -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
|
||||
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
|
||||
(BBT.bin K V size key val (BBT.tip K V) rgt)
|
||||
((~lft P bin tip) key val rgt)
|
34
book/BBT.set.kind2
Normal file
34
book/BBT.set.kind2
Normal file
@ -0,0 +1,34 @@
|
||||
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
|
||||
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
|
||||
// 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)
|
||||
|
||||
// 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)
|
||||
|
||||
// Empty tree, create new node
|
||||
let tip = λkey λval
|
||||
(BBT.singleton K V key val)
|
||||
((~map P bin tip) key val)
|
||||
|
8
book/BBT.singleton.kind2
Normal file
8
book/BBT.singleton.kind2
Normal file
@ -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))
|
8
book/BBT.tip.kind2
Normal file
8
book/BBT.tip.kind2
Normal file
@ -0,0 +1,8 @@
|
||||
BBT.tip
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
(BBT K V)
|
||||
= λK λV
|
||||
~λP λbin λtip
|
||||
tip
|
||||
|
15
book/BBT.to_list.kind2
Normal file
15
book/BBT.to_list.kind2
Normal file
@ -0,0 +1,15 @@
|
||||
BBT.to_list
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
∀(map: (BBT K V))
|
||||
(List (Pair K V))
|
||||
= λK λV λmap
|
||||
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))
|
||||
list
|
||||
let tip = (List.nil (Pair K V))
|
||||
(~map P bin tip)
|
8
book/Bool.show.kind2
Normal file
8
book/Bool.show.kind2
Normal file
@ -0,0 +1,8 @@
|
||||
Bool.show
|
||||
: ∀(x: Bool)
|
||||
String
|
||||
= λx
|
||||
let P = λx(String)
|
||||
let true = "true"
|
||||
let false = "false"
|
||||
(~x P true false)
|
4
book/Cmp.eql.kind2
Normal file
4
book/Cmp.eql.kind2
Normal file
@ -0,0 +1,4 @@
|
||||
Cmp.eql
|
||||
: Cmp
|
||||
= ~λP λltn λeql λgtn
|
||||
eql
|
4
book/Cmp.gtn.kind2
Normal file
4
book/Cmp.gtn.kind2
Normal file
@ -0,0 +1,4 @@
|
||||
Cmp.gtn
|
||||
: Cmp
|
||||
= ~λP λltn λeql λgtn
|
||||
gtn
|
9
book/Cmp.is_gtn.kind2
Normal file
9
book/Cmp.is_gtn.kind2
Normal file
@ -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)
|
8
book/Cmp.kind2
Normal file
8
book/Cmp.kind2
Normal file
@ -0,0 +1,8 @@
|
||||
Cmp
|
||||
: *
|
||||
= $self
|
||||
∀(P: ∀(cmp: Cmp) *)
|
||||
∀(ltn: (P Cmp.ltn))
|
||||
∀(eql: (P Cmp.eql))
|
||||
∀(gtn: (P Cmp.gtn))
|
||||
(P self)
|
4
book/Cmp.ltn.kind2
Normal file
4
book/Cmp.ltn.kind2
Normal file
@ -0,0 +1,4 @@
|
||||
Cmp.ltn
|
||||
: Cmp
|
||||
= ~λP λltn λeql λgtn
|
||||
ltn
|
@ -1,5 +0,0 @@
|
||||
Kind.API.file
|
||||
: ∀(name: String)
|
||||
String
|
||||
= λname
|
||||
(String.concat name ".kind2")
|
@ -1,6 +0,0 @@
|
||||
// TODO
|
||||
Kind.API.load
|
||||
: ∀(name: String)
|
||||
Kind.Book
|
||||
= λname
|
||||
(Kind.API.load.one name)
|
@ -1,6 +0,0 @@
|
||||
Kind.API.load.one
|
||||
: ∀(name: String)
|
||||
Kind.Book
|
||||
= λname
|
||||
(HVM.load Kind.Book (Kind.API.file name) λdata
|
||||
(Kind.Book.parse data))
|
@ -1,3 +1,3 @@
|
||||
Kind.Book.String.cons
|
||||
: Kind.Term
|
||||
= (Kind.hol "TODO" (List.nil Kind.Term))
|
||||
= (Kind.hol "TODO" (List.nil Kind.Term))
|
||||
|
@ -1,5 +1,5 @@
|
||||
Kind.Book.get_refs.go
|
||||
: ∀(book: Kind.Book)
|
||||
: ∀(book: (List (Pair String Kind.Term)))
|
||||
(List.Concatenator String)
|
||||
= λbook
|
||||
let P = λx (List.Concatenator String)
|
||||
|
@ -2,4 +2,6 @@ Kind.Book.get_refs
|
||||
: ∀(book: Kind.Book)
|
||||
(List String)
|
||||
= λbook
|
||||
(List.Concatenator.build String (Kind.Book.get_refs.go book))
|
||||
(List.Concatenator.build String
|
||||
(Kind.Book.get_refs.go
|
||||
(String.Map.to_list Kind.Term book)))
|
||||
|
@ -1,3 +1,3 @@
|
||||
Kind.Book
|
||||
: *
|
||||
= (String.Map Kind.Term)
|
||||
= (String.Map Kind.Term)
|
||||
|
@ -4,5 +4,5 @@ Kind.Book.parse
|
||||
= λcode
|
||||
let P = λx(Kind.Book)
|
||||
let done = λcode λbook book
|
||||
let fail = λerror (List.nil (Pair String Kind.Term))
|
||||
let fail = λerror (String.Map.new Kind.Term)
|
||||
(~(Kind.Book.parser code) P done fail)
|
||||
|
@ -25,4 +25,4 @@ Kind.Book.parser
|
||||
(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))
|
||||
(~is_eof P true false))
|
||||
|
@ -1,5 +1,5 @@
|
||||
Kind.Book.show.go
|
||||
: ∀(book: Kind.Book)
|
||||
: ∀(book: (List (Pair String Kind.Term)))
|
||||
String.Concatenator
|
||||
= λbook
|
||||
let P = λx String.Concatenator
|
||||
@ -14,4 +14,4 @@ Kind.Book.show.go
|
||||
nil)))))))))
|
||||
(~head P new)
|
||||
let nil = λnil nil
|
||||
(~book P cons nil)
|
||||
(~book P cons nil)
|
||||
|
@ -2,4 +2,4 @@ Kind.Book.show
|
||||
: ∀(book: Kind.Book)
|
||||
String
|
||||
= λbook
|
||||
(String.Concatenator.build (Kind.Book.show.go book))
|
||||
(String.Concatenator.build (Kind.Book.show.go (String.Map.to_list Kind.Term book)))
|
||||
|
@ -1,5 +1,5 @@
|
||||
Kind.Book.to_hvm.go
|
||||
: ∀(book: Kind.Book)
|
||||
: ∀(book: (List (Pair String Kind.Term)))
|
||||
String.Concatenator
|
||||
= λbook
|
||||
let P = λx String.Concatenator
|
||||
|
@ -2,4 +2,6 @@ Kind.Book.to_hvm
|
||||
: ∀(book: Kind.Book)
|
||||
String
|
||||
= λbook
|
||||
(String.Concatenator.build (Kind.Book.to_hvm.go book))
|
||||
(String.Concatenator.build
|
||||
(Kind.Book.to_hvm.go
|
||||
(String.Map.to_list Kind.Term book)))
|
||||
|
118
book/Kind.load.kind2
Normal file
118
book/Kind.load.kind2
Normal file
@ -0,0 +1,118 @@
|
||||
|
||||
//// TODO
|
||||
//Kind.load
|
||||
//: ∀(name: String)
|
||||
//Kind.Book
|
||||
//= λname
|
||||
//(Kind.load.name #5 name (String.Map.new Kind.Term))
|
||||
|
||||
//// Gets the source file of a definition
|
||||
//Kind.load.file_of
|
||||
//: ∀(name: String)
|
||||
//String
|
||||
//= λname
|
||||
//(String.concat name ".kind2")
|
||||
|
||||
//// Loads a file into a new book
|
||||
//Kind.load.file
|
||||
//: ∀(file: String)
|
||||
//Kind.Book
|
||||
//= λfile
|
||||
//(HVM.load Kind.Book file λdata
|
||||
//(Kind.Book.parse data))
|
||||
|
||||
//// Loads a name into a book
|
||||
//Kind.load.name
|
||||
//: ∀(lims: #U60)
|
||||
//∀(name: String)
|
||||
//∀(book: Kind.Book)
|
||||
//Kind.Book
|
||||
//= λlims
|
||||
//(HVM.log #U60 ∀(name:String)∀(book:Kind.Book)Kind.Book lims
|
||||
//#match lims = lims {
|
||||
//#0: λname λbook book
|
||||
//#+: λname λbook
|
||||
//(HVM.print Kind.Book (String.concat "LOAD:" name)
|
||||
//// Checks if name is already on book
|
||||
//let P = λx (Kind.Book)
|
||||
//let new = λhas λbook
|
||||
//// If it is, do nothing; otherwise, define it
|
||||
//let P = λx ∀(book: Kind.Book) (Kind.Book)
|
||||
//let true = λbook
|
||||
//(HVM.print Kind.Book (String.concat (String.concat "OLD!:" name) (String.concat " -- " (Kind.keys book))) book)
|
||||
//let false = λbook
|
||||
//(HVM.print Kind.Book (String.concat (String.concat "NEW!:" name) (String.concat " -- " (Kind.keys book)))
|
||||
//let file = (Kind.load.file (Kind.load.file_of name))
|
||||
//let defs = (String.Map.to_list Kind.Term file)
|
||||
//let bok1 = (Kind.load.define defs book)
|
||||
//let file = (Kind.load.file (Kind.load.file_of name))
|
||||
//let refs = (Kind.Book.get_refs file)
|
||||
//let bok2 = (HVM.print ?a (String.concat "REC!:" (Kind.keys bok1)) (Kind.load.name.many lims-1 refs bok1))
|
||||
//bok2)
|
||||
////(HVM.print.many Kind.Book refs book)
|
||||
|
||||
//((~has P true false) book)
|
||||
//(~(String.Map.has.linear Kind.Term name book) P new))
|
||||
//}: ∀(name: String) ∀(book: Kind.Book) Kind.Book)
|
||||
|
||||
//// Loads many names into a book
|
||||
//Kind.load.name.many
|
||||
//: ∀(lims: #U60)
|
||||
//∀(list: (List String))
|
||||
//∀(book: Kind.Book)
|
||||
//Kind.Book
|
||||
//= λlims λlist λbook
|
||||
//let P = λx ∀(book: Kind.Book) (Kind.Book)
|
||||
//let cons = λhead λtail λbook
|
||||
////(HVM.print Kind.Book
|
||||
////(String.concat "DEP:"
|
||||
////(String.concat head
|
||||
////(String.concat " BOOK:"
|
||||
////(Kind.Book.show book))))
|
||||
//let bok2 = (Kind.load.name lims head book)
|
||||
//(Kind.load.name.many lims tail bok2)
|
||||
//let nil = λbook book
|
||||
//((~list P cons nil) book)
|
||||
|
||||
//// Defines a term and loads its dependencies
|
||||
////Kind.load.define
|
||||
////: ∀(name: String)
|
||||
////∀(term: Kind.Term)
|
||||
////∀(book: Kind.Book)
|
||||
////Kind.Book
|
||||
////= λname λterm λbook
|
||||
////let book = (String.Map.set Kind.Term name term book)
|
||||
////let refs = (Kind.Term.get_refs term)
|
||||
////let book = (Kind.load.name.many refs book)
|
||||
////book
|
||||
|
||||
//// Defines many terms
|
||||
//Kind.load.define
|
||||
//: ∀(defs: (List (Pair String Kind.Term)))
|
||||
//∀(book: Kind.Book)
|
||||
//Kind.Book
|
||||
//= λdefs λbook
|
||||
//// If defs list isn't empty...
|
||||
//let P = λx ∀(book: Kind.Book) (Kind.Book)
|
||||
//let cons = λdefs.head λdefs.tail λbook
|
||||
//// Gets the def name/term
|
||||
//let P = λx (Kind.Book)
|
||||
//let new = λname λterm
|
||||
//// Writes it to the book
|
||||
//let bok2 = (String.Map.set Kind.Term name term book)
|
||||
//(HVM.print Kind.Book (String.concat "DEF!:" name)
|
||||
//// Recurses
|
||||
//(Kind.load.define defs.tail bok2))
|
||||
//(~defs.head P new)
|
||||
//// If defs list is empty, return the book
|
||||
//let nil = λbook book
|
||||
//((~defs P cons nil) book)
|
||||
|
||||
|
||||
//Kind.keys
|
||||
//: ∀(book: Kind.Book)
|
||||
//String
|
||||
//= λbook
|
||||
//let defs = (String.Map.to_list Kind.Term book)
|
||||
//let defs = (List.app (Pair String Kind.Term) String (Pair.fst String Kind.Term) defs)
|
||||
//(String.join defs)
|
11
book/List.app.kind2
Normal file
11
book/List.app.kind2
Normal file
@ -0,0 +1,11 @@
|
||||
List.app
|
||||
: ∀(A: *)
|
||||
∀(B: *)
|
||||
∀(f: ∀(x: A) B)
|
||||
∀(x: (List A))
|
||||
(List B)
|
||||
= λA λB λf λx
|
||||
let P = λx(List B)
|
||||
let cons = λh λt (List.cons B (f h) (List.app A B f t))
|
||||
let nil = (List.nil B)
|
||||
(~x P cons nil)
|
@ -1,8 +1,45 @@
|
||||
Main
|
||||
: Kind.Book
|
||||
=
|
||||
let book = (Kind.API.load "Bool.and")
|
||||
book
|
||||
//Main
|
||||
//: Unit
|
||||
//= let map = (String.Map.new Unit)
|
||||
//let map = (String.Map.set Unit "Bool" Unit.one map)
|
||||
//let map = (String.Map.set Unit "Bool.true" Unit.one map)
|
||||
//let has = (String.Map.has Unit "Bool.false" map)
|
||||
//(HVM.print Unit (Bool.show has)
|
||||
//Unit.one)
|
||||
|
||||
//Main
|
||||
//: Unit
|
||||
//= let book = (Kind.load "Bool")
|
||||
//(HVM.print Unit (Kind.Book.show book)
|
||||
//Unit.one)
|
||||
|
||||
//Main = Kind.load.name
|
||||
|
||||
//Main = Kind.load.go.defs
|
||||
|
||||
//Main
|
||||
//: Unit
|
||||
//=
|
||||
////= (HVM.print Unit (Kind.Book.to_hvm (Kind.API.load "Bool.and"))
|
||||
//Unit.one
|
||||
//)
|
||||
|
||||
//Main
|
||||
//: (Maybe #U60)
|
||||
//= let map = (String.Map.new #U60)
|
||||
//let map = (String.Map.set #U60 "foo" #1 map)
|
||||
//let map = (String.Map.set #U60 "bar" #2 map)
|
||||
//let map = (String.Map.set #U60 "tic" #3 map)
|
||||
//let map = (String.Map.set #U60 "tac" #4 map)
|
||||
//let val = (String.Map.get #U60 "bar" map)
|
||||
//val
|
||||
|
||||
//Main
|
||||
//: Kind.Book
|
||||
//=
|
||||
//let book = (Kind.API.load "Bool.and")
|
||||
//book
|
||||
|
||||
//let code = (Kind.Book.to_hvm book)
|
||||
//let refs = (Kind.Book.get_refs book)
|
||||
//(HVM.print Unit code
|
||||
|
9
book/Pair.fst.kind2
Normal file
9
book/Pair.fst.kind2
Normal file
@ -0,0 +1,9 @@
|
||||
Pair.fst
|
||||
: ∀(A: *)
|
||||
∀(B: *)
|
||||
∀(p: (Pair A B))
|
||||
A
|
||||
= λA λB λp
|
||||
let P = λx(A)
|
||||
let new = λa λb a
|
||||
(~p P new)
|
9
book/Pair.snd.kind2
Normal file
9
book/Pair.snd.kind2
Normal file
@ -0,0 +1,9 @@
|
||||
Pair.snd
|
||||
: ∀(A: *)
|
||||
∀(B: *)
|
||||
∀(p: (Pair A B))
|
||||
B
|
||||
= λA λB λp
|
||||
let P = λx(B)
|
||||
let new = λa λb b
|
||||
(~p P new)
|
6
book/String.Map.from_list.kind2
Normal file
6
book/String.Map.from_list.kind2
Normal file
@ -0,0 +1,6 @@
|
||||
String.Map.from_list
|
||||
: ∀(V: *)
|
||||
∀(list: (List (Pair String V)))
|
||||
(String.Map V)
|
||||
= λV λlist
|
||||
(BBT.from_list String V String.cmp list)
|
7
book/String.Map.has.kind2
Normal file
7
book/String.Map.has.kind2
Normal file
@ -0,0 +1,7 @@
|
||||
String.Map.has
|
||||
: ∀(V: *)
|
||||
∀(key: String)
|
||||
∀(map: (BBT String V))
|
||||
Bool
|
||||
= λV λkey λmap
|
||||
(BBT.has String V String.cmp key map)
|
7
book/String.Map.has.linear.kind2
Normal file
7
book/String.Map.has.linear.kind2
Normal file
@ -0,0 +1,7 @@
|
||||
String.Map.has.linear
|
||||
: ∀(V: *)
|
||||
∀(key: String)
|
||||
∀(map: (BBT String V))
|
||||
(Pair Bool (BBT String V))
|
||||
= λV λkey λmap
|
||||
(BBT.has.linear String V String.cmp key map)
|
35
book/String.Map.kind2
Normal file
35
book/String.Map.kind2
Normal file
@ -0,0 +1,35 @@
|
||||
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)
|
||||
|
6
book/String.Map.to_list.kind2
Normal file
6
book/String.Map.to_list.kind2
Normal file
@ -0,0 +1,6 @@
|
||||
String.Map.to_list
|
||||
: ∀(V: *)
|
||||
∀(map: (String.Map V))
|
||||
(List (Pair String V))
|
||||
= λV λmap
|
||||
(BBT.to_list String V map)
|
22
book/String.cmp.kind2
Normal file
22
book/String.cmp.kind2
Normal file
@ -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)
|
8
book/String.join.kind2
Normal file
8
book/String.join.kind2
Normal file
@ -0,0 +1,8 @@
|
||||
String.join
|
||||
: ∀(strs: (List String))
|
||||
String
|
||||
= λstrs
|
||||
let P = λx(String)
|
||||
let cons = λhλt(String.concat h (String.join t))
|
||||
let nil = String.nil
|
||||
(~strs P cons nil)
|
34
book/U60.Map.kind2
Normal file
34
book/U60.Map.kind2
Normal file
@ -0,0 +1,34 @@
|
||||
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)
|
10
book/U60.abs_diff.kind2
Normal file
10
book/U60.abs_diff.kind2
Normal file
@ -0,0 +1,10 @@
|
||||
// Returns the absolute difference between two U60s
|
||||
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)
|
7
book/U60.cmp.kind2
Normal file
7
book/U60.cmp.kind2
Normal file
@ -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)
|
||||
|
6
book/U60.max.kind2
Normal file
6
book/U60.max.kind2
Normal file
@ -0,0 +1,6 @@
|
||||
U60.max
|
||||
: ∀(a: #U60)
|
||||
∀(b: #U60)
|
||||
#U60
|
||||
= λa λb
|
||||
(~(U60.to_bool #(> a b)) λx(#U60) a b)
|
6
book/U60.min.kind2
Normal file
6
book/U60.min.kind2
Normal file
@ -0,0 +1,6 @@
|
||||
U60.min
|
||||
: ∀(a: #U60)
|
||||
∀(b: #U60)
|
||||
#U60
|
||||
= λa λb
|
||||
(~(U60.to_bool #(< a b)) λx(#U60) a b)
|
@ -1,4 +1,180 @@
|
||||
_compile : String = (Kind.Book.to_hvm (Kind.Book.parse `test9
|
||||
_compile : String = (Kind.Book.to_hvm (Kind.Book.parse `// Add_spaces
|
||||
// : ∀(n: #U60)
|
||||
// (String)
|
||||
// = λn
|
||||
// (U60.if #(== n #0) String (String.concat " " (Add_spaces #(- n #1))) "")
|
||||
|
||||
// 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)
|
||||
|
||||
// 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))
|
||||
|
||||
// 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.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
|
||||
// : (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)
|
||||
|
||||
// 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)
|
||||
|
||||
// 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)
|
||||
|
||||
|
||||
// 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!")
|
||||
|
||||
// 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
|
||||
: String
|
||||
= (String.unpar '(' ')' "((foo))")
|
||||
=
|
||||
"
|
||||
File commented for backward compatibility.
|
||||
To run the tests, uncomment the code on:
|
||||
testBBT.kind2
|
||||
U60.Map
|
||||
"
|
||||
// RunTests
|
||||
`))
|
@ -2,4 +2,3 @@ test6
|
||||
: Nat
|
||||
= (Nat.succ (Nat.succ (Nat.succ Nat.zero)))
|
||||
|
||||
|
||||
|
179
book/testBBT.kind2
Normal file
179
book/testBBT.kind2
Normal file
@ -0,0 +1,179 @@
|
||||
// Add_spaces
|
||||
// : ∀(n: #U60)
|
||||
// (String)
|
||||
// = λn
|
||||
// (U60.if #(== n #0) String (String.concat " " (Add_spaces #(- n #1))) "")
|
||||
|
||||
// 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)
|
||||
|
||||
// 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))
|
||||
|
||||
// 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.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
|
||||
// : (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)
|
||||
|
||||
// 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)
|
||||
|
||||
// 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)
|
||||
|
||||
|
||||
// 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!")
|
||||
|
||||
// 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
|
||||
: String
|
||||
=
|
||||
"
|
||||
File commented for backward compatibility.
|
||||
To run the tests, uncomment the code on:
|
||||
testBBT.kind2
|
||||
U60.Map
|
||||
"
|
||||
// RunTests
|
388
bootstrap.hvm1
388
bootstrap.hvm1
@ -7,12 +7,203 @@
|
||||
(Str.view str) = (str 0 λhλt(String.cons h (Str.view t)) String.nil)
|
||||
(Strs.view strs) = (List.view λx(Str.view x) strs)
|
||||
(List.view elem list) = (list 0 λhλt(List.cons (elem h) (List.view elem t)) List.nil)
|
||||
|
||||
Book.A.one = λ_P λ_new (_new 0)
|
||||
`
|
||||
Book.A.match = λ_a λ_P λ_t ((_a _P) λ_tag (U60.match _tag _t λ_tag_1(λ_x (_x λ_x 0))))
|
||||
Book.A = 0
|
||||
Book.A.bad = λ_P λ_new ((_new 1) 0)
|
||||
Book.A.sel = λ_P λ_k (U60.match _k (_P (Book.A.one)) λ_tag_1(0))
|
||||
Book.A = 0
|
||||
Book.A.match = λ_a λ_P λ_t ((_a _P) λ_tag (U60.match _tag _t λ_tag_1(λ_x (_x λ_x 0))))
|
||||
Book.A.one = λ_P λ_new (_new 0)
|
||||
|
||||
Book.BBT.balance.lft_heavier = λ_K λ_V λ_cmp λ_new_size λ_node_key λ_set_key λ_val λ_lft λ_rgt
|
||||
let _P = λ_x (((Book.BBT) _K) _V)
|
||||
let _bin = λ_lft.size λ_lft.key λ_lft.val λ_lft.lft λ_lft.rgt
|
||||
let _P = λ_x 0
|
||||
let _true = λ_new_size λ_key λ_val λ_lft.key λ_lft.val λ_lft.lft λ_lft.rgt λ_rgt
|
||||
let _lft = ((((((((Book.BBT.lft_rotate) _K) _V) _lft.size) _lft.key) _lft.val) _lft.lft) _lft.rgt)
|
||||
((((((((Book.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 = ((((((((Book.BBT.bin) _K) _V) _lft.size) _lft.key) _lft.val) _lft.lft) _lft.rgt)
|
||||
((((((((Book.BBT.rgt_rotate) _K) _V) _new_size) _key) _val) _lft) _rgt)
|
||||
(((((((((((((Book.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 = (((Book.BBT.tip) _K) _V)
|
||||
(((_lft _P) _bin) _tip)
|
||||
Book.BBT.balance = λ_K λ_V λ_cmp λ_set_key λ_node_key λ_val λ_lft λ_rgt
|
||||
let _P = λ_x (((Book.BBT) _K) _V)
|
||||
let _new = λ_lft.size λ_lft
|
||||
let _P = λ_x (((Book.BBT) _K) _V)
|
||||
let _new = λ_rgt.size λ_rgt
|
||||
let _new_size = (+ 1 (((Book.U60.max) _lft.size) _rgt.size))
|
||||
let _balance = (((Book.U60.abs_diff) _lft.size) _rgt.size)
|
||||
let _P = λ_x 0
|
||||
let _true = λ_new_size λ_node_key λ_val λ_lft λ_rgt
|
||||
let _P = λ_x 0
|
||||
let _true = (Book.BBT.balance.lft_heavier)
|
||||
let _false = (Book.BBT.balance_rgt_heavier)
|
||||
((((((((((((((Book.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 ((((((((Book.BBT.bin) _K) _V) _new_size) _node_key) _val) _lft) _rgt)
|
||||
((((((((((Book.U60.to_bool) (> _balance 1)) _P) _true) _false) _new_size) _node_key) _val) _lft) _rgt)
|
||||
((((((Book.BBT.got_size) _K) _V) _rgt) _P) _new)
|
||||
((((((Book.BBT.got_size) _K) _V) _lft) _P) _new)
|
||||
Book.BBT.balance_rgt_heavier = λ_K λ_V λ_cmp λ_new_size λ_node_key λ_set_key λ_val λ_lft λ_rgt
|
||||
let _P = λ_x (((Book.BBT) _K) _V)
|
||||
let _bin = λ_rgt.size λ_rgt.key λ_rgt.val λ_rgt.lft λ_rgt.rgt
|
||||
let _P = λ_x 0
|
||||
let _true = λ_new_size λ_key λ_val λ_lft λ_rgt.key λ_rgt.val λ_rgt.lft λ_rgt.rgt
|
||||
let _rgt = ((((((((Book.BBT.bin) _K) _V) _rgt.size) _rgt.key) _rgt.val) _rgt.lft) _rgt.rgt)
|
||||
((((((((Book.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 = ((((((((Book.BBT.rgt_rotate) _K) _V) _rgt.size) _rgt.key) _rgt.val) _rgt.lft) _rgt.rgt)
|
||||
((((((((Book.BBT.lft_rotate) _K) _V) _new_size) _key) _val) _lft) _rgt)
|
||||
(((((((((((((Book.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 = (((Book.BBT.tip) _K) _V)
|
||||
(((_rgt _P) _bin) _tip)
|
||||
|
||||
Book.BBT.bin = λ_K λ_V λ_size λ_key λ_val λ_lft λ_rgt λ_P λ_bin λ_tip (((((_bin _size) _key) _val) _lft) _rgt)
|
||||
|
||||
Book.BBT.from_list = λ_K λ_V λ_cmp λ_list
|
||||
let _P = λ_x (((Book.BBT) _K) _V)
|
||||
let _cons = λ_head λ_tail
|
||||
let _P = λ_x (((Book.BBT) _K) _V)
|
||||
let _new = λ_key λ_val (((((((Book.BBT.set) _K) _V) _cmp) _key) _val) (((((Book.BBT.from_list) _K) _V) _cmp) _tail))
|
||||
((_head _P) _new)
|
||||
let _nil = (((Book.BBT.tip) _K) _V)
|
||||
(((_list _P) _cons) _nil)
|
||||
|
||||
Book.BBT.get = λ_K λ_V λ_cmp λ_key λ_map
|
||||
let _P = λ_x ((Book.Maybe) _V)
|
||||
let _bin = λ__size λ_next.key λ_next.val λ_next.lft λ_next.rgt
|
||||
let _P = λ_x 0
|
||||
let _ltn = λ_cmp λ_key ((((((Book.BBT.get) _K) _V) _cmp) _key) _next.lft)
|
||||
let _eql = λ_cmp λ_key (((Book.Maybe.some) _V) _next.val)
|
||||
let _gtn = λ_cmp λ_key ((((((Book.BBT.get) _K) _V) _cmp) _key) _next.rgt)
|
||||
((((((((_cmp _key) _next.key) _P) _ltn) _eql) _gtn) _cmp) _key)
|
||||
let _tip = ((Book.Maybe.none) _V)
|
||||
(((_map _P) _bin) _tip)
|
||||
|
||||
Book.BBT.got = λ_K λ_V λ_cmp λ_key λ_map
|
||||
let _P = λ_x (((Book.Pair) ((Book.Maybe) _V)) (((Book.BBT) _K) _V))
|
||||
let _bin = λ_size λ_next.key λ_next.val λ_next.lft λ_next.rgt
|
||||
let _P = λ_x 0
|
||||
let _ltn = λ_cmp λ_key
|
||||
let _new_pair = ((((((Book.BBT.got) _K) _V) _cmp) _key) _next.lft)
|
||||
let _P = λ_x (((Book.Pair) ((Book.Maybe) _V)) (((Book.BBT) _K) _V))
|
||||
let _new = λ_val λ_lft
|
||||
let _map = ((((((((Book.BBT.bin) _K) _V) _size) _next.key) _next.val) _lft) _next.rgt)
|
||||
(((((Book.Pair.new) ((Book.Maybe) _V)) (((Book.BBT) _K) _V)) _val) _map)
|
||||
((_new_pair _P) _new)
|
||||
let _eql = λ_cmp λ_key
|
||||
let _map = ((((((((Book.BBT.bin) _K) _V) _size) _next.key) _next.val) _next.lft) _next.rgt)
|
||||
(((((Book.Pair.new) ((Book.Maybe) _V)) (((Book.BBT) _K) _V)) (((Book.Maybe.some) _V) _next.val)) _map)
|
||||
let _gtn = λ_cmp λ_key
|
||||
let _new_pair = ((((((Book.BBT.got) _K) _V) _cmp) _key) _next.rgt)
|
||||
let _P = λ_x (((Book.Pair) ((Book.Maybe) _V)) (((Book.BBT) _K) _V))
|
||||
let _new = λ_val λ_rgt
|
||||
let _map = ((((((((Book.BBT.bin) _K) _V) _size) _next.key) _next.val) _next.lft) _rgt)
|
||||
(((((Book.Pair.new) ((Book.Maybe) _V)) (((Book.BBT) _K) _V)) _val) _map)
|
||||
((_new_pair _P) _new)
|
||||
((((((((_cmp _key) _next.key) _P) _ltn) _eql) _gtn) _cmp) _key)
|
||||
let _tip = (((((Book.Pair.new) ((Book.Maybe) _V)) (((Book.BBT) _K) _V)) ((Book.Maybe.none) _V)) (((Book.BBT.tip) _K) _V))
|
||||
(((_map _P) _bin) _tip)
|
||||
|
||||
Book.BBT.got_size = λ_K λ_V λ_map
|
||||
let _P = λ_x (((Book.Pair) 0) (((Book.BBT) _K) _V))
|
||||
let _bin = λ_size λ_next.key λ_next.val λ_next.lft λ_next.rgt
|
||||
let _map = ((((((((Book.BBT.bin) _K) _V) _size) _next.key) _next.val) _next.lft) _next.rgt)
|
||||
(((((Book.Pair.new) 0) (((Book.BBT) _K) _V)) _size) _map)
|
||||
let _tip = (((((Book.Pair.new) 0) (((Book.BBT) _K) _V)) 0) (((Book.BBT.tip) _K) _V))
|
||||
(((_map _P) _bin) _tip)
|
||||
|
||||
Book.BBT.has = λ_K λ_V λ_cmp λ_key λ_map
|
||||
let _P = λ_x (Book.Bool)
|
||||
let _bin = λ_next.size λ_next.key λ_next.val λ_next.lft λ_next.rgt
|
||||
let _P = λ_x 0
|
||||
let _ltn = λ_cmp λ_key ((((((Book.BBT.has) _K) _V) _cmp) _key) _next.lft)
|
||||
let _eql = λ_cmp λ_key (Book.Bool.true)
|
||||
let _gtn = λ_cmp λ_key ((((((Book.BBT.has) _K) _V) _cmp) _key) _next.rgt)
|
||||
((((((((_cmp _key) _next.key) _P) _ltn) _eql) _gtn) _cmp) _key)
|
||||
let _tip = (Book.Bool.false)
|
||||
(((_map _P) _bin) _tip)
|
||||
|
||||
Book.BBT.has.linear = λ_K λ_V λ_cmp λ_key λ_map
|
||||
let _P = λ_x (((Book.Pair) (Book.Bool)) (((Book.BBT) _K) _V))
|
||||
let _bin = λ_size λ_node_key λ_val λ_lft λ_rgt
|
||||
let _P = λ_x 0
|
||||
let _ltn = λ_cmp λ_size λ_has_key λ_val λ_lft λ_rgt λ_has_key
|
||||
let _P = λ_x (((Book.Pair) (Book.Bool)) (((Book.BBT) _K) _V))
|
||||
let _new = λ_bool λ_lft
|
||||
let _map = ((((((((Book.BBT.bin) _K) _V) _size) _node_key) _val) _lft) _rgt)
|
||||
(((((Book.Pair.new) (Book.Bool)) (((Book.BBT) _K) _V)) _bool) _map)
|
||||
((((((((Book.BBT.has.linear) _K) _V) _cmp) _has_key) _lft) _P) _new)
|
||||
let _eql = λ_cmp λ_size λ_key λ_val λ_lft λ_rgt λ_has_key (((((Book.Pair.new) (Book.Bool)) (((Book.BBT) _K) _V)) (Book.Bool.true)) ((((((((Book.BBT.bin) _K) _V) _size) _node_key) _val) _lft) _rgt))
|
||||
let _gtn = λ_cmp λ_size λ_key λ_val λ_lft λ_rgt λ_has_key
|
||||
let _P = λ_x (((Book.Pair) (Book.Bool)) (((Book.BBT) _K) _V))
|
||||
let _new = λ_bool λ_rgt
|
||||
let _map = ((((((((Book.BBT.bin) _K) _V) _size) _node_key) _val) _lft) _rgt)
|
||||
(((((Book.Pair.new) (Book.Bool)) (((Book.BBT) _K) _V)) _bool) _rgt)
|
||||
((((((((Book.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)
|
||||
let _tip = (((((Book.Pair.new) (Book.Bool)) (((Book.BBT) _K) _V)) (Book.Bool.false)) (((Book.BBT.tip) _K) _V))
|
||||
(((_map _P) _bin) _tip)
|
||||
|
||||
Book.BBT = λ_K λ_V 0
|
||||
|
||||
Book.BBT.lft_rotate = λ_K λ_V λ_size λ_key λ_val λ_lft λ_rgt
|
||||
let _P = λ_x 0
|
||||
let _bin = λ__size λ_rgt.key λ_rgt.val λ_rgt.lft λ_rgt.rgt λ_key λ_val λ_lft
|
||||
let _b = (((((((Book.BBT.new_node) _K) _V) _key) _val) _lft) _rgt.lft)
|
||||
let _a = (((((((Book.BBT.new_node) _K) _V) _rgt.key) _rgt.val) _b) _rgt.rgt)
|
||||
_a
|
||||
let _tip = λ_key λ_val λ_lft ((((((((Book.BBT.bin) _K) _V) _size) _key) _val) _lft) (((Book.BBT.tip) _K) _V))
|
||||
((((((_rgt _P) _bin) _tip) _key) _val) _lft)
|
||||
|
||||
Book.BBT.new_node = λ_K λ_V λ_key λ_val λ_lft λ_rgt
|
||||
let _P = λ_x (((Book.BBT) _K) _V)
|
||||
let _new = λ_lft.size λ_lft
|
||||
let _P = λ_x (((Book.BBT) _K) _V)
|
||||
let _new = λ_rgt.size λ_rgt
|
||||
let _new_size = (+ 1 (((Book.U60.max) _rgt.size) _lft.size))
|
||||
((((((((Book.BBT.bin) _K) _V) _new_size) _key) _val) _lft) _rgt)
|
||||
((((((Book.BBT.got_size) _K) _V) _rgt) _P) _new)
|
||||
((((((Book.BBT.got_size) _K) _V) _lft) _P) _new)
|
||||
|
||||
Book.BBT.rgt_rotate = λ_K λ_V λ_size λ_key λ_val λ_lft λ_rgt
|
||||
let _P = λ_x 0
|
||||
let _bin = λ__size λ_lft.key λ_lft.val λ_lft.lft λ_lft.rgt λ_key λ_val λ_rgt
|
||||
let _b = (((((((Book.BBT.new_node) _K) _V) _key) _val) _lft.rgt) _rgt)
|
||||
let _a = (((((((Book.BBT.new_node) _K) _V) _lft.key) _lft.val) _lft.lft) _b)
|
||||
_a
|
||||
let _tip = λ_key λ_val λ_rgt ((((((((Book.BBT.bin) _K) _V) _size) _key) _val) (((Book.BBT.tip) _K) _V)) _rgt)
|
||||
((((((_lft _P) _bin) _tip) _key) _val) _rgt)
|
||||
|
||||
Book.BBT.set = λ_K λ_V λ_cmp λ_key λ_val λ_map
|
||||
let _P = λ_x 0
|
||||
let _bin = λ_size λ_next.key λ_next.val λ_next.lft λ_next.rgt λ_key λ_val
|
||||
let _P = λ_x 0
|
||||
let _ltn = λ_key λ_next.key λ_next.val λ_next.lft λ_next.rgt
|
||||
let _new_lft = (((((((Book.BBT.set) _K) _V) _cmp) _key) _val) _next.lft)
|
||||
(((((((((Book.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 ((((((((Book.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 = (((((((Book.BBT.set) _K) _V) _cmp) _key) _val) _next.rgt)
|
||||
(((((((((Book.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 (((((Book.BBT.singleton) _K) _V) _key) _val)
|
||||
(((((_map _P) _bin) _tip) _key) _val)
|
||||
|
||||
Book.BBT.singleton = λ_K λ_V λ_key λ_val ((((((((Book.BBT.bin) _K) _V) 1) _key) _val) (((Book.BBT.tip) _K) _V)) (((Book.BBT.tip) _K) _V))
|
||||
|
||||
Book.BBT.tip = λ_K λ_V λ_P λ_bin λ_tip _tip
|
||||
|
||||
Book.BBT.to_list = λ_K λ_V λ_map
|
||||
let _P = λ_x ((Book.List) (((Book.Pair) _K) _V))
|
||||
let _bin = λ_size λ_key λ_val λ_lft λ_rgt
|
||||
let _lft = ((((Book.BBT.to_list) _K) _V) _lft)
|
||||
let _rgt = ((((Book.BBT.to_list) _K) _V) _rgt)
|
||||
let _pair = (((((Book.Pair.new) _K) _V) _key) _val)
|
||||
let _list = ((((Book.List.cons) (((Book.Pair) _K) _V)) _pair) ((((Book.List.concat) (((Book.Pair) _K) _V)) _lft) _rgt))
|
||||
_list
|
||||
let _tip = ((Book.List.nil) (((Book.Pair) _K) _V))
|
||||
(((_map _P) _bin) _tip)
|
||||
|
||||
Book.Bool.and = λ_a
|
||||
let _P = λ_a 0
|
||||
@ -42,6 +233,12 @@ Book.Bool.or = λ_a
|
||||
let _false = λ_b _b
|
||||
(((_a _P) _true) _false)
|
||||
|
||||
Book.Bool.show = λ_x
|
||||
let _P = λ_x (Book.String)
|
||||
let _true = (Str "true")
|
||||
let _false = (Str "false")
|
||||
(((_x _P) _true) _false)
|
||||
|
||||
Book.Bool.true = λ_P λ_t λ_f _t
|
||||
|
||||
Book.Char.equal = (Book.U60.equal)
|
||||
@ -66,6 +263,21 @@ Book.Char = 0
|
||||
|
||||
Book.Char.slash = 92
|
||||
|
||||
Book.Cmp.eql = λ_P λ_ltn λ_eql λ_gtn _eql
|
||||
|
||||
Book.Cmp.gtn = λ_P λ_ltn λ_eql λ_gtn _gtn
|
||||
|
||||
Book.Cmp.is_gtn = λ_cmp
|
||||
let _P = λ_x (Book.Bool)
|
||||
let _ltn = (Book.Bool.false)
|
||||
let _eql = (Book.Bool.false)
|
||||
let _gtn = (Book.Bool.true)
|
||||
((((_cmp _P) _ltn) _eql) _gtn)
|
||||
|
||||
Book.Cmp = 0
|
||||
|
||||
Book.Cmp.ltn = λ_P λ_ltn λ_eql λ_gtn _ltn
|
||||
|
||||
Book.Empty.absurd = λ_e λ_P (_e λ_x _P)
|
||||
|
||||
Book.Empty = 0
|
||||
@ -76,6 +288,20 @@ Book.Equal = λ_A λ_a λ_b 0
|
||||
|
||||
Book.Equal.refl = λ_A λ_a λ_P λ_p _p
|
||||
|
||||
Book.HVM.load = λ_A λ_file λ_cont (_cont (Book.String.nil))
|
||||
|
||||
Book.HVM.log = λ_A λ_B λ_msg λ_ret _ret
|
||||
|
||||
Book.HVM.print = λ_A λ_msg λ_ret _ret
|
||||
|
||||
Book.HVM.print.many = λ_A λ_msgs λ_ret
|
||||
let _P = λ_x _A
|
||||
let _cons = λ_msg λ_msgs ((((Book.HVM.print) _A) _msg) ((((Book.HVM.print.many) _A) _msgs) _ret))
|
||||
let _nil = _ret
|
||||
(((_msgs _P) _cons) _nil)
|
||||
|
||||
Book.HVM.save = λ_A λ_file λ_data λ_cont _cont
|
||||
|
||||
Book.Kind.Binder = (((Book.Pair) (Book.String)) (Book.Kind.Term))
|
||||
|
||||
Book.Kind.Binder.new = λ_nam λ_typ (((((Book.Pair.new) (Book.String)) (Book.Kind.Term)) _nam) _typ)
|
||||
@ -95,14 +321,14 @@ Book.Kind.Book.get_refs.go = λ_book
|
||||
let _nil = λ_nil _nil
|
||||
(((_book _P) _cons) _nil)
|
||||
|
||||
Book.Kind.Book.get_refs = λ_book (((Book.List.Concatenator.build) (Book.String)) ((Book.Kind.Book.get_refs.go) _book))
|
||||
Book.Kind.Book.get_refs = λ_book (((Book.List.Concatenator.build) (Book.String)) ((Book.Kind.Book.get_refs.go) (((Book.String.Map.to_list) (Book.Kind.Term)) _book)))
|
||||
|
||||
Book.Kind.Book = ((Book.String.Map) (Book.Kind.Term))
|
||||
|
||||
Book.Kind.Book.parse = λ_code
|
||||
let _P = λ_x (Book.Kind.Book)
|
||||
let _done = λ_code λ_book _book
|
||||
let _fail = λ_error ((Book.List.nil) (((Book.Pair) (Book.String)) (Book.Kind.Term)))
|
||||
let _fail = λ_error ((Book.String.Map.new) (Book.Kind.Term))
|
||||
(((((Book.Kind.Book.parser) _code) _P) _done) _fail)
|
||||
|
||||
Book.Kind.Book.parser = (((((Book.Parser.bind) (Book.Bool)) (Book.Kind.Book)) (Book.Parser.is_eof)) λ_is_eof
|
||||
@ -124,7 +350,7 @@ Book.Kind.Book.show.go = λ_book
|
||||
let _nil = λ_nil _nil
|
||||
(((_book _P) _cons) _nil)
|
||||
|
||||
Book.Kind.Book.show = λ_book ((Book.String.Concatenator.build) ((Book.Kind.Book.show.go) _book))
|
||||
Book.Kind.Book.show = λ_book ((Book.String.Concatenator.build) ((Book.Kind.Book.show.go) (((Book.String.Map.to_list) (Book.Kind.Term)) _book)))
|
||||
|
||||
Book.Kind.Book.to_hvm.go = λ_book
|
||||
let _P = λ_x (Book.String.Concatenator)
|
||||
@ -135,7 +361,7 @@ Book.Kind.Book.to_hvm.go = λ_book
|
||||
let _nil = λ_nil _nil
|
||||
(((_book _P) _cons) _nil)
|
||||
|
||||
Book.Kind.Book.to_hvm = λ_book ((Book.String.Concatenator.build) ((Book.Kind.Book.to_hvm.go) _book))
|
||||
Book.Kind.Book.to_hvm = λ_book ((Book.String.Concatenator.build) ((Book.Kind.Book.to_hvm.go) (((Book.String.Map.to_list) (Book.Kind.Term)) _book)))
|
||||
|
||||
Book.Kind.Oper.add = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _add
|
||||
|
||||
@ -485,6 +711,7 @@ Book.Kind.equal.minor = λ_e λ_a λ_b λ_dep
|
||||
(((((Book.Kind.equal.major) ((((Book.Kind.identical) _a_wnf) _b_wnf) _dep)) _a_wnf) _b_wnf) _dep)
|
||||
((((((_e _P) _true) _false) _a) _b) _dep)
|
||||
|
||||
|
||||
Book.Kind.hol = λ_nam λ_ctx λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_hol _nam) _ctx)
|
||||
|
||||
Book.Kind.identical = λ_a λ_b λ_dep (((((Book.Kind.comparer) (Book.Kind.identical)) _a) _b) _dep)
|
||||
@ -847,6 +1074,7 @@ Book.Kind =
|
||||
|
||||
Book.Kind.lam = λ_nam λ_bod λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_lam _nam) _bod)
|
||||
|
||||
|
||||
Book.Kind.mat = λ_nam λ_x λ_z λ_s λ_p λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (((((_mat _nam) _x) _z) _s) _p)
|
||||
|
||||
Book.Kind.normal.go = λ_maj λ_term λ_dep
|
||||
@ -1018,21 +1246,11 @@ Book.List.Folder = λ_T 0
|
||||
|
||||
Book.List.Folder.nil = λ_T λ_P λ_cons λ_nil _nil
|
||||
|
||||
Book.List.Map = λ_K λ_V ((Book.List) (((Book.Pair) _K) _V))
|
||||
Book.List.Map.get = λ_K λ_V λ_eql λ_key λ_map
|
||||
let _P = λ_x ((Book.Maybe) _V)
|
||||
let _cons = λ_head λ_tail
|
||||
let _P = λ_x ((Book.Maybe) _V)
|
||||
let _new = λ_head.fst λ_head.snd
|
||||
let _P = λ_x ((Book.Maybe) _V)
|
||||
let _true = (((Book.Maybe.some) _V) _head.snd)
|
||||
let _false = ((((((Book.List.Map.get) _K) _V) _eql) _key) _tail)
|
||||
(((((_eql _head.fst) _key) _P) _true) _false)
|
||||
((_head _P) _new)
|
||||
let _nil = ((Book.Maybe.none) _V)
|
||||
(((_map _P) _cons) _nil)
|
||||
Book.List.Map.set = λ_K λ_V λ_key λ_val λ_map ((((Book.List.cons) (((Book.Pair) _K) _V)) (((((Book.Pair.new) _K) _V) _key) _val)) _map)
|
||||
Book.List.Map.new = λ_K λ_V ((Book.List.nil) (((Book.Pair) _K) _V))
|
||||
Book.List.app = λ_A λ_B λ_f λ_x
|
||||
let _P = λ_x ((Book.List) _B)
|
||||
let _cons = λ_h λ_t ((((Book.List.cons) _B) (_f _h)) (((((Book.List.app) _A) _B) _f) _t))
|
||||
let _nil = ((Book.List.nil) _B)
|
||||
(((_x _P) _cons) _nil)
|
||||
|
||||
Book.List.begin = λ_A λ_list
|
||||
let _P = λ_x ((Book.List) _A)
|
||||
@ -1096,8 +1314,8 @@ Book.Maybe.pure = (Book.Maybe.some)
|
||||
|
||||
Book.Maybe.some = λ_T λ_value λ_P λ_some λ_none (_some _value)
|
||||
|
||||
Book.Monad = λ_M 0
|
||||
Book.Monad.new = λ_M λ_bind λ_pure λ_P λ_new ((_new _bind) _pure)
|
||||
Book.Monad = λ_M 0
|
||||
|
||||
Book.Nat.double = λ_n (((_n λ_x (Book.Nat)) λ_pred ((Book.Nat.succ) ((Book.Nat.succ) ((Book.Nat.double) _pred)))) (Book.Nat.zero))
|
||||
|
||||
@ -1125,12 +1343,22 @@ Book.Nat.succ = λ_n λ_P λ_succ λ_zero (_succ _n)
|
||||
|
||||
Book.Nat.zero = λ_P λ_succ λ_zero _zero
|
||||
|
||||
Book.Pair.fst = λ_A λ_B λ_p
|
||||
let _P = λ_x _A
|
||||
let _new = λ_a λ_b _a
|
||||
((_p _P) _new)
|
||||
|
||||
Book.Pair.get = λ_A λ_B λ_p λ_P λ_f ((_p λ_x _P) _f)
|
||||
|
||||
Book.Pair = λ_A λ_B 0
|
||||
|
||||
Book.Pair.new = λ_A λ_B λ_a λ_b λ_P λ_new ((_new _a) _b)
|
||||
|
||||
Book.Pair.snd = λ_A λ_B λ_p
|
||||
let _P = λ_x _B
|
||||
let _new = λ_a λ_b _b
|
||||
((_p _P) _new)
|
||||
|
||||
Book.Parser.Guard.get = λ_A (((Book.Pair.get) ((Book.Parser) (Book.Bool))) ((Book.Parser) _A))
|
||||
|
||||
Book.Parser.Guard = λ_A (((Book.Pair) ((Book.Parser) (Book.Bool))) ((Book.Parser) _A))
|
||||
@ -1261,19 +1489,19 @@ Book.Parser.variant = λ_A λ_variants
|
||||
let _nil = (((Book.Parser.fail) _A) (Str "error"))
|
||||
(((_variants _P) _cons) _nil)
|
||||
|
||||
Book.QBool.true = λ_P λ_S λ_p ((_p 0) λ_x _x)
|
||||
Book.QBool.false = λ_P λ_S λ_p ((_p 1) λ_x _x)
|
||||
Book.QBool = 0
|
||||
Book.QBool.match = λ_a λ_P λ_t λ_f (((_a _P) λ_x (_P _a)) λ_tag (U60.match _tag λ_x (_x _t) λ_tag_1(λ_x ((U60.match _tag_1 λ_x (_x _f) λ_tag_1_1(λ_x (_x λ_e (((Book.Empty.absurd) _e) 0)))) _x))))
|
||||
Book.QBool.true = λ_P λ_S λ_p ((_p 0) λ_x _x)
|
||||
|
||||
Book.QBool2.true = λ_P λ_new (_new 0)
|
||||
Book.QBool2.false = λ_P λ_new (_new 1)
|
||||
Book.QBool2.bad = λ_P λ_new ((_new 2) 0)
|
||||
Book.QBool2 = 0
|
||||
Book.QBool2.match = λ_a λ_P λ_t λ_f ((_a _P) λ_tag (U60.match _tag _t λ_tag_1((U60.match _tag_1 _f λ_tag_1_1(λ_e (_e λ_x 0))))))
|
||||
Book.QBool2.false = λ_P λ_new (_new 1)
|
||||
Book.QBool2.true = λ_P λ_new (_new 0)
|
||||
|
||||
Book.QUnit.one = λ_P λ_SP λ_new ((_new 0) λ_one _one)
|
||||
Book.QUnit = 0
|
||||
Book.QUnit.one = λ_P λ_SP λ_new ((_new 0) λ_one _one)
|
||||
|
||||
Book.Sigma = λ_A λ_B 0
|
||||
|
||||
@ -1289,13 +1517,41 @@ Book.String.Concatenator.join = ((Book.List.Concatenator.join) (Book.Char))
|
||||
|
||||
Book.String.Concatenator = ((Book.List.Concatenator) (Book.Char))
|
||||
|
||||
Book.String.Map = ((Book.List.Map) (Book.String))
|
||||
Book.String.Map.get = λ_A λ_key λ_map ((((((Book.List.Map.get) (Book.String)) _A) (Book.String.equal)) _key) _map)
|
||||
Book.String.Map.set = λ_A λ_key λ_val λ_map ((((((Book.List.Map.set) (Book.String)) _A) _key) _val) _map)
|
||||
Book.String.Map.new = λ_V (((Book.List.Map.new) (Book.String)) _V)
|
||||
Book.String.Map.from_list = λ_V λ_list (((((Book.BBT.from_list) (Book.String)) _V) (Book.String.cmp)) _list)
|
||||
|
||||
Book.String.Map.has = λ_V λ_key λ_map ((((((Book.BBT.has) (Book.String)) _V) (Book.String.cmp)) _key) _map)
|
||||
|
||||
Book.String.Map.has.linear = λ_V λ_key λ_map ((((((Book.BBT.has.linear) (Book.String)) _V) (Book.String.cmp)) _key) _map)
|
||||
|
||||
Book.String.Map.new = λ_V (((Book.BBT.tip) (Book.String)) _V)
|
||||
Book.String.Map.get = λ_V λ_key λ_map ((((((Book.BBT.get) (Book.String)) _V) (Book.String.cmp)) _key) _map)
|
||||
Book.String.Map = λ_V (((Book.BBT) (Book.String)) _V)
|
||||
Book.String.Map.got = λ_V λ_key λ_map ((((((Book.BBT.got) (Book.String)) _V) (Book.String.cmp)) _key) _map)
|
||||
Book.String.Map.set = λ_V λ_key λ_val λ_map (((((((Book.BBT.set) (Book.String)) _V) (Book.String.cmp)) _key) _val) _map)
|
||||
|
||||
Book.String.Map.to_list = λ_V λ_map ((((Book.BBT.to_list) (Book.String)) _V) _map)
|
||||
|
||||
Book.String.begin = λ_str (((Book.List.begin) (Book.Char)) _str)
|
||||
|
||||
Book.String.cmp = λ_a λ_b
|
||||
let _P = λ_x 0
|
||||
let _cons = λ_a.head λ_a.tail λ_b
|
||||
let _P = λ_x 0
|
||||
let _cons = λ_b.head λ_b.tail λ_a.head λ_a.tail
|
||||
let _P = λ_x (Book.Cmp)
|
||||
let _ltn = (Book.Cmp.ltn)
|
||||
let _eql = (((Book.String.cmp) _a.tail) _b.tail)
|
||||
let _gtn = (Book.Cmp.gtn)
|
||||
(((((((Book.U60.cmp) _a.head) _b.head) _P) _ltn) _eql) _gtn)
|
||||
let _nil = λ_a.head λ_a.tail (Book.Cmp.gtn)
|
||||
(((((_b _P) _cons) _nil) _a.head) _a.tail)
|
||||
let _nil = λ_b
|
||||
let _P = λ_x (Book.Cmp)
|
||||
let _cons = λ_b.head λ_b.tail (Book.Cmp.ltn)
|
||||
let _nil = (Book.Cmp.eql)
|
||||
(((_b _P) _cons) _nil)
|
||||
((((_a _P) _cons) _nil) _b)
|
||||
|
||||
Book.String.concat = ((Book.List.concat) (Book.Char))
|
||||
|
||||
Book.String.cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
|
||||
@ -1320,6 +1576,12 @@ Book.String.indent = λ_tab
|
||||
let _zero = (Book.String.nil)
|
||||
(((_tab _P) _succ) _zero)
|
||||
|
||||
Book.String.join = λ_strs
|
||||
let _P = λ_x (Book.String)
|
||||
let _cons = λ_h λ_t (((Book.String.concat) _h) ((Book.String.join) _t))
|
||||
let _nil = (Book.String.nil)
|
||||
(((_strs _P) _cons) _nil)
|
||||
|
||||
Book.String = ((Book.List) (Book.Char))
|
||||
|
||||
Book.String.length = λ_a (((Book.List.length) (Book.Char)) _a)
|
||||
@ -1330,6 +1592,15 @@ Book.String.nil = λ_P λ_cons λ_nil _nil
|
||||
|
||||
Book.String.quote = (((Book.String.cons) 34) (Book.String.nil))
|
||||
|
||||
Book.String.skip.comment = λ_str
|
||||
let _P = λ_x (Book.String)
|
||||
let _cons = λ_c0 λ_cs
|
||||
let _P = λ_x 0
|
||||
let _true = λ_c0 λ_cs ((Book.String.skip) _cs)
|
||||
let _false = λ_c0 λ_cs ((Book.String.skip.comment) _cs)
|
||||
(((((((Book.Char.is_newline) _c0) _P) _true) _false) _c0) _cs)
|
||||
let _nil = (Book.String.nil)
|
||||
(((_str _P) _cons) _nil)
|
||||
Book.String.skip = λ_str
|
||||
let _P = λ_x (Book.String)
|
||||
let _cons = λ_c0 λ_cs
|
||||
@ -1351,15 +1622,6 @@ Book.String.skip = λ_str
|
||||
(((((((Book.Char.is_blank) _c0) _P) _true) _false) _c0) _cs)
|
||||
let _nil = (Book.String.nil)
|
||||
(((_str _P) _cons) _nil)
|
||||
Book.String.skip.comment = λ_str
|
||||
let _P = λ_x (Book.String)
|
||||
let _cons = λ_c0 λ_cs
|
||||
let _P = λ_x 0
|
||||
let _true = λ_c0 λ_cs ((Book.String.skip) _cs)
|
||||
let _false = λ_c0 λ_cs ((Book.String.skip.comment) _cs)
|
||||
(((((((Book.Char.is_newline) _c0) _P) _true) _false) _c0) _cs)
|
||||
let _nil = (Book.String.nil)
|
||||
(((_str _P) _cons) _nil)
|
||||
|
||||
Book.String.unpar = λ_fst λ_lst λ_str
|
||||
let _P = λ_x (Book.String)
|
||||
@ -1371,10 +1633,19 @@ Book.String.unpar = λ_fst λ_lst λ_str
|
||||
let _nil = (Book.String.nil)
|
||||
(((_str _P) _cons) _nil)
|
||||
|
||||
Book.U60.Map = ((Book.List.Map) 0)
|
||||
Book.U60.Map.get = λ_A λ_key λ_map ((((((Book.List.Map.get) 0) _A) (Book.U60.equal)) _key) _map)
|
||||
Book.U60.Map.set = λ_A λ_key λ_val λ_map ((((((Book.List.Map.set) 0) _A) _key) _val) _map)
|
||||
Book.U60.Map.new = λ_V (((Book.List.Map.new) 0) _V)
|
||||
Book.U60.Map.new = λ_V (((Book.BBT.tip) 0) _V)
|
||||
Book.U60.Map.get = λ_V λ_key λ_map ((((((Book.BBT.get) 0) _V) (Book.U60.cmp)) _key) _map)
|
||||
Book.U60.Map = λ_V (((Book.BBT) 0) _V)
|
||||
Book.U60.Map.got = λ_V λ_key λ_map ((((((Book.BBT.got) 0) _V) (Book.U60.cmp)) _key) _map)
|
||||
Book.U60.Map.set = λ_V λ_key λ_val λ_map (((((((Book.BBT.set) 0) _V) (Book.U60.cmp)) _key) _val) _map)
|
||||
|
||||
Book.U60.abs_diff = λ_a λ_b
|
||||
let _P = λ_x 0
|
||||
let _true = (- _b _a)
|
||||
let _false = (- _a _b)
|
||||
(((((Book.U60.to_bool) (< _a _b)) _P) _true) _false)
|
||||
|
||||
Book.U60.cmp = λ_a λ_b (((((Book.U60.if) (== _a _b)) (Book.Cmp)) (((((Book.U60.if) (< _a _b)) (Book.Cmp)) (Book.Cmp.gtn)) (Book.Cmp.ltn))) (Book.Cmp.eql))
|
||||
|
||||
Book.U60.equal = λ_a λ_b (U60.match (== _a _b) (Book.Bool.false) λ_x_1((Book.Bool.true)))
|
||||
|
||||
@ -1388,6 +1659,10 @@ Book.U60.if = λ_x λ_P λ_t λ_f (U60.match _x _t λ_x_1(_f))
|
||||
|
||||
Book.U60.match = λ_x λ_P λ_s λ_z (U60.match _x _z λ_self_1((_s _self_1)))
|
||||
|
||||
Book.U60.max = λ_a λ_b (((((Book.U60.to_bool) (> _a _b)) λ_x 0) _a) _b)
|
||||
|
||||
Book.U60.min = λ_a λ_b (((((Book.U60.to_bool) (< _a _b)) λ_x 0) _a) _b)
|
||||
|
||||
Book.U60.name.go = λ_n (U60.match _n λ_nil _nil λ_n_1(λ_nil (((Book.String.cons) (+ 97 (% _n_1 26))) (((Book.U60.name.go) (/ _n_1 26)) _nil))))
|
||||
|
||||
Book.U60.name = λ_n ((Book.String.Concatenator.build) ((Book.U60.name.go) (+ _n 1)))
|
||||
@ -1410,13 +1685,15 @@ Book.test0 = λ_A λ_B λ_aa λ_ab λ_ba λ_bb λ_a λ_b (_ba (_ab (_aa (_aa _a)
|
||||
|
||||
Book.test1 = λ_x (+ 50 12)
|
||||
|
||||
Book._EXP = ((((Book.Kind.all) (Str "n")) (Book._Nat)) λ_n ((((Book.Kind.all) (Str "m")) (Book._Nat)) λ_m (Book._Nat)))
|
||||
Book._exp = (((Book.Kind.lam) (Str "n")) λ_n (((Book.Kind.lam) (Str "m")) λ_m (((Book.Kind.lam) (Str "P")) λ_P (((Book.Kind.app) (((Book.Kind.app) _m) ((((Book.Kind.all) (Str "x")) _P) λ_x _P))) (((Book.Kind.app) _n) _P)))))
|
||||
Book._C2 = (Book._Nat)
|
||||
Book._c2 = (((Book.Kind.lam) (Str "P")) λ_P (((Book.Kind.lam) (Str "s")) λ_s (((Book.Kind.lam) (Str "z")) λ_z (((Book.Kind.app) _s) (((Book.Kind.app) _s) _z)))))
|
||||
Book._C2 = (Book._Nat)
|
||||
Book._EXP = ((((Book.Kind.all) (Str "n")) (Book._Nat)) λ_n ((((Book.Kind.all) (Str "m")) (Book._Nat)) λ_m (Book._Nat)))
|
||||
Book.test10 =
|
||||
let _term = (((Book.Kind.app) (((Book.Kind.app) (Book._exp)) (Book._c2))) (Book._c2))
|
||||
(((Book.Kind.Term.show) ((((Book.Kind.normal) (Book.Bool.true)) _term) (Book.Nat.zero))) (Book.Nat.zero))
|
||||
Book._exp = (((Book.Kind.lam) (Str "n")) λ_n (((Book.Kind.lam) (Str "m")) λ_m (((Book.Kind.lam) (Str "P")) λ_P (((Book.Kind.app) (((Book.Kind.app) _m) ((((Book.Kind.all) (Str "x")) _P) λ_x _P))) (((Book.Kind.app) _n) _P)))))
|
||||
|
||||
Book.test11 = 0
|
||||
|
||||
Book.test2 =
|
||||
let _xs = ((((Book.List.cons) 0) 0) ((((Book.List.cons) 0) 1) ((((Book.List.cons) 0) 2) ((Book.List.nil) 0))))
|
||||
@ -1437,12 +1714,9 @@ Book.test8 = λ_a ((((Book.U60.if) _a) 0) (Str "test"))
|
||||
|
||||
Book.test9 = ((((Book.String.unpar) 40) 41) (Str "((foo))"))
|
||||
|
||||
|
||||
Main = (Str.view ((Book.Kind.Book.to_hvm) ((Book.Kind.Book.parse) (Str "F = λf λx (f (f x))"))))
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Book.testBBT = (Str "
|
||||
File commented for backward compatibility.
|
||||
To run the tests, uncomment the code on:
|
||||
testBBT.kind2
|
||||
U60.Map
|
||||
")
|
||||
|
2
bootstrap.js
vendored
2
bootstrap.js
vendored
@ -28,7 +28,7 @@ fs.readdirSync(bookDir).forEach(file => {
|
||||
});
|
||||
|
||||
// Loads prelude
|
||||
var prelude = fs.readFileSync("./book/Kind.Book.to_hvm.prelude", "utf8");
|
||||
var prelude = fs.readFileSync("./book/Kind.Book.to_hvm.prelude.kind2", "utf8");
|
||||
const lines = prelude.split("\n");
|
||||
lines.shift();
|
||||
lines.pop();
|
||||
|
@ -101,7 +101,7 @@
|
||||
(Reduce 1 (Txt txt)) = (Reduce.txt 1 txt)
|
||||
(Reduce r val) = val
|
||||
|
||||
(Reduce.app r (Lam nam bod) arg) = (Reduce r (bod (Reduce r arg)))
|
||||
(Reduce.app r (Lam nam bod) arg) = (Reduce r (bod (Reduce 0 arg)))
|
||||
//(Reduce.app r (Hol nam ctx ars) arg) = (Hol nam ctx (List.cons arg ars))
|
||||
(Reduce.app r fun arg) = (App fun arg)
|
||||
|
||||
@ -155,6 +155,7 @@
|
||||
// --------
|
||||
|
||||
// Check if two terms are identical. If not...
|
||||
(Equal a b 24) = 0 // limits depth FIXME: won't be necessary with better ref-ids equality
|
||||
(Equal a b dep) = (Equal.minor (Identical a b dep) a b dep)
|
||||
|
||||
// Check if they're identical after a minor weak reduction. If not...
|
||||
@ -418,7 +419,8 @@ Compile.primitives = [
|
||||
|
||||
(Normalizer (Ref nam val)) = (Normalizer val)
|
||||
(Normalizer (Ann val typ)) = (Normalizer val)
|
||||
(Normalizer val) = (Compile val)
|
||||
//(Normalizer val) = (Compile val)
|
||||
(Normalizer val) = (Str.view (Compile val))
|
||||
|
||||
(Checker (Ref nam val)) = (Checker val)
|
||||
(Checker (Ann val typ)) = (Checker.report (Check val typ 0))
|
||||
@ -426,4 +428,3 @@ Compile.primitives = [
|
||||
|
||||
(Checker.report (Some x)) = (HVM.print "Check!" OK)
|
||||
(Checker.report None) = (HVM.print "Error." ERR)
|
||||
|
||||
|
165
kind2.ts
165
kind2.ts
@ -1,3 +1,123 @@
|
||||
//// TODO
|
||||
//Kind.load
|
||||
//: ∀(name: String)
|
||||
//Kind.Book
|
||||
//= λname
|
||||
//(Kind.load.name #5 name (String.Map.new Kind.Term))
|
||||
|
||||
//// Gets the source file of a definition
|
||||
//Kind.load.file_of
|
||||
//: ∀(name: String)
|
||||
//String
|
||||
//= λname
|
||||
//(String.concat name ".kind2")
|
||||
|
||||
//// Loads a file into a new book
|
||||
//Kind.load.file
|
||||
//: ∀(file: String)
|
||||
//Kind.Book
|
||||
//= λfile
|
||||
//(HVM.load Kind.Book file λdata
|
||||
//(Kind.Book.parse data))
|
||||
|
||||
//// Loads a name into a book
|
||||
//Kind.load.name
|
||||
//: ∀(lims: #U60)
|
||||
//∀(name: String)
|
||||
//∀(book: Kind.Book)
|
||||
//Kind.Book
|
||||
//= λlims
|
||||
//(HVM.log #U60 ∀(name:String)∀(book:Kind.Book)Kind.Book lims
|
||||
//#match lims = lims {
|
||||
//#0: λname λbook book
|
||||
//#+: λname λbook
|
||||
//(HVM.print Kind.Book (String.concat "LOAD:" name)
|
||||
//// Checks if name is already on book
|
||||
//let P = λx (Kind.Book)
|
||||
//let new = λhas λbook
|
||||
//// If it is, do nothing; otherwise, define it
|
||||
//let P = λx ∀(book: Kind.Book) (Kind.Book)
|
||||
//let true = λbook
|
||||
//(HVM.print Kind.Book (String.concat (String.concat "OLD!:" name) (String.concat " -- " (Kind.keys book))) book)
|
||||
//let false = λbook
|
||||
//(HVM.print Kind.Book (String.concat (String.concat "NEW!:" name) (String.concat " -- " (Kind.keys book)))
|
||||
//let file = (Kind.load.file (Kind.load.file_of name))
|
||||
//let defs = (String.Map.to_list Kind.Term file)
|
||||
//let bok1 = (Kind.load.define defs book)
|
||||
//let file = (Kind.load.file (Kind.load.file_of name))
|
||||
//let refs = (Kind.Book.get_refs file)
|
||||
//let bok2 = (HVM.print ?a (String.concat "REC!:" (Kind.keys bok1)) (Kind.load.name.many lims-1 refs bok1))
|
||||
//bok2)
|
||||
////(HVM.print.many Kind.Book refs book)
|
||||
|
||||
//((~has P true false) book)
|
||||
//(~(String.Map.has.linear Kind.Term name book) P new))
|
||||
//}: ∀(name: String) ∀(book: Kind.Book) Kind.Book)
|
||||
|
||||
//// Loads many names into a book
|
||||
//Kind.load.name.many
|
||||
//: ∀(lims: #U60)
|
||||
//∀(list: (List String))
|
||||
//∀(book: Kind.Book)
|
||||
//Kind.Book
|
||||
//= λlims λlist λbook
|
||||
//let P = λx ∀(book: Kind.Book) (Kind.Book)
|
||||
//let cons = λhead λtail λbook
|
||||
////(HVM.print Kind.Book
|
||||
////(String.concat "DEP:"
|
||||
////(String.concat head
|
||||
////(String.concat " BOOK:"
|
||||
////(Kind.Book.show book))))
|
||||
//let bok2 = (Kind.load.name lims head book)
|
||||
//(Kind.load.name.many lims tail bok2)
|
||||
//let nil = λbook book
|
||||
//((~list P cons nil) book)
|
||||
|
||||
//// Defines a term and loads its dependencies
|
||||
////Kind.load.define
|
||||
////: ∀(name: String)
|
||||
////∀(term: Kind.Term)
|
||||
////∀(book: Kind.Book)
|
||||
////Kind.Book
|
||||
////= λname λterm λbook
|
||||
////let book = (String.Map.set Kind.Term name term book)
|
||||
////let refs = (Kind.Term.get_refs term)
|
||||
////let book = (Kind.load.name.many refs book)
|
||||
////book
|
||||
|
||||
//// Defines many terms
|
||||
//Kind.load.define
|
||||
//: ∀(defs: (List (Pair String Kind.Term)))
|
||||
//∀(book: Kind.Book)
|
||||
//Kind.Book
|
||||
//= λdefs λbook
|
||||
//// If defs list isn't empty...
|
||||
//let P = λx ∀(book: Kind.Book) (Kind.Book)
|
||||
//let cons = λdefs.head λdefs.tail λbook
|
||||
//// Gets the def name/term
|
||||
//let P = λx (Kind.Book)
|
||||
//let new = λname λterm
|
||||
//// Writes it to the book
|
||||
//let bok2 = (String.Map.set Kind.Term name term book)
|
||||
//(HVM.print Kind.Book (String.concat "DEF!:" name)
|
||||
//// Recurses
|
||||
//(Kind.load.define defs.tail bok2))
|
||||
//(~defs.head P new)
|
||||
//// If defs list is empty, return the book
|
||||
//let nil = λbook book
|
||||
//((~defs P cons nil) book)
|
||||
|
||||
|
||||
//Kind.keys
|
||||
//: ∀(book: Kind.Book)
|
||||
//String
|
||||
//= λbook
|
||||
//let defs = (String.Map.to_list Kind.Term book)
|
||||
//let defs = (List.app (Pair String Kind.Term) String (Pair.fst String Kind.Term) defs)
|
||||
//(String.join defs)
|
||||
|
||||
|
||||
|
||||
import { execSync } from 'child_process';
|
||||
import * as fs from 'fs';
|
||||
|
||||
@ -15,10 +135,6 @@ export function str(result: string): string {
|
||||
return result.slice(1,-1).trim();
|
||||
}
|
||||
|
||||
export function load(name: string): string {
|
||||
return fs.readFileSync("./book/"+name+".kind2", "utf8");
|
||||
}
|
||||
|
||||
export function get_refs(code: string): string {
|
||||
return run(`(Strs.view ((Book.Kind.Book.get_refs) ((Book.Kind.Book.parse) (Str \`${code}\`))))`).trim();
|
||||
}
|
||||
@ -27,4 +143,43 @@ export function to_hvm(code: string): string {
|
||||
return str(run(`(Str.view ((Book.Kind.Book.to_hvm) ((Book.Kind.Book.parse) (Str \`${code}\`))))`).trim());
|
||||
}
|
||||
|
||||
console.log(get_refs(`plus2 = λx (Nat.succ (Nat.succ x))`));
|
||||
//// Loads a name into a book
|
||||
//Kind.load.name
|
||||
//: ∀(lims: #U60)
|
||||
//∀(name: String)
|
||||
//∀(book: Kind.Book)
|
||||
//Kind.Book
|
||||
//= λlims
|
||||
//(HVM.log #U60 ∀(name:String)∀(book:Kind.Book)Kind.Book lims
|
||||
//#match lims = lims {
|
||||
//#0: λname λbook book
|
||||
//#+: λname λbook
|
||||
//(HVM.print Kind.Book (String.concat "LOAD:" name)
|
||||
//// Checks if name is already on book
|
||||
//let P = λx (Kind.Book)
|
||||
//let new = λhas λbook
|
||||
//// If it is, do nothing; otherwise, define it
|
||||
//let P = λx ∀(book: Kind.Book) (Kind.Book)
|
||||
//let true = λbook
|
||||
//(HVM.print Kind.Book (String.concat (String.concat "OLD!:" name) (String.concat " -- " (Kind.keys book))) book)
|
||||
//let false = λbook
|
||||
//(HVM.print Kind.Book (String.concat (String.concat "NEW!:" name) (String.concat " -- " (Kind.keys book)))
|
||||
//let file = (Kind.load.file (Kind.load.file_of name))
|
||||
//let defs = (String.Map.to_list Kind.Term file)
|
||||
//let bok1 = (Kind.load.define defs book)
|
||||
//let file = (Kind.load.file (Kind.load.file_of name))
|
||||
//let refs = (Kind.Book.get_refs file)
|
||||
//let bok2 = (HVM.print ?a (String.concat "REC!:" (Kind.keys bok1)) (Kind.load.name.many lims-1 refs bok1))
|
||||
//bok2)
|
||||
////(HVM.print.many Kind.Book refs book)
|
||||
//((~has P true false) book)
|
||||
//(~(String.Map.has.linear Kind.Term name book) P new))
|
||||
//}: ∀(name: String) ∀(book: Kind.Book) Kind.Book)
|
||||
|
||||
export function load_file(file: string): string {
|
||||
return fs.readFileSync("./book/"+file, "utf8");
|
||||
}
|
||||
|
||||
export function load_name(
|
||||
|
||||
console.log(get_refs(load("Bool")));
|
||||
|
Loading…
Reference in New Issue
Block a user