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)