skip comments

book/Char.is_whitespace.kind2

@@ -1,7 +0,0 @@
-Char.is_whitespace
-: ∀(a: Char)
-  Bool
-= λa (Bool.or
-  (Char.equal a #10) // newline
-  (Char.equal a #32)) // space
-

book/Kind.kind2

@@ -732,7 +732,8 @@ Kind.show
 : ∀(term: Kind.Term)
   ∀(dep: Nat)
   String
-= λterm λdep (String.Concatenator.build (Kind.show.go term dep))
+= λterm λdep
+  (String.Concatenator.build (Kind.show.go term dep))
 
 Kind.Oper.show.go
 : ∀(oper: Kind.Oper)
@@ -1378,6 +1379,79 @@ Kind.report
   let false = λinferred λexpected λvalue λdep none // TODO: HVM.log error
   (~e P true false inferred expected value dep)
 
+// Compilers
+// ---------
+
+Kind.compile.hvm.go
+: ∀(term: Kind.Term)
+  ∀(dep: Nat)
+  String.Concatenator
+= λterm λdep
+  let P   = λx String.Concatenator
+  let all = λnam λinp λbod
+    (Kind.Text.show.go "0")
+  let lam = λnam λbod λnil
+    ((Kind.Text.show.go "λ")
+    ((Kind.Text.show.go (U60.name (U60.from_nat dep)))
+    ((Kind.Text.show.go " "
+    ((Kind.compile.hvm.go (bod (Kind.var nam dep)) (Nat.succ dep))
+    nil)))))
+  let app = λfun λarg λnil
+    ((Kind.Text.show.go "(")
+    ((Kind.compile.hvm.go fun dep)
+    ((Kind.Text.show.go " ")
+    ((Kind.compile.hvm.go arg dep)
+    ((Kind.Text.show.go ")")
+    nil)))))
+  let ann = λval λtyp
+    (Kind.compile.hvm.go val dep)
+  let slf = λnam λbod
+    (Kind.Text.show.go "0")
+  let ins = λval
+    (Kind.compile.hvm.go val dep)
+  let ref = λnam λval
+    (Kind.Text.show.go nam)
+  let def = λnam λval λbod λnil
+    ((Kind.Text.show.go "let ")
+    ((Kind.Text.show.go nam)
+    ((Kind.Text.show.go " = ")
+    ((Kind.compile.hvm.go val dep)
+    ((Kind.Text.show.go "; ")
+    ((Kind.compile.hvm.go (bod (Kind.var nam dep)) (Nat.succ dep))
+    nil))))))
+  let set =
+    (Kind.Text.show.go "*")
+  let u60 =
+    (Kind.Text.show.go "*")
+  let num = λval
+    (U60.show.go val)
+  let op2 = λopr λfst λsnd λnil
+    ((Kind.Text.show.go "(")
+    ((Kind.Oper.show.go opr)
+    ((Kind.Text.show.go " ")
+    ((Kind.compile.hvm.go fst dep)
+    ((Kind.Text.show.go " ")
+    ((Kind.compile.hvm.go snd dep)
+    ((Kind.Text.show.go ")")
+    nil)))))))
+  let txt = λtxt λnil
+    ((Kind.Text.show.go String.quote)
+    ((Kind.Text.show.go txt)
+    ((Kind.Text.show.go String.quote)
+    nil)))
+  let hol = λnam λctx
+    (Kind.Text.show.go "0")
+  let var = λnam λidx
+    (Kind.Text.show.go (U60.name (U60.from_nat idx)))
+  (~term P all lam app ann slf ins ref def set u60 num op2 txt hol var)
+
+Kind.compile.hvm
+: ∀(term: Kind.Term)
+  ∀(dep: Nat)
+  String
+= λterm λdep
+  (String.Concatenator.build (Kind.compile.hvm.go term dep))
+
 // Tests
 // -----
 

book/Main.kind2

@@ -2,10 +2,18 @@
 
 //Main = Parser.skip
 
+Main = (String.skip "//oimeugrandeamigo... tudo bem?
+eu to, e vc?
+foo
+")
+
 //Main = Parser.text
-Main
-: String
-= (Kind.show (Kind.Term.parser.run "λx λy (y x)") Nat.zero)
+//Main
+//: String
+//= let term = (Kind.Term.parser.run "
+    //λf λx (f (f x))
+  //")
+  //(Kind.compile.hvm term Nat.zero)
 
 
 

book/Parser.kind2

@@ -111,7 +111,8 @@ Parser.skip
 : ∀(A: *)
   ∀(parser: (Parser A))
   (Parser A)
-= λA λparser λcode (parser (String.skip code))
+= λA λparser λcode
+  (parser (String.skip code))
 
 // Takes characters while a condition is true.
 Parser.pick_while

book/String.skip.kind2

@@ -1,14 +1,46 @@
-// TODO: implement comment skipper
+// Skips space characters and comments
 String.skip
 : ∀(str: String)
   String
 = λstr
+  // Pattern-matches str
   let P    = λx(String)
-  let cons = λhead λtail
-    let skip  = (Char.is_whitespace head)
-    let P     = λx ∀(head: Char) ∀(tail: String) (String)
-    let true  = λhead λtail (String.skip tail)
-    let false = λhead λtail (String.cons head tail)
-    (~skip P true false head tail)
+  let cons = λc0 λcs
+    // If first char is space, skip it
+    let P     = λx ∀(c0: Char) ∀(cs: String) (String)
+    let true  = λc0 λcs (String.skip cs)
+    let false = λc0 λcs
+      // If first char is slash, check next char
+      let P     = λx ∀(c0: Char) ∀(cs: String) (String)
+      let true  = λc0 λcs
+        // Pattern-matches str's tail
+        let P    = λx ∀(c0: Char) (String)
+        let cons = λc1 λcs λc0 
+          // If second char is slash, skip comment
+          let P     = λx ∀(c0: Char) ∀(c1: Char) ∀(cs: String) (String)
+          let true  = λc0 λc1 λcs (String.skip.comment cs)
+          let false = λc0 λc1 λcs (String.cons c0 (String.cons c1 cs))
+          (~(Char.is_slash c1) P true false c0 c1 cs)
+        let nil  = λc0 (String.cons c0 String.nil)
+        (~cs P cons nil c0)
+      let false = λc0 λcs (String.cons c0 cs)
+      (~(Char.is_slash c0) P true false c0 cs)
+    (~(Char.is_blank c0) P true false c0 cs)
+  let nil  = String.nil
+  (~str P cons nil)
+
+// Skips all characters until Char.is_newline is true
+String.skip.comment
+: ∀(str: String)
+  String
+= λstr
+  // Pattern-matches str
+  let P    = λx(String)
+  let cons = λc0 λcs
+    // If first char is not a newline, skip and recurse
+    let P     = λx ∀(c0: Char) ∀(cs: String) (String)
+    let true  = λc0 λcs cs
+    let false = λc0 λcs (String.skip.comment cs)
+    (~(Char.is_newline c0) P true false c0 cs)
   let nil  = String.nil
   (~str P cons nil)