1	import Base
2	import ./class.bend as C
3	
4	# tree.bend: binary trees reduced with parallel calls.
5	#
6	#   import ./tree.bend as Tree
7	#   Tree.reduce(~Nat, ~Nat.add_sg(), t)
8	#
9	# reduce evaluates the two halves of each Fork with a parallel call. The
10	# law reduce_foldr says that for any C.Semigroup, reduce gives the same
11	# result as Base's List.foldr over the leaves in order. It needs no
12	# identity element, because a tree always has a leaf.
13	#
14	# Not yet measured: the speedup of reduce on the CPU, and any run on the
15	# GPU.
16	
17	type Tree<-A: Data> is Data:
18	  Tip{x: A}
19	  Fork{l: Tree<A>, r: Tree<A>}
20	
21	def reduce(~A: Data, ~m: C.Semigroup<A>, t: Tree<A>) -> A:
22	  match t:
23	    case Tip{x}:
24	      x
25	    case Fork{l, r}:
26	      a b = reduce(~A, ~m, l) reduce(~A, ~m, r)
27	      C.Semigroup.op(A, m, a, b)
28	
29	# the leaves, left to right, in front of acc
30	def to_list.go(-A: Data, t: Tree<A>, acc: List<&2, A>) -> List<&2, A>:
31	  match t:
32	    case Tip{x}:
33	      x <> acc
34	    case Fork{l, r}:
35	      to_list.go(A, l, to_list.go(A, r, acc))
36	
37	def to_list(-A: Data, t: Tree<A>) -> List<&2, A>:
38	  to_list.go(A, t, Nil{})
39	
40	# a balanced tree with 2^d leaves f(lo), f(lo+1), ..., so both halves of
41	# each parallel call do the same amount of work
42	def build(~A: Data, ~f: Nat -> A, +d: Nat, +lo: Nat) -> Tree<A>:
43	  match d:
44	    case 0n:
45	      Tip{f(lo)}
46	    case 1n+p:
47	      l r = build(~A, ~f, p, lo) build(~A, ~f, p, Nat.add(lo, Nat.pow(2n, p)))
48	      Fork{l, r}
49	
50	# reduce agrees with foldr. With acc = Nil{}:
51	# {op(reduce(t), z) == foldr(to_list(t), z)}.
52	law reduce_foldr:
53	  for ~A: Data
54	  for ~m: C.Semigroup<A>
55	  for t: Tree<A>
56	  for +acc: List<&2, A>
57	  for +z: A
58	  {C.Semigroup.op(A, m, reduce(~A, ~m, t), List.foldr(~&2, ~A, ~A, ~C.Semigroup.fn(~A, ~m), acc, z)) == List.foldr(~&2, ~A, ~A, ~C.Semigroup.fn(~A, ~m), to_list.go(A, t, acc), z) : A}
59	
60	def reduce_foldr(A, m, t, acc, z):
61	  match t:
62	    case Tip{x}:
63	      {==}
64	    case Fork{+l, +r}:
65	      -fz = List.foldr(~&2, ~A, ~A, ~C.Semigroup.fn(~A, ~m), acc, z)
66	      -g = C.Semigroup.op(A, m, C.Semigroup.op(A, m, reduce(~A, ~m, l), reduce(~A, ~m, r)), fz)
67	      %reduce_foldr(~A, ~m, l, to_list.go(A, r, acc), z) : {g == _ : A}
68	      %reduce_foldr(~A, ~m, r, acc, z) : {g == C.Semigroup.op(A, m, reduce(~A, ~m, l), _) : A}
69	      Equal.sym(A, C.Semigroup.op(A, m, reduce(~A, ~m, l), C.Semigroup.op(A, m, reduce(~A, ~m, r), fz)), g,
70	        C.Semigroup.assoc(A, m, reduce(~A, ~m, l), reduce(~A, ~m, r), List.foldr(~&2, ~A, ~A, ~C.Semigroup.fn(~A, ~m), acc, z)))