1	# Numbers kept as text. Bend's Nat stops at 2^48, so an integer of any size
2	# is a list of decimal digits, and a float is exact decimal text.
3	
4	import Base
5	
6	# The exponent after "e": its sign and digits, as an offset point shift.
7	type Exp is Data:
8	  Exp{neg: Bool, n: Nat}
9	
10	def when(-A: Type, hit: Bool, yes: Unit -> A, no: Unit -> A) -> A:
11	  match hit:
12	    case True{}:
13	      yes(Unit{})
14	    case False{}:
15	      no(Unit{})
16	
17	def code(c: Char) -> U32:
18	  match c:
19	    case Chr{x}:
20	      x
21	
22	# A digit's value, for digits up to base 36 ("a" and "A" are 10).
23	def digit(c: Char) -> Nat:
24	  +x = code(c)
25	  U32.to_nat(U32.sub(x, Bool.pick(U32, U32.is_ge(x, 97), 87, Bool.pick(U32, U32.is_ge(x, 65), 55, 48))))
26	
27	def digit.char(n: Nat) -> Char:
28	  Chr{U32.add(48, U32.from_nat(n))}
29	
30	# Big numbers
31	# -----------
32	
33	# A natural number's decimal digits, least significant first, with no
34	# zeros at the end of the list. Zero is the empty list.
35	
36	def big.chars(s: String) -> List<&2, Nat>:
37	  match s:
38	    case SNil{}:
39	      []
40	    case SCon{c, t}:
41	      digit(c) <> big.chars(t)
42	
43	def big.trim.go(ds: List<&2, Nat>) -> List<&2, Nat>:
44	  match ds:
45	    case Nil{}:
46	      []
47	    case Con{+d, +rest}:
48	      when(List<&2, Nat>, Nat.is_eq(d, 0n), u => big.trim.go(rest), u => d <> rest)
49	
50	def big.trim(ds: List<&2, Nat>) -> List<&2, Nat>:
51	  List.reverse(&2, Nat, big.trim.go(List.reverse(&2, Nat, ds)))
52	
53	# A Nat that fits, as a big number.
54	def big.of.nat(+n: Nat) -> List<&2, Nat>:
55	  big.trim(List.reverse(&2, Nat, big.chars(Nat.show(n))))
56	
57	# +ds+ times +base+, plus +carry+.
58	def big.mul.add(ds: List<&2, Nat>, +base: Nat, carry: Nat) -> List<&2, Nat>:
59	  match ds:
60	    case Nil{}:
61	      big.of.nat(carry)
62	    case Con{d, rest}:
63	      +x = Nat.add(Nat.mul(d, base), carry)
64	      Nat.mod(x, 10n) <> big.mul.add(rest, base, Nat.div(x, 10n))
65	
66	# The digits of +s+ in +base+ (each a digit of that base) as a big number.
67	def big.read(s: String, +base: Nat, acc: List<&2, Nat>) -> List<&2, Nat>:
68	  match s:
69	    case SNil{}:
70	      acc
71	    case SCon{c, t}:
72	      big.read(t, base, big.mul.add(acc, base, digit(c)))
73	
74	def big.digits(ds: List<&2, Nat>) -> String:
75	  match ds:
76	    case Nil{}:
77	      ""
78	    case Con{d, rest}:
79	      SCon{digit.char(d), big.digits(rest)}
80	
81	def big.show(+ds: List<&2, Nat>) -> String:
82	  Bool.pick(String, List.is_empty(&2, Nat, ds), "0", String.reverse(big.digits(ds)))
83	
84	# An integer's text: "-" when negative and not zero.
85	def signed(+neg: Bool, +digits: String) -> String:
86	  Bool.pick(String, Bool.and(neg, Bool.not(String.eq(digits, "0"))), "-" ++ digits, digits)
87	
88	# +s+, digits of +base+, as decimal text with the sign.
89	def int.text(+neg: Bool, s: String, +base: Nat) -> String:
90	  signed(neg, big.show(big.read(s, base, [])))
91	
92	# Exact decimals
93	# --------------
94	
95	def zeros(n: Nat) -> String:
96	  String.repeat("0", n)
97	
98	def drop.zeros(s: String) -> String:
99	  match s:
100	    case SNil{}:
101	      ""
102	    case SCon{c, t}:
103	      match c:
104	        case '0':
105	          drop.zeros(t)
106	        case _:
107	          SCon{c, t}
108	
109	def take.digits(s: String) -> String:
110	  match s:
111	    case SNil{}:
112	      ""
113	    case SCon{+c, t}:
114	      when(String, Char.is_digit(c), u => SCon{c, take.digits(t)}, u => "")
115	
116	# The decimal whose digits are +ds+ (no zeros at either end) with the point
117	# +point+ places from their left, written "12.5", "0.001" or "300.0". The
118	# point is offset by +off+ so it can be negative.
119	def dec.place(+ds: String, +point: Nat, +off: Nat) -> String:
120	  +n = String.length(ds)
121	  when(String, String.is_empty(ds), u => "0.0",
122	    u => when(String, Nat.is_le(point, off), u => "0." ++ zeros(Nat.sub(off, point)) ++ ds,
123	      u => when(String, Nat.is_ge(Nat.sub(point, off), n), u => ds ++ zeros(Nat.sub(Nat.sub(point, off), n)) ++ ".0",
124	        u => String.take(ds, Nat.sub(point, off)) ++ "." ++ String.drop(ds, Nat.sub(point, off)))))
125	
126	# Where a decimal's point is counted from, so it can go left of the
127	# digits; an exponent is capped below it.
128	def dec.off() -> Nat:
129	  1000n
130	
131	def big.small(s: String, acc: Nat) -> Nat:
132	  match s:
133	    case SNil{}:
134	      acc
135	    case SCon{c, t}:
136	      big.small(t, Nat.add(Nat.mul(acc, 10n), digit(c)))
137	
138	# Exponent digits as a Nat, capped past where a double ends (about 308).
139	def exp.nat(+s: String) -> Nat:
140	  +n = big.small(s, 0n)
141	  when(Nat, Bool.or(Nat.is_gt(String.length(s), 3n), Nat.is_gt(n, 999n)), u => 999n, u => n)
142	
143	def exp.read(s: String) -> Exp:
144	  match s:
145	    case SCon{c, t}:
146	      match c:
147	        case '-':
148	          Exp{True{}, exp.nat(t)}
149	        case '+':
150	          Exp{False{}, exp.nat(t)}
151	        case _:
152	          Exp{False{}, exp.nat(SCon{c, t})}
153	    case SNil{}:
154	      Exp{False{}, 0n}
155	
156	def after.e(s: String) -> String:
157	  match s:
158	    case SNil{}:
159	      ""
160	    case SCon{c, t}:
161	      match c:
162	        case 'e':
163	          t
164	        case 'E':
165	          t
166	        case _:
167	          after.e(t)
168	
169	def after.dot(s: String) -> String:
170	  match s:
171	    case SNil{}:
172	      ""
173	    case SCon{c, t}:
174	      match c:
175	        case '.':
176	          t
177	        case _:
178	          after.dot(t)
179	
180	def point.at(+ip: Nat, e: Exp) -> Nat:
181	  match e:
182	    case Exp{neg, +n}:
183	      Bool.pick(Nat, neg, Nat.sub(Nat.add(dec.off(), ip), n), Nat.add(Nat.add(dec.off(), ip), n))
184	
185	def strip.end.zeros(s: String) -> String:
186	  String.reverse(drop.zeros(String.reverse(s)))
187	
188	# The value of a decimal literal ("1_000.5" without the "_", ".5", "1.",
189	# "2.5e-3"), written exactly: "1000.5", "0.5", "1.0", "0.0025". Past what a
190	# double holds it is ".inf"; under, zero.
191	def dec.exact(+s: String) -> String:
192	  +neg = String.starts_with(s, "-")
193	  +body = Bool.pick(String, Bool.or(neg, String.starts_with(s, "+")), String.drop(s, 1n), s)
194	  +ip = take.digits(body)
195	  +fp = take.digits(after.dot(body))
196	  +e = exp.read(after.e(body))
197	  +all = ip ++ fp
198	  +lead = Nat.sub(String.length(all), String.length(drop.zeros(all)))
199	  +ds = strip.end.zeros(drop.zeros(all))
200	  +point = Nat.sub(point.at(String.length(ip), e), lead)
201	  +sign = Bool.pick(String, neg, "-", "")
202	  when(String, Bool.and(Bool.not(String.is_empty(ds)), Nat.is_gt(point, Nat.add(dec.off(), 309n))), u => sign ++ ".inf",
203	    u => when(String, Bool.or(String.is_empty(ds), Nat.is_lt(Nat.add(point, 330n), dec.off())), u => sign ++ "0.0",
204	      u => sign ++ dec.place(ds, point, dec.off())))