src/fixed.bend

emerging-ezjson@1.3.0.0 · 319 lines · 41 definitions

1# src/fixed: a JSON number's text written with a fixed count of decimals.
2# The digits are rounded half to even as decimal digits, never through a
3# binary float. The text is split at its `e` (or `E`) and its `.`; the
4# exponent moves the point; the digits past the last kept place decide
5# whether the kept ones go up by one; the integer part loses its leading
6# zeros. A `-` is kept even when the rounded value is zero, as C's printf
7# and Python's `'%.Nf'` keep it.
8import Base
9import emerging-ezjson@1.3.0.0/src/value.bend as V
10
11# where a number's point is: the digits before it, last digit first, and the
12# digits after it
13type Dec is Data:
14  Dec{left: String, right: String}
15
16# --- splitting the text ---
17
18# an exponent mark, `e` or `E`
19def mark.e(+ch: Char) -> Bool:
20  Bool.or(Char.is_eq(ch, 'e'), Char.is_eq(ch, 'E'))
21
22# a decimal point
23def mark.dot(+ch: Char) -> Bool:
24  Char.is_eq(ch, '.')
25
26# put a character before the first of a pair
27def cut.put(ch: Char, pair: String & String) -> String & String:
28  (a, b) = pair
29  (SCon{ch, a}, b)
30
31# at a mark the cut is made; any other character is kept before it
32def cut.at(
33  hit: Bool,
34  ch: Char,
35  after: String,
36  more: Unit -> String & String
37) -> String & String:
38  match hit:
39    case True{}:
40      ("", after)
41    case False{}:
42      cut.put(ch, more(Unit{}))
43
44# a text cut at its first exponent mark: what is before it, and after it
45def cut.e(txt: String) -> String & String:
46  match txt:
47    case SNil{}:
48      ("", "")
49    case SCon{+hd, +tl}:
50      cut.at(mark.e(hd), hd, tl, _u => cut.e(tl))
51
52# a text cut at its first decimal point: what is before it, and after it
53def cut.dot(txt: String) -> String & String:
54  match txt:
55    case SNil{}:
56      ("", "")
57    case SCon{+hd, +tl}:
58      cut.at(mark.dot(hd), hd, tl, _u => cut.dot(tl))
59
60# an exponent's sign and digits: `-` makes it negative, `+` is dropped
61def esign.at(minus: Bool, plus: Bool, ch: Char, tl: String) -> Bool & String:
62  match minus plus:
63    case True{} _:
64      (True{}, tl)
65    case False{} True{}:
66      (False{}, tl)
67    case False{} False{}:
68      (False{}, SCon{ch, tl})
69
70# an exponent's sign and digits
71def esign(txt: String) -> Bool & String:
72  match txt:
73    case SNil{}:
74      (False{}, "")
75    case SCon{+hd, tl}:
76      esign.at(Char.is_eq(hd, '-'), Char.is_eq(hd, '+'), hd, tl)
77
78# the parts of a text cut at its exponent mark
79def parts.of(cut: String & String) -> (String & String) & (Bool & String):
80  (mant, exp) = cut
81  (cut.dot(mant), esign(exp))
82
83# an unsigned number's parts: its integer and fraction digits, and its
84# exponent's sign and digits
85def parts(txt: String) -> (String & String) & (Bool & String):
86  parts.of(cut.e(txt))
87
88# --- the exponent ---
89
90# a digit's value
91def digit.nat(ch: Char) -> Nat:
92  U32.to_nat(U32.sub(Char.to_u32(ch), 48))
93
94# decimal digits read onto acc, most significant first
95def nat.go(txt: String, acc: Nat) -> Nat:
96  match txt:
97    case SNil{}:
98      acc
99    case SCon{hd, tl}:
100      nat.go(tl, Nat.add(Nat.mul(acc, 10n), digit.nat(hd)))
101
102# decimal digits' value
103def nat(txt: String) -> Nat:
104  nat.go(txt, 0n)
105
106# the point one place right: the first fraction digit, or a 0 past the
107# last, moves before the point
108def up(dec: Dec) -> Dec:
109  match dec:
110    case Dec{left, right}:
111      match right:
112        case SNil{}:
113          Dec{SCon{'0', left}, ""}
114        case SCon{hd, tl}:
115          Dec{SCon{hd, left}, tl}
116
117# the point one place left: the last integer digit, or a 0 before the
118# first, moves after the point
119def down(dec: Dec) -> Dec:
120  match dec:
121    case Dec{left, right}:
122      match left:
123        case SNil{}:
124          Dec{"", SCon{'0', right}}
125        case SCon{hd, tl}:
126          Dec{tl, SCon{hd, right}}
127
128# the point `kk` places right
129def ups(kk: Nat, dec: Dec) -> Dec:
130  match kk:
131    case 0n:
132      dec
133    case 1n+j:
134      ups(j, up(dec))
135
136# the point `kk` places left
137def downs(kk: Nat, dec: Dec) -> Dec:
138  match kk:
139    case 0n:
140      dec
141    case 1n+j:
142      downs(j, down(dec))
143
144# the digits with the point moved by the exponent
145def move(neg: Bool, kk: Nat, dec: Dec) -> Dec:
146  match neg:
147    case False{}:
148      ups(kk, dec)
149    case True{}:
150      downs(kk, dec)
151
152# the parts as digits around the point, the point moved by the exponent
153def place(pts: (String & String) & (Bool & String)) -> Dec:
154  ((int, frac), (neg, exp)) = pts
155  move(neg, nat(exp), Dec{String.reverse(int), frac})
156
157# --- rounding ---
158
159# the first `nn` fraction digits, 0s past the last, and the digits dropped
160def pad(nn: Nat, right: String) -> String & String:
161  match nn:
162    case 0n:
163      ("", right)
164    case 1n+m:
165      match right:
166        case SNil{}:
167          cut.put('0', pad(m, ""))
168        case SCon{hd, tl}:
169          cut.put(hd, pad(m, tl))
170
171# a 0 digit leaves the answer to the rest; any other digit is nonzero
172def nonzero.at(zero: Bool, more: Unit -> Bool) -> Bool:
173  match zero:
174    case False{}:
175      True{}
176    case True{}:
177      more(Unit{})
178
179# whether any digit is not 0
180def nonzero(txt: String) -> Bool:
181  match txt:
182    case SNil{}:
183      False{}
184    case SCon{hd, +tl}:
185      nonzero.at(Char.is_eq(hd, '0'), _u => nonzero(tl))
186
187# whether the last kept digit is odd; no digit is an even 0
188def odd(kept: String) -> Bool:
189  match kept:
190    case SNil{}:
191      False{}
192    case SCon{hd, _tl}:
193      U32.is_eq(U32.mod(Char.to_u32(hd), 2), 1)
194
195# a first dropped digit of 5 with no other nonzero digit dropped is a tie,
196# which goes to the even neighbour
197def tie(sticky: Bool, kept: String) -> Bool:
198  match sticky:
199    case True{}:
200      True{}
201    case False{}:
202      odd(kept)
203
204# the first dropped digit against 5
205def round.at(order: Cmp, rest: String, kept: String) -> Bool:
206  match order:
207    case LT{}:
208      False{}
209    case EQ{}:
210      tie(nonzero(rest), kept)
211    case GT{}:
212      True{}
213
214# whether the kept digits (last first) go up by one, from the dropped ones
215def round.up(dropped: String, kept: String) -> Bool:
216  match dropped:
217    case SNil{}:
218      False{}
219    case SCon{hd, rest}:
220      round.at(U32.cmp(Char.to_u32(hd), 53), rest, kept)
221
222# one more on a digit, carried: a 9 is 0 and carries
223def inc.at(nine: Bool, ch: Char, tl: String, more: Unit -> String) -> String:
224  match nine:
225    case True{}:
226      SCon{'0', more(Unit{})}
227    case False{}:
228      SCon{Char.from_u32(U32.add(Char.to_u32(ch), 1)), tl}
229
230# one more on digits written last first
231def inc(digits: String) -> String:
232  match digits:
233    case SNil{}:
234      "1"
235    case SCon{+hd, +tl}:
236      inc.at(Char.is_eq(hd, '9'), hd, tl, _u => inc(tl))
237
238# the kept digits, one more when they round up
239def bump(go_up: Bool, kept: String) -> String:
240  match go_up:
241    case True{}:
242      inc(kept)
243    case False{}:
244      kept
245
246# the kept digits split at the last place
247def round.keep(+left: String, pair: String & String) -> String:
248  (kept, dropped) = pair
249  +all = String.reverse.go(kept, left)
250  bump(round.up(dropped, all), all)
251
252# every digit to the last kept place, last first, rounded half to even
253def round(+nn: Nat, dec: Dec) -> String:
254  match dec:
255    case Dec{+left, right}:
256      round.keep(left, pad(nn, right))
257
258# --- writing ---
259
260# an integer part with its leading 0s dropped; no digit is 0
261def trim.at(zero: Bool, ch: Char, tl: String, more: Unit -> String) -> String:
262  match zero:
263    case True{}:
264      more(Unit{})
265    case False{}:
266      SCon{ch, tl}
267
268# an integer part with its leading 0s dropped; no digit is 0
269def trim(int: String) -> String:
270  match int:
271    case SNil{}:
272      "0"
273    case SCon{+hd, +tl}:
274      trim.at(Char.is_eq(hd, '0'), hd, tl, _u => trim(tl))
275
276# the integer part, then a point and the fraction when there is one
277def point(nn: Nat, int: String, frac: String) -> String:
278  match nn:
279    case 0n:
280      int
281    case 1n+_m:
282      int ++ "." ++ frac
283
284# rounded digits, last first, written with `nn` decimals
285def write(+nn: Nat, +digits: String) -> String:
286  point(nn, trim(String.reverse(String.drop(digits, nn))),
287    String.reverse(String.take(digits, nn)))
288
289# an unsigned number's text with `nn` decimals
290def unsigned(txt: String, +nn: Nat) -> String:
291  write(nn, round(nn, place(parts(txt))))
292
293# a sign kept in front of the unsigned rest
294def text.at(minus: Bool, ch: Char, tl: String, +nn: Nat) -> String:
295  match minus:
296    case True{}:
297      "-" ++ unsigned(tl, nn)
298    case False{}:
299      unsigned(SCon{ch, tl}, nn)
300
301# a number's text with `nn` decimals
302def text(txt: String, +nn: Nat) -> String:
303  match txt:
304    case SNil{}:
305      unsigned("", nn)
306    case SCon{+hd, tl}:
307      text.at(Char.is_eq(hd, '-'), hd, tl, nn)
308
309# Some of the text with `nn` decimals when `ok`, else None
310def fixed.go(ok: Bool, raw: String, +nn: Nat) -> Maybe<&2, String>:
311  match ok:
312    case True{}:
313      Some{text(raw, nn)}
314    case False{}:
315      None{}
316
317# a JSON number's text with `nn` decimals, or None when it is not one
318def fixed(+raw: String, +nn: Nat) -> Maybe<&2, String>:
319  fixed.go(V.num.ok(raw), raw, nn)