Kind.mat

book/Char.is_decimal.kind2

@@ -0,0 +1,5 @@
+Char.is_decimal
+: ∀(a: Char)
+  Bool
+= λa
+  (Char.is_between '0' '9' a)

book/Main.kind2

@@ -1,3 +1,5 @@
+//Main = Kind.reduce.mat
+
 BOOK
 : String
 = "id = λx x
@@ -12,13 +14,14 @@ Bool
 
 Bool.true  : Bool = ~λP λt λf t
 Bool.false : Bool = ~λP λt λf f
+
+Foo = #12345
 "
 
 Main
 : String
 = (Kind.Book.show (Kind.Book.parse BOOK))
 
-
 //Main
 //: String
 //= let P    = λx(String)

book/Parser.kind2

@@ -149,6 +149,11 @@ Parser.oper
 : (Parser String)
 = (Parser.pick_while Char.is_oper)
 
+// Parses a sequence of decimal characters.
+Parser.decimal
+: (Parser String)
+= (Parser.pick_while Char.is_decimal)
+
 // Checks if the next character is EOF.
 Parser.is_eof
 : (Parser Bool)
@@ -282,7 +287,7 @@ Parser.map
 // Parses repeatedly until a terminator parser succeeds.
 Parser.until
 : ∀(A: *)
-  ∀(until: (Parser Unit))
+  ∀(until: (Parser Bool))
   ∀(parse: (Parser A))
   (Parser (List A))
 = λA λuntil λparse
@@ -291,17 +296,21 @@ Parser.until
 
 Parser.until.go
 : ∀(A: *)
-  ∀(until: (Parser Unit))
+  ∀(until: (Parser Bool))
   ∀(parse: (Parser A))
   ∀(terms: (List.Concatenator A))
   (Parser (List.Concatenator A))
 = λA λuntil λparse λterms λcode
   let P    = λx(Parser.Result (List.Concatenator A))
-  let fail = λcode
-    let P    = λx(Parser.Result (List.Concatenator A))
-    let done = λcode λvalue (Parser.until.go A until parse λx(terms (List.cons A value x)) code)
-    let fail = λcode (Parser.Result.fail (List.Concatenator A) code)
-    (~(parse code) P done fail)
-  let done = λcode λvalue
-    (Parser.Result.done (List.Concatenator A) code terms)
+  let done = λcode λstop
+    let P     = λx ∀(code: String) (Parser.Result (List.Concatenator A))
+    let true  = λcode
+      (Parser.Result.done (List.Concatenator A) code terms)
+    let false = λcode
+      let P    = λx (Parser.Result (List.Concatenator A))
+      let done = λcode λvalue (Parser.until.go A until parse λx(terms (List.cons A value x)) code)
+      let fail = λerror (Parser.Result.fail (List.Concatenator A) error)
+      (~(parse code) P done fail)
+    ((~stop P true false) code)
+  let fail = λerror (Parser.Result.fail (List.Concatenator A) error)
   (~(until code) P done fail)

book/U60.parser.decimal.kind2

@@ -1,3 +1,5 @@
 U60.parser.decimal
 : (Parser #U60)
-= ?TODO
+= (Parser.bind String #U60 Parser.decimal λchars
+  (Parser.pure #U60
+  (List.fold Char chars ∀(r:#U60)#U60 λhλtλr(t #(+ #(- h '0') #(* r #10))) λr(r) #0)))

kind2.hvm1

@@ -145,9 +145,9 @@
 (Normal.term r Set               dep) = Set
 (Normal.term r U60               dep) = U60
 (Normal.term r (Num val)         dep) = (Num val)
-(Normal.term r (Txt val)         dep) = (Txt val)
 (Normal.term r (Op2 opr fst snd) dep) = (Op2 opr (Normal.term r fst dep) (Normal.term r snd dep))
 (Normal.term r (Mat nam x z s p) dep) = (Mat nam (Normal r x dep) (Normal r z dep) λk(Normal r (s (Var (Concat nam "-1") dep)) dep) λk(Normal r (p (Var nam dep)) dep))
+(Normal.term r (Txt val)         dep) = (Txt val)
 (Normal.term r (Var nam idx)     dep) = (Var nam idx)
 
 // Equality

main.ts

@@ -428,21 +428,30 @@ export function main() {
   // Runs 'hvm1 kind2.hvm1 -s -L -1'
 
   //const output = execSync("hvm1 run .kind2.hvm1 -s -L -1").toString();
-  const output = execSync("hvm1 run -t 1 -c -f .kind2.hvm1 \"(Main)\"").toString();
-  try {
-    var check_text = output.slice(output.indexOf("[["), output.indexOf("RWTS")).trim();
-    var stats_text = output.slice(output.indexOf("RWTS"));
-    var [logs, check] = JSON.parse(check_text);
-    logs.reverse();
-    for (var log of logs) {
-      console.log(log);
+  
+
+
+  //for (let name in book) {
+    //console.log("Checking: " + name);
+
+    const output = execSync("hvm1 run -t 1 -c -f .kind2.hvm1 \"(Main)\"").toString();
+    //const output = execSync(`hvm1 run -t 1 -c -f .kind2.hvm1 "(Checker Book.${name})"`).toString();
+    try {
+      var check_text = output.slice(output.indexOf("[["), output.indexOf("RWTS")).trim();
+      var stats_text = output.slice(output.indexOf("RWTS"));
+      var [logs, check] = JSON.parse(check_text);
+      logs.reverse();
+      for (var log of logs) {
+        console.log(log);
+      }
+      console.log(check ? "Check!" : "Error.");
+      console.log("");
+      console.log(stats_text);
+    } catch (e) {
+      console.log(output);
     }
-    console.log(check ? "Check!" : "Error.");
-    console.log("");
-    console.log(stats_text);
-  } catch (e) {
-    console.log(output);
-  }
+
+  //}
 
 };