1	import Base
2	import lawful-words@0.1.0.0/defs.bend as W
3	import 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	
9	def 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	
16	def 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 [[], []].
25	def 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	
32	def 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).
40	def digit(+x: U32) -> Maybe<&2, Nat>:
41	  digit.if(x, U32.is_ge(x, 48) && U32.is_le(x, 57))
42	
43	def 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	
50	def 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).
59	def 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	
66	def decb.if(+n: Nat, fits: Bool) -> Maybe<&2, Nat>:
67	  match fits:
68	    case True{}:
69	      Some{n}
70	    case False{}:
71	      None{}
72	
73	def 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.
83	def 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.
87	def 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).
96	def 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.
104	def 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	
111	def 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.
119	def 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	
126	def 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).
136	def 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.
145	def 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	
152	def 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	
159	def 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).
167	def 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.
172	def 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.
181	def 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).
189	def all_digits(xs: List<&2, U32>) -> Bool:
190	  Maybe.is_some(&2, Nat, dec(xs))