From 24510cedbe64f5d8408939d761003d3988563b01 Mon Sep 17 00:00:00 2001 From: Victor Taelin Date: Fri, 5 Jul 2024 02:03:05 -0300 Subject: [PATCH] WIP --- .gitignore | 1 + book/BBT.kind2 | 19 --- book/BBT/balance.kind2 | 97 --------------- book/BBT/balance/lft_heavier.kind2 | 80 ------------ book/BBT/balance/rgt_heavier.kind2 | 80 ------------ book/BBT/bin.kind2 | 11 -- book/BBT/from_list.kind2 | 28 ----- book/BBT/get.kind2 | 34 ------ book/BBT/got.kind2 | 70 ----------- book/BBT/got_size.kind2 | 20 --- book/BBT/has.kind2 | 33 ----- book/BBT/has/linear.kind2 | 74 ------------ book/BBT/lft_rotate.kind2 | 31 ----- book/BBT/new_node.kind2 | 30 ----- book/BBT/rgt_rotate.kind2 | 31 ----- book/BBT/set.kind2 | 81 ------------- book/BBT/singleton.kind2 | 10 -- book/BBT/tip.kind2 | 3 - book/BBT/to_list.kind2 | 32 ----- book/{BMap.kind2 => BMap/_.kind2} | 2 +- book/BMap/leaf.kind2 | 2 +- book/BMap/node.kind2 | 2 +- book/{Bool.kind2 => Bool/_.kind2} | 0 book/Bool/and.kind2 | 2 +- book/Bool/lemma/double_negation.kind2 | 5 +- book/{Char.kind2 => Char/_.kind2} | 0 book/{Cmp.kind2 => Cmp/_.kind2} | 0 book/{Empty.kind2 => Empty/_.kind2} | 0 book/{Equal.kind2 => Equal/_.kind2} | 0 book/Equal/match.kind2 | 12 -- book/{IO.kind2 => IO/_.kind2} | 0 book/{Kind.kind2 => Kind/_.kind2} | 0 book/{List.kind2 => List/_.kind2} | 0 book/{Maybe.kind2 => Maybe/_.kind2} | 2 +- book/{Monad.kind2 => Monad/_.kind2} | 0 book/{Nat.kind2 => Nat/_.kind2} | 0 book/Nat/is_zero.kind2 | 167 ++++++++++++++++++++++++++ book/{Pair.kind2 => Pair/_.kind2} | 2 +- book/{Parser.kind2 => Parser/_.kind2} | 0 book/{QBool.kind2 => QBool/_.kind2} | 0 book/{QBool2.kind2 => QBool2/_.kind2} | 0 book/{QUnit.kind2 => QUnit/_.kind2} | 0 book/{Sigma.kind2 => Sigma/_.kind2} | 0 book/{String.kind2 => String/_.kind2} | 0 book/{The.kind2 => The/_.kind2} | 0 book/{Tree.kind2 => Tree/_.kind2} | 0 book/U60/abs_diff.kind2 | 2 +- book/U60/name.kind2 | 2 +- book/U60/show.kind2 | 2 +- book/{Unit.kind2 => Unit/_.kind2} | 0 book/{Vector.kind2 => Vector/_.kind2} | 0 book/foo.ts | 9 ++ book/{ => tmp}/_OBLITERATE.kind2 | 0 book/{ => tmp}/_err.txt | 0 book/{ => tmp}/_main | Bin book/{ => tmp}/_main.hvm2 | 0 book/{ => tmp}/_main.hvmc | 0 book/{ => tmp}/_main.js | 0 book/{ => tmp}/_main.kind2 | 0 book/{ => tmp}/test0.kind2 | 0 book/{ => tmp}/test1.kind2 | 0 book/{ => tmp}/test10.kind2 | 0 book/{ => tmp}/test11.kind2 | 0 book/{ => tmp}/test2.kind2 | 0 book/{ => tmp}/test3.kind2 | 0 book/{ => tmp}/test4.kind2 | 0 book/{ => tmp}/test5.kind2 | 0 book/{ => tmp}/test6.kind2 | 0 book/{ => tmp}/test7.kind2 | 0 book/{ => tmp}/test8.kind2 | 0 book/{ => tmp}/test9.kind2 | 0 book/{ => tmp}/testBBT.kind2 | 0 src/book/mod.rs | 8 +- src/info/mod.rs | 4 +- src/kindc.hs | 52 ++++---- 75 files changed, 228 insertions(+), 812 deletions(-) delete mode 100644 book/BBT.kind2 delete mode 100644 book/BBT/balance.kind2 delete mode 100644 book/BBT/balance/lft_heavier.kind2 delete mode 100644 book/BBT/balance/rgt_heavier.kind2 delete mode 100644 book/BBT/bin.kind2 delete mode 100644 book/BBT/from_list.kind2 delete mode 100644 book/BBT/get.kind2 delete mode 100644 book/BBT/got.kind2 delete mode 100644 book/BBT/got_size.kind2 delete mode 100644 book/BBT/has.kind2 delete mode 100644 book/BBT/has/linear.kind2 delete mode 100644 book/BBT/lft_rotate.kind2 delete mode 100644 book/BBT/new_node.kind2 delete mode 100644 book/BBT/rgt_rotate.kind2 delete mode 100644 book/BBT/set.kind2 delete mode 100644 book/BBT/singleton.kind2 delete mode 100644 book/BBT/tip.kind2 delete mode 100644 book/BBT/to_list.kind2 rename book/{BMap.kind2 => BMap/_.kind2} (79%) rename book/{Bool.kind2 => Bool/_.kind2} (100%) rename book/{Char.kind2 => Char/_.kind2} (100%) rename book/{Cmp.kind2 => Cmp/_.kind2} (100%) rename book/{Empty.kind2 => Empty/_.kind2} (100%) rename book/{Equal.kind2 => Equal/_.kind2} (100%) rename book/{IO.kind2 => IO/_.kind2} (100%) rename book/{Kind.kind2 => Kind/_.kind2} (100%) rename book/{List.kind2 => List/_.kind2} (100%) rename book/{Maybe.kind2 => Maybe/_.kind2} (58%) rename book/{Monad.kind2 => Monad/_.kind2} (100%) rename book/{Nat.kind2 => Nat/_.kind2} (100%) create mode 100644 book/Nat/is_zero.kind2 rename book/{Pair.kind2 => Pair/_.kind2} (60%) rename book/{Parser.kind2 => Parser/_.kind2} (100%) rename book/{QBool.kind2 => QBool/_.kind2} (100%) rename book/{QBool2.kind2 => QBool2/_.kind2} (100%) rename book/{QUnit.kind2 => QUnit/_.kind2} (100%) rename book/{Sigma.kind2 => Sigma/_.kind2} (100%) rename book/{String.kind2 => String/_.kind2} (100%) rename book/{The.kind2 => The/_.kind2} (100%) rename book/{Tree.kind2 => Tree/_.kind2} (100%) rename book/{Unit.kind2 => Unit/_.kind2} (100%) rename book/{Vector.kind2 => Vector/_.kind2} (100%) create mode 100644 book/foo.ts rename book/{ => tmp}/_OBLITERATE.kind2 (100%) rename book/{ => tmp}/_err.txt (100%) rename book/{ => tmp}/_main (100%) rename book/{ => tmp}/_main.hvm2 (100%) rename book/{ => tmp}/_main.hvmc (100%) rename book/{ => tmp}/_main.js (100%) rename book/{ => tmp}/_main.kind2 (100%) rename book/{ => tmp}/test0.kind2 (100%) rename book/{ => tmp}/test1.kind2 (100%) rename book/{ => tmp}/test10.kind2 (100%) rename book/{ => tmp}/test11.kind2 (100%) rename book/{ => tmp}/test2.kind2 (100%) rename book/{ => tmp}/test3.kind2 (100%) rename book/{ => tmp}/test4.kind2 (100%) rename book/{ => tmp}/test5.kind2 (100%) rename book/{ => tmp}/test6.kind2 (100%) rename book/{ => tmp}/test7.kind2 (100%) rename book/{ => tmp}/test8.kind2 (100%) rename book/{ => tmp}/test9.kind2 (100%) rename book/{ => tmp}/testBBT.kind2 (100%) diff --git a/.gitignore b/.gitignore index 9bd00440..1b515f59 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ /target +.bkp/ .tmp/ .kind21/ plans.txt diff --git a/book/BBT.kind2 b/book/BBT.kind2 deleted file mode 100644 index 1c3cd31a..00000000 --- a/book/BBT.kind2 +++ /dev/null @@ -1,19 +0,0 @@ -//BBT -//: ∀(K: *) ∀(V: *) * -//= λK λV - //$(self: (BBT K V)) - //∀(P: ∀(bbt: (BBT K V)) *) - //∀(bin: - //∀(size: U60) - //∀(key: K) - //∀(val: V) - //∀(lft: (BBT K V)) - //∀(rgt: (BBT K V)) - //(P (BBT.bin K V size key val lft rgt)) - //) - //∀(tip: (P (BBT.tip K V))) - //(P self) - -data BBT K V -| bin (size: U60) (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V)) -| tip diff --git a/book/BBT/balance.kind2 b/book/BBT/balance.kind2 deleted file mode 100644 index a6846f1d..00000000 --- a/book/BBT/balance.kind2 +++ /dev/null @@ -1,97 +0,0 @@ -use BBT/{bin,tip} -use Bool/{true,false} - -balance - (cmp: ∀(a: K) ∀(b: K) Cmp) - (set_key: K) - (node_key: K) - (val: V) - (lft: (BBT K V)) - (rgt: (BBT K V)) -: (BBT K V) = - match got_lft = (BBT/got_size lft) { - Pair/new: - match got_rgt = (BBT/got_size rgt) { - Pair/new: - use new_size = (+ got_lft.fst got_rgt.fst) - use balance = (U60/abs_diff got_lft.fst got_rgt.fst) - - match _ = (U60/to_bool (> balance 1)) { - true: - match _ = (U60/to_bool (< got_lft.fst got_rgt.fst)) { - true: (BBT/balance/lft_heavier cmp new_size node_key set_key val lft rgt) - false: (BBT/balance/rgt_heavier cmp new_size node_key set_key val lft rgt) - } - false: (bin K V new_size node_key val lft rgt) - } - } - } - - - -//BBT.balance -//: ∀(K: *) - //∀(V: *) - //∀(cmp: ∀(a: K) ∀(b: K) Cmp) - //∀(set_key: K) - //∀(node_key: K) - //∀(val: V) - //∀(lft: (BBT K V)) - //∀(rgt: (BBT K V)) - //(BBT K V) -//= λK λV λcmp λset_key λnode_key λval λlft λrgt - //use P = λx (BBT K V) - //use new = λlft.size λlft - //use P = λx (BBT K V) - //use new = λrgt.size λrgt - //use new_size = (+ 1 (U60.max lft.size rgt.size)) - //use balance = (U60.abs_diff lft.size rgt.size) - //use P = λx - //∀(new_size: U60) - //∀(node_key: K) - //∀(val: V) - //∀(lft: (BBT K V)) - //∀(rgt: (BBT K V)) - //(BBT K V) - //use true = λnew_size λnode_key λval λlft λrgt - //use P = λx - //∀(K: *) - //∀(V: *) - //∀(cmp: ∀(a: K) ∀(b: K) Cmp) - //∀(new_size: U60) - //∀(node_key: K) - //∀(set_key: K) - //∀(val: V) - //∀(lft: (BBT K V)) - //∀(rgt: (BBT K V)) - //(BBT K V) - //use true = BBT.balance.lft_heavier - //use false = BBT.balance.rgt_heavier - //(~(U60.to_bool (< rgt.size lft.size)) - //P - //true - //false - //K - //V - //cmp - //new_size - //node_key - //set_key - //val - //lft - //rgt - //) - //use false = λnew_size λnode_key λval λlft λrgt - //(BBT.bin K V new_size node_key val lft rgt) - //(~(U60.to_bool (> balance 1)) - //P - //true - //false - //new_size - //node_key - //val - //lft - //rgt - //) - //(~(BBT.got_size K V rgt) P new) - //(~(BBT.got_size K V lft) P new) diff --git a/book/BBT/balance/lft_heavier.kind2 b/book/BBT/balance/lft_heavier.kind2 deleted file mode 100644 index 8b64b37d..00000000 --- a/book/BBT/balance/lft_heavier.kind2 +++ /dev/null @@ -1,80 +0,0 @@ -use BBT/{bin,tip,lft_rotate,rgt_rotate} -use Bool/{true,false} - -lft_heavier - (cmp: ∀(a: K) ∀(b: K) Cmp) - (new_size: U60) - (node_key: K) - (set_key: K) - (val: V) - (lft: (BBT K V)) - (rgt: (BBT K V)) -: (BBT K V) = - match lft { - bin: - match _ = (Cmp/is_gtn (cmp set_key lft.key)) { - true: - use lft = (lft_rotate lft.size lft.key lft.val lft.lft lft.rgt) - (rgt_rotate new_size lft.key val lft rgt) - false: - use lft = (bin K V lft.size lft.key lft.val lft.lft lft.rgt) - (rgt_rotate new_size lft.key val lft rgt) - } - tip: (tip K V) - } - - - -//BBT.balance.lft_heavier -//: ∀(K: *) - //∀(V: *) - //∀(cmp: ∀(a: K) ∀(b: K) Cmp) - //∀(new_size: U60) - //∀(node_key: K) - //∀(set_key: K) - //∀(val: V) - //∀(lft: (BBT K V)) - //∀(rgt: (BBT K V)) - //(BBT K V) -//= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt - //use P = λx (BBT K V) - //use bin = λlft.size λlft.key λlft.val λlft.lft λlft.rgt - //use P = λx - //∀(new_size: U60) - //∀(key: K) - //∀(val: V) - //∀(lft.key: K) - //∀(lft.val: V) - //∀(lft.lft: (BBT K V)) - //∀(lft.rgt: (BBT K V)) - //∀(rgt: (BBT K V)) - //(BBT K V) - //use true = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt - //use lft = (BBT.lft_rotate - //K - //V - //lft.size - //lft.key - //lft.val - //lft.lft - //lft.rgt - //) - //(BBT.rgt_rotate K V new_size key val lft rgt) - //use false = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt - //use lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt) - //(BBT.rgt_rotate K V new_size key val lft rgt) - //(~(Cmp.is_gtn (cmp set_key lft.key)) - //P - //true - //false - //new_size - //node_key - //val - //lft.key - //lft.val - //lft.lft - //lft.rgt - //rgt - //) - //use tip = (BBT.tip K V) - //(~lft P bin tip) diff --git a/book/BBT/balance/rgt_heavier.kind2 b/book/BBT/balance/rgt_heavier.kind2 deleted file mode 100644 index b61b2508..00000000 --- a/book/BBT/balance/rgt_heavier.kind2 +++ /dev/null @@ -1,80 +0,0 @@ -use BBT/{bin,tip,lft_rotate,rgt_rotate} -use Bool/{true,false} - -rgt_heavier - (cmp: ∀(a: K) ∀(b: K) Cmp) - (new_size: U60) - (node_key: K) - (set_key: K) - (val: V) - (lft: (BBT K V)) - (rgt: (BBT K V)) -: (BBT K V) = - match rgt { - bin: - match _ = (Cmp/is_gtn (cmp set_key rgt.key)) { - true: - use rgt = (bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt) - (lft_rotate new_size rgt.key val lft rgt) - false: - use rgt = (rgt_rotate rgt.size rgt.key rgt.val rgt.lft rgt.rgt) - (lft_rotate new_size rgt.key val lft rgt) - } - tip: (tip K V) - } - - - -//BBT.balance.rgt_heavier -//: ∀(K: *) - //∀(V: *) - //∀(cmp: ∀(a: K) ∀(b: K) Cmp) - //∀(new_size: U60) - //∀(node_key: K) - //∀(set_key: K) - //∀(val: V) - //∀(lft: (BBT K V)) - //∀(rgt: (BBT K V)) - //(BBT K V) -//= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt - //use P = λx (BBT K V) - //use bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt - //use P = λx - //∀(new_size: U60) - //∀(key: K) - //∀(val: V) - //∀(lft: (BBT K V)) - //∀(rgt.key: K) - //∀(rgt.val: V) - //∀(rgt.lft: (BBT K V)) - //∀(rgt.rgt: (BBT K V)) - //(BBT K V) - //use true = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt - //use rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt) - //(BBT.lft_rotate K V new_size key val lft rgt) - //use false = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt - //use rgt = (BBT.rgt_rotate - //K - //V - //rgt.size - //rgt.key - //rgt.val - //rgt.lft - //rgt.rgt - //) - //(BBT.lft_rotate K V new_size key val lft rgt) - //(~(Cmp.is_gtn (cmp set_key rgt.key)) - //P - //true - //false - //new_size - //node_key - //val - //lft - //rgt.key - //rgt.val - //rgt.lft - //rgt.rgt - //) - //use tip = (BBT.tip K V) - //(~rgt P bin tip) diff --git a/book/BBT/bin.kind2 b/book/BBT/bin.kind2 deleted file mode 100644 index 863fa070..00000000 --- a/book/BBT/bin.kind2 +++ /dev/null @@ -1,11 +0,0 @@ -BBT.bin -: ∀(K: *) - ∀(V: *) - ∀(size: U60) - ∀(key: K) - ∀(val: V) - ∀(lft: (BBT K V)) - ∀(rgt: (BBT K V)) - (BBT K V) -= λK λV λsize λkey λval λlft λrgt - ~λP λbin λtip (bin size key val lft rgt) diff --git a/book/BBT/from_list.kind2 b/book/BBT/from_list.kind2 deleted file mode 100644 index f80a2514..00000000 --- a/book/BBT/from_list.kind2 +++ /dev/null @@ -1,28 +0,0 @@ -use BBT/{bin,tip,set} - -from_list (cmp: ∀(a: K) ∀(b: K) Cmp) (list: (List (Pair K V))) : (BBT K V) = - match list { - List/cons: - match pair = list.head { - Pair/new: (set cmp pair.fst pair.snd (from_list cmp list.tail)) - } - List/nil: (tip K V) - } - - - -//BBT.from_list -//: ∀(K: *) - //∀(V: *) - //∀(cmp: ∀(a: K) ∀(b: K) Cmp) - //∀(list: (List (Pair K V))) - //(BBT K V) -//= λK λV λcmp λlist - //use P = λx (BBT K V) - //use cons = λhead λtail - //use P = λx (BBT K V) - //use new = λkey λval - //(BBT.set K V cmp key val (BBT.from_list K V cmp tail)) - //(~head P new) - //use nil = (BBT.tip K V) - //(~list P cons nil) diff --git a/book/BBT/get.kind2 b/book/BBT/get.kind2 deleted file mode 100644 index 8f634285..00000000 --- a/book/BBT/get.kind2 +++ /dev/null @@ -1,34 +0,0 @@ -use BBT/{bin,tip} -use Cmp/{ltn,eql,gtn} - -get (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : (Maybe V) = - match map { - bin: - match _ = (cmp key map.key) { - ltn: (get cmp key map.lft) - eql: (Maybe/some map.val) - gtn: (get cmp key map.rgt) - } - tip: Maybe/none - } - - - -//BBT.get -//: ∀(K: *) - //∀(V: *) - //∀(cmp: ∀(a: K) ∀(b: K) Cmp) - //∀(key: K) - //∀(map: (BBT K V)) - //(Maybe V) -//= λK λV λcmp λkey λmap - //use P = λx (Maybe V) - //use bin = λ_size λnext.key λnext.val λnext.lft λnext.rgt - //use P = λx - //∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) (Maybe V) - //use ltn = λcmp λkey (BBT.get K V cmp key next.lft) - //use eql = λcmp λkey (Maybe.some V next.val) - //use gtn = λcmp λkey (BBT.get K V cmp key next.rgt) - //(~(cmp key next.key) P ltn eql gtn cmp key) - //use tip = (Maybe.none V) - //(~map P bin tip) diff --git a/book/BBT/got.kind2 b/book/BBT/got.kind2 deleted file mode 100644 index f97fb18e..00000000 --- a/book/BBT/got.kind2 +++ /dev/null @@ -1,70 +0,0 @@ -use BBT/{bin,tip} -use Maybe/{some,none} -use Cmp/{ltn,eql,gtn} - -got (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : (Pair (Maybe V) (BBT K V)) = - match map { - bin: - match _ = (cmp key map.key) { - ltn: - match new_pair = (got cmp key map.lft) { - Pair/new: - let map = (bin K V map.size map.key map.val new_pair.snd map.rgt) - (Pair/new new_pair.fst map) - } - eql: (Pair/new (some map.val) map) - gtn: - match new_pair = (got cmp key map.rgt) { - Pair/new: - let map = (bin K V map.size map.key map.val map.lft new_pair.snd) - (Pair/new new_pair.fst map) - } - } - tip: (Pair/new none (tip K V)) - } - - - -//BBT.got -//: ∀(K: *) - //∀(V: *) - //∀(cmp: ∀(a: K) ∀(b: K) Cmp) - //∀(key: K) - //∀(map: (BBT K V)) - //(Pair (Maybe V) (BBT K V)) -//= λK λV λcmp λkey λmap - //use P = λx (Pair (Maybe V) (BBT K V)) - //use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt - //use P = λx - //∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) - //(Pair (Maybe V) (BBT K V)) - //use ltn = λcmp λkey - //use new_pair = (BBT.got K V cmp key next.lft) - //use P = λx (Pair (Maybe V) (BBT K V)) - //use new = λval λlft - //use map = (BBT.bin K V size next.key next.val lft next.rgt) - //(Pair.new (Maybe V) (BBT K V) val map) - //(~new_pair P new) - //use eql = λcmp λkey - //use map = (BBT.bin K V size next.key next.val next.lft next.rgt) - //(Pair.new - //(Maybe V) - //(BBT K V) - //(Maybe.some V next.val) - //map - //) - //use gtn = λcmp λkey - //use new_pair = (BBT.got K V cmp key next.rgt) - //use P = λx (Pair (Maybe V) (BBT K V)) - //use new = λval λrgt - //use map = (BBT.bin K V size next.key next.val next.lft rgt) - //(Pair.new (Maybe V) (BBT K V) val map) - //(~new_pair P new) - //(~(cmp key next.key) P ltn eql gtn cmp key) - //use tip = (Pair.new - //(Maybe V) - //(BBT K V) - //(Maybe.none V) - //(BBT.tip K V) - //) - //(~map P bin tip) diff --git a/book/BBT/got_size.kind2 b/book/BBT/got_size.kind2 deleted file mode 100644 index 245dc23a..00000000 --- a/book/BBT/got_size.kind2 +++ /dev/null @@ -1,20 +0,0 @@ -use BBT/{bin,tip} - -got_size (map: (BBT K V)) : (Pair U60 (BBT K V)) = - match map { - bin: (Pair/new map.size map) - tip: (Pair/new 0 (tip K V)) - } - - - -//BBT.got_size -//: ∀(K: *) ∀(V: *) ∀(map: (BBT K V)) - //(Pair U60 (BBT K V)) -//= λK λV λmap - //use P = λx (Pair U60 (BBT K V)) - //use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt - //use map = (BBT.bin K V size next.key next.val next.lft next.rgt) - //(Pair.new U60 (BBT K V) size map) - //use tip = (Pair.new U60 (BBT K V) 0 (BBT.tip K V)) - //(~map P bin tip) diff --git a/book/BBT/has.kind2 b/book/BBT/has.kind2 deleted file mode 100644 index 22b9462c..00000000 --- a/book/BBT/has.kind2 +++ /dev/null @@ -1,33 +0,0 @@ -use BBT/{bin,tip} -use Cmp/{ltn,eql,gtn} - -has (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : Bool = - match map { - bin: - match _ = (cmp key map.key) { - ltn: (has cmp key map.lft) - eql: Bool/true - gtn: (has cmp key map.rgt) - } - tip: Bool/false - } - - - -//BBT.has -//: ∀(K: *) - //∀(V: *) - //∀(cmp: ∀(a: K) ∀(b: K) Cmp) - //∀(key: K) - //∀(map: (BBT K V)) - //Bool -//= λK λV λcmp λkey λmap - //use P = λx Bool - //use bin = λnext.size λnext.key λnext.val λnext.lft λnext.rgt - //use P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) Bool - //use ltn = λcmp λkey (BBT.has K V cmp key next.lft) - //use eql = λcmp λkey Bool.true - //use gtn = λcmp λkey (BBT.has K V cmp key next.rgt) - //(~(cmp key next.key) P ltn eql gtn cmp key) - //use tip = Bool.false - //(~map P bin tip) diff --git a/book/BBT/has/linear.kind2 b/book/BBT/has/linear.kind2 deleted file mode 100644 index 38daf43e..00000000 --- a/book/BBT/has/linear.kind2 +++ /dev/null @@ -1,74 +0,0 @@ -use BBT/{bin,tip} -use Bool/{false,true} -use Cmp/{ltn,eql,gtn} - -linear (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : (Pair Bool (BBT K V)) = - match map { - bin: - match _ = (cmp key map.key) { - ltn: - match result = (linear cmp key map.lft) { - Pair/new: - (Pair/new result.fst (bin K V map.size map.key map.val result.snd map.rgt)) - } - eql: (Pair/new true (bin K V map.size map.key map.val map.lft map.rgt)) - gtn: - match result = (linear cmp key map.rgt) { - Pair/new: - (Pair/new result.fst (bin K V map.size map.key map.val map.lft result.snd)) - } - } - tip: (Pair/new false (tip K V)) - } - - - -//BBT.has.linear -//: ∀(K: *) - //∀(V: *) - //∀(cmp: ∀(a: K) ∀(b: K) Cmp) - //∀(key: K) - //∀(map: (BBT K V)) - //(Pair Bool (BBT K V)) -//= λK λV λcmp λhas_key λmap - //use P = λx (Pair Bool (BBT K V)) - //use bin = λsize λnode_key λval λlft λrgt - //use P = λx - //∀(cmp: ∀(a: K) ∀(b: K) Cmp) - //∀(size: U60) - //∀(node_key: K) - //∀(val: V) - //∀(lft: (BBT K V)) - //∀(rgt: (BBT K V)) - //∀(key: K) - //(Pair Bool (BBT K V)) - //use ltn = λcmp λsize λnode_key λval λlft λrgt λhas_key - //use P = λx (Pair Bool (BBT K V)) - //use new = λbool λlft - //use map = (BBT.bin K V size node_key val lft rgt) - //(Pair.new Bool (BBT K V) bool map) - //(~(BBT.has.linear K V cmp has_key lft) P new) - //use eql = λcmp λsize λnode_key λval λlft λrgt λhas_key - //(Pair.new - //Bool - //(BBT K V) - //Bool.true - //(BBT.bin K V size node_key val lft rgt) - //) - //use gtn = λcmp λsize λnode_key λval λlft λrgt λhas_key - //use P = λx (Pair Bool (BBT K V)) - //use new = λbool λrgt - //use map = (BBT.bin K V size node_key val lft rgt) - //(Pair.new Bool (BBT K V) bool rgt) - //(~(BBT.has.linear K V cmp has_key rgt) P new) - //((~(cmp has_key node_key) P ltn eql gtn) - //cmp - //size - //node_key - //val - //lft - //rgt - //has_key - //) - //use tip = (Pair.new Bool (BBT K V) Bool.false (BBT.tip K V)) - //(~map P bin tip) diff --git a/book/BBT/lft_rotate.kind2 b/book/BBT/lft_rotate.kind2 deleted file mode 100644 index fa8b8afe..00000000 --- a/book/BBT/lft_rotate.kind2 +++ /dev/null @@ -1,31 +0,0 @@ -use BBT/{bin,tip} - -lft_rotate (size: U60) (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V)) : (BBT K V) = - match rgt { - bin: - use b = (BBT/new_node key val lft rgt.lft) - use a = (BBT/new_node rgt.key rgt.val b rgt.rgt) - a - tip: (bin K V size key val lft (tip K V)) - } - - - -//BBT.lft_rotate -//: ∀(K: *) - //∀(V: *) - //∀(size: U60) - //∀(key: K) - //∀(val: V) - //∀(lft: (BBT K V)) - //∀(rgt: (BBT K V)) - //(BBT K V) -//= λK λV λsize λkey λval λlft λrgt - //use P = λx ∀(key: K) ∀(val: V) ∀(lft: (BBT K V)) (BBT K V) - //use bin = λ_size λrgt.key λrgt.val λrgt.lft λrgt.rgt λkey λval λlft - //use b = (BBT.new_node K V key val lft rgt.lft) - //use a = (BBT.new_node K V rgt.key rgt.val b rgt.rgt) - //a - //use tip = λkey λval λlft - //(BBT.bin K V size key val lft (BBT.tip K V)) - //(~rgt P bin tip key val lft) diff --git a/book/BBT/new_node.kind2 b/book/BBT/new_node.kind2 deleted file mode 100644 index 7048b16a..00000000 --- a/book/BBT/new_node.kind2 +++ /dev/null @@ -1,30 +0,0 @@ -use BBT/{bin} - -new_node (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V)) : (BBT K V) = - match lft_size = (BBT/got_size lft) { - Pair/new: match rgt_size = (BBT/got_size rgt) { - Pair/new: - use new_size = (+ 1 (U60/max lft_size.fst rgt_size.fst)) - (bin K V new_size key val lft rgt) - } - } - - - -//BBT.new_node -//: ∀(K: *) - //∀(V: *) - //∀(key: K) - //∀(val: V) - //∀(lft: (BBT K V)) - //∀(rgt: (BBT K V)) - //(BBT K V) -//= λK λV λkey λval λlft λrgt - //use P = λx (BBT K V) - //use new = λlft.size λlft - //use P = λx (BBT K V) - //use new = λrgt.size λrgt - //use new_size = (+ 1 (U60.max rgt.size lft.size)) - //(BBT.bin K V new_size key val lft rgt) - //(~(BBT.got_size K V rgt) P new) - //(~(BBT.got_size K V lft) P new) diff --git a/book/BBT/rgt_rotate.kind2 b/book/BBT/rgt_rotate.kind2 deleted file mode 100644 index 765f7ee5..00000000 --- a/book/BBT/rgt_rotate.kind2 +++ /dev/null @@ -1,31 +0,0 @@ -use BBT/{bin,tip} - -rgt_rotate (size: U60) (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V)) : (BBT K V) = - match lft { - bin: - use b = (BBT/new_node key val lft.rgt rgt) - use a = (BBT/new_node lft.key lft.val lft.lft b) - a - tip: (bin K V size key val (tip K V) rgt) - } - - - -//BBT.rgt_rotate -//: ∀(K: *) - //∀(V: *) - //∀(size: U60) - //∀(key: K) - //∀(val: V) - //∀(lft: (BBT K V)) - //∀(rgt: (BBT K V)) - //(BBT K V) -//= λK λV λsize λkey λval λlft λrgt - //use P = λx ∀(key: K) ∀(val: V) ∀(rgt: (BBT K V)) (BBT K V) - //use bin = λ_size λlft.key λlft.val λlft.lft λlft.rgt λkey λval λrgt - //use b = (BBT.new_node K V key val lft.rgt rgt) - //use a = (BBT.new_node K V lft.key lft.val lft.lft b) - //a - //use tip = λkey λval λrgt - //(BBT.bin K V size key val (BBT.tip K V) rgt) - //(~lft P bin tip key val rgt) diff --git a/book/BBT/set.kind2 b/book/BBT/set.kind2 deleted file mode 100644 index 05578d98..00000000 --- a/book/BBT/set.kind2 +++ /dev/null @@ -1,81 +0,0 @@ -use BBT/{bin,tip} -use Cmp/{ltn,eql,gtn} - -set (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (val: V) (map: (BBT K V)) : (BBT K V) = - match map { - bin: - match _ = (cmp key map.key) { - ltn: - use new_lft = (set cmp key val map.lft) - (BBT/balance cmp key map.key map.val new_lft map.rgt) - eql: (bin K V map.size map.key val map.lft map.rgt) - gtn: - use new_rgt = (set cmp key val map.rgt) - (BBT/balance cmp key map.key map.val map.lft new_rgt) - } - tip: (BBT/singleton key val) - } - - - -//BBT.set -//: ∀(K: *) - //∀(V: *) - //∀(cmp: ∀(a: K) ∀(b: K) Cmp) - //∀(key: K) - //∀(val: V) - //∀(map: (BBT K V)) - //(BBT K V) -//= λK λV λcmp λkey λval λmap - //use P = λx ∀(key: K) ∀(val: V) (BBT K V) - //use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt λkey λval - //use P = λx - //∀(key: K) - //∀(next.key: K) - //∀(next.val: V) - //∀(next.lft: (BBT K V)) - //∀(next.rgt: (BBT K V)) - //∀(key: K) - //∀(val: V) - //(BBT K V) - //use ltn = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval - //use new_lft = (BBT.set K V cmp key val next.lft) - //(BBT.balance - //K - //V - //cmp - //key - //next.key - //next.val - //new_lft - //next.rgt - //) - //use eql = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval - //(BBT.bin K V size next.key val next.lft next.rgt) - //use gtn = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval - //use new_rgt = (BBT.set K V cmp key val next.rgt) - //(BBT.balance - //K - //V - //cmp - //key - //next.key - //next.val - //next.lft - //new_rgt - //) - //(~(cmp key next.key) - //P - //ltn - //eql - //gtn - //key - //next.key - //next.val - //next.lft - //next.rgt - //key - //val - //) - //use tip = λkey λval (BBT.singleton K V key val) - //(~map P bin tip key val) diff --git a/book/BBT/singleton.kind2 b/book/BBT/singleton.kind2 deleted file mode 100644 index d4524f51..00000000 --- a/book/BBT/singleton.kind2 +++ /dev/null @@ -1,10 +0,0 @@ -singleton (key: K) (val: V) : (BBT K V) = - use tip = (BBT/tip K V) - (BBT/bin K V 1 key val tip tip) - - - -//BBT.singleton -//: ∀(K: *) ∀(V: *) ∀(key: K) ∀(val: V) (BBT K V) -//= λK λV λkey λval - //(BBT.bin K V 1 key val (BBT.tip K V) (BBT.tip K V)) diff --git a/book/BBT/tip.kind2 b/book/BBT/tip.kind2 deleted file mode 100644 index 7c421a82..00000000 --- a/book/BBT/tip.kind2 +++ /dev/null @@ -1,3 +0,0 @@ -BBT.tip -: ∀(K: *) ∀(V: *) (BBT K V) -= λK λV ~λP λbin λtip tip diff --git a/book/BBT/to_list.kind2 b/book/BBT/to_list.kind2 deleted file mode 100644 index 63ac28c3..00000000 --- a/book/BBT/to_list.kind2 +++ /dev/null @@ -1,32 +0,0 @@ -use BBT/{bin,tip} - -to_list (map: (BBT K V)) : (List (Pair K V)) = - match map { - bin: - use lft = (to_list map.lft) - use rgt = (to_list map.rgt) - use pair = (Pair/new map.key map.val) - use list = (List/cons pair (List/concat lft rgt)) - list - tip: List/nil - } - - - -//BBT.to_list -//: ∀(K: *) ∀(V: *) ∀(map: (BBT K V)) - //(List (Pair K V)) -//= λK λV λmap - //use P = λx (List (Pair K V)) - //use bin = λsize λkey λval λlft λrgt - //use lft = (BBT.to_list K V lft) - //use rgt = (BBT.to_list K V rgt) - //use pair = (Pair.new K V key val) - //use list = (List.cons - //(Pair K V) - //pair - //(List.concat (Pair K V) lft rgt) - //) - //list - //use tip = (List.nil (Pair K V)) - //(~map P bin tip) diff --git a/book/BMap.kind2 b/book/BMap/_.kind2 similarity index 79% rename from book/BMap.kind2 rename to book/BMap/_.kind2 index 9c7a378e..ab25b14d 100644 --- a/book/BMap.kind2 +++ b/book/BMap/_.kind2 @@ -1,3 +1,3 @@ -data BMap A +data BMap | node (lft: (BMap A)) (val: A) (rgt: (BMap A)) | leaf diff --git a/book/BMap/leaf.kind2 b/book/BMap/leaf.kind2 index b02c535f..114936a6 100644 --- a/book/BMap/leaf.kind2 +++ b/book/BMap/leaf.kind2 @@ -1,3 +1,3 @@ -BMap.leaf +BMap/leaf : ∀(A: *) (BMap A) = λA ~λP λnode λleaf leaf diff --git a/book/BMap/node.kind2 b/book/BMap/node.kind2 index 956e54f9..9c835809 100644 --- a/book/BMap/node.kind2 +++ b/book/BMap/node.kind2 @@ -1,4 +1,4 @@ -BMap.node +BMap/node : ∀(A: *) ∀(lft: (BMap A)) ∀(val: A) diff --git a/book/Bool.kind2 b/book/Bool/_.kind2 similarity index 100% rename from book/Bool.kind2 rename to book/Bool/_.kind2 diff --git a/book/Bool/and.kind2 b/book/Bool/and.kind2 index c3d9ba8a..1eb7f560 100644 --- a/book/Bool/and.kind2 +++ b/book/Bool/and.kind2 @@ -2,6 +2,6 @@ use Bool/{true,false,and} and (a: Bool) (b: Bool) : Bool = match a { - true: "foo" + true: b false: false } diff --git a/book/Bool/lemma/double_negation.kind2 b/book/Bool/lemma/double_negation.kind2 index 05ae3109..61d980a7 100644 --- a/book/Bool/lemma/double_negation.kind2 +++ b/book/Bool/lemma/double_negation.kind2 @@ -1,4 +1,7 @@ use Bool/{true,false,not} double_negation (x: Bool) : (Equal Bool (not (not x)) x) = - ?a + match x { + true : {=} + false: {=} + } diff --git a/book/Char.kind2 b/book/Char/_.kind2 similarity index 100% rename from book/Char.kind2 rename to book/Char/_.kind2 diff --git a/book/Cmp.kind2 b/book/Cmp/_.kind2 similarity index 100% rename from book/Cmp.kind2 rename to book/Cmp/_.kind2 diff --git a/book/Empty.kind2 b/book/Empty/_.kind2 similarity index 100% rename from book/Empty.kind2 rename to book/Empty/_.kind2 diff --git a/book/Equal.kind2 b/book/Equal/_.kind2 similarity index 100% rename from book/Equal.kind2 rename to book/Equal/_.kind2 diff --git a/book/Equal/match.kind2 b/book/Equal/match.kind2 index 96cd6875..565cc699 100644 --- a/book/Equal/match.kind2 +++ b/book/Equal/match.kind2 @@ -4,15 +4,3 @@ match (e: (Equal T a b)) : (P a b e) = (~e P refl) - -can you understand this? - -Yes, this appears to be a dependently-typed pattern matching function, likely written in a language similar to Idris, Agda, or Coq. It's implementing the principle of indiscernibility of identicals, also known as Leibniz's law. Here's a brief explanation: - -1. It takes two values `a` and `b` of some type `T`. -2. It takes a predicate `P` that depends on two values of type `T` and a proof of their equality. -3. It takes a proof `refl` that the predicate holds for any value `x` when compared to itself. -4. It takes a proof `e` that `a` and `b` are equal. -5. It returns a proof that the predicate `P` holds for `a`, `b`, and the equality proof `e`. - -The implementation uses the equality proof `e` to rewrite the goal, effectively turning it into `P a a (Equal/refl/ T a)`, which can be solved by the `refl` argument. diff --git a/book/IO.kind2 b/book/IO/_.kind2 similarity index 100% rename from book/IO.kind2 rename to book/IO/_.kind2 diff --git a/book/Kind.kind2 b/book/Kind/_.kind2 similarity index 100% rename from book/Kind.kind2 rename to book/Kind/_.kind2 diff --git a/book/List.kind2 b/book/List/_.kind2 similarity index 100% rename from book/List.kind2 rename to book/List/_.kind2 diff --git a/book/Maybe.kind2 b/book/Maybe/_.kind2 similarity index 58% rename from book/Maybe.kind2 rename to book/Maybe/_.kind2 index b0278c0d..1e5bf49f 100644 --- a/book/Maybe.kind2 +++ b/book/Maybe/_.kind2 @@ -1,3 +1,3 @@ -data Maybe T +data Maybe | some (value: T) | none diff --git a/book/Monad.kind2 b/book/Monad/_.kind2 similarity index 100% rename from book/Monad.kind2 rename to book/Monad/_.kind2 diff --git a/book/Nat.kind2 b/book/Nat/_.kind2 similarity index 100% rename from book/Nat.kind2 rename to book/Nat/_.kind2 diff --git a/book/Nat/is_zero.kind2 b/book/Nat/is_zero.kind2 new file mode 100644 index 00000000..5a6fbfd7 --- /dev/null +++ b/book/Nat/is_zero.kind2 @@ -0,0 +1,167 @@ +// EXAMPLES IN BEND LANG + +type Map_: + Free + Used + Both {~a, ~b} + +type Arr: + Null + Leaf {~a} + Node {~a, ~b} + +def swap(s, a, b): + switch s: + case 0: + return Map_/Both{ a: a, b: b } + case _: + return Map_/Both{ a: b, b: a } + + +# Sort : Arr -> Arr +def sort(t): + return to_arr(0, to_map(t)) + +# ToMap : Arr -> Map +def to_map(t): + match t: + case Arr/Null: + return Map_/Free + case Arr/Leaf: + return radix(t.a) + case Arr/Node: + return merge(to_map(t.a), to_map(t.b)) + +# ToArr : U60 -> Map -> Arr +def to_arr(x, m): + match m: + case Map_/Free: + return Arr/Null + case Map_/Used: + return Arr/Leaf{ a: x } + case Map_/Both: + return Arr/Node{ a: to_arr(x * 2, m.a), b: to_arr(x * 2 + 1, m.b) } + +# Merge : Map -> Map -> Map +def merge(a, b): + match a: + case Map_/Free: + return b + case Map_/Used: + return Map_/Used + case Map_/Both: + match b: + case Map_/Free: + return a + case Map_/Used: + return Map_/Used + case Map_/Both: + return Map_/Both{ a: merge(a.a, b.a), b: merge(a.b, b.b) } + +# Radix : U60 -> Map +def radix(n): + r = Map_/Used + r = swap(n & 1, r, Map_/Free) + r = swap(n & 2, r, Map_/Free) + r = swap(n & 4, r, Map_/Free) + r = swap(n & 8, r, Map_/Free) + r = swap(n & 16, r, Map_/Free) + r = swap(n & 32, r, Map_/Free) + r = swap(n & 64, r, Map_/Free) + r = swap(n & 128, r, Map_/Free) + r = swap(n & 256, r, Map_/Free) + r = swap(n & 512, r, Map_/Free) + return radix2(n, r) + +# At the moment, we need to manually break very large functions into smaller ones +# if we want to run this program on the GPU. +# In a future version of Bend, we will be able to do this automatically. +def radix2(n, r): + r = swap(n & 1024, r, Map_/Free) + r = swap(n & 2048, r, Map_/Free) + r = swap(n & 4096, r, Map_/Free) + r = swap(n & 8192, r, Map_/Free) + r = swap(n & 16384, r, Map_/Free) + r = swap(n & 32768, r, Map_/Free) + r = swap(n & 65536, r, Map_/Free) + r = swap(n & 131072, r, Map_/Free) + r = swap(n & 262144, r, Map_/Free) + r = swap(n & 524288, r, Map_/Free) + return radix3(n, r) + +def radix3(n, r): + r = swap(n & 1048576, r, Map_/Free) + r = swap(n & 2097152, r, Map_/Free) + r = swap(n & 4194304, r, Map_/Free) + r = swap(n & 8388608, r, Map_/Free) + return r + +def reverse(t): + match t: + case Arr/Null: + return Arr/Null + case Arr/Leaf: + return t + case Arr/Node: + return Arr/Node{ a: reverse(t.b), b: reverse(t.a) } + +# Sum : Arr -> U60 +def sum(t): + match t: + case Arr/Null: + return 0 + case Arr/Leaf: + return t.a + case Arr/Node: + return sum(t.a) + sum(t.b) + +# Gen : U60 -> Arr +def gen(n): + return gen_go(n, 0) + +def gen_go(n, x): + switch n: + case 0: + return Arr/Leaf{ a: x } + case _: + a = x * 2 + b = x * 2 + 1 + return Arr/Node{ a: gen_go(n-1, a), b: gen_go(n-1, b) } + +Main = (sum (sort(reverse(gen 4)))) + +// FUNCTION IN KIND LANG + +use Nat/{succ,zero} + +is_zero (a: Nat) : String = + match a { + zero: "é zero" + succ: "não é zero" + } + +// TASK: translate this kind function to bend + + + +def is_zero(a): + match a: + case Nat/zero: + return "é zero" + case Nat/succ: + return "não é zero" + + + + + + + + + + + + + + + diff --git a/book/Pair.kind2 b/book/Pair/_.kind2 similarity index 60% rename from book/Pair.kind2 rename to book/Pair/_.kind2 index 7cada691..3b5bdbbe 100644 --- a/book/Pair.kind2 +++ b/book/Pair/_.kind2 @@ -1,2 +1,2 @@ -data Pair A B +data Pair | new (fst: A) (snd: B) : (Pair A B) diff --git a/book/Parser.kind2 b/book/Parser/_.kind2 similarity index 100% rename from book/Parser.kind2 rename to book/Parser/_.kind2 diff --git a/book/QBool.kind2 b/book/QBool/_.kind2 similarity index 100% rename from book/QBool.kind2 rename to book/QBool/_.kind2 diff --git a/book/QBool2.kind2 b/book/QBool2/_.kind2 similarity index 100% rename from book/QBool2.kind2 rename to book/QBool2/_.kind2 diff --git a/book/QUnit.kind2 b/book/QUnit/_.kind2 similarity index 100% rename from book/QUnit.kind2 rename to book/QUnit/_.kind2 diff --git a/book/Sigma.kind2 b/book/Sigma/_.kind2 similarity index 100% rename from book/Sigma.kind2 rename to book/Sigma/_.kind2 diff --git a/book/String.kind2 b/book/String/_.kind2 similarity index 100% rename from book/String.kind2 rename to book/String/_.kind2 diff --git a/book/The.kind2 b/book/The/_.kind2 similarity index 100% rename from book/The.kind2 rename to book/The/_.kind2 diff --git a/book/Tree.kind2 b/book/Tree/_.kind2 similarity index 100% rename from book/Tree.kind2 rename to book/Tree/_.kind2 diff --git a/book/U60/abs_diff.kind2 b/book/U60/abs_diff.kind2 index 86949003..a78d3822 100644 --- a/book/U60/abs_diff.kind2 +++ b/book/U60/abs_diff.kind2 @@ -1,7 +1,7 @@ use Bool/{true,false} abs_diff (a: U60) (b: U60) : U60 = - match x = (U60/to_bool (< a b)) { + match Bool/true { true: (- b a) false: (- a b) } diff --git a/book/U60/name.kind2 b/book/U60/name.kind2 index fb081d25..114e5877 100644 --- a/book/U60/name.kind2 +++ b/book/U60/name.kind2 @@ -1,2 +1,2 @@ -U60.name (n: U60) : String = +U60/name (n: U60) : String = (String/Chunk/build (U60/name/go (+ n 1))) diff --git a/book/U60/show.kind2 b/book/U60/show.kind2 index e4af9f75..73794244 100644 --- a/book/U60/show.kind2 +++ b/book/U60/show.kind2 @@ -1,2 +1,2 @@ -U60.show (n: U60) : String = +U60/show (n: U60) : String = (String/Chunk/build (U60/show/go n)) diff --git a/book/Unit.kind2 b/book/Unit/_.kind2 similarity index 100% rename from book/Unit.kind2 rename to book/Unit/_.kind2 diff --git a/book/Vector.kind2 b/book/Vector/_.kind2 similarity index 100% rename from book/Vector.kind2 rename to book/Vector/_.kind2 diff --git a/book/foo.ts b/book/foo.ts new file mode 100644 index 00000000..26a66575 --- /dev/null +++ b/book/foo.ts @@ -0,0 +1,9 @@ +// create a function in typescript with + +function foo(n: number) : string { + return "foo"; +} + +let x : any = "bar"; + +console.log(foo(x)); diff --git a/book/_OBLITERATE.kind2 b/book/tmp/_OBLITERATE.kind2 similarity index 100% rename from book/_OBLITERATE.kind2 rename to book/tmp/_OBLITERATE.kind2 diff --git a/book/_err.txt b/book/tmp/_err.txt similarity index 100% rename from book/_err.txt rename to book/tmp/_err.txt diff --git a/book/_main b/book/tmp/_main similarity index 100% rename from book/_main rename to book/tmp/_main diff --git a/book/_main.hvm2 b/book/tmp/_main.hvm2 similarity index 100% rename from book/_main.hvm2 rename to book/tmp/_main.hvm2 diff --git a/book/_main.hvmc b/book/tmp/_main.hvmc similarity index 100% rename from book/_main.hvmc rename to book/tmp/_main.hvmc diff --git a/book/_main.js b/book/tmp/_main.js similarity index 100% rename from book/_main.js rename to book/tmp/_main.js diff --git a/book/_main.kind2 b/book/tmp/_main.kind2 similarity index 100% rename from book/_main.kind2 rename to book/tmp/_main.kind2 diff --git a/book/test0.kind2 b/book/tmp/test0.kind2 similarity index 100% rename from book/test0.kind2 rename to book/tmp/test0.kind2 diff --git a/book/test1.kind2 b/book/tmp/test1.kind2 similarity index 100% rename from book/test1.kind2 rename to book/tmp/test1.kind2 diff --git a/book/test10.kind2 b/book/tmp/test10.kind2 similarity index 100% rename from book/test10.kind2 rename to book/tmp/test10.kind2 diff --git a/book/test11.kind2 b/book/tmp/test11.kind2 similarity index 100% rename from book/test11.kind2 rename to book/tmp/test11.kind2 diff --git a/book/test2.kind2 b/book/tmp/test2.kind2 similarity index 100% rename from book/test2.kind2 rename to book/tmp/test2.kind2 diff --git a/book/test3.kind2 b/book/tmp/test3.kind2 similarity index 100% rename from book/test3.kind2 rename to book/tmp/test3.kind2 diff --git a/book/test4.kind2 b/book/tmp/test4.kind2 similarity index 100% rename from book/test4.kind2 rename to book/tmp/test4.kind2 diff --git a/book/test5.kind2 b/book/tmp/test5.kind2 similarity index 100% rename from book/test5.kind2 rename to book/tmp/test5.kind2 diff --git a/book/test6.kind2 b/book/tmp/test6.kind2 similarity index 100% rename from book/test6.kind2 rename to book/tmp/test6.kind2 diff --git a/book/test7.kind2 b/book/tmp/test7.kind2 similarity index 100% rename from book/test7.kind2 rename to book/tmp/test7.kind2 diff --git a/book/test8.kind2 b/book/tmp/test8.kind2 similarity index 100% rename from book/test8.kind2 rename to book/tmp/test8.kind2 diff --git a/book/test9.kind2 b/book/tmp/test9.kind2 similarity index 100% rename from book/test9.kind2 rename to book/tmp/test9.kind2 diff --git a/book/testBBT.kind2 b/book/tmp/testBBT.kind2 similarity index 100% rename from book/testBBT.kind2 rename to book/tmp/testBBT.kind2 diff --git a/src/book/mod.rs b/src/book/mod.rs index 334ead78..9617028d 100644 --- a/src/book/mod.rs +++ b/src/book/mod.rs @@ -64,7 +64,13 @@ impl Book { if !self.defs.contains_key(name) { // Parses a file into a new book let file = format!("{}/{}.kind2", base, name); - let text = std::fs::read_to_string(&file).map_err(|_| format!("Could not read file: {}", file))?; + let text = match std::fs::read_to_string(&file) { + Ok(content) => content, + Err(_) => { + let backup_file = format!("{}/{}/_.kind2", base, name); + std::fs::read_to_string(&backup_file).map_err(|_| format!("Could not read file: {} or {}", file, backup_file))? + } + }; let fid = self.get_file_id(&file); let defs = KindParser::new(&text).parse_book(name, fid)?; // Merges new book into book diff --git a/src/info/mod.rs b/src/info/mod.rs index 8bf7bfa8..6d71a4a0 100644 --- a/src/info/mod.rs +++ b/src/info/mod.rs @@ -53,7 +53,9 @@ impl Info { let det = format!("- detected: \x1b[31m{}\x1b[0m", det.show()); let bad = format!("- bad_term: \x1b[2m{}\x1b[0m", bad.show()); let file = book.get_file_name(src.fid).unwrap_or_else(|| "unknown_file".to_string()); - let text = std::fs::read_to_string(&file).unwrap_or_else(|_| "Could not read source file.".to_string()); + let text = std::fs::read_to_string(&file) + .or_else(|_| std::fs::read_to_string(format!("{}/_.kind2", file))) + .unwrap_or_else(|_| "Could not read source file.".to_string()); let orig = highlight_error(src.ini as usize, src.end as usize, &text); let src = format!("\x1b[4m{}\x1b[0m\n{}", file, orig); format!("\x1b[1mERROR:\x1b[0m\n{}\n{}\n{}\n{}", exp, det, bad, src) diff --git a/src/kindc.hs b/src/kindc.hs index 07ff5a33..3f51b4aa 100644 --- a/src/kindc.hs +++ b/src/kindc.hs @@ -200,9 +200,9 @@ bind term = go term [] where -- ---------- -- Evaluation levels: --- - 0: reduces refs never --- - 1: reduces refs on redexes --- - 2: reduces refs always +-- - 0: reduces refs: never +-- - 1: reduces refs: redexes +-- - 2: reduces refs: always reduce :: Book -> Fill -> Int -> Term -> Term reduce book fill lv (App fun arg) = reduceApp book fill lv (reduce book fill lv fun) arg @@ -315,15 +315,16 @@ normal book fill lv term dep = normalGo book fill lv (reduce book fill lv term) equal :: Term -> Term -> Int -> Env Bool equal a b dep = do - book <- envGetBook - fill <- envGetFill - let a' = reduce book fill 2 a - let b' = reduce book fill 2 b - same <- tryIdentical a' b' dep - if same then do - return True - else do - similar a' b' dep + -- trace ("= " ++ termStr a dep ++ "\n? " ++ termStr b dep) $ do + book <- envGetBook + fill <- envGetFill + let a' = reduce book fill 2 a + let b' = reduce book fill 2 b + same <- tryIdentical a' b' dep + if same then do + return True + else do + similar a' b' dep tryIdentical :: Term -> Term -> Int -> Env Bool tryIdentical a b dep = do @@ -802,7 +803,7 @@ checkDef (Ref nam) = do Just val -> case val of Ann chk val typ -> check 0 val typ 0 >> return () Ref nm2 -> checkDef (Ref nm2) - _ -> trace ("oxi" ++ termStr val 0) $ infer val 0 >> return () + _ -> infer val 0 >> return () Nothing -> do envLog (Error 0 (Hol "undefined_reference" []) (Hol "unknown_type" []) (Ref nam) 0) envFail @@ -901,7 +902,7 @@ contextStrAnn book fill term dep = termStr (normal book fill 0 term infoStr :: Book -> Fill -> Info -> String infoStr book fill (Found name typ ctx dep) = - let typ' = termStr (normal book fill 1 typ dep) dep + let typ' = termStr (normal book fill 0 typ dep) dep ctx' = drop 1 (contextStr book fill ctx dep) in concat ["#found{", name, " ", typ', " [", ctx', "]}"] infoStr book fill (Error src expected detected value dep) = @@ -930,6 +931,7 @@ parseTerm :: P.Parsec String () Term parseTerm = P.choice [ parseAll , parseLam + , parseOp2 , parseApp , parseAnn , parseSlf @@ -937,9 +939,7 @@ parseTerm = P.choice , parseUse , parseLet , parseSet - , parseU60 , parseNum - , parseOp2 , parseSwi , parseTxt , parseNat @@ -1003,7 +1003,11 @@ parseIns = do val <- parseTerm return $ Ins val -parseRef = Ref <$> parseName +parseRef = do + name <- parseName + return $ case name of + "U60" -> U60 + _ -> Ref name parseUse = do P.try (P.string "use ") @@ -1033,13 +1037,13 @@ parseLet = do parseSet = P.char '*' >> return Set -parseU60 = P.try $ P.string "U60" >> return U60 - parseNum = Num . read <$> P.many1 P.digit parseOp2 = do - P.char '(' - opr <- parseOper + opr <- P.try $ do + P.string "(" + opr <- parseOper + return opr P.spaces fst <- parseTerm P.spaces @@ -1108,7 +1112,7 @@ parseSrc = do parseName :: P.Parsec String () String parseName = do head <- P.letter - tail <- P.many (P.alphaNum <|> P.char '/' <|> P.char '.' <|> P.char '_') + tail <- P.many (P.alphaNum <|> P.char '/' <|> P.char '.' <|> P.char '_' <|> P.char '-') return (head : tail) parseOper = P.choice @@ -1117,12 +1121,12 @@ parseOper = P.choice , P.string "*" >> return MUL , P.string "/" >> return DIV , P.string "%" >> return MOD + , P.string "<" >> return LT + , P.string ">" >> return GT , P.string "==" >> return EQ , P.string "!=" >> return NE , P.string "<=" >> return LTE , P.string ">=" >> return GTE - , P.string "<" >> return LT - , P.string ">" >> return GT , P.string "&" >> return AND , P.string "|" >> return OR , P.string "^" >> return XOR