1	# lazy: branches that do not run both ways. Bool.pick, Bool.and and Bool.or
2	# are ordinary defs, so every argument is evaluated before the call: a
3	# search written as `Bool.pick(T, hit, here, go(rest))` walks the whole list
4	# whatever `hit` says (measured native, 100 iterations over 100k cells: the
5	# hit at the head costs 0.10 s, the same as the hit at the end, while the
6	# forms here cost 0.00 s). A thunk `Unit -> T` is a value, so the branch
7	# that is not taken is never applied. Keep them for work that does not
8	# recurse: a thunk around a search's own recursive step allocates a closure
9	# and leaves the loop on every step, where carrying the test as a Bool into
10	# the next call keeps it a loop (the `thunk` rule, U015).
11	#
12	# No law can say that a branch is not taken, since a law states what a term
13	# equals, not what evaluation skipped: each form here matches on the Bool
14	# before it applies the thunk, and laws/LazyMatchesEagerCombinators.bend proves the
15	# values agree with the strict forms.
16	import Base
17	
18	# `a` when c, else what rest gives: the early exit of a search
19	def stop(-A: Type, cc: Bool, aa: A, rest: Unit -> A) -> A:
20	  match cc:
21	    case True{}:
22	      aa
23	    case False{}:
24	      rest(Unit{})
25	
26	# True when a, else what rest gives: `or` that stops at the first True
27	def or_else(aa: Bool, rest: Unit -> Bool) -> Bool:
28	  match aa:
29	    case True{}:
30	      True{}
31	    case False{}:
32	      rest(Unit{})
33	
34	# what rest gives when a, else False: `and` that stops at the first False
35	def and_then(aa: Bool, rest: Unit -> Bool) -> Bool:
36	  match aa:
37	    case True{}:
38	      rest(Unit{})
39	    case False{}:
40	      False{}
41	
42	# what yes gives when c, else what no gives: a pick whose two branches each
43	# recurse, only the one taken run
44	def either(-A: Type, cc: Bool, yes: Unit -> A, no: Unit -> A) -> A:
45	  match cc:
46	    case True{}:
47	      yes(Unit{})
48	    case False{}:
49	      no(Unit{})