num.bend
yaml-for-bend@0.1.0.0 · 204 lines · 0 definitions
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
4import Base
5
6# The exponent after "e": its sign and digits, as an offset point shift.
7type Exp is Data:
8 Exp{neg: Bool, n: Nat}
9
10def 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
17def 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).
23def 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
27def 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
36def 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
43def 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
50def 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.
54def 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+.
58def 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.
67def 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
74def 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
81def 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.
85def 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.
89def int.text(+neg: Bool, s: String, +base: Nat) -> String:
90 signed(neg, big.show(big.read(s, base, [])))
91
92# Exact decimals
93# --------------
94
95def zeros(n: Nat) -> String:
96 String.repeat("0", n)
97
98def 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
109def 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.
119def 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.
128def dec.off() -> Nat:
129 1000n
130
131def 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).
139def 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
143def 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
156def 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
169def 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
180def 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
185def 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.
191def 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())))