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.
8	import Base
9	import ./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
13	type Dec is Data:
14	  Dec{left: String, right: String}
15	
16	# --- splitting the text ---
17	
18	# an exponent mark, `e` or `E`
19	def mark.e(+ch: Char) -> Bool:
20	  Bool.or(Char.is_eq(ch, 'e'), Char.is_eq(ch, 'E'))
21	
22	# a decimal point
23	def mark.dot(+ch: Char) -> Bool:
24	  Char.is_eq(ch, '.')
25	
26	# put a character before the first of a pair
27	def 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
32	def 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
45	def 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
53	def 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
61	def 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
71	def 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
79	def 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
85	def parts(txt: String) -> (String & String) & (Bool & String):
86	  parts.of(cut.e(txt))
87	
88	# --- the exponent ---
89	
90	# a digit's value
91	def 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
95	def 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
103	def 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
108	def 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
119	def 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
129	def 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
137	def 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
145	def 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
153	def 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
160	def 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
172	def 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
180	def 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
188	def 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
197	def 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
205	def 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
215	def 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
223	def 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
231	def 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
239	def 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
247	def 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
253	def 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
261	def 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
269	def 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
277	def 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
285	def 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
290	def 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
294	def 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
302	def 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
310	def 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
318	def fixed(+raw: String, +nn: Nat) -> Maybe<&2, String>:
319	  fixed.go(V.num.ok(raw), raw, nn)