src/tensor/projection_PROOF.bend
bendtorch-core@0.1.0.0 · 92 lines · 4 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/shape/flat.bend as Flat
4import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
5import bendtorch-core@0.1.0.0/src/shape/PROOF.bend as ShapeProof
6import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as Boundary
7import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates
8import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
9import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
10import bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend as Laws
11
12def projected_pair(+plan: Shape.BroadcastPlan,
13 +map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>,
14 +index: Shape.FlatIndex<Shape.output_shape(plan)>) ->
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
31def Laws.actual_flat_projection(plan, index):
32 projected_pair(plan, Shape.index_map(plan), index)
33
34def checked_projection(+plan: Shape.BroadcastPlan, +position: Nat,
35 decision: Shape.BoolCase<Nat.is_lt(position, Shape.elements(Shape.output_shape(plan)))>) ->
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
54def 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
58def checked_acceptance(+plan: Shape.BroadcastPlan, +position: Nat,
59 decision: Shape.BoolCase<Nat.is_lt(position, Shape.elements(Shape.output_shape(plan)))>) ->
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
69def 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
73def 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
84def 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)))