1	import Base
2	import ../../shape/core.bend as Shape
3	import ../../storage/LAWS.bend as StorageLaws
4	import ../core.bend as Core
5	import ../lifecycle.bend as Lifecycle
6	import ../reduction.bend as Reduction
7	import ../word_conversion.bend as Conversion
8	import ./replayed.bend as Replayed
9	import ./pointwise.bend as Pointwise
10	import ./fold.bend as Fold
11	import ./fold_records.bend as Records
12	import ./fold_proof.bend as Proof
13	import ./sum.bend as Sum
14	import ./LAWS.bend as Laws
15	
16	def sequential_snoc(+values: List<&2, F32>, +word: F32, +accumulator: F32) ->
17	  {Reduction.sequential_sum(List.append(&2, F32, values, [word]), accumulator) ==
18	    F32.add(Reduction.sequential_sum(values, accumulator), word) : F32}:
19	  match values:
20	    case Nil{}:
21	      {==}
22	    case +value <> +rest:
23	      sequential_snoc(rest, word, F32.add(accumulator, value))
24	
25	def total_words(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat) ->
26	  {Fold.total(~Unit, ~Sum.add, ~Unit, ~Sum.position, ~Sum.every, Unit{}, Unit{}, shape, fill, ops, count) ==
27	    Reduction.sequential_sum(Laws.words(shape, fill, ops, count), 0.0) : F32}:
28	  match count:
29	    case 0n:
30	      {==}
31	    case 1n+previous:
32	      +word = Replayed.value(shape, fill, ops, U32.from_nat(previous))
33	      %Equal.sym(F32, Reduction.sequential_sum(List.append(&2, F32, Laws.words(shape, fill, ops, previous), [word]), 0.0),
34	        F32.add(Reduction.sequential_sum(Laws.words(shape, fill, ops, previous), 0.0), word),
35	        sequential_snoc(Laws.words(shape, fill, ops, previous), word, 0.0)) :
36	        {F32.add(Fold.total(~Unit, ~Sum.add, ~Unit, ~Sum.position, ~Sum.every, Unit{}, Unit{}, shape, fill, ops, previous), word) == _ : F32}
37	      Equal.cong(F32, F32, total => F32.add(total, word),
38	        Fold.total(~Unit, ~Sum.add, ~Unit, ~Sum.position, ~Sum.every, Unit{}, Unit{}, shape, fill, ops, previous),
39	        Reduction.sequential_sum(Laws.words(shape, fill, ops, previous), 0.0),
40	        total_words(shape, fill, ops, previous))
41	
42	def position_inside(+count: Nat, +bound: Nat, +room: {Nat.is_le(count, bound) == True{} : Bool}) ->
43	  {Pointwise.inside(~Unit, ~Sum.position, Unit{}, count, bound) == True{} : Bool}:
44	  match count:
45	    case 0n:
46	      {==}
47	    case 1n+previous:
48	      %Equal.sym(Bool, Pointwise.inside(~Unit, ~Sum.position, Unit{}, previous, bound), True{},
49	        position_inside(previous, bound, Conversion.le_predecessor(previous, bound, room))) :
50	        {Bool.and(_, Nat.is_lt(previous, bound)) == True{} : Bool}
51	      %Equal.sym(Bool, Nat.is_lt(previous, bound), True{}, Conversion.le_successor_lt(previous, bound, room)) :
52	        {Bool.and(True{}, _) == True{} : Bool}
53	      {==}
54	
55	def elements_room(+shape: Shape.Shape) ->
56	  {Nat.is_le(Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}:
57	  %Equal.sym(Nat, Shape.elements(shape), Shape.numel(Shape.extents(shape)), Shape.elements_exact(shape)) :
58	    {Nat.is_le(_, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
59	  Conversion.le_reflexive(Shape.logical_numel(Shape.dimensions(shape)))
60	
61	def sum_ordered(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>,
62	  -fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
63	  Records.FoldContract<shape, Reduction.sequential_sum(Laws.words(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape))), 0.0),
64	    other => Replayed.value(shape, fill, ops, other),
65	    Sum.sum(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}})>:
66	  +count = Shape.elements(shape)
67	  %Shape.elements_exact(shape) :
68	    Records.FoldContract<shape, Reduction.sequential_sum(Laws.words(shape, fill, ops, _), 0.0),
69	      other => Replayed.value(shape, fill, ops, other),
70	      Fold.run(~Unit, ~Sum.add, ~Unit, ~Sum.position, ~Sum.every, Unit{}, Unit{}, count,
71	        Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}})>
72	  %total_words(shape, fill, ops, count) :
73	    Records.FoldContract<shape, _,
74	      other => Replayed.value(shape, fill, ops, other),
75	      Fold.run(~Unit, ~Sum.add, ~Unit, ~Sum.position, ~Sum.every, Unit{}, Unit{}, count,
76	        Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}})>
77	  Proof.contract(~Unit, ~Sum.add, ~Unit, ~Sum.position, ~Sum.every, Unit{}, Unit{}, shape, fill, ops, count,
78	    position_inside(count, Shape.logical_numel(Shape.dimensions(shape)), elements_room(shape)), fits)