defs.bend
lawful-fields@0.1.0.0 · 190 lines · 0 definitions
1import Base
2import lawful-words@0.1.0.0/defs.bend as W
3import lawful-bytes@0.1.0.0/defs.bend as D
4
5# lawful-fields definitions: splitting a list of bytes and reading decimal
6# numbers, as plain list functions. The operations on packed bytes are in
7# fields.bend, the laws in LAWS.bend.
8
9def split.push(+c: U32, ps: List<&2, List<&2, U32>>) -> List<&2, List<&2, U32>>:
10 match ps:
11 case Nil{}:
12 [[c]]
13 case Con{h, t}:
14 Con{Con{c, h}, t}
15
16def split.fin(+c: U32, r: List<&2, List<&2, U32>>, cut: Bool) -> List<&2, List<&2, U32>>:
17 match cut:
18 case False{}:
19 split.push(c, r)
20 case True{}:
21 Con{Nil{}, r}
22
23# The pieces of xs between separators, as Base's String.split does for text:
24# always at least one piece, so [] gives [[]] and [sep] gives [[], []].
25def split(xs: List<&2, U32>, +sep: U32) -> List<&2, List<&2, U32>>:
26 match xs:
27 case Nil{}:
28 [Nil{}]
29 case Con{+x, t}:
30 split.fin(x, split(t, sep), U32.is_eq(x, sep))
31
32def digit.if(+x: U32, ok: Bool) -> Maybe<&2, Nat>:
33 match ok:
34 case True{}:
35 Some{Nat.sub(U32.to_nat(x), 48n)}
36 case False{}:
37 None{}
38
39# The value of a decimal digit byte ('0' is 48).
40def digit(+x: U32) -> Maybe<&2, Nat>:
41 digit.if(x, U32.is_ge(x, 48) && U32.is_le(x, 57))
42
43def dec.push(acc: Maybe<&2, Nat>, d: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
44 match acc d:
45 case Some{a} Some{k}:
46 Some{Nat.add(Nat.mul(a, 10n), k)}
47 case _ _:
48 None{}
49
50def dec.go(xs: List<&2, U32>, acc: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
51 match xs:
52 case Nil{}:
53 acc
54 case Con{x, t}:
55 dec.go(t, dec.push(acc, digit(x)))
56
57# A decimal number: one or more digits (leading zeros allowed), nothing else;
58# any size (framebender's Pos.read on text is the same function).
59def dec(xs: List<&2, U32>) -> Maybe<&2, Nat>:
60 match xs:
61 case Nil{}:
62 None{}
63 case Con{x, t}:
64 dec.go(Con{x, t}, Some{0n})
65
66def decb.if(+n: Nat, fits: Bool) -> Maybe<&2, Nat>:
67 match fits:
68 case True{}:
69 Some{n}
70 case False{}:
71 None{}
72
73def decb.of(m: Maybe<&2, Nat>, +bound: Nat) -> Maybe<&2, Nat>:
74 match m:
75 case Some{+n}:
76 decb.if(n, Nat.is_lt(n, bound))
77 case None{}:
78 None{}
79
80# A decimal number below bound; None otherwise. The laws use bound = 2^32 (what
81# fits a U32), written Nat.pow(2n, 32n) in each law: the checker evaluates a
82# constant hidden in a definition, and 2^32 in unary is too deep.
83def decb(xs: List<&2, U32>, +bound: Nat) -> Maybe<&2, Nat>:
84 decb.of(dec(xs), bound)
85
86# The number a Maybe<U32> stands for.
87def nat_of(m: Maybe<&2, U32>) -> Maybe<&2, Nat>:
88 match m:
89 case Some{x}:
90 Some{U32.to_nat(x)}
91 case None{}:
92 None{}
93
94# The pieces of xs that end at each offset of es, the first starting at from
95# and each next one just after the previous end (where the separator was).
96def pieces(es: List<&2, U32>, +xs: List<&2, U32>, +from: Nat) -> List<&2, List<&2, U32>>:
97 match es:
98 case Nil{}:
99 Nil{}
100 case Con{+e, t}:
101 Con{D.slice(xs, from, Nat.sub(U32.to_nat(e), from)), pieces(t, xs, Nat.add(U32.to_nat(e), 1n))}
102
103# Every offset in es lies in from .. to.
104def within(es: List<&2, U32>, +from: Nat, +to: Nat) -> Bool:
105 match es:
106 case Nil{}:
107 True{}
108 case Con{+e, t}:
109 (Nat.is_le(from, U32.to_nat(e)) && Nat.is_le(U32.to_nat(e), to)) && within(t, from, to)
110
111def count.if(hit: Bool, +n: Nat) -> Nat:
112 match hit:
113 case True{}:
114 Nat.add(1n, n)
115 case False{}:
116 n
117
118# How many times sep occurs in xs.
119def count(xs: List<&2, U32>, +sep: U32) -> Nat:
120 match xs:
121 case Nil{}:
122 0n
123 case Con{+x, t}:
124 count.if(U32.is_eq(x, sep), count(t, sep))
125
126def join.go(ps: List<&2, List<&2, U32>>, +sep: U32) -> List<&2, U32>:
127 match ps:
128 case Nil{}:
129 Nil{}
130 case Con{p, t}:
131 Con{sep, List.append(&2, U32, p, join.go(t, sep))}
132
133# The pieces joined with sep between them. join undoes split:
134# join(split(xs, sep), sep) == xs (the other way round fails when a piece holds
135# sep).
136def join(ps: List<&2, List<&2, U32>>, +sep: U32) -> List<&2, U32>:
137 match ps:
138 case Nil{}:
139 Nil{}
140 case Con{p, t}:
141 List.append(&2, U32, p, join.go(t, sep))
142
143# Bytes as text and back: one Char per byte (Chr{b}), with no decoding (the
144# way framebender reads files). For text whose characters are all below 256.
145def text(xs: List<&2, U32>) -> String:
146 match xs:
147 case Nil{}:
148 SNil{}
149 case Con{x, t}:
150 SCon{Chr{x}, text(t)}
151
152def texts(ps: List<&2, List<&2, U32>>) -> List<&2, String>:
153 match ps:
154 case Nil{}:
155 Nil{}
156 case Con{p, t}:
157 Con{text(p), texts(t)}
158
159def codes(s: String) -> List<&2, U32>:
160 match s:
161 case SNil{}:
162 Nil{}
163 case SCon{c, t}:
164 Con{Char.to_u32(c), codes(t)}
165
166# The decimal digits of a number, as bytes (Base's Nat.show).
167def show(n: U32) -> List<&2, U32>:
168 codes(Nat.show(U32.to_nat(n)))
169
170# The end offset of each piece, the first piece starting at from and each next
171# one just after the previous end.
172def ends(ps: List<&2, List<&2, U32>>, +from: Nat) -> List<&2, Nat>:
173 match ps:
174 case Nil{}:
175 Nil{}
176 case Con{p, t}:
177 +e = Nat.add(from, List.length(&2, U32, p))
178 Con{e, ends(t, Nat.add(e, 1n))}
179
180# The numbers words stand for.
181def nats(es: List<&2, U32>) -> List<&2, Nat>:
182 match es:
183 case Nil{}:
184 Nil{}
185 case Con{e, t}:
186 Con{U32.to_nat(e), nats(t)}
187
188# xs is one or more digits (any value).
189def all_digits(xs: List<&2, U32>) -> Bool:
190 Maybe.is_some(&2, Nat, dec(xs))