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	# Exact decimals
89	# --------------
90	
91	def zeros(n: Nat) -> String:
92	  String.repeat("0", n)
93	
94	def drop.zeros(s: String) -> String:
95	  match s:
96	    case SNil{}:
97	      ""
98	    case SCon{c, t}:
99	      match c:
100	        case '0':
101	          drop.zeros(t)
102	        case _:
103	          SCon{c, t}
104	
105	# Decimal digits as they'd be written, without zeros in front.
106	def decimal(+s: String) -> String:
107	  +ds = drop.zeros(s)
108	  Bool.pick(String, String.is_empty(ds), "0", ds)
109	
110	# +s+, digits of +base+, as decimal text with the sign. Decimal digits are
111	# copied; other bases are converted, in time that grows with the square of
112	# their length.
113	def int.text(+neg: Bool, +s: String, +base: Nat) -> String:
114	  signed(neg, when(String, Nat.is_eq(base, 10n), u => decimal(s), u => big.show(big.read(s, base, []))))
115	
116	def take.digits(s: String) -> String:
117	  match s:
118	    case SNil{}:
119	      ""
120	    case SCon{+c, t}:
121	      when(String, Char.is_digit(c), u => SCon{c, take.digits(t)}, u => "")
122	
123	# The decimal whose digits are +ds+ (no zeros at either end) with the point
124	# +point+ places from their left, written "12.5", "0.001" or "300.0". The
125	# point is offset by +off+ so it can be negative.
126	def dec.place(+ds: String, +point: Nat, +off: Nat) -> String:
127	  +n = String.length(ds)
128	  when(String, String.is_empty(ds), u => "0.0",
129	    u => when(String, Nat.is_le(point, off), u => "0." ++ zeros(Nat.sub(off, point)) ++ ds,
130	      u => when(String, Nat.is_ge(Nat.sub(point, off), n), u => ds ++ zeros(Nat.sub(Nat.sub(point, off), n)) ++ ".0",
131	        u => String.take(ds, Nat.sub(point, off)) ++ "." ++ String.drop(ds, Nat.sub(point, off)))))
132	
133	# Where a decimal's point is counted from, so it can go left of the
134	# digits; an exponent is capped below it.
135	def dec.off() -> Nat:
136	  1000n
137	
138	def big.small(s: String, acc: Nat) -> Nat:
139	  match s:
140	    case SNil{}:
141	      acc
142	    case SCon{c, t}:
143	      big.small(t, Nat.add(Nat.mul(acc, 10n), digit(c)))
144	
145	# Exponent digits as a Nat, capped past where a double ends (about 308).
146	def exp.nat(+s: String) -> Nat:
147	  +n = big.small(s, 0n)
148	  when(Nat, Bool.or(Nat.is_gt(String.length(s), 3n), Nat.is_gt(n, 999n)), u => 999n, u => n)
149	
150	def exp.read(s: String) -> Exp:
151	  match s:
152	    case SCon{c, t}:
153	      match c:
154	        case '-':
155	          Exp{True{}, exp.nat(t)}
156	        case '+':
157	          Exp{False{}, exp.nat(t)}
158	        case _:
159	          Exp{False{}, exp.nat(SCon{c, t})}
160	    case SNil{}:
161	      Exp{False{}, 0n}
162	
163	def after.e(s: String) -> String:
164	  match s:
165	    case SNil{}:
166	      ""
167	    case SCon{c, t}:
168	      match c:
169	        case 'e':
170	          t
171	        case 'E':
172	          t
173	        case _:
174	          after.e(t)
175	
176	def after.dot(s: String) -> String:
177	  match s:
178	    case SNil{}:
179	      ""
180	    case SCon{c, t}:
181	      match c:
182	        case '.':
183	          t
184	        case _:
185	          after.dot(t)
186	
187	def point.at(+ip: Nat, e: Exp) -> Nat:
188	  match e:
189	    case Exp{neg, +n}:
190	      Bool.pick(Nat, neg, Nat.sub(Nat.add(dec.off(), ip), n), Nat.add(Nat.add(dec.off(), ip), n))
191	
192	def strip.end.zeros(s: String) -> String:
193	  String.reverse(drop.zeros(String.reverse(s)))
194	
195	# The value of a decimal literal ("1_000.5" without the "_", ".5", "1.",
196	# "2.5e-3"), written exactly: "1000.5", "0.5", "1.0", "0.0025". Past what a
197	# double holds it is ".inf"; under, zero.
198	def dec.exact(+s: String) -> String:
199	  +neg = String.starts_with(s, "-")
200	  +body = Bool.pick(String, Bool.or(neg, String.starts_with(s, "+")), String.drop(s, 1n), s)
201	  +ip = take.digits(body)
202	  +fp = take.digits(after.dot(body))
203	  +e = exp.read(after.e(body))
204	  +all = ip ++ fp
205	  +lead = Nat.sub(String.length(all), String.length(drop.zeros(all)))
206	  +ds = strip.end.zeros(drop.zeros(all))
207	  +point = Nat.sub(point.at(String.length(ip), e), lead)
208	  +sign = Bool.pick(String, neg, "-", "")
209	  when(String, Bool.and(Bool.not(String.is_empty(ds)), Nat.is_gt(point, Nat.add(dec.off(), 309n))), u => sign ++ ".inf",
210	    u => when(String, Bool.or(String.is_empty(ds), Nat.is_lt(Nat.add(point, 330n), dec.off())), u => sign ++ "0.0",
211	      u => sign ++ dec.place(ds, point, dec.off())))