fields.bend
lawful-fields@0.1.0.0 · 110 lines · 0 definitions
1import Base
2import lawful-bytes@0.1.0.0/defs.bend as D
3import lawful-bytes@0.1.0.0/bytes.bend as B
4
5# lawful-fields operations on packed bytes: cutting a line into fields at a
6# separator, and reading a decimal number. Reference versions, built on
7# lawful-bytes' find and at.
8
9def cut.cons(+e: U32, r: D.Bytes & List<&2, U32>) -> D.Bytes & List<&2, U32>:
10 (b, t) = r
11 (b, Con{e, t})
12
13# The end of the piece starting at from, searched only when want is set (no
14# scan past the last field asked for; the answer is then unused).
15def cut.next(want: Bool, b: D.Bytes, +from: U32, +to: U32, +sep: U32) -> D.Bytes & U32:
16 match want:
17 case True{}:
18 B.find(b, from, to, sep)
19 case False{}:
20 (b, to)
21
22# n counts the pieces still wanted, this one included; more says the previous
23# piece ended at a separator; r holds this piece's end.
24def cut.go(+n: Nat, more: Bool, r: D.Bytes & U32, +to: U32, +sep: U32) -> D.Bytes & List<&2, U32>:
25 match n more:
26 case 0n _:
27 (b, e) = r
28 (b, Nil{})
29 case 1n+m False{}:
30 (b, e) = r
31 (b, Nil{})
32 case 1n+m True{}:
33 (b, +e) = r
34 +go = U32.is_lt(e, to)
35 cut.cons(e, cut.go(m, go, cut.next(go && Bool.not(Nat.is_eq(m, 0n)), b, (e + 1 : U32), to, sep), to, sep))
36
37# The end offsets of the first n pieces of bytes from .. to-1, split at sep:
38# each end is where a separator is, or to for the last piece.
39def cut(b: D.Bytes, +from: U32, +to: U32, +sep: U32, +n: Nat) -> D.Bytes & List<&2, U32>:
40 cut.go(n, True{}, cut.next(Bool.not(Nat.is_eq(n, 0n)), b, from, to, sep), to, sep)
41
42def num.fin(+acc: U32, ok: Bool) -> Maybe<&2, U32>:
43 match ok:
44 case True{}:
45 Some{acc}
46 case False{}:
47 None{}
48
49def num.out(+acc: U32, ok: Bool, r: D.Bytes & U32) -> D.Bytes & Maybe<&2, U32>:
50 (b, x) = r
51 (b, num.fin(acc, ok))
52
53# r holds byte j; acc is the value so far; ok says every byte was a digit and
54# nothing overflowed.
55def num.go(n: Nat, r: D.Bytes & U32, +j: U32, +acc: U32, ok: Bool) -> D.Bytes & Maybe<&2, U32>:
56 match n:
57 case 0n:
58 num.out(acc, ok, r)
59 case 1n+m:
60 (b, +x) = r
61 +d = (x - 48 : U32)
62 +digit = U32.is_ge(x, 48) && U32.is_le(x, 57)
63 +fits = U32.is_lt(acc, 429496729) || (U32.is_eq(acc, 429496729) && U32.is_le(d, 5))
64 num.go(m, B.at(b, (j + 1 : U32)), (j + 1 : U32), ((acc * 10 : U32) + d : U32), ok && (digit && fits))
65
66# The decimal number in bytes from .. to-1, if it is one and below 2^32.
67def num(b: D.Bytes, +from: U32, +to: U32) -> D.Bytes & Maybe<&2, U32>:
68 num.go(Nat.sub(U32.to_nat(to), U32.to_nat(from)), B.at(b, from), from, 0, U32.is_lt(from, to))
69
70def digits.out(ok: Bool, r: D.Bytes & U32) -> D.Bytes & Bool:
71 (b, x) = r
72 (b, ok)
73
74# r holds byte j; ok says every byte so far was a digit.
75def digits.go(n: Nat, r: D.Bytes & U32, +j: U32, ok: Bool) -> D.Bytes & Bool:
76 match n:
77 case 0n:
78 digits.out(ok, r)
79 case 1n+m:
80 (b, +x) = r
81 digits.go(m, B.at(b, (j + 1 : U32)), (j + 1 : U32), ok && (U32.is_ge(x, 48) && U32.is_le(x, 57)))
82
83# Bytes from .. to-1 are one or more decimal digits (a number of any size).
84def digits(b: D.Bytes, +from: U32, +to: U32) -> D.Bytes & Bool:
85 digits.go(Nat.sub(U32.to_nat(to), U32.to_nat(from)), B.at(b, from), from, U32.is_lt(from, to))
86
87def put_dec.go(xs: List<&2, U32>, b: D.Bytes) -> D.Bytes:
88 match xs:
89 case Nil{}:
90 b
91 case Con{x, t}:
92 put_dec.go(t, B.push(b, x))
93
94# The decimal digits of n, most significant first, before acc; small says
95# n < 10 (the last digit). At most 10 steps for a U32.
96def put_dec.digits(k: Nat, small: Bool, +n: U32, acc: List<&2, U32>) -> List<&2, U32>:
97 match k small:
98 case _ True{}:
99 Con{(n + 48 : U32), acc}
100 case 0n False{}:
101 acc
102 case 1n+m False{}:
103 put_dec.digits(m, U32.is_lt((n / 10 : U32), 10), (n / 10 : U32), Con{((n % 10 : U32) + 48 : U32), acc})
104
105def put_dec.list(+n: U32) -> List<&2, U32>:
106 put_dec.digits(10n, U32.is_lt(n, 10), n, Nil{})
107
108# n written in decimal at the end of b (for room enough: at most 10 bytes).
109def put_dec(b: D.Bytes, +n: U32) -> D.Bytes:
110 put_dec.go(put_dec.list(n), b)