1	import Base
2	import lawful-bytes@0.1.0.0/defs.bend as D
3	import 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	
9	def 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).
15	def 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.
24	def 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.
39	def 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	
42	def num.fin(+acc: U32, ok: Bool) -> Maybe<&2, U32>:
43	  match ok:
44	    case True{}:
45	      Some{acc}
46	    case False{}:
47	      None{}
48	
49	def 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.
55	def 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.
67	def 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	
70	def 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.
75	def 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).
84	def 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	
87	def 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.
96	def 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	
105	def 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).
109	def put_dec(b: D.Bytes, +n: U32) -> D.Bytes:
110	  put_dec.go(put_dec.list(n), b)