Feature/u32-and-f32-to-literals

bend2/bend.ts

@@ -67,8 +67,8 @@
 // List   | "[" [A ","?] "]", A "<>" B | Con{A, ..Nil{}}, Con{A, B}
 // Array  | "[" A ":" T ("*" 2^D "n" | "^" D) "]" | Array.new(T, D, A)
 // Nat    | NUMBER "n" ("+" T)?        | Lit, read as Succ{..Zero{}}; Succ{..T}
-// U32    | NUMBER                     | U32{WCon{b, ..WNil{}}}
-// F32    | NUMBER "." NUMBER [EXP]    | F32{WCon{b, ..WNil{}}}
+// U32    | NUMBER                     | Lit, read as U32{WCon{b, ..WNil{}}}
+// F32    | NUMBER "." NUMBER [EXP]    | Lit, read as F32{WCon{b, ..WNil{}}}
 // Chr    | "'" CHAR "'"               | Chr{U32}
 // Str    | "\"" [CHAR] "\""           | Lit, read as SCon{Chr, ..SNil{}}
 // Index  | x "[" i "]" ("<-" v)?      | Array.get(U32, x, i), ..set(..)
@@ -91,7 +91,7 @@
 // a bare Bind name is -Name: Quant. Fill and Plus omit a datatype's
 // leading Quant parameters as a block; Plus alone fills a quant-only D.
 // a literal expands to one node per unit, unbounded by design, but a
-// string and a nat stay one Lit node and unfold a unit at a time where
+// string, nat, u32 and f32 stay one Lit node and unfold where
 // a chain is read (a match, a comparison, a descent, a pattern); a full
 // word, a Nat, a Char, a String, a list, a tuple and an array (its
 // slots) print back as literals; "*" takes a power of two. Arrow is
@@ -288,7 +288,7 @@ export type TermOf<B> = (
   | { $: "App"; f: TermOf<B>; x: TermOf<B> }                                       // f(x)
   | { $: "ADT"; k: Name; x: TermOf<B>[]; r: Name[] }                               // A<x0,x1,...>
   | { $: "Ctr"; k: Name; x: TermOf<B>[] }                                          // A{x0,x1,...}
-  | { $: "Lit"; v: string | number }                                               // "text", 3n
+  | { $: "Lit"; v: string | number; k?: "U32" | "F32" }                           // "text", 3n; k tags a 32-bit word
   | { $: "Mat"; k: Name; h: TermOf<B>; m: TermOf<B> }                              // \{A: h; m}
   | { $: "Efq" }                                                                   // \{}
   | { $: "Eql"; a: TermOf<B>; b: TermOf<B>; T: TermOf<B> }                         // {a == b : T}
@@ -410,8 +410,8 @@ export function Ctr<X>(k: Name, x: TermOf<X>[], s?: Span): TermOf<X> {
   return { $: "Ctr", k, x, s };
 }
 
-export function Lit<X>(v: string | number, s?: Span): TermOf<X> {
-  return { $: "Lit", v, s };
+export function Lit<X>(v: string | number, s?: Span, k?: "U32" | "F32"): TermOf<X> {
+  return { $: "Lit", v, s, k };
 }
 
 export function Mat<X>(k: Name, h: TermOf<X>, m: TermOf<X>, s?: Span): TermOf<X> {
@@ -1181,6 +1181,8 @@ export function u32_to_term(n: U32, s?: Span): LTerm {
 // unit at a time where a chain is read, so the checker pays nothing per
 // unit. a JS string holds Unicode scalar values only, so a literal that
 // spells a surrogate or a code point past U+10FFFF is its chain.
+// U32 and F32 literals tag their raw bits with the enclosing constructor;
+// both unfold to that constructor around the same 32-bit Word chain.
 
 export function lit_of(cs: U32[], s?: Span): LTerm {
   return cs.every((c) => c <= 0x10ffff && (c < 0xd800 || c > 0xdfff))
@@ -1194,6 +1196,9 @@ export function lit_chain(cs: U32[], s?: Span): LTerm {
 
 // one step: "" is SNil{}, "ct.." is SCon{Chr{c}, "t.."}, 0n is Zero{}, n is Succ{n-1}
 export function lit_step(t: Extract<LTerm, { $: "Lit" }>): LTerm {
+  if (t.k !== undefined) {
+    return Ctr(t.k, [word_to_term(t.v as U32, t.s)], t.s);
+  }
   if (typeof t.v === "number") {
     return t.v === 0 ? Ctr("Zero", [], t.s) : Ctr("Succ", [Lit(t.v - 1, t.s)], t.s);
   }
@@ -1204,6 +1209,9 @@ export function lit_step(t: Extract<LTerm, { $: "Lit" }>): LTerm {
 
 // the whole chain: a pattern's view
 export function lit_full(t: Extract<LTerm, { $: "Lit" }>): LTerm {
+  if (t.k !== undefined) {
+    return lit_step(t);
+  }
   if (typeof t.v === "string") {
     return lit_chain([...t.v].map((c) => c.codePointAt(0) as U32), t.s);
   }
@@ -1225,12 +1233,15 @@ export function nat_from_term(t: LTerm): number | null {
     t = t.x[0];
   }
   return t.$ === "Ctr" && t.k === "Zero" && t.x.length === 0 ? n
-    : t.$ === "Lit" && typeof t.v === "number" && n + t.v <= 0xffffffff
+    : t.$ === "Lit" && t.k === undefined && typeof t.v === "number" && n + t.v <= 0xffffffff
     ? n + t.v : null;
 }
 
 export function u32_from_term<X>(tm: TermOf<X>, k: Name = "U32"): number | null {
   const w0 = term_strip(tm);
+  if (w0.$ === "Lit") {
+    return w0.k === k ? w0.v as U32 : null;
+  }
   if (w0.$ !== "Ctr" || w0.k !== k || w0.x.length !== 1) {
     return null;
   }
@@ -1480,6 +1491,9 @@ export function term_show(term: LTerm, top: number = -1, bnd: Name[] = []): stri
         return tm.k + "{" + as.join(", ") + "}";
       }
       case "Lit": {
+        if (tm.k !== undefined) {
+          return tm.k === "U32" ? String(tm.v) : f32_show(f32_from_bits(tm.v as U32));
+        }
         return typeof tm.v === "number" ? String(tm.v) + "n" : "\"" + lit_text(tm.v) + "\"";
       }
       case "Mat": {
@@ -2304,7 +2318,7 @@ export function parse_term_num(p: Parse): LTerm {
       parse_fail(p, "a float literal with a finite f32 value (got " + m[0] + ")");
     }
     const spn = parse_span(p, beg);
-    return Ctr("F32", [word_to_term(f32_to_bits(v), spn)], spn);
+    return Lit(f32_to_bits(v), spn, "F32");
   }
   if (m[2] === undefined) {
     if (char_is_name(parse_peek(p))) {
@@ -2314,7 +2328,7 @@ export function parse_term_num(p: Parse): LTerm {
     if (w > 0xffffffff) {
       parse_fail(p, "a u32 literal up to 4294967295 (got " + s + ")");
     }
-    return u32_to_term(w, parse_span(p, beg));
+    return Lit(w, parse_span(p, beg), "U32");
   }
   const n = Number(s);
   if (n > 0xffffffff) {
@@ -2323,7 +2337,7 @@ export function parse_term_num(p: Parse): LTerm {
   if (parse_take(p, "+")) {
     let out = parse_term(p);
     const spn = parse_span(p, beg);
-    if (out.$ === "Lit" && typeof out.v === "number" && n + out.v <= 0xffffffff) {
+    if (out.$ === "Lit" && out.k === undefined && typeof out.v === "number" && n + out.v <= 0xffffffff) {
       return Lit(n + out.v, spn);
     }
     if (n > NAT_LITERAL_MAX) {
@@ -3279,7 +3293,7 @@ export function term_compare(mode: "EQ" | "LE", book: Book, lhs: HTerm, rhs: HTe
           && a.x.every((x, j) => term_compare("EQ", book, x, b.x[j], dep));
     }
     case "Lit": {
-      return b.$ === "Lit" && a.v === b.v;
+      return b.$ === "Lit" && a.k === b.k && a.v === b.v;
     }
     case "Mat": {
       return b.$ === "Mat" && a.k === b.k
@@ -3619,15 +3633,15 @@ export function term_check(book: Book, lhs: LHS, tm: HTerm, qt: Quant, ty: HTerm
       const { xs, us } = tele_check(book, lhs, tel, tm.x, qt, ctx, d, tm.s);
       return Check(Ctr(tm.k, xs, tm.s), ty, us);
     }
-    // T == Base's String (or Nat) with the literal's head: SNil/SCon (Zero/Succ)
+    // T == Base's String, Nat, U32 or F32 with the literal's head
     // where any other T checks the literal's first step, which reports
     //       as the constructor it is
     // ----------------------------------------------------------- check-lit
     // Γ ⊢ "text" : T ~ {}    Γ ⊢ 3n : T ~ {}
     case "Lit": {
       const t_wnf = term_wnf(book, ty);
-      const c = typeof tm.v === "number" ? tm.v === 0 ? "Zero" : "Succ"
-              : tm.v === "" ? "SNil" : "SCon";
+      const c = tm.k ?? (typeof tm.v === "number" ? tm.v === 0 ? "Zero" : "Succ"
+              : tm.v === "" ? "SNil" : "SCon");
       if (t_wnf.$ === "ADT" && book.tlds[t_wnf.k]?.b === true
         && ctrs_find(book_adt(book, t_wnf, ctx, lhs.def).c, c) !== null) {
         return Check(tm, ty, uses_nil());

bend2/comp.ts

@@ -691,7 +691,7 @@ function term_force(t: HTerm): HTerm {
   }
   // a Nat literal past the cap is U32.to_nat of its word
   return memo(LITS, s, () => Bend.term_higher(
-    typeof s.v === "number" && s.v > Bend.NAT_LITERAL_MAX
+    s.k === undefined && typeof s.v === "number" && s.v > Bend.NAT_LITERAL_MAX
       ? Bend.App(Bend.Ref("U32.to_nat"), Bend.u32_to_term(s.v))
       : Bend.lit_full(s)));
 }

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", 43000);
+allow("bend2/bend.ts", 43300);
 allow("bend2/comp.ts", 64000);
 allow("bend2/main.ts", 10000);
 allow(/^bend2\/effs\/[a-z0-9_]+\.(c|js)$/, 4000);

tests/check/f32_literal_own_f32.bend

@@ -0,0 +1,17 @@
+# a float literal is an F32 only where F32 declares the F32
+# constructor: a module's own F32 with another constructor checks the
+# literal's word, which reports as the constructor it is
+type F32 is Data:
+  Foo{}
+
+def n() -> F32:
+  1.5
+
+#|Error:
+#|- expected : a declared constructor (F32 declares Foo)
+#|- observed : 1.5
+#|Location: n
+#|7 | def n() -> F32:
+#|8>|   1.5
+#|9 | 
+#|exit 1

tests/check/u32_literal_own_u32.bend

@@ -0,0 +1,17 @@
+# a literal is a U32 only where U32 declares the U32 constructor: a
+# module's own U32 with another constructor checks the literal's word,
+# which reports as the constructor it is
+type U32 is Data:
+  Foo{}
+
+def n() -> U32:
+  5
+
+#|Error:
+#|- expected : a declared constructor (U32 declares Foo)
+#|- observed : 5
+#|Location: n
+#|7 | def n() -> U32:
+#|8>|   5
+#|9 | 
+#|exit 1

tests/compile/f32_literal_word.bend

@@ -0,0 +1,18 @@
+# a float literal is one Lit node; the compiler reads it as its word,
+# so a float immediate, float arithmetic and a match on float literal
+# patterns reach all three lanes as the number they are
+import Base
+
+def key(x: F32) -> U32:
+  match x:
+    case 1.5:
+      10
+    case 2.5:
+      20
+    case _:
+      30
+
+def main() -> IO(Unit):
+  IO.print(F32.show(F32.add(1.5, 2.5)) ++ " " ++ U32.show(key(1.5)))
+
+#|4 10

tests/compile/u32_literal_word.bend

@@ -0,0 +1,27 @@
+# a u32 literal is one Lit node; the compiler reads it as its word, so a
+# wide immediate, a wrapping operation and a match on wide literal
+# patterns reach all three lanes as the number they are
+import Base
+
+def key(n: U32) -> U32:
+  match n:
+    case 0:
+      10
+    case 3000000000:
+      20
+    case 4294967295:
+      30
+    case _:
+      40
+
+def word() -> U32:
+  U32.add(4294967290, 10)
+
+def main() -> IO(Unit):
+  a = key(3000000000)
+  b = key(4294967295)
+  c = key(7)
+  d = word()
+  IO.print(U32.show(U32.add(a, U32.add(b, U32.add(c, d)))) ++ " " ++ Char.show('q'))
+
+#|94 q

tests/parse/nat_plus_u32.bend

@@ -0,0 +1,16 @@
+# a nat literal plus a u32 literal is not a nat sum: 1n+5 is Succ{u32 5}
+# whose field is a U32, so it is refused at a Nat rather than folded
+import Base
+
+def main() -> Nat:
+  1n+5
+
+#|
+#|Error:
+#|- expected : Nat
+#|- observed : U32
+#|Location: main
+#|5 | def main() -> Nat:
+#|6>|   1n+5
+#|7 | 
+#|exit 1

tests/printer/f32_literal_print.bend

@@ -0,0 +1,11 @@
+# a float literal prints back as its number, and a term built on float
+# literals prints as it was written
+import Base
+
+def wide(a: F32) -> F32:
+  F32.add(3.14159, a)
+
+def main(a: F32, b: F32) -> F32:
+  F32.add(wide(a), F32.add(1.5e3, b))
+
+#|a => b => F32.add(F32.add(3.14159, a), F32.add(1500.0, b))

tests/printer/u32_literal_print.bend

@@ -0,0 +1,11 @@
+# a u32 literal prints back as its number, and a term built on wide
+# literals prints as it was written
+import Base
+
+def wide(a: U32) -> U32:
+  U32.add(3000000000, a)
+
+def main(a: U32, b: U32) -> U32:
+  U32.add(wide(a), U32.add(4294967295, b))
+
+#|a => b => U32.add(U32.add(3000000000, a), U32.add(4294967295, b))

tests/proof/f32_literal_unfolds.bend

@@ -0,0 +1,20 @@
+# a float literal is one Lit node holding its bits: two spellings of
+# the same f32 compare equal, and the exponent form is the same literal
+import Base
+
+law sci_eq:
+  {1.5e3 == 1500.0 : F32}
+
+def sci_eq():
+  {==}
+
+law exp_eq:
+  {1.25e-2 == 0.0125 : F32}
+
+def exp_eq():
+  {==}
+
+def main() -> U32:
+  0
+
+#|0

tests/proof/u32_literal_unfolds.bend

@@ -0,0 +1,49 @@
+# a u32 literal is one Lit node whose word unfolds whole where a chain
+# is read: a comparison sees a wide literal as its U32{WCon{..}} and a
+# wrapping operation reduces onto one, and a match reads a wide literal
+# pattern
+import Base
+
+law wrap_inc:
+  {U32.inc(4294967295) == 0 : U32}
+
+def wrap_inc():
+  {==}
+
+law wrap_add:
+  {U32.add(4294967290, 10) == 4 : U32}
+
+def wrap_add():
+  {==}
+
+law add_zero:
+  {U32.add(3000000000, 0) == 3000000000 : U32}
+
+def add_zero():
+  {==}
+
+law sub_wrap:
+  {U32.sub(0, 1) == 4294967295 : U32}
+
+def sub_wrap():
+  {==}
+
+def classify(n: U32) -> U32:
+  match n:
+    case 3000000000:
+      7
+    case 4294967295:
+      9
+    case _:
+      1
+
+law classify_big:
+  {classify(3000000000) == 7 : U32}
+
+def classify_big():
+  {==}
+
+def main() -> U32:
+  U32.add(classify(3000000000), classify(4294967295))
+
+#|16