diff savida

Cargo.lock

@@ -4,9 +4,9 @@ version = 3
 
 [[package]]
 name = "TSPL"
-version = "0.0.8"
+version = "0.0.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1cf26cc6171f5f62baf926d04bc23eab3412598d76908fff83fda919bba486f0"
+checksum = "5a9423b1e6e2d6c0bbc03660f58f9c30f55359e13afea29432e6e767c0f7dc25"
 dependencies = [
  "highlight_error",
 ]

Cargo.toml

@@ -8,7 +8,7 @@ name = "kind2"
 path = "src/main.rs"
 
 [dependencies]
-TSPL = "0.0.8"
+TSPL = "0.0.9"
 highlight_error = "0.1.1"
 im = "15.1.0"
 clap = "4.5.2"

README.md

@@ -78,26 +78,22 @@ data List T
 | nil
 
 // Applies a function to all elements of a list
-map A B (f: ∀(x: A) B) (xs: (List A)) : (List B) =
-  match xs {
-    cons:
-      let head = (f xs.head)
-      let tail = (map _ _ f xs.tail)
-      (cons _ head tail)
-    nil:
-      []
+map <A> <B> (xs: (List A)) (f: A -> B) : (List B) =
+  fold xs {
+    ++: (f xs.head) ++ xs.tail
+    []: []
   }
 ```
 
 ### Theorems and Proofs:
 
 ```javascript
-use Nat.{succ,zero,half,double}
+use Nat/{succ,zero,half,double}
 
 // Proof that `∀n. n*2/2 = n`
-bft (n: Nat) : {(half (double n)) = n} =
+bft (n: Nat) : (half (double n)) == n =
   match n {
-    succ: (Equal.apply _ _ succ _ _ (bft n.pred))
+    succ: (Equal/apply succ (bft n.pred))
     zero: {=}
   }
 ```

book/Bool.if.kind2

@@ -1,5 +0,0 @@
-Bool.if (b: Bool) (P: *) (t: P) (f: P) : P =
-  match b {
-    Bool.true: t
-    Bool.false: f
-  }

book/Bool.lemma.notnot.kind2

@@ -1,7 +0,0 @@
-use Bool.{true,false,not}
-
-notnot (x: Bool) : (not (not x)) == x =
-  match x {
-    true: {=}
-    false: {=}
-  }

book/Bool.match.kind2

@@ -1,7 +0,0 @@
-Bool.match
-  (b: Bool)
-  (P: ∀(x: Bool) *)
-  (t: (P Bool.true))
-  (f: (P Bool.false))
-: (P b)
-= (~b P t f)

book/Bool.not.kind2

@@ -1,7 +0,0 @@
-use Bool.{true,false}
-
-Bool.not (x: Bool) : Bool =
-  match x {
-    true: false
-    false: true
-  }

book/Bool.or.kind2

@@ -1,7 +0,0 @@
-use Bool.{true,false}
-
-Bool.or (a: Bool) (b: Bool) : Bool =
-  match a {
-    true: true
-    false: b
-  }

book/Bool.show.kind2

@@ -1,5 +0,0 @@
-Bool.show (x: Bool) : String =
-  match x {
-    Bool.true: "true"
-    Bool.false: "false"
-  }

book/Bool.true.kind2

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

book/Bool/and.kind2

@@ -1,4 +1,4 @@
-use Bool.{true,false,and}
+use Bool/{true,false,and}
 
 and (a: Bool) (b: Bool) : Bool =
   match b {

book/Bool/if.kind2

@@ -0,0 +1,7 @@
+use Bool/{true,false}
+
+if (b: Bool) (P: *) (t: P) (f: P) : P =
+  match b {
+    true: t
+    false: f
+  }

book/Bool/lemma/double_negation.kind2

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

book/Bool/match.kind2

@@ -0,0 +1,9 @@
+use Bool/{true,false}
+
+match
+  (b: Bool)
+  (P: ∀(x: Bool) *)
+  (t: (P true))
+  (f: (P false))
+: (P b)
+= (~b P t f)

book/Bool/not.kind2

@@ -0,0 +1,7 @@
+use Bool/{true,false}
+
+not (x: Bool) : Bool =
+  match x {
+    true: false
+    false: true
+  }

book/Bool/or.kind2

@@ -0,0 +1,7 @@
+use Bool/{true,false}
+
+or (a: Bool) (b: Bool) : Bool =
+  match a {
+    true: true
+    false: b
+  }

book/Bool/show.kind2

@@ -0,0 +1,7 @@
+use Bool/{true,false}
+
+show (x: Bool) : String =
+  match x {
+    true: "true"
+    false: "false"
+  }

book/Bool/true.kind2

@@ -0,0 +1,2 @@
+true : Bool =
+  ~λP λt λf t

book/Char.equal.kind2

@@ -1,2 +0,0 @@
-Char.equal (a: Char) (b: Char) : Bool =
-  (U60.equal a b)

book/Char.escapes.kind2

@@ -1,14 +0,0 @@
-Char.escapes
-: (List (Pair Char Char))
-= [
-  (Pair.new _ _ 98 8)
-  (Pair.new _ _ 102 12)
-  (Pair.new _ _ 110 10)
-  (Pair.new _ _ 114 13)
-  (Pair.new _ _ 116 9)
-  (Pair.new _ _ 118 11)
-  (Pair.new _ _ 92 92)
-  (Pair.new _ _ 34 34)
-  (Pair.new _ _ 48 0)
-  (Pair.new _ _ 39 39)
-]

book/Char.is_between.kind2

@@ -1,5 +0,0 @@
-Char.is_between (min: Char) (max: Char) (chr: Char) : Bool
-= (Bool.and
-    (U60.to_bool (>= chr min))
-    (U60.to_bool (<= chr max))
-  )

book/Char.is_blank.kind2

@@ -1,2 +0,0 @@
-Char.is_blank (a: Char) : Bool =
-  (Bool.or (Char.equal a 10) (Char.equal a 32))

book/Char.is_decimal.kind2

@@ -1,2 +0,0 @@
-Char.is_decimal (a: Char) : Bool =
-  (Char.is_between 48 57 a)

book/Char.is_name.kind2

@@ -1,21 +0,0 @@
-Char.is_name
-: ∀(a: Char) Bool
-= λa
-  (Bool.or
-    (Char.is_between 97 122 a)
-    (Bool.or
-      (Char.is_between 65 90 a)
-      (Bool.or
-        (Char.is_between 48 57 a)
-        (Bool.or
-          (Char.equal 95 a)
-          (Bool.or
-            (Char.equal 46 a)
-            (Bool.or (Char.equal 45 a) Bool.false)
-          )
-        )
-      )
-    )
-  )
-
-

book/Char.is_newline.kind2

@@ -1,3 +0,0 @@
-Char.is_newline
-: ∀(a: Char) Bool
-= λa (Char.equal a 10)

book/Char.is_oper.kind2

@@ -1,40 +0,0 @@
-Char.is_oper
-: ∀(a: Char) Bool
-= λa
-  (Bool.or
-    (Char.equal 43 a)
-    (Bool.or
-      (Char.equal 45 a)
-      (Bool.or
-        (Char.equal 42 a)
-        (Bool.or
-          (Char.equal 47 a)
-          (Bool.or
-            (Char.equal 37 a)
-            (Bool.or
-              (Char.equal 60 a)
-              (Bool.or
-                (Char.equal 62 a)
-                (Bool.or
-                  (Char.equal 61 a)
-                  (Bool.or
-                    (Char.equal 38 a)
-                    (Bool.or
-                      (Char.equal 124 a)
-                      (Bool.or
-                        (Char.equal 94 a)
-                        (Bool.or
-                          (Char.equal 33 a)
-                          (Bool.or (Char.equal 126 a) Bool.false)
-                        )
-                      )
-                    )
-                  )
-                )
-              )
-            )
-          )
-        )
-      )
-    )
-  )

book/Char.is_slash.kind2

@@ -1,3 +0,0 @@
-Char.is_slash
-: ∀(a: Char) Bool
-= λa (Char.equal a 47)

book/Char.slash.kind2

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

book/Char/equal.kind2

@@ -0,0 +1,2 @@
+equal (a: Char) (b: Char) : Bool =
+  (U60/equal a b)

book/Char/escapes.kind2

@@ -0,0 +1,15 @@
+use Pair/{new}
+
+escapes : (List (Pair Char Char)) =
+  [
+    (new 98 8)
+    (new 102 12)
+    (new 110 10)
+    (new 114 13)
+    (new 116 9)
+    (new 118 11)
+    (new 92 92)
+    (new 34 34)
+    (new 48 0)
+    (new 39 39)
+  ]

book/Char/is_between.kind2

@@ -0,0 +1,4 @@
+is_between (min: Char) (max: Char) (chr: Char) : Bool =
+  (Bool/and
+    (U60/to_bool (>= chr min))
+    (U60/to_bool (<= chr max)))

book/Char/is_blank.kind2

@@ -0,0 +1,2 @@
+is_blank (a: Char) : Bool =
+  (Bool/or (Char/equal a 10) (Char/equal a 32))

book/Char/is_decimal.kind2

@@ -0,0 +1,2 @@
+is_decimal (a: Char) : Bool =
+  (Char/is_between 48 57 a)

book/Char/is_name.kind2

@@ -0,0 +1,13 @@
+use Bool/{true,false,or}
+use Char/{is_between,equal}
+
+is_name (a: Char) : Bool =
+  (or (is_between 97 122 a)
+  (or (is_between 65 90 a)
+  (or (is_between 48 57 a)
+  (or (equal 95 a)
+  (or (equal 46 a)
+  (or (equal 45 a)
+  false))))))
+
+

book/Char/is_newline.kind2

@@ -0,0 +1,2 @@
+is_newline (a: Char) : Bool =
+  (Char/equal a 10)

book/Char/is_oper.kind2

@@ -0,0 +1,18 @@
+use Bool/{true,false,or}
+use Char/{equal}
+
+is_oper (a: Char) : Bool =
+  (or (equal 43 a)
+  (or (equal 45 a)
+  (or (equal 42 a)
+  (or (equal 47 a)
+  (or (equal 37 a)
+  (or (equal 60 a)
+  (or (equal 62 a)
+  (or (equal 61 a)
+  (or (equal 38 a)
+  (or (equal 124 a)
+  (or (equal 94 a)
+  (or (equal 33 a)
+  (or (equal 126 a)
+  false)))))))))))))

book/Char/is_slash.kind2

@@ -0,0 +1,2 @@
+is_slash (a: Char) : Bool =
+  (Char/equal a 47)

book/Char/slash.kind2

@@ -0,0 +1,2 @@
+slash : Char =
+  47

book/Cmp.eql.kind2

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

book/Cmp.gtn.kind2

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

book/Cmp.is_gtn.kind2

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

book/Cmp.kind2

@@ -1,8 +1,4 @@
-Cmp
-: *
-= $(self: Cmp)
-  ∀(P: ∀(cmp: Cmp) *)
-  ∀(ltn: (P Cmp.ltn))
-  ∀(eql: (P Cmp.eql))
-  ∀(gtn: (P Cmp.gtn))
-  (P self)
+data Cmp
+| ltn
+| eql
+| gtn

book/Cmp.ltn.kind2

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

book/Cmp/eql.kind2

@@ -0,0 +1,2 @@
+eql : Cmp =
+  ~λP λltn λeql λgtn eql

book/Cmp/gtn.kind2

@@ -0,0 +1,2 @@
+Cmp.gtn : Cmp =
+  ~λP λltn λeql λgtn gtn

book/Cmp/is_gtn.kind2

@@ -0,0 +1,9 @@
+use Bool/{true,false}
+use Cmp/{ltn,eql,gtn}
+
+Cmp.is_gtn (cmp: Cmp) : Bool =
+  match cmp {
+    ltn: false
+    eql: false
+    gtn: true
+  }

book/Cmp/ltn.kind2

@@ -0,0 +1,2 @@
+Cmp.ltn : Cmp =
+  ~λP λltn λeql λgtn ltn

book/Empty.absurd.kind2

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

book/Empty.kind2

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

book/Empty/absurd.kind2

@@ -0,0 +1,2 @@
+absurd (e: Empty) (P: *) : P =
+  (~e λx(P))

book/Equal.kind2

@@ -1,6 +1,13 @@
 data Equal T (a: T) (b: T)
 | refl (a: T) : (Equal T a a)
 
+//Equal : ∀(T: *) ∀(a: T) ∀(b: T) * =
+  //λT λa λb
+  //$(self: (Equal T a b))
+  //∀(P: ∀(a: T) ∀(b: T) ∀(x: (Equal T a b)) *)
+  //∀(refl: ∀(x: T) (P x x (Equal/refl T x)))
+  //(P a b self)
+
 //Equal
 //: ∀(A: *) ∀(a: A) ∀(b: A) *
 //= λA λa λb ∀(P: ∀(x: A) *) ∀(p: (P a)) (P b)

book/Equal.refl.kind2

@@ -1,4 +0,0 @@
-Equal.refl
-: ∀(A: *) ∀(x: A) (Equal A x x)
-= λA λx
-  ~ λP λrefl (refl x)

book/Equal/apply.kind2

@@ -1,8 +1,8 @@
-use Equal.{refl}
+//use Equal/{refl}
 
-apply <A> <B> <a> <b> (f: A -> B) (e: a == b) : (f a) == (f b) =
+apply <A: *> <B: *> <a: A> <b: B> (f: A -> B) (e: (Equal A a b)) : (Equal B (f a) (f b)) =
   match e {
-    refl: {=}
+    Equal/refl: {=}
   }
 
 

book/Equal/refl.kind2

@@ -0,0 +1,2 @@
+refl <A> (x: A) : (Equal A x x) =
+  ~ λP λrefl (refl x)

book/HVM/load.kind2

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

book/Kind.Text.show.go.kind2

@@ -1,3 +0,0 @@
-Kind.Text.show.go
-: ∀(text: Kind.Text) String.Concatenator
-= String.Concatenator.from_string

book/Kind/Book/get_refs.kind2

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

book/Kind/Book/get_refs/go.kind2

@@ -1,10 +1,10 @@
 Kind.Book.get_refs.go
 : ∀(book: (List (Pair String Kind.Term)))
-  (List.Concatenator String)
+  (List.Chunk String)
 = λbook
-  use P = λx (List.Concatenator String)
+  use P = λx (List.Chunk String)
   use cons = λhead λtail
-    use P = λx (List.Concatenator String)
+    use P = λx (List.Chunk String)
     use new = λhead.fst λhead.snd λnil
       (Kind.Term.get_refs.go
         head.snd