1 import Base 2 import ../shape/core.bend as Shape 3 import ../shape/flat.bend as Flat 4 import ../shape/LAWS.bend as ShapeLaws 5 import ../shape/PROOF.bend as ShapeProof 6 import ../shape/boundary_proofs.bend as Boundary 7 import ../shape/coordinate_proofs.bend as Coordinates 8 import ./core.bend as Core 9 import ./elementwise.bend as Elementwise 10 import ./projection_LAWS.bend as Laws 11 12 def projected_pair(+plan: Shape.BroadcastPlan, 13 +map: Shape.Index, 14 +index: Shape.FlatIndex) -> 15 {Some{(Shape.index_value(Shape.left_shape(plan), Flat.project_left_index(plan, map, index)), 16 Shape.index_value(Shape.right_shape(plan), Flat.project_right_index(plan, map, index)))} == 17 Laws.offset_spec(plan, ShapeLaws.position(Shape.output_shape(plan), index)) : Maybe<&1, U32 & U32>}: 18 +left = Shape.extents(Shape.left_shape(plan)) 19 +right = Shape.extents(Shape.right_shape(plan)) 20 +output = Shape.extents(Shape.output_shape(plan)) 21 +decoded = ShapeLaws.fin_of(Shape.numel(output), ShapeLaws.position(Shape.output_shape(plan), index)) 22 +left_value = Shape.index_value(Shape.left_shape(plan), Flat.project_left_index(plan, map, index)) 23 +right_value = Shape.index_value(Shape.right_shape(plan), Flat.project_right_index(plan, map, index)) 24 %ShapeLaws.project_left_index_refines(plan, map, index) : 25 {Some{(left_value, right_value)} == Laws.pair_offsets(_, ShapeLaws.flatten_spec(right, 26 ShapeLaws.project_right_coordinate(left, right, output, Shape.alignment(plan), decoded))) : Maybe<&1, U32 & U32>} 27 %ShapeLaws.project_right_index_refines(plan, map, index) : 28 {Some{(left_value, right_value)} == Laws.pair_offsets(Some{left_value}, _) : Maybe<&1, U32 & U32>} 29 {==} 30 31 def Laws.actual_flat_projection(plan, index): 32 projected_pair(plan, Shape.index_map(plan), index) 33 34 def checked_projection(+plan: Shape.BroadcastPlan, +position: Nat, 35 decision: Shape.BoolCase) -> 36 {Laws.indices_result(Elementwise.flat_input_indices(plan, 37 Shape.flat_checked.finish(Shape.output_shape(plan), position, decision))) == 38 Laws.offset_spec(plan, position) : Maybe<&1, U32 & U32>}: 39 match decision: 40 case Shape.BFalse{equal}: 41 %Boundary.fin_of_none(Shape.numel(Shape.extents(Shape.output_shape(plan))), position, 42 Coordinates.size_misses(Shape.output_shape(plan), position, equal)) : 43 {None{} == Laws.pair_offsets( 44 ShapeLaws.flatten_spec(Shape.extents(Shape.left_shape(plan)), ShapeLaws.project_left_coordinate( 45 Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), 46 Shape.extents(Shape.output_shape(plan)), Shape.alignment(plan), _)), 47 ShapeLaws.flatten_spec(Shape.extents(Shape.right_shape(plan)), ShapeLaws.project_right_coordinate( 48 Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), 49 Shape.extents(Shape.output_shape(plan)), Shape.alignment(plan), _))) : Maybe<&1, U32 & U32>} 50 {==} 51 case Shape.BTrue{equal}: 52 Laws.actual_flat_projection(plan, Shape.FIndex{position, equal}) 53 54 def Laws.input_indices_refines(plan, index): 55 checked_projection(plan, U32.to_nat(index), 56 Shape.bool_case(Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))))) 57 58 def checked_acceptance(+plan: Shape.BroadcastPlan, +position: Nat, 59 decision: Shape.BoolCase) -> 60 {Laws.indices_accepted(Elementwise.flat_input_indices(plan, 61 Shape.flat_checked.finish(Shape.output_shape(plan), position, decision))) == 62 Nat.is_lt(position, Shape.numel(Shape.extents(Shape.output_shape(plan)))) : Bool}: 63 match decision: 64 case Shape.BFalse{equal}: 65 Coordinates.size_misses(Shape.output_shape(plan), position, equal) 66 case Shape.BTrue{equal}: 67 Coordinates.size_fits(Shape.output_shape(plan), position, equal) 68 69 def Laws.input_indices_acceptance(plan, index): 70 checked_acceptance(plan, U32.to_nat(index), 71 Shape.bool_case(Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))))) 72 73 def expected_indices_view(+operation: Elementwise.Operation, -left: Core.Dynamic, -right: Core.Dynamic, 74 result: Result<&2, &1, Core.Error, U32 & U32>) -> 75 {Elementwise.expected_indices(operation, left, right, result) == 76 Laws.specified_expected(operation, left, right, Laws.indices_result(result)) : Maybe<&2, F32>}: 77 match result: 78 case Fail{error}: 79 {==} 80 case Done{indices}: 81 (left_index, right_index) = indices 82 {==} 83 84 def Laws.expected_projection_refines(operation, plan, left, right, index): 85 Equal.trans(Maybe<&2, F32>, Elementwise.expected(operation, plan, left, right, index), 86 Laws.specified_expected(operation, left, right, Laws.indices_result(Elementwise.input_indices(plan, index))), 87 Laws.specified_expected(operation, left, right, Laws.offset_spec(plan, U32.to_nat(index))), 88 expected_indices_view(operation, left, right, Elementwise.input_indices(plan, index)), 89 Equal.cong(Maybe<&1, U32 & U32>, Maybe<&2, F32>, 90 offsets => Laws.specified_expected(operation, left, right, offsets), 91 Laws.indices_result(Elementwise.input_indices(plan, index)), Laws.offset_spec(plan, U32.to_nat(index)), 92 Laws.input_indices_refines(plan, index)))