1	# Shrinkers: each maps a value to its simpler candidates, simplest first.
2	# Candidates come as List<&1, T> for every T, so Data and affine types share one runner.
3	# A shrinker never lists its input, so a runner that takes the first failing candidate and
4	# shrinks again halts at a value none of whose candidates fail.
5	# Numbers try 0, then the halving steps n - n/2, n - n/4, ..., n - 1: at most 33 candidates,
6	# and n - 1 is always among them, so a descent reaches the exact failure boundary.
7	# Lists try [], then drop chunks of n/2, n/4, ..., 1 elements (about 2n candidates), then
8	# simplify one element at a time, left to right, through the element's own shrinker.
9	import Base
10	import bend-kit-bytes@0.3.3.0/bytes.bend as Bytes
11	
12	# (n - d), then (n - d/2), ..., while d > 0; stop tells whether d is 0.
13	def u32.go(f: Nat, stop: Bool, +n: U32, +d: U32) -> List<&1, U32>:
14	  match f stop:
15	    case 0n _:
16	      Nil{}
17	    case 1n+p True{}:
18	      Nil{}
19	    case 1n+p False{}:
20	      +h = (d >> 1n : U32)
21	      (n - d : U32) <> u32.go(p, U32.is_eq(h, 0), n, h)
22	
23	# 0, n - n/2, n - n/4, ..., n - 1. None for 0.
24	def u32(n: U32) -> List<&1, U32>:
25	  +m = n
26	  u32.go(33n, U32.is_eq(m, 0), m, m)
27	
28	def nat.go(f: Nat, stop: Bool, +n: Nat, +d: Nat) -> List<&1, Nat>:
29	  match f stop:
30	    case 0n _:
31	      Nil{}
32	    case 1n+p True{}:
33	      Nil{}
34	    case 1n+p False{}:
35	      +h = Nat.div(d, 2n)
36	      (n - d : Nat) <> nat.go(p, Nat.is_eq(h, 0n), n, h)
37	
38	# 0n, n - n/2, n - n/4, ..., n - 1. None for 0n.
39	def nat(n: Nat) -> List<&1, Nat>:
40	  +m = n
41	  nat.go(m, Nat.is_eq(m, 0n), m, m)
42	
43	# Every run of k elements at offsets o, o + k, ... that fits in n; stop tells whether o + k > n.
44	def list.chunks(-A: Data, f: Nat, stop: Bool, +o: Nat, +k: Nat, +n: Nat, +xs: List<&2, A>) -> List<&1, List<&2, A>>:
45	  match f stop:
46	    case 0n _:
47	      Nil{}
48	    case 1n+p True{}:
49	      Nil{}
50	    case 1n+p False{}:
51	      +e = (o + k : Nat)
52	      List.append(&2, A, List.take(&2, A, xs, o), List.drop(&2, A, xs, e))
53	        <> list.chunks(A, p, Nat.is_gt((e + k : Nat), n), e, k, n, xs)
54	
55	# Chunk deletions for k = n, n/2, ..., 1; k = n is the lone candidate [].
56	def list.dels(-A: Data, f: Nat, stop: Bool, +k: Nat, +n: Nat, +xs: List<&2, A>) -> List<&1, List<&2, A>>:
57	  match f stop:
58	    case 0n _:
59	      Nil{}
60	    case 1n+p True{}:
61	      Nil{}
62	    case 1n+p False{}:
63	      +h = Nat.div(k, 2n)
64	      List.append(&1, List<&2, A>, list.chunks(A, n, Nat.is_gt(k, n), 0n, k, n, xs),
65	        list.dels(A, p, Nat.is_eq(h, 0n), h, n, xs))
66	
67	def list.heads(-A: Data, cs: List<&1, A>, +t: List<&2, A>) -> List<&1, List<&2, A>>:
68	  match cs:
69	    case Nil{}:
70	      Nil{}
71	    case c <> r:
72	      (c <> t) <> list.heads(A, r, t)
73	
74	def list.cons(-A: Data, +h: A, rs: List<&1, List<&2, A>>) -> List<&1, List<&2, A>>:
75	  match rs:
76	    case Nil{}:
77	      Nil{}
78	    case r <> t:
79	      (h <> r) <> list.cons(A, h, t)
80	
81	# One element replaced by one of its candidates: the head's first, then the tail's.
82	def list.ones(~A: Data, ~shrink: A -> List<&1, A>, +xs: List<&2, A>) -> List<&1, List<&2, A>>:
83	  match xs:
84	    case Nil{}:
85	      Nil{}
86	    case h <> t:
87	      List.append(&1, List<&2, A>, list.heads(A, shrink(h), t),
88	        list.cons(A, h, list.ones(~A, ~shrink, t)))
89	
90	# [], chunk deletions (halves down to single elements), then single-element simplifications.
91	def list(~A: Data, ~shrink: A -> List<&1, A>, xs: List<&2, A>) -> List<&1, List<&2, A>>:
92	  +ys = xs
93	  +n = List.length(&2, A, ys)
94	  List.append(&1, List<&2, A>, list.dels(A, n, Nat.is_eq(n, 0n), n, n, ys),
95	    list.ones(~A, ~shrink, ys))
96	
97	def maybe.some(-A: Data, xs: List<&1, A>) -> List<&1, Maybe<&2, A>>:
98	  match xs:
99	    case Nil{}:
100	      Nil{}
101	    case x <> t:
102	      Some{x} <> maybe.some(A, t)
103	
104	# None, then Some of each candidate of x. None for None.
105	def maybe(~A: Data, ~shrink: A -> List<&1, A>, m: Maybe<&2, A>) -> List<&1, Maybe<&2, A>>:
106	  match m:
107	    case None{}:
108	      Nil{}
109	    case Some{x}:
110	      None{} <> maybe.some(A, shrink(x))
111	
112	def char.lift(xs: List<&1, U32>, +base: U32) -> List<&1, Char>:
113	  match xs:
114	    case Nil{}:
115	      Nil{}
116	    case x <> t:
117	      Chr{(base + x : U32)} <> char.lift(t, base)
118	
119	def char.of(o: Cmp, +c: U32) -> List<&1, Char>:
120	  match o:
121	    case LT{}:
122	      Chr{97} <> char.lift(u32(c), 0)
123	    case EQ{}:
124	      Nil{}
125	    case GT{}:
126	      char.lift(u32((c - 97 : U32)), 97)
127	
128	# Toward 'a': a code above it halves toward it; one below tries 'a', then halves toward 0.
129	def char(c: Char) -> List<&1, Char>:
130	  match c:
131	    case Chr{+x}:
132	      char.of(U32.cmp(x, 97), x)
133	
134	def string.of(xs: List<&1, List<&2, Char>>) -> List<&1, String>:
135	  match xs:
136	    case Nil{}:
137	      Nil{}
138	    case x <> t:
139	      String.from_list(x) <> string.of(t)
140	
141	# A String as a list of Chars under char.
142	def string(s: String) -> List<&1, String>:
143	  string.of(list(~Char, ~char, String.to_list(s)))
144	
145	def bytes.codes(s: String) -> List<&2, U32>:
146	  match s:
147	    case SNil{}:
148	      Nil{}
149	    case SCon{Chr{x}, t}:
150	      x <> bytes.codes(t)
151	
152	def bytes.chars(xs: List<&2, U32>) -> String:
153	  match xs:
154	    case Nil{}:
155	      SNil{}
156	    case x <> t:
157	      SCon{Chr{x}, bytes.chars(t)}
158	
159	def bytes.of(xs: List<&1, List<&2, U32>>) -> List<&1, Bytes.Bytes>:
160	  match xs:
161	    case Nil{}:
162	      Nil{}
163	    case x <> t:
164	      Bytes.from_string(bytes.chars(x)) <> bytes.of(t)
165	
166	# Bytes is affine, so this never copies b: it reads the octets out once and builds each
167	# candidate as a fresh buffer, shrinking the octets as a list with bytes toward 0.
168	def bytes(b: Bytes.Bytes) -> List<&1, Bytes.Bytes>:
169	  bytes.of(list(~U32, ~u32, bytes.codes(Bytes.to_string(b))))