1	import Base
2	import ../shape/core.bend as Shape
3	import ../storage/arith.bend as Arith
4	import ../tensor/core.bend as Core
5	import ../tensor/layout.bend as Layout
6	import ../tensor/elementwise_totality.bend as Totality
7	import ../tensor/construction_LAWS.bend as ConstructionLaws
8	import ../tensor/construction_PROOF.bend as ConstructionProof
9	import ../tensor/transform_PROOF.bend as TransformProof
10	import ./reduce.bend as Reduce
11	import ./reduce_LAWS.bend as ReduceLaws
12	import ./reduce_PROOF.bend as ReduceProof
13	import ./sum_to_size.bend as SumToSize
14	import ./sum_to_size_LAWS.bend as Laws
15	
16	type Holds<-P: Type> is Data:
17	  Holds{-proof: P}
18	
19	def FirstKept(-shape: Shape.Shape, -original: Core.Tensor<shape>, pair: Core.Tensor<shape> & Core.Tensor<shape>) -> Type:
20	  (@+index: U32 -> {ConstructionLaws.clone_first_checked(shape, pair, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}) &
21	    (@+index: U32 -> {ConstructionLaws.clone_first_model(shape, pair, index) == Core.observe(shape, original, index) : Maybe<&2, F32>})
22	
23	def SecondKept(-shape: Shape.Shape, -original: Core.Tensor<shape>, pair: Core.Tensor<shape> & Core.Tensor<shape>) -> Type:
24	  (@+index: U32 -> {ConstructionLaws.clone_second_checked(shape, pair, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}) &
25	    (@+index: U32 -> {ConstructionLaws.clone_second_model(shape, pair, index) == Core.observe(shape, original, index) : Maybe<&2, F32>})
26	
27	def first_kept(+shape: Shape.Shape, original: Core.Tensor<shape>) -> Holds<FirstKept(shape, original, Core.clone(shape, original))>:
28	  {\{ConstructionLaws.CloneMeaning: first_checked => second_checked => first_model => second_model =>
29	    Holds{(first_checked, first_model)}} :
30	    ConstructionLaws.CloneMeaning<shape, original> -> Holds<FirstKept(shape, original, Core.clone(shape, original))>}(
31	    ConstructionLaws.public_clone_elements(shape, original))
32	
33	def second_kept(+shape: Shape.Shape, original: Core.Tensor<shape>) -> Holds<SecondKept(shape, original, Core.clone(shape, original))>:
34	  {\{ConstructionLaws.CloneMeaning: first_checked => second_checked => first_model => second_model =>
35	    Holds{(second_checked, second_model)}} :
36	    ConstructionLaws.CloneMeaning<shape, original> -> Holds<SecondKept(shape, original, Core.clone(shape, original))>}(
37	    ConstructionLaws.public_clone_elements(shape, original))
38	
39	def first_property(+property: Totality.Property, -shape: Shape.Shape, -original: Core.Tensor<shape>, -first: Core.Tensor<shape>,
40	  checked: @+index: U32 -> {Core.checked_observe(shape, first, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>},
41	  model: @+index: U32 -> {Core.observe(shape, first, index) == Core.observe(shape, original, index) : Maybe<&2, F32>}) ->
42	  {Totality.inspect(property, Core.Packed{shape, first}) == Totality.inspect(property, Core.Packed{shape, original}) : Totality.Inspection}:
43	  match property:
44	    case Totality.Dimensions{}:
45	      {==}
46	    case Totality.Checked{+index}:
47	      Equal.cong(Maybe<&2, F32>, Totality.Inspection, value => Totality.Value{value},
48	        Core.checked_observe(shape, first, index), Core.checked_observe(shape, original, index), checked(index))
49	    case Totality.Raw{+index}:
50	      Equal.cong(Maybe<&2, F32>, Totality.Inspection, value => Totality.Value{value},
51	        Core.observe(shape, first, index), Core.observe(shape, original, index), model(index))
52	
53	def cloned_retains(+shape: Shape.Shape, -original: Core.Tensor<shape>, pair: Core.Tensor<shape> & Core.Tensor<shape>,
54	  -kept: FirstKept(shape, original, pair)) ->
55	  ReduceLaws.Retained<Core.Packed{shape, original}, SumToSize.cloned(shape, pair)>:
56	  (first, second) = pair
57	  ReduceLaws.Retained{property => first_property(property, shape, original, first,
58	    Pair.fst(@+index: U32 -> {Core.checked_observe(shape, first, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}, @+index: U32 -> {Core.observe(shape, first, index) == Core.observe(shape, original, index) : Maybe<&2, F32>}, kept), Pair.snd(@+index: U32 -> {Core.checked_observe(shape, first, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}, @+index: U32 -> {Core.observe(shape, first, index) == Core.observe(shape, original, index) : Maybe<&2, F32>}, kept))}
59	
60	def decided_retains(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, same: Bool) ->
61	  ReduceLaws.Retained<Core.Packed{shape, tensor}, SumToSize.decided(shape, tensor, target, same)>:
62	  match same:
63	    case False{}:
64	      ReduceLaws.reduce_retains_input(Core.Packed{shape, tensor}, target)
65	    case True{}:
66	      cloned_retains(shape, tensor, Core.clone(shape, tensor),
67	        {\{Holds: proof => proof} : Holds<FirstKept(shape, tensor, Core.clone(shape, tensor))> -> FirstKept(shape, tensor, Core.clone(shape, tensor))}(
68	          first_kept(shape, tensor)))
69	
70	def Laws.sum_to_size_retains_input(input, target):
71	  Core.Packed{+shape, tensor} = input
72	  decided_retains(shape, tensor, target, Layout.words_same(Shape.dimensions(shape), Shape.dimensions(target)))
73	
74	def cloned_identity(+shape: Shape.Shape, -original: Core.Tensor<shape>, +target: Shape.Shape, pair: Core.Tensor<shape> & Core.Tensor<shape>,
75	  -same: {Shape.dimensions(shape) == Shape.dimensions(target) : List<&2, U32>},
76	  -kept: SecondKept(shape, original, pair)) ->
77	  Holds<Laws.Identity(Core.Packed{shape, original}, target, SumToSize.cloned(shape, pair))>:
78	  (first, second) = pair
79	  Holds{(same, index => (Pair.fst(@+index: U32 -> {Core.checked_observe(shape, second, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}, @+index: U32 -> {Core.observe(shape, second, index) == Core.observe(shape, original, index) : Maybe<&2, F32>}, kept)(index), Pair.snd(@+index: U32 -> {Core.checked_observe(shape, second, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}, @+index: U32 -> {Core.observe(shape, second, index) == Core.observe(shape, original, index) : Maybe<&2, F32>}, kept)(index)))}
80	
81	def decided_identity(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, flag: Bool,
82	  -decided: {flag == Layout.words_same(Shape.dimensions(shape), Shape.dimensions(target)) : Bool},
83	  -same: {Shape.dimensions(shape) == Shape.dimensions(target) : List<&2, U32>}) ->
84	  Holds<Laws.Identity(Core.Packed{shape, tensor}, target, SumToSize.decided(shape, tensor, target, flag))>:
85	  match flag:
86	    case False{}:
87	      Holds{Empty.absurd(Laws.Identity(Core.Packed{shape, tensor}, target, SumToSize.decided(shape, tensor, target, False{})),
88	        Arith.clash(Equal.trans(Bool, False{}, Layout.words_same(Shape.dimensions(shape), Shape.dimensions(target)), True{}, decided,
89	          %same : {Layout.words_same(Shape.dimensions(shape), _) == True{} : Bool}
90	          TransformProof.words_same_refl(Shape.dimensions(shape)))))}
91	    case True{}:
92	      cloned_identity(shape, tensor, target, Core.clone(shape, tensor), same,
93	        {\{Holds: proof => proof} : Holds<SecondKept(shape, tensor, Core.clone(shape, tensor))> -> SecondKept(shape, tensor, Core.clone(shape, tensor))}(
94	          second_kept(shape, tensor)))
95	
96	def Laws.sum_to_size_identity(input, target, same):
97	  Core.Packed{+shape, tensor} = input
98	  Laws.IdentityModel{
99	    {\{Holds: proof => proof} :
100	      Holds<Laws.Identity(Core.Packed{shape, tensor}, target,
101	        SumToSize.decided(shape, tensor, target, Layout.words_same(Shape.dimensions(shape), Shape.dimensions(target))))> ->
102	      Laws.Identity(Core.Packed{shape, tensor}, target, SumToSize.sum_to_size(Core.Packed{shape, tensor}, target))}(
103	      decided_identity(shape, tensor, target, Layout.words_same(Shape.dimensions(shape), Shape.dimensions(target)), {==}, same))}
104	
105	def decided_reduces(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, flag: Bool,
106	  decided: {flag == Layout.words_same(Shape.dimensions(shape), Shape.dimensions(target)) : Bool},
107	  differ: {Shape.dimensions(shape) != Shape.dimensions(target) : List<&2, U32>}) ->
108	  {SumToSize.decided(shape, tensor, target, flag) == Reduce.reduce_to(Core.Packed{shape, tensor}, target) :
109	    Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>}:
110	  match flag:
111	    case False{}:
112	      {==}
113	    case True{}:
114	      Empty.absurd({SumToSize.decided(shape, tensor, target, True{}) == Reduce.reduce_to(Core.Packed{shape, tensor}, target) :
115	        Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>},
116	        differ(TransformProof.words_equal(Shape.dimensions(shape), Shape.dimensions(target), decided)))
117	
118	def Laws.sum_to_size_reduces(input, target, differ):
119	  Core.Packed{+shape, tensor} = input
120	  decided_reduces(shape, tensor, target, Layout.words_same(Shape.dimensions(shape), Shape.dimensions(target)), {==}, differ)