fields.bend

lawful-fields@0.1.1.0 · 110 lines · 15 definitions

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