1	# Reproducible property checks with generated inputs and greedy shrinking.
2	import Base
3	import bend-kit-random@0.1.0.1/random.bend as Rand
4	import ./generate.bend as Gen
5	import ./shrink.bend as Shrink
6	
7	type Failure<-T: Type> is Type:
8	  Failure{seed: U32, trial: Nat, value: T}
9	
10	# Scan candidates in order; a predicate returns its input so affine values work.
11	def smaller(~T: Type, ~test: T -> T & Bool, xs: List<&1, T>, tested: T & Bool) -> Maybe<&1, T>:
12	  match xs:
13	    case Nil{}:
14	      (candidate, ok) = tested
15	      match ok:
16	        case False{}:
17	          Some{candidate}
18	        case True{}:
19	          None{}
20	    case Con{x, rest}:
21	      (candidate, ok) = tested
22	      match ok:
23	        case False{}:
24	          Some{candidate}
25	        case True{}:
26	          smaller(~T, ~test, rest, test(x))
27	
28	def smaller.start(~T: Type, ~test: T -> T & Bool, xs: List<&1, T>) -> Maybe<&1, T>:
29	  match xs:
30	    case Nil{}:
31	      None{}
32	    case Con{x, rest}:
33	      smaller(~T, ~test, rest, test(x))
34	
35	def attempt.pair(~T: Type, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool, pair: T & T) -> T & Maybe<&1, T>:
36	  (original, probe) = pair
37	  (original, smaller.start(~T, ~test, shrink(probe)))
38	
39	def attempt(~T: Type, ~copy: T -> T & T, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool, value: T) -> T & Maybe<&1, T>:
40	  attempt.pair(~T, ~shrink, ~test, copy(value))
41	
42	# Each accepted failure restarts shrinking; fuel bounds user-supplied shrinkers.
43	def minimize(~T: Type, ~copy: T -> T & T, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool,
44	  fuel: Nat, state: T & Maybe<&1, T>) -> T:
45	  match fuel:
46	    case 0n:
47	      (original, choice) = state
48	      Maybe.default(&1, T, choice, original)
49	    case 1n+p:
50	      (original, choice) = state
51	      match choice:
52	        case None{}:
53	          original
54	        case Some{candidate}:
55	          minimize(~T, ~copy, ~shrink, ~test, p, attempt(~T, ~copy, ~shrink, ~test, candidate))
56	
57	def minimize.start(~T: Type, ~copy: T -> T & T, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool,
58	  value: T) -> T:
59	  minimize(~T, ~copy, ~shrink, ~test, 1024n, attempt(~T, ~copy, ~shrink, ~test, value))
60	
61	def draw.pair(~T: Type, ~test: T -> T & Bool, pair: T & Rand.Rng) -> (T & Bool) & Rand.Rng:
62	  (sample, next) = pair
63	  (test(sample), next)
64	
65	def draw(~T: Type, ~gen: Rand.Rng -> T & Rand.Rng, ~test: T -> T & Bool, rng: Rand.Rng) -> (T & Bool) & Rand.Rng:
66	  draw.pair(~T, ~test, gen(rng))
67	
68	def check.go(~T: Type, ~gen: Rand.Rng -> T & Rand.Rng, ~copy: T -> T & T,
69	  ~shrink: T -> List<&1, T>, ~test: T -> T & Bool,
70	  remaining: Nat, +seed: U32, +trial: Nat, state: (T & Bool) & Rand.Rng) -> Maybe<&1, Failure<T>>:
71	  match remaining:
72	    case 0n:
73	      None{}
74	    case 1n+p:
75	      match p:
76	        case 0n:
77	          (tested, next) = state
78	          (value, ok) = tested
79	          match ok:
80	            case False{}:
81	              Some{Failure{seed, trial, minimize.start(~T, ~copy, ~shrink, ~test, value)}}
82	            case True{}:
83	              None{}
84	        case 1n+q:
85	          (tested, next) = state
86	          (value, ok) = tested
87	          match ok:
88	            case False{}:
89	              Some{Failure{seed, trial, minimize.start(~T, ~copy, ~shrink, ~test, value)}}
90	            case True{}:
91	              check.go(~T, ~gen, ~copy, ~shrink, ~test, p, seed, (1n+trial), draw(~T, ~gen, ~test, next))
92	
93	def check.start(~T: Type, ~gen: Rand.Rng -> T & Rand.Rng, ~copy: T -> T & T,
94	  ~shrink: T -> List<&1, T>, ~test: T -> T & Bool,
95	  remaining: Nat, seed: U32, rng: Rand.Rng) -> Maybe<&1, Failure<T>>:
96	  match remaining:
97	    case 0n:
98	      None{}
99	    case 1n+p:
100	      check.go(~T, ~gen, ~copy, ~shrink, ~test, remaining, seed, 0n, draw(~T, ~gen, ~test, rng))
101	
102	# Return the first failure and its smallest reachable counterexample.
103	def check(~T: Type, ~gen: Rand.Rng -> T & Rand.Rng, ~copy: T -> T & T,
104	  ~shrink: T -> List<&1, T>, ~test: T -> T & Bool,
105	  +seed: U32, trials: Nat) -> Maybe<&1, Failure<T>>:
106	  check.start(~T, ~gen, ~copy, ~shrink, ~test, trials, seed, Rand.seed(seed))
107	
108	# Print the seed and draw index so a failing check can be replayed.
109	def report(~T: Type, ~show: T -> String, result: Maybe<&1, Failure<T>>) -> IO(Bool):
110	  match result:
111	    case None{}:
112	      IO.pure(Bool, True{})
113	    case Some{Failure{seed, trial, value}}:
114	      do IO<Bool>:
115	        IO.print("property failed: seed=" ++ U32.show(seed) ++ " trial=" ++ Nat.show(trial) ++ " counterexample=" ++ show(value))
116	        return False{}
117	
118	def run(~T: Type, ~gen: Rand.Rng -> T & Rand.Rng, ~copy: T -> T & T,
119	  ~shrink: T -> List<&1, T>, ~test: T -> T & Bool, ~show: T -> String,
120	  seed: U32, trials: Nat) -> IO(Bool):
121	  report(~T, ~show, check(~T, ~gen, ~copy, ~shrink, ~test, seed, trials))