WIP - breaking; will update after the map merge

book/HVM.load.kind2

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

book/HVM.log.kind2

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

book/HVM.print.kind2

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

book/HVM.print.many.kind2

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

book/HVM.save.kind2

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

book/Kind.API.file.kind2

@@ -0,0 +1,5 @@
+Kind.API.file
+: ∀(name: String)
+  String
+= λname
+  (String.concat name ".kind2")

book/Kind.API.load.kind2

@@ -0,0 +1,6 @@
+// TODO
+Kind.API.load
+: ∀(name: String)
+  Kind.Book
+= λname
+  (Kind.API.load.one name)

book/Kind.API.load.one.kind2

@@ -0,0 +1,6 @@
+Kind.API.load.one
+: ∀(name: String)
+  Kind.Book
+= λname
+  (HVM.load Kind.Book (Kind.API.file name) λdata
+  (Kind.Book.parse data))

book/Kind.Book.get_refs.go.kind2

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

book/Kind.Book.get_refs.kind2

@@ -0,0 +1,5 @@
+Kind.Book.get_refs
+: ∀(book: Kind.Book)
+  (List String)
+= λbook
+  (List.Concatenator.build String (Kind.Book.get_refs.go book))

book/Kind.Book.parse.kind2

@@ -5,4 +5,4 @@ Kind.Book.parse
   let P    = λx(Kind.Book)
   let done = λcode λbook book
   let fail = λerror (List.nil (Pair String Kind.Term))
-  (~(Kind.Book.parser code) P done fail)
+  (~(Kind.Book.parser code) P done fail)

book/Kind.Book.to_hvm.go.kind2

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

book/Kind.Book.to_hvm.prelude.kind2

@@ -1,9 +1,11 @@
-Kind.Book.to_hvm.prelude
-: String
-= `
+Kind.Book.to_hvm.prelude : String = `
 (U60.match 0 z s) = z
 (U60.match n z s) = (s (- n 1))
 
 (Str String.nil)         = λP λcons λnil nil
 (Str (String.cons x xs)) = λP λcons λnil (cons x (Str xs))
+
+(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/Kind.Term.get_refs.go.kind2

@@ -0,0 +1,50 @@
+Kind.Term.get_refs.go
+: ∀(term: Kind.Term)
+  (List.Concatenator String)
+= λterm
+  let P   = λx(List.Concatenator String)
+  let all = λnam λinp λbod λnil
+    ((Kind.Term.get_refs.go inp)
+    ((Kind.Term.get_refs.go (bod Kind.set))
+    nil))
+  let lam = λnam λbod λnil
+    ((Kind.Term.get_refs.go (bod Kind.set))
+    nil)
+  let app = λfun λarg λnil
+    ((Kind.Term.get_refs.go fun)
+    ((Kind.Term.get_refs.go arg)
+    nil))
+  let ann = λval λtyp λnil
+    ((Kind.Term.get_refs.go val)
+    ((Kind.Term.get_refs.go typ)
+    nil))
+  let slf = λnam λbod λnil
+    ((Kind.Term.get_refs.go (bod Kind.set))
+    nil)
+  let ins = λval λnil
+    ((Kind.Term.get_refs.go val)
+    nil)
+  let ref = λnam λval λnil
+    ((List.cons String nam)
+    nil)
+  let def = λnam λval λbod λnil
+    ((Kind.Term.get_refs.go val)
+    ((Kind.Term.get_refs.go (bod Kind.set))
+    nil))
+  let set = λnil nil
+  let u60 = λnil nil
+  let num = λval λnil nil
+  let op2 = λopr λfst λsnd λnil
+    ((Kind.Term.get_refs.go fst)
+    ((Kind.Term.get_refs.go snd)
+    nil))
+  let mat = λnam λx λz λs λp λnil
+    ((Kind.Term.get_refs.go x)
+    ((Kind.Term.get_refs.go z)
+    ((Kind.Term.get_refs.go (s Kind.set))
+    ((Kind.Term.get_refs.go (p Kind.set))
+    nil))))
+  let txt = λtext λnil nil
+  let hol = λnam λctx λnil nil
+  let var = λnam λidx λnil nil
+  (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var)

book/Kind.Term.get_refs.kind2

@@ -0,0 +1,6 @@
+// Returns a list with all the references of given term.
+Kind.Term.get_refs
+: ∀(term: Kind.Term)
+  (List String)
+= λterm
+  (List.Concatenator.build String (Kind.Term.get_refs.go term))

book/Kind.Term.kind2

@@ -18,4 +18,4 @@ Kind.Term
   ∀(txt: ∀(lit: Kind.Text) (P (Kind.txt lit)))
   ∀(hol: ∀(nam: String) ∀(ctx: (List Kind.Term)) (P (Kind.hol nam ctx)))
   ∀(var: ∀(nam: String) ∀(idx: Nat) (P (Kind.var nam idx)))
-  (P self)
+  (P self)

book/Kind.Term.to_hvm.go.kind2

@@ -40,7 +40,7 @@ Kind.Term.to_hvm.go
     nil))
   let ref = λnam λval λnil
     ((Kind.Term.to_hvm.nl inc tab)
-    ((Kind.Text.show.go "(F.")
+    ((Kind.Text.show.go "(Book.")
     ((Kind.Text.show.go nam)
     ((Kind.Text.show.go ")")
     nil))))

book/Kind.file.kind2

@@ -0,0 +1,2 @@
+//Kind.file
+//: ∀(name: 

book/List.Map.kind2

@@ -1,42 +0,0 @@
-List.Map
-: ∀(K: *)
-  ∀(V: *)
-  *
-= λK λV
-  (List (Pair K V))
-
-List.Map.get
-: ∀(K: *)
-  ∀(V: *)
-  ∀(eql: ∀(a: K) ∀(b: K) Bool)
-  ∀(key: K)
-  ∀(map: (List.Map K V))
-  (Maybe V)
-= λK λV λeql λkey λmap
-  let P    = λx(Maybe V)
-  let cons = λhead λtail
-    let P   = λx(Maybe V)
-    let new = λhead.fst λhead.snd
-      let P     = λx(Maybe V)
-      let true  = (Maybe.some V head.snd)
-      let false = (List.Map.get K V eql key tail)
-      (~(eql head.fst key) P true false)
-    (~head P new)
-  let nil  = (Maybe.none V)
-  (~map P cons nil)
-
-List.Map.set
-: ∀(K: *)
-  ∀(V: *)
-  ∀(key: K)
-  ∀(val: V)
-  ∀(map: (List.Map K V))
-  (List.Map K V)
-= λK λV λkey λval λmap
-  (List.cons (Pair K V) (Pair.new K V key val) map)
-
-List.Map.new
-: ∀(K: *)
-  ∀(V: *)
-  (List.Map K V)
-= λK λV (List.nil (Pair K V))

book/Main.kind2

@@ -1,3 +1,13 @@
+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
+  //Unit.one)
+
 //BOOK
 //: String
 //= "id = λx x

book/QBool.kind2

@@ -1,4 +1,5 @@
 // Ideal:
+// 
 // QBool.true  : QBool = ~λP (#0, λx x)
 // QBool.false : QBool = ~λP (#1, λx x)
 // 
@@ -9,7 +10,7 @@
 //   ∀(x: match t {
 //     0: (P QBool.true)
 //     1: (P QBool.false)
-//     +: Empty
+//     +: ∀(x: Empty) *
 //   })
 //   (P self)
 // 
@@ -55,16 +56,16 @@ QBool.match
 = λa λP λt λf
   (~(~a P) λx(P a) λtag #match tag = tag {
     #0: λx (x t)
-    #+: λx ((#match tag-1 = tag-1 {
+    #+: λx ((#match tag_1 = tag-1 {
       #0: λx (x f)
       #+: λx (x λe (Empty.absurd e *))
-    }: ∀(x: ∀(x: #match tag-1 = tag-1 {
+    }: ∀(x: ∀(x: #match tag_1 = tag_1 {
       #0: (P QBool.false)
       #+: ∀(x: Empty) *
     }: *) (P a)) (P a)) x)
   }: ∀(x: (∀(x: #match tag = tag {
     #0: (P QBool.true)
-    #+: #match tag-1 = tag-1 {
+    #+: #match tag_1 = tag-1 {
       #0: (P QBool.false)
       #+: ∀(x: Empty) *
     }: *

book/QBool2.kind2

@@ -0,0 +1,63 @@
+// Ideal:
+// 
+// QBool2.true  : QBool2 = ~λP λnew (new #0)
+// QBool2.false : QBool2 = ~λP λnew (new #1)
+// QBool2.bad   : QBool2 = ~λP λnew (new #2 ?impossible)
+// 
+// QBool2 : * =
+//   $self
+//   ∀(P: ∀(x: QBool2) *)
+//   ∀(new: ∀(tag: #U60) #match tag = tag {
+//     #0: (P QBool2.true)
+//     #1: (P QBool2.false)
+//     #+: ∀(e: Empty) *
+//   }: *)
+//   (P self)
+// 
+// QBool2.match
+// : ∀(a: QBool2)
+//   ∀(P: ∀(x: QBool2) *)
+//   ∀(t: (P QBool2.true))
+//   ∀(f: (P QBool2.false))
+//   (P a)
+// = λa λP λt λf
+//   (~a P λtag #match tag = tag {
+//     #0: t
+//     #1: f
+//     #+: λe (~e λx(*))
+//   })
+
+QBool2.true  : QBool2 = ~λP λnew (new #0)
+QBool2.false : QBool2 = ~λP λnew (new #1)
+QBool2.bad   : QBool2 = ~λP λnew (new #2 ?impossible)
+
+QBool2 : * =
+  $self
+  ∀(P: ∀(x: QBool2) *)
+  ∀(new: ∀(tag: #U60) #match tag = tag {
+    #0: (P QBool2.true)
+    #+: #match tag_1 = tag-1 {
+      #0: (P QBool2.false)
+      #+: ∀(e: Empty) *
+    }: *
+  }: *)
+  (P self)
+
+QBool2.match
+: ∀(a: QBool2)
+  ∀(P: ∀(x: QBool2) *)
+  ∀(t: (P QBool2.true))
+  ∀(f: (P QBool2.false))
+  (P a)
+= λa λP λt λf
+  (~a P λtag #match tag = tag {
+    #0: t
+    #+: #match tag_1 = tag-1 {
+      #0: f
+      #+: λe (~e λx(*))
+    }: #match tag_1 = tag_1 { #0: (P QBool2.false) #+: ∀(e: Empty) * }: *
+  }: #match tag = tag { #0: (P QBool2.true) #+: #match tag_1 = tag-1 { #0: (P QBool2.false) #+: ∀(e: Empty) * }: * }: *)
+
+
+
+

book/String.Map.kind2

@@ -1,27 +0,0 @@
-// Temporarily just a list of key/val
-
-String.Map
-: ∀(A: *) *
-= (List.Map String)
-
-String.Map.get
-: ∀(A: *)
-  ∀(key: String)
-  ∀(map: (String.Map A))
-  (Maybe A)
-= λA λkey λmap
-  (List.Map.get String A String.equal key map)
-
-String.Map.set
-: ∀(A: *)
-  ∀(key: String)
-  ∀(val: A)
-  ∀(map: (String.Map A))
-  (String.Map A)
-= λA λkey λval λmap
-  (List.Map.set String A key val map)
-
-String.Map.new
-: ∀(V: *)
-  (String.Map V)
-= λV (List.Map.new String V)

book/U60.Map.kind2

@@ -1,27 +0,0 @@
-// Temporarily just a list of key/val
-
-U60.Map
-: ∀(A: *) *
-= (List.Map #U60)
-
-U60.Map.get
-: ∀(A: *)
-  ∀(key: #U60)
-  ∀(map: (U60.Map A))
-  (Maybe A)
-= λA λkey λmap
-  (List.Map.get #U60 A U60.equal key map)
-
-U60.Map.set
-: ∀(A: *)
-  ∀(key: #U60)
-  ∀(val: A)
-  ∀(map: (U60.Map A))
-  (U60.Map A)
-= λA λkey λval λmap
-  (List.Map.set #U60 A key val map)
-
-U60.Map.new
-: ∀(V: *)
-  (U60.Map V)
-= λV (List.Map.new #U60 V)

book/_compile.kind2

@@ -0,0 +1,4 @@
+_compile : String = (Kind.Book.to_hvm (Kind.Book.parse `test9
+: String
+= (String.unpar '(' ')' "((foo))")
+`))

book/test10.kind2

@@ -6,9 +6,8 @@ _exp = (Kind.lam "n" λn(Kind.lam "m" λm(Kind.lam "P" λP(Kind.app (Kind.app m
 _C2 = _Nat
 _c2 = (Kind.lam "P" λP(Kind.lam "s" λs(Kind.lam "z" λz(Kind.app s (Kind.app s z)))))
 
-// Checks if `(work 2^4)` is propositionally equal to `true`
+// Checks if (work 2^4) is propositionally equal to true
 test10
 : String
 = let term = (Kind.app (Kind.app _exp _c2) _c2)
   (Kind.Term.show (Kind.normal Bool.true term Nat.zero) Nat.zero)
-

book/test11.kind2

@@ -0,0 +1,3 @@
+test11
+: String
+= #0

book/test7.kind2

@@ -1,20 +1,11 @@
 test7.book
 : String
 = `
-// exp : ∀(n: Nat) Nat = λn λm λP λs λz (m ∀(x:P)P (n P))
-_EXP = (Kind.all "n" _Nat λn(Kind.all "m" _Nat λm(_Nat)))
-_exp = (Kind.lam "n" λn(Kind.lam "m" λm(Kind.lam "P" λP(Kind.app (Kind.app m (Kind.all "x" P λx(P))) (Kind.app n P)))))
-
-// C2 : Nat = λs λz (s (s z))
-_C2 = _Nat
-_c2 = (Kind.lam "P" λP(Kind.lam "s" λs(Kind.lam "z" λz(Kind.app s (Kind.app s z)))))
-
-// Checks if (work 2^4) is propositionally equal to true
-test10
-: String
-= let term = (Kind.app (Kind.app _exp _c2) _c2)
-  (Kind.Term.show (Kind.normal Bool.true term Nat.zero) Nat.zero)
-
+Kind.API.get_refs
+: ∀(code: String)
+  (List String)
+= λcode
+  (Kind.Term.get_refs (Kind.Term.parse code))
 `
 
 test7

bootstrap.js

@@ -0,0 +1,38 @@
+// Bootstrap by compiling ALL book/ functions to a single HVM1 file.
+
+const fs = require('fs');
+const { execSync } = require('child_process');
+const path = require('path');
+
+const bookDir = './book';
+const outputFilePath = './bootstrap.hvm1';
+let outputs = [];
+
+fs.readdirSync(bookDir).forEach(file => {
+  if (path.extname(file) === '.kind2') {
+    try {
+      const filePath = path.join(bookDir, file);
+      const fileContent = fs.readFileSync(filePath, 'utf8');
+      const compileString = `_compile : String = (Kind.Book.to_hvm (Kind.Book.parse \`${fileContent}\`))`;
+      const compileFilePath = path.join(bookDir, '_compile.kind2');
+      fs.writeFileSync(compileFilePath, compileString);
+      console.log("COMPILING", filePath);
+      const command = `kind2 run _compile`;
+      const result = execSync(command, { cwd: bookDir }).toString().trim().slice(1,-1);
+      console.log(result);
+      outputs.push(result);
+    } catch (e) {
+      console.log(e);
+    }
+  }
+});
+
+// Loads prelude
+var prelude = fs.readFileSync("./book/Kind.Book.to_hvm.prelude", "utf8");
+const lines = prelude.split("\n");
+lines.shift();
+lines.pop();
+var prelude = lines.join("\n");
+
+const finalOutput = prelude + "\n" + outputs.join('\n');
+fs.writeFileSync(outputFilePath, finalOutput);

kind2.hvm1

@@ -186,9 +186,9 @@
 (Comparer rec (Var a.nam a.idx)           (Var b.nam b.idx)           dep) = (== a.idx b.idx)
 (Comparer rec (Ann a.val a.typ)           b                           dep) = (rec a.val b dep)
 (Comparer rec a                           (Ann b.val b.typ)           dep) = (rec a b.val dep)
-(Comparer rec (Hol a.nam a.ctx)           (Hol b.nam b.ctx)           dep) = (Same a.nam b.nam)
 (Comparer rec (Hol a.nam a.ctx)           b                           dep) = (Debug dep ["Found: ?" a.nam " = " (Show (Normal 0 b dep) dep)] 1)
 (Comparer rec a                           (Hol b.nam b.ctx)           dep) = (Debug dep ["Found: ?" b.nam " = " (Show (Normal 0 a dep) dep)] 1)
+(Comparer rec (Hol a.nam a.ctx)           (Hol b.nam b.ctx)           dep) = (Same a.nam b.nam)
 (Comparer rec U60                         U60                         dep) = 1
 (Comparer rec (Num a.val)                 (Num b.val)                 dep) = (== a.val b.val)
 (Comparer rec (Op2 a.opr a.fst a.snd)     (Op2 b.opr b.fst b.snd)     dep) = (& (rec a.fst b.fst dep) (rec a.snd b.snd dep))
@@ -358,25 +358,37 @@
 // Compilation
 // -----------
 
+(Str.view str) = (str 0 λheadλtail(String.cons head (Str.view tail)) String.nil)
+
+(Str.make (String.cons x xs)) = λP λcons λnil (cons x (Str.make xs))
+(Str.make String.nil)         = λP λcons λnil nil
+
+Compile.primitives = [
+  (Pair "HVM.log" λA λB λmsg λret (HVM.log msg ret))
+  (Pair "HVM.print" λA λmsg λret (HVM.print (Str.view msg) ret))
+  (Pair "HVM.save" λA λname λdata λret (HVM.save (Str.view name) (Str.view data) ret))
+  (Pair "HVM.load" λA λname λret (HVM.load (Str.view name) λdata (ret (Str.make data))))
+]
+
 (Compile (All nam inp bod)) = 0
 (Compile (Lam nam bod))     = λx(Compile (bod (Var "" x)))
 (Compile (App fun arg))     = ((Compile fun) (Compile arg))
 (Compile (Ann val typ))     = (Compile val)
 (Compile (Slf nam bod))     = 0
 (Compile (Ins val))         = (Compile val)
-(Compile (Ref nam val))     = (Compile val)
+(Compile (Ref nam val))     = (Compile.ref Compile.primitives nam val)
 (Compile (Let nam val bod)) = (Compile (bod val))
 (Compile Set)               = 0
 (Compile U60)               = 0
 (Compile (Num val))         = val
 (Compile (Op2 opr fst snd)) = (Compile.op2 opr (Compile fst) (Compile snd))
 (Compile (Mat nam x z s p)) = (Compile.mat (Compile x) (Compile z) λx(Compile (s (Var "" x))))
-(Compile (Txt txt))         = (Compile (Compile.txt txt))
+(Compile (Txt txt))         = (Str.make txt)
 (Compile (Hol nam ctx))     = 0
 (Compile (Var nam val))     = val
 
-(Compile.txt (String.cons x xs)) = (App (App Book.String.cons (Num x)) (Compile.txt xs))
-(Compile.txt String.nil)         = Book.String.nil
+//(Compile.txt (String.cons x xs)) = (App (App Book.String.cons (Num x)) (Compile.txt xs))
+//(Compile.txt String.nil)         = Book.String.nil
 
 (Compile.op2 ADD fst snd) = (+ fst snd)
 (Compile.op2 SUB fst snd) = (- fst snd)
@@ -398,16 +410,15 @@
 (Compile.mat 0 z s) = z
 (Compile.mat n z s) = (s (- n 1))
 
+(Compile.ref (List.cons (Pair prim_name prim_func) prims) nam val) = (If (Same prim_name nam) prim_func (Compile.ref prims nam val))
+(Compile.ref List.nil nam val) = (Compile val)
+
 // API
 // ---
 
-(Read str) = (str 0 λheadλtail(String.cons head (Read tail)) String.nil)
-
 (Normalizer (Ref nam val)) = (Normalizer val)
 (Normalizer (Ann val typ)) = (Normalizer val)
-(Normalizer val)           = (Read (Compile val)) // compiles to native and reads as string
-//(Normalizer val)           = ((Compile val)) // compiles to native and show it
-//(Normalizer val)           = (Normal 1 val  1) // uses the normalizer function
+(Normalizer val)           = (Compile val)
 
 (Checker (Ref nam val)) = (Checker val)
 (Checker (Ann val typ)) = (Checker.report (Check val typ 0))

kind2.ts

@@ -0,0 +1,30 @@
+import { execSync } from 'child_process';
+import * as fs from 'fs';
+
+export function run(expr: string): string {
+  var command = `hvm1 run -t 1 -c -f bootstrap.hvm1 '${expr}'`;
+  try {
+    const output = execSync(command).toString();
+    return output;
+  } catch (error) {
+    throw error;
+  }
+}
+
+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();
+}
+
+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))`));