Feature/nat literal term

bend2/comp.ts

@@ -631,6 +631,8 @@ const CYCLES: Map<Bend.Name, boolean> = new Map();
 
 const CONSTS: Map<HTerm, boolean> = new Map();
 
+const LITS = new Map<HTerm, HTerm>();
+
 // Name
 // ====
 
@@ -679,6 +681,7 @@ function tpl(t: Gen, xs: string[]): string {
 
 function tpl_nat(u: string, f: string): Gen {
   return ([p]) => /^\d/.test(p) ? (BigInt(parseInt(p)) + 1n) + u
+    : /^nat_chk\(.* \+ \d+n?\)$/.test(p) ? p.replace(/(\d+)(n?)\)$/, (_, k, n) => `${+k + 1}${n})`)
     : tpl(f, [p]);
 }
 
@@ -696,7 +699,7 @@ function memo<K, V>(m: Map<K, V>, k: K, f: () => V): V {
 }
 
 function memo_gc(): void {
-  [OPENS, USES, FOLDS, SPINES, CONSTS].forEach((m) => m.clear());
+  [OPENS, USES, FOLDS, SPINES, CONSTS, LITS].forEach((m) => m.clear());
 }
 
 // Probe
@@ -784,7 +787,7 @@ function term_eta(book: Bend.Book, t: HTerm, T: HTerm, n: number): HTerm {
 }
 
 function term_kids(cf: Carb, tm: HTerm): HTerm[] {
-  const t = Bend.term_force(tm);
+  const t = term_lit(Bend.term_force(tm));
   switch (t.$) {
     case "Ann": return [t.x];
     case "Lam": return [term_open(t).b];
@@ -807,7 +810,7 @@ function term_kids(cf: Carb, tm: HTerm): HTerm[] {
 // tail position (under annotations, binders, arms and let bodies).
 function term_any(cf: Carb, t: HTerm, p: (s: HTerm, tail: boolean) => boolean,
   tail = true, seen: Set<HTerm> = new Set()): boolean {
-  const s = Bend.term_force(t);
+  const s = term_lit(Bend.term_force(t));
   if (seen.has(s)) {
     return false;
   }
@@ -828,8 +831,13 @@ function term_nodes(cf: Carb, t: HTerm): number {
   return n;
 }
 
+function term_lit(t: HTerm): HTerm {
+  return t.$ === "Lit" ? memo(LITS, t, () => Bend.term_higher(typeof t.v === "number" && t.v > Bend.NAT_LITERAL_MAX
+    ? Bend.App(Bend.Ref("U32.to_nat"), Bend.u32_to_term(t.v)) : Bend.lit_full(t))) : t;
+}
+
 function term_const(t: HTerm): boolean {
-  const s = Bend.term_strip(t);
+  const s = term_lit(Bend.term_strip(t));
   return s.$ === "Ctr" && memo(CONSTS, s, () => s.x.every(term_const));
 }
 
@@ -929,7 +937,7 @@ function ty_peel(tm: HTerm,
     ty = x.$ === "Ann" ? x.T : ty;
     x = Bend.term_force(x.$ === "Ann" ? x.x : x.f);
   }
-  return [x, ty];
+  return [term_lit(x), ty];
 }
 
 function ty_adt(book: Bend.Book, A: HTerm | null): HAdt | null {
@@ -2389,7 +2397,7 @@ function emit_unfold(fl: File, s: HTerm): HTerm | null {
         xs = xs.slice(1);
         continue;
       }
-      const c = w.$ === "Mat" ? Bend.term_strip(xs[0]) : null;
+      const c = w.$ === "Mat" ? term_lit(Bend.term_strip(xs[0])) : null;
       if (c === null || c.$ !== "Ctr" || !term_const(c)) {
         return null;
       }

gates/repo.ts

@@ -39,7 +39,7 @@ allow("LICENSE", 4000);
 allow("flake.nix", 1500);
 allow("bend2/base.bend", 32000);
 allow("bend2/bend.lean", 400000);
-allow("bend2/bend.ts", 42000);
+allow("bend2/bend.ts", 43000);
 allow("bend2/comp.ts", 65000);
 allow("bend2/main.ts", 10000);
 allow(/^bend2\/effs\/[a-z0-9_]+\.(c|js)$/, 4000);

tests/check/nat_literal_own_nat.bend

@@ -0,0 +1,16 @@
+# a literal is a Nat only where Nat declares Succ and Zero: a module's
+# own Nat with other constructors rejects it
+type Nat is Data:
+  Foo{}
+
+def n() -> Nat:
+  3n
+
+#|Error:
+#|- expected : a declared constructor (Nat declares Foo)
+#|- observed : 3n
+#|Location: n
+#|6 | def n() -> Nat:
+#|7>|   3n
+#|8 | 
+#|exit 1

tests/check/nat_literal_pattern_empty.bend

@@ -1,7 +1,7 @@
 # the unchecked literal pattern let a closed term inhabit Empty: the
-# longhand U32.to_nat(0) matched a Zero that carries a field as a bare
-# Zero, the arm's goal became @w:U -> Empty, and the self-call f(q)
-# passed without descending. the literal is refused like Zero{} is
+# literal 0n matched a Zero that carries a field as a bare Zero, the
+# arm's goal became @w:U -> Empty, and the self-call f(q) passed without
+# descending. the literal is refused like Zero{} is
 type U is Data:
   Un{}
 type N is Data:
@@ -13,7 +13,7 @@ type Empty is Data:
 
 def f(b: N) -> Empty:
   match b:
-    case U32.to_nat(0):
+    case 0n:
       {\{K: q => w => f(q)} : D -> U -> Empty}(K{Zero{Un{}}})
     case Succ{p}:
       f(p)
@@ -25,6 +25,6 @@ def boom() -> Empty:
 #|- message  : a Zero pattern with 1 field
 #|Location:
 #|15 |   match b:
-#|16>|     case U32.to_nat(0):
+#|16>|     case 0n:
 #|17 |       {\{K: q => w => f(q)} : D -> U -> Empty}(K{Zero{Un{}}})
 #|exit 1

tests/check/string_literal_descends.bend

@@ -0,0 +1,15 @@
+# a literal argument descends when it is a strict tail of its case's
+# literal pattern: the termination check unfolds the literal
+import Base
+
+def f(s: String) -> Nat:
+  match s:
+    case "ab":
+      f("b")
+    case _:
+      0n
+
+def main() -> Nat:
+  f("ab")
+
+#|0n

tests/check/string_literal_long.bend

@@ -0,0 +1,13 @@
+# a 6000-character string literal checks: the checker holds a literal as
+# one Lit node, not as a constructor per character (which overflowed its
+# stack near 5000 characters). main is a function, so the test is checked
+# and interpreted; the interpreter unfolds the literal to count it.
+import Base
+
+def text() -> String:
+  "abcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghijabcdefghij"
+
+def main(n: Nat) -> Nat:
+  Nat.add(n, String.length(text()))
+
+#|n => Nat.add(n, 6000n)

tests/check/string_literal_own_string.bend

@@ -0,0 +1,16 @@
+# a literal is a String only where String declares SCon and SNil: a
+# module's own String with other constructors rejects it
+type String is Data:
+  Foo{}
+
+def s() -> String:
+  "abc"
+
+#|Error:
+#|- expected : a declared constructor (String declares Foo)
+#|- observed : "abc"
+#|Location: s
+#|6 | def s() -> String:
+#|7>|   "abc"
+#|8 | 
+#|exit 1

tests/compile/nat_pattern_deep.bend

@@ -0,0 +1,16 @@
+# a literal pattern past 256 whose default arm uses the scrutinee rebuilds
+# it as one checked sum, nat_chk(e, x + 300), not a check per Succ: 300
+# nested calls topped clang's bracket nesting and the C lane failed
+import Base
+
+def down(n: Nat) -> Nat:
+  match n:
+    case 300n:
+      down(299n)
+    case _:
+      n
+
+def main() -> Nat:
+  Nat.add(down(300n), down(7n))
+
+#|306n

tests/printer/nat_literal_print.bend

@@ -0,0 +1,17 @@
+# a nat literal prints back as a literal, a Succ chain that ends in a
+# literal prints as one number, and "n + T" past 256 is Nat.add
+import Base
+
+def small(n: Nat) -> Nat:
+  2n+n
+
+def big(n: Nat) -> Nat:
+  300n+n
+
+def chain() -> Nat:
+  Succ{Succ{300n}}
+
+def main(a: Nat, b: Nat) -> Nat:
+  Nat.add(small(a), Nat.add(big(b), Nat.add(chain(), 4294967295n)))
+
+#|a => b => 2n+Nat.add(a, 300n+Nat.add(b, 4294967597n))

tests/printer/string_literal_tail.bend

@@ -0,0 +1,14 @@
+# a literal prints back as a literal, and a chain that ends in a literal
+# prints as one string: SCon{'a', SCon{'b', "cd"}} is "abcd"
+import Base
+
+def greet(b: Bool) -> String:
+  Bool.pick(String, b, "yes\"\n", "no")
+
+def cons(s: String) -> String:
+  SCon{'a', SCon{'b', s}}
+
+def main(b: Bool) -> String:
+  String.append(greet(b), cons("cd"))
+
+#|b => String.append(Bool.pick(String, b, "yes\"\n", "no"), "abcd")

tests/proof/nat_literal_unfolds.bend

@@ -0,0 +1,69 @@
+# a nat literal is one Lit node in the checker; it unfolds a Succ at a
+# time where a chain is read: a comparison sees 300n as Succ{299n} and
+# 0n as Zero{}, a match reads a literal pattern past 256 and a literal
+# scrutinee, a self-call on a smaller literal descends, and the
+# evaluator steps through a literal's count. the laws hold the patterns
+# past 256: a compiled match on one rebuilds its scrutinee 300 deep,
+# past clang's bracket nesting.
+import Base
+
+law big_is_succ:
+  {300n == Succ{299n} : Nat}
+
+def big_is_succ():
+  {==}
+
+law zero_is_zero:
+  {0n == Zero{} : Nat}
+
+def zero_is_zero():
+  {==}
+
+law add_lits:
+  {Nat.add(999n, 1n) == 1000n : Nat}
+
+def add_lits():
+  {==}
+
+def classify(n: Nat) -> Nat:
+  match n:
+    case 300n:
+      1n
+    case 5n:
+      2n
+    case _:
+      0n
+
+law classify_big:
+  {classify(300n) == 1n : Nat}
+
+def classify_big():
+  {==}
+
+def down(n: Nat) -> Nat:
+  match n:
+    case 300n:
+      down(299n)
+    case _:
+      n
+
+law down_steps:
+  {down(300n) == 299n : Nat}
+
+def down_steps():
+  {==}
+
+def small(n: Nat) -> Nat:
+  match n:
+    case 5n:
+      2n
+    case _:
+      0n
+
+def bound() -> Nat:
+  4294967295n
+
+def main() -> List<Nat>:
+  [small(5n), small(7n), Nat.add(299n, 1n), Nat.add(0n, bound())]
+
+#|[2n, 0n, 300n, 4294967295n]

tests/proof/string_literal_unfolds.bend

@@ -0,0 +1,70 @@
+# a string literal is one Lit node in the checker; it unfolds a character
+# at a time where a chain is read: a comparison sees "ab" as
+# SCon{'a', "b"}, "" as SNil{}, a match reads a literal pattern and a
+# literal scrutinee, and the evaluator steps through a literal's length.
+# a character is any u32, so a literal may spell a surrogate pair.
+import Base
+
+law ab_is_chain:
+  {"ab" == SCon{'a', "b"} : String}
+
+def ab_is_chain():
+  {==}
+
+law empty_is_nil:
+  {"" == SNil{} : String}
+
+def empty_is_nil():
+  {==}
+
+law length_three:
+  {String.length("abc") == 3n : Nat}
+
+def length_three():
+  {==}
+
+law append_lits:
+  {String.append("ab", "cd") == "abcd" : String}
+
+def append_lits():
+  {==}
+
+law eq_lits:
+  {String.eq("héllo", "héllo") == True{} : Bool}
+
+def eq_lits():
+  {==}
+
+law surrogates_two:
+  {String.length("\u{d83d}\u{de00}") == 2n : Nat}
+
+def surrogates_two():
+  {==}
+
+def classify(s: String) -> Nat:
+  match s:
+    case "":
+      0n
+    case "one":
+      1n
+    case "two":
+      2n
+    case _:
+      9n
+
+law classify_two:
+  {classify("two") == 2n : Nat}
+
+def classify_two():
+  {==}
+
+law classify_more:
+  {classify("twoo") == 9n : Nat}
+
+def classify_more():
+  {==}
+
+def main() -> List<&2, Nat>:
+  [classify(""), classify("one"), classify("two"), classify("x"), String.length("😀é")]
+
+#|[0n, 1n, 2n, 9n, 2n]