num.bend

yaml-for-bend@0.1.1.0 · 211 lines · 29 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# Exact decimals
89# --------------
90
91def zeros(n: Nat) -> String:
92  String.repeat("0", n)
93
94def 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.
106def 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.
113def 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
116def 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.
126def 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.
135def dec.off() -> Nat:
136  1000n
137
138def 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).
146def 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
150def 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
163def 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
176def 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
187def 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
192def 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.
198def 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())))