defs.bend

lawful-fields@0.1.1.0 · 190 lines · 25 definitions

1import Base
2import lawful-words@0.1.0.0/defs.bend as W
3import lawful-bytes@0.1.1.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))