From 33dee09d6af8e9dbd33f90402632f536a7018c69 Mon Sep 17 00:00:00 2001 From: Noah Gardner Date: Fri, 23 Oct 2026 01:15:34 -0400 Subject: [PATCH] feat(num): num.fixed writes a number with N decimals, half to even (JSON-FIX) `num.fixed(raw, places)` writes a JSON number's text with exactly `places` decimals, rounding half to even on its decimal digits, as Python's `Decimal(raw).quantize(..., ROUND_HALF_EVEN)` does and as Python's `'%.Nf' % x` does whenever the text is exactly a double. It reads exponents, keeps a minus on a value that rounds to zero (`-0.0`), and is None when the text is not a JSON number. Services were formatting `'%.1f'` by hand on number text. Spec-first: JSON-FIX-1 to JSON-FIX-5 are new Proved rows (result and None, sign, cut and exponent, rounding, writing), proved by 53 tagged quantified laws in LAWS.bend. SPEC.md documents where Python's binary rounding differs (2.675, 0.15, 1e23, 1e400). The trust boundary is unchanged. Co-Authored-By: Claude Opus 5.5 --- LAWS.bend | 440 +++++++++++++++++++++++++++++++++++++++++++++++++ PROOF.bend | 394 +++++++++++++++++++++++++++++++++++++++++++ README.md | 9 + SPEC.md | 14 +- main.bend | 9 + src/fixed.bend | 319 +++++++++++++++++++++++++++++++++++ 6 files changed, 1184 insertions(+), 1 deletion(-) create mode 100644 src/fixed.bend diff --git a/LAWS.bend b/LAWS.bend index ba8c8b4..aeaca30 100644 --- a/LAWS.bend +++ b/LAWS.bend @@ -6,6 +6,7 @@ import ./src/value.bend as V import ./main.bend as Ezjson import ./src/print.bend as Print import ./src/pull.bend as Pull +import ./src/fixed.bend as F # a boolean def is_bool(val: V.Json) -> Bool: @@ -2026,3 +2027,442 @@ law pull_skip_next: for +h_s: {short(rest_of(cur)) == True{} : Bool} for +h_v: {val_len(pulled(mm, cur), 0n) == Some{mm} : Maybe<&2, Nat>} {ev_of(Ezjson.next(Ezjson.skip(cur))) == ev_of(Ezjson.next(nexts(mm, cur))) : Pull.Ev} + +# --- fixed decimals (JSON-FIX) --- + +# no character of the text is an exponent mark, `e` or `E` +def no_e(+txt: String) -> Bool: + match txt: + case SNil{}: + True{} + case SCon{+ch, +tl}: + when(F.mark.e(ch), False{}, no_e(tl)) + +# no character of the text is a decimal point +def no_dot(+txt: String) -> Bool: + match txt: + case SNil{}: + True{} + case SCon{+ch, +tl}: + when(F.mark.dot(ch), False{}, no_dot(tl)) + +# a character's place against `5` +def vs5(+ch: Char) -> Cmp: + U32.cmp(Char.to_u32(ch), 53) + +# LAW: num.fixed of a text that is not a JSON number is None +# JSON-FIX-1 +law fixed_none: + for +txt: String + for +nn: Nat + for +h: {V.num.ok(txt) == False{} : Bool} + {Ezjson.num.fixed(txt, nn) == None{} : Maybe<&2, String>} + +# LAW: num.fixed of a JSON number is Some of its text with nn decimals +# JSON-FIX-1 +law fixed_some: + for +txt: String + for +nn: Nat + for +h: {V.num.ok(txt) == True{} : Bool} + {Ezjson.num.fixed(txt, nn) == Some{F.text(txt, nn)} : Maybe<&2, String>} + +# LAW: a leading minus is written, then the rest unsigned, whatever the +# digits round to +# JSON-FIX-2 +law text_minus: + for +txt: String + for +nn: Nat + {F.text("-" ++ txt, nn) == "-" ++ F.unsigned(txt, nn) : String} + +# LAW: a text that starts with anything but a minus is written unsigned +# JSON-FIX-2 +law text_plain: + for +ch: Char + for +tl: String + for +nn: Nat + for +h: {Char.is_eq(ch, '-') == False{} : Bool} + {F.text(SCon{ch, tl}, nn) == F.unsigned(SCon{ch, tl}, nn) : String} + +# LAW: the empty text is written unsigned +# JSON-FIX-2 +law text_empty: + for +nn: Nat + {F.text("", nn) == F.unsigned("", nn) : String} + +# LAW: an unsigned text is split, its point moved, rounded at nn places and +# written +# JSON-FIX-3 +law unsigned_steps: + for +txt: String + for +nn: Nat + {F.unsigned(txt, nn) == F.write(nn, F.round(nn, F.place(F.parts(txt)))) + : String} + +# LAW: a text with an exponent mark is cut at the first one: the mantissa +# before it, the exponent after it +# JSON-FIX-3 +law parts_exp: + for +mant: String + for +ch: Char + for +exp: String + for +h_m: {no_e(mant) == True{} : Bool} + for +h_c: {F.mark.e(ch) == True{} : Bool} + {F.parts(mant ++ SCon{ch, exp}) == (F.cut.dot(mant), F.esign(exp)) + : (String & String) & (Bool & String)} + +# LAW: a text with no exponent mark is all mantissa, with exponent 0 +# JSON-FIX-3 +law parts_plain: + for +mant: String + for +h_m: {no_e(mant) == True{} : Bool} + {F.parts(mant) == (F.cut.dot(mant), (False{}, "")) + : (String & String) & (Bool & String)} + +# LAW: a mantissa with a point is cut at the first one: the integer digits +# before it, the fraction digits after it +# JSON-FIX-3 +law mant_dot: + for +int: String + for +frac: String + for +h_i: {no_dot(int) == True{} : Bool} + {F.cut.dot(int ++ "." ++ frac) == (int, frac) : String & String} + +# LAW: a mantissa with no point is all integer digits +# JSON-FIX-3 +law mant_int: + for +int: String + for +h_i: {no_dot(int) == True{} : Bool} + {F.cut.dot(int) == (int, "") : String & String} + +# LAW: an exponent's leading minus makes it negative +# JSON-FIX-3 +law esign_minus: + for +exp: String + {F.esign("-" ++ exp) == (True{}, exp) : Bool & String} + +# LAW: an exponent's leading plus is dropped +# JSON-FIX-3 +law esign_plus: + for +exp: String + {F.esign("+" ++ exp) == (False{}, exp) : Bool & String} + +# LAW: an exponent with no sign is positive and keeps every digit +# JSON-FIX-3 +law esign_digits: + for +ch: Char + for +tl: String + for +h_m: {Char.is_eq(ch, '-') == False{} : Bool} + for +h_p: {Char.is_eq(ch, '+') == False{} : Bool} + {F.esign(SCon{ch, tl}) == (False{}, SCon{ch, tl}) : Bool & String} + +# LAW: the integer digits, last first, and the fraction digits stand around +# the point, which the exponent moves +# JSON-FIX-3 +law place_parts: + for +int: String + for +frac: String + for +neg: Bool + for +exp: String + {F.place(((int, frac), (neg, exp))) + == F.move(neg, F.nat(exp), F.Dec{String.reverse(int), frac}) : F.Dec} + +# LAW: an exponent's digits are read from 0 +# JSON-FIX-3 +law nat_start: + for +exp: String + {F.nat(exp) == F.nat.go(exp, 0n) : Nat} + +# LAW: reading no more digits leaves the value read +# JSON-FIX-3 +law nat_end: + for +acc: Nat + {F.nat.go("", acc) == acc : Nat} + +# LAW: one more digit at the end is ten times the value so far plus that +# digit: most significant first +# JSON-FIX-3 +law nat_snoc: + for +exp: String + for +ch: Char + for +acc: Nat + {F.nat.go(exp ++ SCon{ch, SNil{}}, acc) + == Nat.add(Nat.mul(F.nat.go(exp, acc), 10n), + U32.to_nat(U32.sub(Char.to_u32(ch), 48))) : Nat} + +# LAW: a positive exponent moves the point right, a negative one left +# JSON-FIX-3 +law move_right: + for +kk: Nat + for +dec: F.Dec + {F.move(False{}, kk, dec) == F.ups(kk, dec) : F.Dec} + +# LAW: a negative exponent moves the point left +# JSON-FIX-3 +law move_left: + for +kk: Nat + for +dec: F.Dec + {F.move(True{}, kk, dec) == F.downs(kk, dec) : F.Dec} + +# LAW: moving the point no places right leaves it +# JSON-FIX-3 +law ups_zero: + for +dec: F.Dec + {F.ups(0n, dec) == dec : F.Dec} + +# LAW: moving the point k + 1 places right is one move, then k +# JSON-FIX-3 +law ups_succ: + for +kk: Nat + for +dec: F.Dec + {F.ups(1n+kk, dec) == F.ups(kk, F.up(dec)) : F.Dec} + +# LAW: moving the point no places left leaves it +# JSON-FIX-3 +law downs_zero: + for +dec: F.Dec + {F.downs(0n, dec) == dec : F.Dec} + +# LAW: moving the point k + 1 places left is one move, then k +# JSON-FIX-3 +law downs_succ: + for +kk: Nat + for +dec: F.Dec + {F.downs(1n+kk, dec) == F.downs(kk, F.down(dec)) : F.Dec} + +# LAW: one move right carries the first fraction digit before the point +# JSON-FIX-3 +law up_digit: + for +left: String + for +ch: Char + for +tl: String + {F.up(F.Dec{left, SCon{ch, tl}}) == F.Dec{SCon{ch, left}, tl} : F.Dec} + +# LAW: one move right with no fraction digit carries a 0 before the point +# JSON-FIX-3 +law up_zero: + for +left: String + {F.up(F.Dec{left, ""}) == F.Dec{SCon{'0', left}, ""} : F.Dec} + +# LAW: one move left carries the last integer digit after the point +# JSON-FIX-3 +law down_digit: + for +ch: Char + for +tl: String + for +right: String + {F.down(F.Dec{SCon{ch, tl}, right}) == F.Dec{tl, SCon{ch, right}} : F.Dec} + +# LAW: one move left with no integer digit carries a 0 after the point +# JSON-FIX-3 +law down_zero: + for +right: String + {F.down(F.Dec{"", right}) == F.Dec{"", SCon{'0', right}} : F.Dec} + +# LAW: a move right then left gives back the digits around the point +# JSON-FIX-3 +law up_down: + for +left: String + for +ch: Char + for +tl: String + {F.down(F.up(F.Dec{left, SCon{ch, tl}})) == F.Dec{left, SCon{ch, tl}} + : F.Dec} + +# LAW: a move left then right gives back the digits around the point +# JSON-FIX-3 +law down_up: + for +ch: Char + for +tl: String + for +right: String + {F.up(F.down(F.Dec{SCon{ch, tl}, right})) == F.Dec{SCon{ch, tl}, right} + : F.Dec} + +# LAW: rounding cuts the fraction after nn places, joins the kept digits +# last first, and adds one when the dropped digits say so +# JSON-FIX-4 +law round_cut: + for +nn: Nat + for +left: String + for +right: String + for +kept: String + for +dropped: String + for +h: {F.pad(nn, right) == (kept, dropped) : String & String} + {F.round(nn, F.Dec{left, right}) + == F.bump(F.round.up(dropped, String.reverse.go(kept, left)), + String.reverse.go(kept, left)) : String} + +# LAW: the kept fraction digits are exactly nn +# JSON-FIX-4 +law pad_width: + for +nn: Nat + for +right: String + {String.length(Pair.fst(String, String, F.pad(nn, right))) == nn : Nat} + +# LAW: no place kept keeps nothing and drops every fraction digit +# JSON-FIX-4 +law pad_none: + for +right: String + {F.pad(0n, right) == ("", right) : String & String} + +# LAW: a kept place takes the next fraction digit +# JSON-FIX-4 +law pad_digit: + for +mm: Nat + for +ch: Char + for +tl: String + {F.pad(1n+mm, SCon{ch, tl}) == F.cut.put(ch, F.pad(mm, tl)) + : String & String} + +# LAW: a kept place past the last fraction digit is a 0 +# JSON-FIX-4 +law pad_past: + for +mm: Nat + {F.pad(1n+mm, "") == F.cut.put('0', F.pad(mm, "")) : String & String} + +# LAW: no dropped digit: no rounding +# JSON-FIX-4 +law up_exact: + for +kept: String + {F.round.up("", kept) == False{} : Bool} + +# LAW: a first dropped digit below 5 rounds down +# JSON-FIX-4 +law up_below: + for +dd: Char + for +rest: String + for +kept: String + for +h: {vs5(dd) == LT{} : Cmp} + {F.round.up(SCon{dd, rest}, kept) == False{} : Bool} + +# LAW: a first dropped digit above 5 rounds up +# JSON-FIX-4 +law up_above: + for +dd: Char + for +rest: String + for +kept: String + for +h: {vs5(dd) == GT{} : Cmp} + {F.round.up(SCon{dd, rest}, kept) == True{} : Bool} + +# LAW: a first dropped digit of 5 with a later nonzero dropped digit is past +# half, and rounds up +# JSON-FIX-4 +law up_past_half: + for +dd: Char + for +rest: String + for +kept: String + for +h_d: {vs5(dd) == EQ{} : Cmp} + for +h_r: {F.nonzero(rest) == True{} : Bool} + {F.round.up(SCon{dd, rest}, kept) == True{} : Bool} + +# LAW: an exact half rounds up exactly when the last kept digit is odd +# JSON-FIX-4 +law up_tie: + for +dd: Char + for +rest: String + for +last: Char + for +kept: String + for +h_d: {vs5(dd) == EQ{} : Cmp} + for +h_r: {F.nonzero(rest) == False{} : Bool} + {F.round.up(SCon{dd, rest}, SCon{last, kept}) + == U32.is_eq(U32.mod(Char.to_u32(last), 2), 1) : Bool} + +# LAW: an exact half with no kept digit (an empty integer part and no +# places) counts as even 0, and rounds down +# JSON-FIX-4 +law up_tie_none: + for +dd: Char + for +rest: String + for +h_d: {vs5(dd) == EQ{} : Cmp} + for +h_r: {F.nonzero(rest) == False{} : Bool} + {F.round.up(SCon{dd, rest}, "") == False{} : Bool} + +# LAW: dropped digits that are all 0 are not past half +# JSON-FIX-4 +law nonzero_zeros: + for +kk: Nat + {F.nonzero(String.repeat("0", kk)) == False{} : Bool} + +# LAW: a digit other than 0 anywhere among the dropped digits is past half +# JSON-FIX-4 +law nonzero_digit: + for +pre: String + for +ch: Char + for +post: String + for +h: {Char.is_eq(ch, '0') == False{} : Bool} + {F.nonzero(pre ++ SCon{ch, post}) == True{} : Bool} + +# LAW: rounding up adds one, rounding down keeps the digits +# JSON-FIX-4 +law bump_up: + for +kept: String + {F.bump(True{}, kept) == F.inc(kept) : String} + +# LAW: rounding down keeps the digits +# JSON-FIX-4 +law bump_down: + for +kept: String + {F.bump(False{}, kept) == kept : String} + +# LAW: adding one to a last digit other than 9 makes it the next digit +# JSON-FIX-4 +law inc_digit: + for +ch: Char + for +tl: String + for +h: {Char.is_eq(ch, '9') == False{} : Bool} + {F.inc(SCon{ch, tl}) == SCon{Char.from_u32(U32.add(Char.to_u32(ch), 1)), tl} + : String} + +# LAW: adding one to a last digit 9 makes it 0 and carries one +# JSON-FIX-4 +law inc_nine: + for +tl: String + {F.inc(SCon{'9', tl}) == SCon{'0', F.inc(tl)} : String} + +# LAW: adding one to all 9s makes them 0s and a new leading 1 +# JSON-FIX-4 +law inc_nines: + for +kk: Nat + {F.inc(String.repeat("9", kk)) == String.repeat("0", kk) ++ "1" : String} + +# LAW: the rounded digits (last first) are written as the integer part, the +# digits before the last nn, and the fraction, the last nn +# JSON-FIX-5 +law write_parts: + for +nn: Nat + for +digits: String + {F.write(nn, digits) + == F.point(nn, F.trim(String.reverse(String.drop(digits, nn))), + String.reverse(String.take(digits, nn))) : String} + +# LAW: no places writes the integer part alone, with no point +# JSON-FIX-5 +law point_none: + for +int: String + for +frac: String + {F.point(0n, int, frac) == int : String} + +# LAW: one or more places write the integer part, a point and the fraction +# JSON-FIX-5 +law point_some: + for +mm: Nat + for +int: String + for +frac: String + {F.point(1n+mm, int, frac) == int ++ "." ++ frac : String} + +# LAW: a leading 0 of the integer part is dropped +# JSON-FIX-5 +law trim_zero: + for +tl: String + {F.trim(SCon{'0', tl}) == F.trim(tl) : String} + +# LAW: an integer part that starts with another digit is kept whole +# JSON-FIX-5 +law trim_lead: + for +ch: Char + for +tl: String + for +h: {Char.is_eq(ch, '0') == False{} : Bool} + {F.trim(SCon{ch, tl}) == SCon{ch, tl} : String} + +# LAW: an integer part of only 0s, or none, is written 0 +# JSON-FIX-5 +law trim_zeros: + for +kk: Nat + {F.trim(String.repeat("0", kk)) == "0" : String} diff --git a/PROOF.bend b/PROOF.bend index d7634f6..8a50e65 100644 --- a/PROOF.bend +++ b/PROOF.bend @@ -7,6 +7,7 @@ import ./src/lex.bend as Lex import ./src/parse.bend as Parse import ./src/print.bend as Print import ./src/pull.bend as Pull +import ./src/fixed.bend as F import ./LAWS.bend as Laws # Unit for True, Empty for False: tells them apart @@ -53093,3 +53094,396 @@ def Laws.pretty_parse(val, h_wf, h_s): Laws.text_some(gg, "", "", pq.ok(val, "", "", V.WVal{}, h_wf, {==}, {==}), {==}, {==}, es), Equal.cong(V.Json, Maybe<&2, V.Json>, zz => Some{zz}, Laws.g.val(gg), Laws.fixv(Laws.own(val)), pq.val(val, "", "", V.WVal{}, h_wf)))) + +# --- fixed decimals (JSON-FIX) --- + +# a true `when` with a false yes: its test is false +law fx_when_test: + for +cc: Bool + for +rest: Bool + for +h: {Laws.when(cc, False{}, rest) == True{} : Bool} + {cc == False{} : Bool} + +def fx_when_test(cc, _rest, h): + match cc: + case True{}: + Empty.absurd({True{} == False{} : Bool}, false_true(h)) + case False{}: + {==} + +# a true `when` with a false yes: its no is true +law fx_when_rest: + for +cc: Bool + for +rest: Bool + for +h: {Laws.when(cc, False{}, rest) == True{} : Bool} + {rest == True{} : Bool} + +def fx_when_rest(cc, _rest, h): + match cc: + case True{}: + Empty.absurd({_rest == True{} : Bool}, false_true(h)) + case False{}: + h + +# a text with no exponent mark, then a mark: the cut is at that mark +law fx_cut_e_hit: + for +aa: String + for +ch: Char + for +bb: String + for +h_a: {Laws.no_e(aa) == True{} : Bool} + for +h_c: {F.mark.e(ch) == True{} : Bool} + {F.cut.e(aa ++ SCon{ch, bb}) == (aa, bb) : String & String} + +def fx_cut_e_hit(aa, ch, bb, h_a, h_c): + match aa: + case SNil{}: + %Equal.sym(Bool, F.mark.e(ch), True{}, h_c) + : {F.cut.at(_, ch, bb, _u => F.cut.e(bb)) == ("", bb) : String & String} + {==} + case SCon{+cc, +tl}: + %Equal.sym(Bool, F.mark.e(cc), False{}, + fx_when_test(F.mark.e(cc), Laws.no_e(tl), h_a)) + : {F.cut.at(_, cc, tl ++ SCon{ch, bb}, _u => F.cut.e(tl ++ SCon{ch, bb})) + == (SCon{cc, tl}, bb) : String & String} + Equal.cong(String & String, String & String, pp => F.cut.put(cc, pp), + F.cut.e(tl ++ SCon{ch, bb}), (tl, bb), + fx_cut_e_hit(tl, ch, bb, fx_when_rest(F.mark.e(cc), Laws.no_e(tl), h_a), + h_c)) + +# a text with no exponent mark is not cut +law fx_cut_e_none: + for +aa: String + for +h_a: {Laws.no_e(aa) == True{} : Bool} + {F.cut.e(aa) == (aa, "") : String & String} + +def fx_cut_e_none(aa, h_a): + match aa: + case SNil{}: + {==} + case SCon{+cc, +tl}: + %Equal.sym(Bool, F.mark.e(cc), False{}, + fx_when_test(F.mark.e(cc), Laws.no_e(tl), h_a)) + : {F.cut.at(_, cc, tl, _u => F.cut.e(tl)) == (SCon{cc, tl}, "") + : String & String} + Equal.cong(String & String, String & String, pp => F.cut.put(cc, pp), + F.cut.e(tl), (tl, ""), + fx_cut_e_none(tl, fx_when_rest(F.mark.e(cc), Laws.no_e(tl), h_a))) + +# a text with no point, then a point: the cut is at that point +law fx_cut_dot_hit: + for +aa: String + for +bb: String + for +h_a: {Laws.no_dot(aa) == True{} : Bool} + {F.cut.dot(aa ++ SCon{'.', bb}) == (aa, bb) : String & String} + +def fx_cut_dot_hit(aa, bb, h_a): + match aa: + case SNil{}: + {==} + case SCon{+cc, +tl}: + %Equal.sym(Bool, F.mark.dot(cc), False{}, + fx_when_test(F.mark.dot(cc), Laws.no_dot(tl), h_a)) + : {F.cut.at(_, cc, tl ++ SCon{'.', bb}, _u => F.cut.dot(tl ++ SCon{'.', bb})) + == (SCon{cc, tl}, bb) : String & String} + Equal.cong(String & String, String & String, pp => F.cut.put(cc, pp), + F.cut.dot(tl ++ SCon{'.', bb}), (tl, bb), + fx_cut_dot_hit(tl, bb, fx_when_rest(F.mark.dot(cc), Laws.no_dot(tl), h_a))) + +# a text with no point is not cut +law fx_cut_dot_none: + for +aa: String + for +h_a: {Laws.no_dot(aa) == True{} : Bool} + {F.cut.dot(aa) == (aa, "") : String & String} + +def fx_cut_dot_none(aa, h_a): + match aa: + case SNil{}: + {==} + case SCon{+cc, +tl}: + %Equal.sym(Bool, F.mark.dot(cc), False{}, + fx_when_test(F.mark.dot(cc), Laws.no_dot(tl), h_a)) + : {F.cut.at(_, cc, tl, _u => F.cut.dot(tl)) == (SCon{cc, tl}, "") + : String & String} + Equal.cong(String & String, String & String, pp => F.cut.put(cc, pp), + F.cut.dot(tl), (tl, ""), + fx_cut_dot_none(tl, fx_when_rest(F.mark.dot(cc), Laws.no_dot(tl), h_a))) + +def Laws.fixed_none(txt, nn, h): + %Equal.sym(Bool, V.num.ok(txt), False{}, h) + : {F.fixed.go(_, txt, nn) == None{} : Maybe<&2, String>} + {==} + +def Laws.fixed_some(txt, nn, h): + %Equal.sym(Bool, V.num.ok(txt), True{}, h) + : {F.fixed.go(_, txt, nn) == Some{F.text(txt, nn)} : Maybe<&2, String>} + {==} + +def Laws.text_minus(_txt, _nn): + {==} + +def Laws.text_plain(ch, tl, nn, h): + %Equal.sym(Bool, Char.is_eq(ch, '-'), False{}, h) + : {F.text.at(_, ch, tl, nn) == F.unsigned(SCon{ch, tl}, nn) : String} + {==} + +def Laws.text_empty(_nn): + {==} + +def Laws.unsigned_steps(_txt, _nn): + {==} + +def Laws.parts_exp(mant, ch, exp, h_m, h_c): + Equal.cong(String & String, (String & String) & (Bool & String), + pp => F.parts.of(pp), F.cut.e(mant ++ SCon{ch, exp}), (mant, exp), + fx_cut_e_hit(mant, ch, exp, h_m, h_c)) + +def Laws.parts_plain(mant, h_m): + Equal.cong(String & String, (String & String) & (Bool & String), + pp => F.parts.of(pp), F.cut.e(mant), (mant, ""), fx_cut_e_none(mant, h_m)) + +def Laws.mant_dot(int, frac, h_i): + fx_cut_dot_hit(int, frac, h_i) + +def Laws.mant_int(int, h_i): + fx_cut_dot_none(int, h_i) + +def Laws.esign_minus(_exp): + {==} + +def Laws.esign_plus(_exp): + {==} + +def Laws.esign_digits(ch, tl, h_m, h_p): + %Equal.sym(Bool, Char.is_eq(ch, '-'), False{}, h_m) + : {F.esign.at(_, Char.is_eq(ch, '+'), ch, tl) == (False{}, SCon{ch, tl}) + : Bool & String} + %Equal.sym(Bool, Char.is_eq(ch, '+'), False{}, h_p) + : {F.esign.at(False{}, _, ch, tl) == (False{}, SCon{ch, tl}) + : Bool & String} + {==} + +def Laws.place_parts(_int, _frac, _neg, _exp): + {==} + +def Laws.nat_start(_exp): + {==} + +def Laws.nat_end(_acc): + {==} + +def Laws.nat_snoc(exp, ch, acc): + match exp: + case SNil{}: + {==} + case SCon{+cc, +tl}: + Laws.nat_snoc(tl, ch, Nat.add(Nat.mul(acc, 10n), F.digit.nat(cc))) + +def Laws.move_right(_kk, _dec): + {==} + +def Laws.move_left(_kk, _dec): + {==} + +def Laws.ups_zero(_dec): + {==} + +def Laws.ups_succ(_kk, _dec): + {==} + +def Laws.downs_zero(_dec): + {==} + +def Laws.downs_succ(_kk, _dec): + {==} + +def Laws.up_digit(_left, _ch, _tl): + {==} + +def Laws.up_zero(_left): + {==} + +def Laws.down_digit(_ch, _tl, _right): + {==} + +def Laws.down_zero(_right): + {==} + +def Laws.up_down(_left, _ch, _tl): + {==} + +def Laws.down_up(_ch, _tl, _right): + {==} + +def Laws.round_cut(nn, left, right, kept, dropped, h): + %Equal.sym(String & String, F.pad(nn, right), (kept, dropped), h) + : {F.round.keep(left, _) + == F.bump(F.round.up(dropped, String.reverse.go(kept, left)), + String.reverse.go(kept, left)) : String} + {==} + +# a character put before a pair's first is the first's head +law fx_put_fst: + for +ch: Char + for pp: String & String + {Pair.fst(String, String, F.cut.put(ch, pp)) + == SCon{ch, Pair.fst(String, String, pp)} : String} + +def fx_put_fst(_ch, pp): + match pp: + case (_a, _b): + {==} + +def Laws.pad_width(nn, right): + match nn: + case 0n: + {==} + case 1n+mm: + match right: + case SNil{}: + Equal.trans(Nat, + String.length(Pair.fst(String, String, F.cut.put('0', F.pad(mm, "")))), + 1n+String.length(Pair.fst(String, String, F.pad(mm, ""))), + 1n+mm, + Equal.cong(String, Nat, ss => String.length(ss), + Pair.fst(String, String, F.cut.put('0', F.pad(mm, ""))), + SCon{'0', Pair.fst(String, String, F.pad(mm, ""))}, + fx_put_fst('0', F.pad(mm, ""))), + Equal.cong(Nat, Nat, kk => 1n+kk, + String.length(Pair.fst(String, String, F.pad(mm, ""))), mm, + Laws.pad_width(mm, ""))) + case SCon{+cc, +tl}: + Equal.trans(Nat, + String.length(Pair.fst(String, String, F.cut.put(cc, F.pad(mm, tl)))), + 1n+String.length(Pair.fst(String, String, F.pad(mm, tl))), + 1n+mm, + Equal.cong(String, Nat, ss => String.length(ss), + Pair.fst(String, String, F.cut.put(cc, F.pad(mm, tl))), + SCon{cc, Pair.fst(String, String, F.pad(mm, tl))}, + fx_put_fst(cc, F.pad(mm, tl))), + Equal.cong(Nat, Nat, kk => 1n+kk, + String.length(Pair.fst(String, String, F.pad(mm, tl))), mm, + Laws.pad_width(mm, tl))) + +def Laws.pad_none(_right): + {==} + +def Laws.pad_digit(_mm, _ch, _tl): + {==} + +def Laws.pad_past(_mm): + {==} + +def Laws.up_exact(_kept): + {==} + +def Laws.up_below(dd, rest, kept, h): + %Equal.sym(Cmp, Laws.vs5(dd), LT{}, h) + : {F.round.at(_, rest, kept) == False{} : Bool} + {==} + +def Laws.up_above(dd, rest, kept, h): + %Equal.sym(Cmp, Laws.vs5(dd), GT{}, h) + : {F.round.at(_, rest, kept) == True{} : Bool} + {==} + +def Laws.up_past_half(dd, rest, kept, h_d, h_r): + %Equal.sym(Cmp, Laws.vs5(dd), EQ{}, h_d) + : {F.round.at(_, rest, kept) == True{} : Bool} + %Equal.sym(Bool, F.nonzero(rest), True{}, h_r) + : {F.tie(_, kept) == True{} : Bool} + {==} + +def Laws.up_tie(dd, rest, last, kept, h_d, h_r): + %Equal.sym(Cmp, Laws.vs5(dd), EQ{}, h_d) + : {F.round.at(_, rest, SCon{last, kept}) + == U32.is_eq(U32.mod(Char.to_u32(last), 2), 1) : Bool} + %Equal.sym(Bool, F.nonzero(rest), False{}, h_r) + : {F.tie(_, SCon{last, kept}) + == U32.is_eq(U32.mod(Char.to_u32(last), 2), 1) : Bool} + {==} + +def Laws.up_tie_none(dd, rest, h_d, h_r): + %Equal.sym(Cmp, Laws.vs5(dd), EQ{}, h_d) + : {F.round.at(_, rest, "") == False{} : Bool} + %Equal.sym(Bool, F.nonzero(rest), False{}, h_r) + : {F.tie(_, "") == False{} : Bool} + {==} + +def Laws.nonzero_zeros(kk): + match kk: + case 0n: + {==} + case 1n+jj: + Laws.nonzero_zeros(jj) + +# a nonzero step whose rest is true is true +law fx_at_true: + for +zero: Bool + for more: Unit -> Bool + for h: {more(Unit{}) == True{} : Bool} + {F.nonzero.at(zero, more) == True{} : Bool} + +def fx_at_true(zero, _more, h): + match zero: + case False{}: + {==} + case True{}: + h + +def Laws.nonzero_digit(pre, ch, post, h): + match pre: + case SNil{}: + %Equal.sym(Bool, Char.is_eq(ch, '0'), False{}, h) + : {F.nonzero.at(_, _u => F.nonzero(post)) == True{} : Bool} + {==} + case SCon{+cc, +tl}: + fx_at_true(Char.is_eq(cc, '0'), _u => F.nonzero(tl ++ SCon{ch, post}), + Laws.nonzero_digit(tl, ch, post, h)) + +def Laws.bump_up(_kept): + {==} + +def Laws.bump_down(_kept): + {==} + +def Laws.inc_digit(ch, tl, h): + %Equal.sym(Bool, Char.is_eq(ch, '9'), False{}, h) + : {F.inc.at(_, ch, tl, _u => F.inc(tl)) + == SCon{Char.from_u32(U32.add(Char.to_u32(ch), 1)), tl} : String} + {==} + +def Laws.inc_nine(_tl): + {==} + +def Laws.inc_nines(kk): + match kk: + case 0n: + {==} + case 1n+jj: + Equal.cong(String, String, ss => SCon{'0', ss}, + F.inc(String.repeat("9", jj)), String.repeat("0", jj) ++ "1", + Laws.inc_nines(jj)) + +def Laws.write_parts(_nn, _digits): + {==} + +def Laws.point_none(_int, _frac): + {==} + +def Laws.point_some(_mm, _int, _frac): + {==} + +def Laws.trim_zero(_tl): + {==} + +def Laws.trim_lead(ch, tl, h): + %Equal.sym(Bool, Char.is_eq(ch, '0'), False{}, h) + : {F.trim.at(_, ch, tl, _u => F.trim(tl)) == SCon{ch, tl} : String} + {==} + +def Laws.trim_zeros(kk): + match kk: + case 0n: + {==} + case 1n+jj: + Laws.trim_zeros(jj) diff --git a/README.md b/README.md index a676058..d857fcd 100644 --- a/README.md +++ b/README.md @@ -67,6 +67,15 @@ array's elements in order in one walk (a loop over `at` walks the array again for every index), and gives `[]` for anything that is not an array. `is_arr` and `is_obj` tell whether a value is an array or an object. +`num.fixed(s, n)` writes a number's text with exactly `n` decimals, as +Python's `'%.Nf'` does, but rounding half to even on the decimal digits +rather than through a binary float: `num.fixed("2.675", 2n)` is +`Some{"2.68"}` where Python's `'%.2f' % 2.675` is `2.67`. It reads +exponents (`1e-05` to 7 places is `0.0000100`), keeps a minus on a value +that rounds to zero (`-0.04` to 1 place is `-0.0`), and is `None` when the +text is not a JSON number. Pass it what `as_num` reads. SPEC.md's JSON-FIX +rows list where it and Python's float formatting differ. + ``` import emerging-ezjson@1.1.0.0/main.bend as Ezjson import emerging-ezjson@1.1.0.0/src/value.bend as Value diff --git a/SPEC.md b/SPEC.md index 3f86891..b9d1893 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1,6 +1,6 @@ # ezjson specification -This is the list of every behavior ezjson guarantees, each under a stable requirement ID. There are two families: conformance to [RFC 8259](https://www.rfc-editor.org/rfc/rfc8259) (JSON-TEXT, JSON-NUM, JSON-STR, JSON-PRINT) and the public interface in `main.bend` (JSON-TREE, JSON-PULL). Every other module is internal and carries no promise. +This is the list of every behavior ezjson guarantees, each under a stable requirement ID. There are two families: conformance to [RFC 8259](https://www.rfc-editor.org/rfc/rfc8259) (JSON-TEXT, JSON-NUM, JSON-STR, JSON-PRINT) and the public interface in `main.bend` (JSON-TREE, JSON-PULL, JSON-FIX). Every other module is internal and carries no promise. Every requirement has one of two levels. A **Proved** requirement holds for every input, and is backed by a quantified law (a `for` or `exs` binder) in `LAWS.bend` that passes the proof gate. A **Trusted** requirement is an assumption ezjson cannot check from inside its own gate, and it is listed in the trust boundary below. A Proved requirement whose laws have not all landed has status **pending**: we intend to prove it, and until then it is not guaranteed. The proof gate is this check: the first line `bend PROOF.bend` prints is exactly `ALL PROOFS CHECK`. Tests and fixtures are never evidence for a requirement. @@ -90,6 +90,18 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | JSON-PULL-5 | `skip` at a position where no value may start (before an object key, at a close bracket, after the root, or on a failed cursor) returns a failed cursor | Proved | proved | LAWS.bend pull_failed_skip; LAWS.bend pull_over_skip; LAWS.bend skip_key; LAWS.bend skip_close_arr; LAWS.bend skip_close_obj | | JSON-PULL-6 | `text(ev)` is `Some` of the decoded characters for a string or key event, span or owned, and of the spelling for a number event, and `None` for every other event | Proved | proved | LAWS.bend text_str; LAWS.bend text_key; LAWS.bend text_str_span; LAWS.bend text_key_span; LAWS.bend text_num; LAWS.bend text_none | +### Fixed decimals (JSON-FIX) + +`num.fixed(s, n)` writes a number's text with exactly `n` digits after the point, rounding half to even on its decimal digits. The reference is Python's `format(Decimal(s).quantize(Decimal(10) ** -n, ROUND_HALF_EVEN), 'f')`, which is IEEE 754's roundTiesToEven applied to the exact decimal value of `s`; on every input where that decimal value is exactly a binary double, this is also Python's `'%.{n}f' % float(s)` (C's `printf("%.*f")`). Python's `'%.Nf'` rounds the double nearest to `s`, not `s`, so the two differ where the double falls on the other side of a rounding boundary: `2.675` to 2 places is `2.68` here and `2.67` in Python (the double is 2.67499999999999982236431605997495353221893310546875), `0.15` to 1 is `0.2` here and `0.1` there, `0.45` is `0.4` here and `0.5` there, `0.0005` to 3 is `0.000` here and `0.001` there, `9.995` to 2 is `10.00` here and `9.99` there. They also differ past the 17 significant digits a double holds (`1e23` to 0 places is a 1 and 23 zeros here, `99999999999999991611392` there; `123456789012345678.5` to 0 is `123456789012345678` here, `123456789012345680` there) and past the double's range (`1e400` is written out in full here, `inf` there). Exact values agree (`0.125`, `2.5` to 0 places is `2`, `0.5` is `0`). The laws below state the steps over `src/fixed.bend`; together they define the result for every text, and LAWS.bend states each step in the order the text is read: the sign (JSON-FIX-2), the cut and the exponent (JSON-FIX-3), the rounding (JSON-FIX-4), the writing (JSON-FIX-5). The exponent is read as a natural number and the point moved one place a step, so the time and memory of a call grow with the exponent's value: `1e999999999` asks for a billion digits, and a caller formatting untrusted numbers bounds the exponent first. + +| ID | Requirement | Level | Status | Law | +| :---- | :---- | :---- | :---- | :---- | +| JSON-FIX-1 | For every text `s` and count `n`, `num.fixed(s, n)` is `None` when `num.ok(s)` is false, and `Some{F.text(s, n)}` when it is true, where `F.text` is `src/fixed.bend`'s writer that JSON-FIX-2 to JSON-FIX-5 describe | Proved | proved | LAWS.bend fixed_none; LAWS.bend fixed_some | +| JSON-FIX-2 | For every text `s` and count `n`, the text of `-` followed by `s` is `-` followed by the unsigned text of `s`, and a text that does not start with `-` (the empty one too) is written unsigned: the minus is kept even when every digit rounds to `0`, so `-0.04` to 1 place is `-0.0` and `-0` to 2 is `-0.00`, as Python's `'%.Nf'` and C's `printf` write a negative zero | Proved | proved | LAWS.bend text_minus; LAWS.bend text_plain; LAWS.bend text_empty | +| JSON-FIX-3 | An unsigned text is cut at its first `e` or `E` into a mantissa and an exponent (no mark: the exponent is empty), and the mantissa at its first `.` into integer and fraction digits (no point: the fraction is empty). An exponent's leading `-` makes it negative, a leading `+` is dropped, and any other exponent is positive and keeps every character. The exponent's digits are read most significant first as the natural number `k` (empty: 0). The integer digits, last first, and the fraction digits stand around the point, and the point moves `k` places right for a positive exponent and left for a negative one, one place a step: a move right carries the first fraction digit before the point, or a `0` when there is none, and a move left carries the last integer digit after the point, or a `0` when there is none; a move right then left, or left then right, gives the same digits back. So `1e-05` is `0.00001` and `2.5e1` is `25` | Proved | proved | LAWS.bend unsigned_steps; LAWS.bend parts_exp; LAWS.bend parts_plain; LAWS.bend mant_dot; LAWS.bend mant_int; LAWS.bend esign_minus; LAWS.bend esign_plus; LAWS.bend esign_digits; LAWS.bend place_parts; LAWS.bend nat_start; LAWS.bend nat_end; LAWS.bend nat_snoc; LAWS.bend move_right; LAWS.bend move_left; LAWS.bend ups_zero; LAWS.bend ups_succ; LAWS.bend downs_zero; LAWS.bend downs_succ; LAWS.bend up_digit; LAWS.bend up_zero; LAWS.bend down_digit; LAWS.bend down_zero; LAWS.bend up_down; LAWS.bend down_up | +| JSON-FIX-4 | The digits are cut after the `n`-th fraction place: exactly `n` fraction digits are kept, `0`s past the last fraction digit, and the rest are dropped. The kept digits go up by one in the last kept place exactly when the first dropped digit is above `5`; or is `5` and a later dropped digit is not `0`; or is `5`, every later dropped digit is `0`, and the last kept digit is odd (a tie goes to the even neighbour, and no kept digit at all counts as an even `0`). No dropped digit, or a first dropped digit below `5`, keeps the digits as they are. Going up by one makes a last `9` a `0` and carries, and all `9`s become `0`s under a new leading `1` | Proved | proved | LAWS.bend round_cut; LAWS.bend pad_width; LAWS.bend pad_none; LAWS.bend pad_digit; LAWS.bend pad_past; LAWS.bend up_exact; LAWS.bend up_below; LAWS.bend up_above; LAWS.bend up_past_half; LAWS.bend up_tie; LAWS.bend up_tie_none; LAWS.bend nonzero_zeros; LAWS.bend nonzero_digit; LAWS.bend bump_up; LAWS.bend bump_down; LAWS.bend inc_digit; LAWS.bend inc_nine; LAWS.bend inc_nines | +| JSON-FIX-5 | The rounded digits are written as the integer part, every digit before the last `n` with its leading `0`s dropped (`0` when none is left), followed by `.` and the last `n` digits when `n` is at least 1, and by nothing when `n` is 0: no point, as Python writes `'%.0f' % 2.5` as `2` | Proved | proved | LAWS.bend write_parts; LAWS.bend point_none; LAWS.bend point_some; LAWS.bend trim_zero; LAWS.bend trim_lead; LAWS.bend trim_zeros | + ## Left to prove Every row is proved. JSON-PULL-4 carries the same bound as JSON-PULL-1: its unread text is shorter than 2^32 characters. Without it the row fails for texts of about 2^35 characters or more: `skip` walks a whole value on one budget of 4 × (2^33 − 1) jumps and spends two on each bare word, so an array of about 2^34 numbers uses the budget up, and `skip` returns a failed cursor where `next` would read on. diff --git a/main.bend b/main.bend index 637bfa1..c63749b 100644 --- a/main.bend +++ b/main.bend @@ -11,6 +11,7 @@ import ./src/value.bend as Value import ./src/parse.bend as Parse import ./src/print.bend as Print import ./src/pull.bend as Pull +import ./src/fixed.bend as Fixed # a text as a value, or None when it is not JSON def parse(txt: String) -> Maybe<&2, Value.Json>: @@ -92,6 +93,14 @@ def as_str(val: Value.Json) -> Maybe<&2, String>: def as_num(val: Value.Json) -> Maybe<&2, String>: Value.as_num(val) +# a number's text written with `places` decimals, rounded half to even on +# its decimal digits (not through a binary float), as Python's `'%.Nf'` +# writes a value whose decimal text is exact; None when the text is not a +# JSON number. A `-` is kept even when the result is zero: `-0.04` to one +# place is `-0.0` +def num.fixed(raw: String, places: Nat) -> Maybe<&2, String>: + Fixed.fixed(raw, places) + # a number as a U32, or none when it is not one or does not fit def as_u32(val: Value.Json) -> Maybe<&2, U32>: Value.as_u32(val) diff --git a/src/fixed.bend b/src/fixed.bend new file mode 100644 index 0000000..5a9daa3 --- /dev/null +++ b/src/fixed.bend @@ -0,0 +1,319 @@ +# src/fixed: a JSON number's text written with a fixed count of decimals. +# The digits are rounded half to even as decimal digits, never through a +# binary float. The text is split at its `e` (or `E`) and its `.`; the +# exponent moves the point; the digits past the last kept place decide +# whether the kept ones go up by one; the integer part loses its leading +# zeros. A `-` is kept even when the rounded value is zero, as C's printf +# and Python's `'%.Nf'` keep it. +import Base +import ./value.bend as V + +# where a number's point is: the digits before it, last digit first, and the +# digits after it +type Dec is Data: + Dec{left: String, right: String} + +# --- splitting the text --- + +# an exponent mark, `e` or `E` +def mark.e(+ch: Char) -> Bool: + Bool.or(Char.is_eq(ch, 'e'), Char.is_eq(ch, 'E')) + +# a decimal point +def mark.dot(+ch: Char) -> Bool: + Char.is_eq(ch, '.') + +# put a character before the first of a pair +def cut.put(ch: Char, pair: String & String) -> String & String: + (a, b) = pair + (SCon{ch, a}, b) + +# at a mark the cut is made; any other character is kept before it +def cut.at( + hit: Bool, + ch: Char, + after: String, + more: Unit -> String & String +) -> String & String: + match hit: + case True{}: + ("", after) + case False{}: + cut.put(ch, more(Unit{})) + +# a text cut at its first exponent mark: what is before it, and after it +def cut.e(txt: String) -> String & String: + match txt: + case SNil{}: + ("", "") + case SCon{+hd, +tl}: + cut.at(mark.e(hd), hd, tl, _u => cut.e(tl)) + +# a text cut at its first decimal point: what is before it, and after it +def cut.dot(txt: String) -> String & String: + match txt: + case SNil{}: + ("", "") + case SCon{+hd, +tl}: + cut.at(mark.dot(hd), hd, tl, _u => cut.dot(tl)) + +# an exponent's sign and digits: `-` makes it negative, `+` is dropped +def esign.at(minus: Bool, plus: Bool, ch: Char, tl: String) -> Bool & String: + match minus plus: + case True{} _: + (True{}, tl) + case False{} True{}: + (False{}, tl) + case False{} False{}: + (False{}, SCon{ch, tl}) + +# an exponent's sign and digits +def esign(txt: String) -> Bool & String: + match txt: + case SNil{}: + (False{}, "") + case SCon{+hd, tl}: + esign.at(Char.is_eq(hd, '-'), Char.is_eq(hd, '+'), hd, tl) + +# the parts of a text cut at its exponent mark +def parts.of(cut: String & String) -> (String & String) & (Bool & String): + (mant, exp) = cut + (cut.dot(mant), esign(exp)) + +# an unsigned number's parts: its integer and fraction digits, and its +# exponent's sign and digits +def parts(txt: String) -> (String & String) & (Bool & String): + parts.of(cut.e(txt)) + +# --- the exponent --- + +# a digit's value +def digit.nat(ch: Char) -> Nat: + U32.to_nat(U32.sub(Char.to_u32(ch), 48)) + +# decimal digits read onto acc, most significant first +def nat.go(txt: String, acc: Nat) -> Nat: + match txt: + case SNil{}: + acc + case SCon{hd, tl}: + nat.go(tl, Nat.add(Nat.mul(acc, 10n), digit.nat(hd))) + +# decimal digits' value +def nat(txt: String) -> Nat: + nat.go(txt, 0n) + +# the point one place right: the first fraction digit, or a 0 past the +# last, moves before the point +def up(dec: Dec) -> Dec: + match dec: + case Dec{left, right}: + match right: + case SNil{}: + Dec{SCon{'0', left}, ""} + case SCon{hd, tl}: + Dec{SCon{hd, left}, tl} + +# the point one place left: the last integer digit, or a 0 before the +# first, moves after the point +def down(dec: Dec) -> Dec: + match dec: + case Dec{left, right}: + match left: + case SNil{}: + Dec{"", SCon{'0', right}} + case SCon{hd, tl}: + Dec{tl, SCon{hd, right}} + +# the point `kk` places right +def ups(kk: Nat, dec: Dec) -> Dec: + match kk: + case 0n: + dec + case 1n+j: + ups(j, up(dec)) + +# the point `kk` places left +def downs(kk: Nat, dec: Dec) -> Dec: + match kk: + case 0n: + dec + case 1n+j: + downs(j, down(dec)) + +# the digits with the point moved by the exponent +def move(neg: Bool, kk: Nat, dec: Dec) -> Dec: + match neg: + case False{}: + ups(kk, dec) + case True{}: + downs(kk, dec) + +# the parts as digits around the point, the point moved by the exponent +def place(pts: (String & String) & (Bool & String)) -> Dec: + ((int, frac), (neg, exp)) = pts + move(neg, nat(exp), Dec{String.reverse(int), frac}) + +# --- rounding --- + +# the first `nn` fraction digits, 0s past the last, and the digits dropped +def pad(nn: Nat, right: String) -> String & String: + match nn: + case 0n: + ("", right) + case 1n+m: + match right: + case SNil{}: + cut.put('0', pad(m, "")) + case SCon{hd, tl}: + cut.put(hd, pad(m, tl)) + +# a 0 digit leaves the answer to the rest; any other digit is nonzero +def nonzero.at(zero: Bool, more: Unit -> Bool) -> Bool: + match zero: + case False{}: + True{} + case True{}: + more(Unit{}) + +# whether any digit is not 0 +def nonzero(txt: String) -> Bool: + match txt: + case SNil{}: + False{} + case SCon{hd, +tl}: + nonzero.at(Char.is_eq(hd, '0'), _u => nonzero(tl)) + +# whether the last kept digit is odd; no digit is an even 0 +def odd(kept: String) -> Bool: + match kept: + case SNil{}: + False{} + case SCon{hd, _tl}: + U32.is_eq(U32.mod(Char.to_u32(hd), 2), 1) + +# a first dropped digit of 5 with no other nonzero digit dropped is a tie, +# which goes to the even neighbour +def tie(sticky: Bool, kept: String) -> Bool: + match sticky: + case True{}: + True{} + case False{}: + odd(kept) + +# the first dropped digit against 5 +def round.at(order: Cmp, rest: String, kept: String) -> Bool: + match order: + case LT{}: + False{} + case EQ{}: + tie(nonzero(rest), kept) + case GT{}: + True{} + +# whether the kept digits (last first) go up by one, from the dropped ones +def round.up(dropped: String, kept: String) -> Bool: + match dropped: + case SNil{}: + False{} + case SCon{hd, rest}: + round.at(U32.cmp(Char.to_u32(hd), 53), rest, kept) + +# one more on a digit, carried: a 9 is 0 and carries +def inc.at(nine: Bool, ch: Char, tl: String, more: Unit -> String) -> String: + match nine: + case True{}: + SCon{'0', more(Unit{})} + case False{}: + SCon{Char.from_u32(U32.add(Char.to_u32(ch), 1)), tl} + +# one more on digits written last first +def inc(digits: String) -> String: + match digits: + case SNil{}: + "1" + case SCon{+hd, +tl}: + inc.at(Char.is_eq(hd, '9'), hd, tl, _u => inc(tl)) + +# the kept digits, one more when they round up +def bump(go_up: Bool, kept: String) -> String: + match go_up: + case True{}: + inc(kept) + case False{}: + kept + +# the kept digits split at the last place +def round.keep(+left: String, pair: String & String) -> String: + (kept, dropped) = pair + +all = String.reverse.go(kept, left) + bump(round.up(dropped, all), all) + +# every digit to the last kept place, last first, rounded half to even +def round(+nn: Nat, dec: Dec) -> String: + match dec: + case Dec{+left, right}: + round.keep(left, pad(nn, right)) + +# --- writing --- + +# an integer part with its leading 0s dropped; no digit is 0 +def trim.at(zero: Bool, ch: Char, tl: String, more: Unit -> String) -> String: + match zero: + case True{}: + more(Unit{}) + case False{}: + SCon{ch, tl} + +# an integer part with its leading 0s dropped; no digit is 0 +def trim(int: String) -> String: + match int: + case SNil{}: + "0" + case SCon{+hd, +tl}: + trim.at(Char.is_eq(hd, '0'), hd, tl, _u => trim(tl)) + +# the integer part, then a point and the fraction when there is one +def point(nn: Nat, int: String, frac: String) -> String: + match nn: + case 0n: + int + case 1n+_m: + int ++ "." ++ frac + +# rounded digits, last first, written with `nn` decimals +def write(+nn: Nat, +digits: String) -> String: + point(nn, trim(String.reverse(String.drop(digits, nn))), + String.reverse(String.take(digits, nn))) + +# an unsigned number's text with `nn` decimals +def unsigned(txt: String, +nn: Nat) -> String: + write(nn, round(nn, place(parts(txt)))) + +# a sign kept in front of the unsigned rest +def text.at(minus: Bool, ch: Char, tl: String, +nn: Nat) -> String: + match minus: + case True{}: + "-" ++ unsigned(tl, nn) + case False{}: + unsigned(SCon{ch, tl}, nn) + +# a number's text with `nn` decimals +def text(txt: String, +nn: Nat) -> String: + match txt: + case SNil{}: + unsigned("", nn) + case SCon{+hd, tl}: + text.at(Char.is_eq(hd, '-'), hd, tl, nn) + +# Some of the text with `nn` decimals when `ok`, else None +def fixed.go(ok: Bool, raw: String, +nn: Nat) -> Maybe<&2, String>: + match ok: + case True{}: + Some{text(raw, nn)} + case False{}: + None{} + +# a JSON number's text with `nn` decimals, or None when it is not one +def fixed(+raw: String, +nn: Nat) -> Maybe<&2, String>: + fixed.go(V.num.ok(raw), raw, nn)