1 import Base 2 import ../shape/core.bend as Shape 3 import ../shape/nat_proofs.bend as Nats 4 import ./layout.bend as Layout 5 import ./axis_spec.bend as Axis 6 import ./axis_algebra.bend as Algebra 7 import ./axis_LAWS.bend as Laws 8 9 def inverse_selected(-rank: Nat, -axes: List<&2, Nat>, certificate: Algebra.Facts) -> 10 {Axis.inverse(rank, axes) == Some{Axis.inverse_axes(rank, axes)} : Maybe<&2, List<&2, Nat>>}: 11 Algebra.Certified{iv, selected, restored, lists, product, fit} = certificate 12 selected 13 14 def inverse_involution(-rank: Nat, -axes: List<&2, Nat>, certificate: Algebra.Facts) -> 15 {Axis.inverse_axes(rank, Axis.inverse_axes(rank, axes)) == axes : List<&2, Nat>}: 16 Algebra.Certified{iv, selected, restored, lists, product, fit} = certificate 17 restored 18 19 def reverse_composition(-A: Data, -rank: Nat, -axes: List<&2, Nat>, -items: List<&2, A>, certificate: Algebra.ListFacts) -> 20 {Axis.order(A, Axis.order(A, items, Axis.inverse_axes(rank, axes)), axes) == items : List<&2, A>}: 21 Algebra.Lists{selected, ranked, scattered, restored, reverse_restored, scatter_restored} = certificate 22 reverse_restored 23 24 def coordinate_fit(-rank: Nat, -axes: List<&2, Nat>, +dimensions: List<&2, Nat>, +coordinates: List<&2, Nat>, 25 dimensions_length: {List.length(&2, Nat, dimensions) == rank : Nat}, coordinates_length: {List.length(&2, Nat, coordinates) == rank : Nat}, certificate: Algebra.Facts) -> 26 {Shape.fit(Axis.order(Nat, dimensions, axes), Axis.order(Nat, coordinates, axes)) == Shape.fit(dimensions, coordinates) : Bool}: 27 Algebra.Certified{iv, selected, restored, lists, product, fit} = certificate 28 fit(dimensions, coordinates, dimensions_length, coordinates_length) 29 30 def plan_valid(-shape: Shape.Shape, -axes: List<&2, U32>, plan: Layout.Plan) -> {True{} == Layout.bijective(shape, axes) : Bool}: 31 Layout.Permutation{output, valid, ordered, count} = plan 32 valid 33 34 def permutation_rejects(+shape: Shape.Shape, +axes: List<&2, U32>, result: Result<&2, &2, Layout.Error, Layout.Plan>, rejected: {False{} == Layout.bijective(shape, axes) : Bool}) -> 35 {Laws.axis_plan_succeeded(shape, axes, result) == False{} : Bool}: 36 match result: 37 case Fail{error}: 38 {==} 39 case Done{plan}: 40 Empty.absurd({True{} == False{} : Bool}, Nats.contradiction(Layout.bijective(shape, axes), plan_valid(shape, axes, plan), rejected)) 41 42 def Laws.axis_lookup_refines(items, index): 43 Algebra.lookup(items, index) 44 45 def Laws.axis_gather_refines(axes, items): 46 Algebra.reorder(axes, items) 47 48 def Laws.axis_scatter_refines(shape, axes, coordinates): 49 Algebra.inverse_coordinates(shape, axes, coordinates) 50 51 def Laws.axis_validity_refines(shape, axes, accepted): 52 Algebra.valid(shape, axes, accepted) 53 54 def Laws.axis_lookup_complete(A, items, index, bound): 55 Algebra.lookup_complete(A, items, index, bound) 56 57 def Laws.axis_permutation_complete(shape, axes, accepted): 58 Algebra.permutation_complete(shape, axes, accepted) 59 60 def Laws.axis_permutation_rejects(shape, axes, rejected): 61 permutation_rejects(shape, axes, Layout.permutation(shape, axes), rejected) 62 63 def Laws.axis_dimension_rank(shape, axes, accepted): 64 Algebra.permutation_rank(shape, axes, accepted) 65 66 def Laws.axis_dimension_product(shape, axes, accepted): 67 Algebra.permutation_product(shape, axes, accepted) 68 69 def Laws.axis_scatter_complete(shape, axes, coordinates, accepted, length): 70 Algebra.scatter_complete(shape, axes, coordinates, accepted, length) 71 72 def Laws.axis_scatter_gather(shape, axes, coordinates, accepted, length): 73 Algebra.scatter_gather(shape, axes, coordinates, accepted, length) 74 75 def Laws.axis_inverse_valid(rank, axes, bound, accepted): 76 Algebra.inverse_valid(rank, axes, bound, accepted) 77 78 def Laws.axis_inverse_selected(rank, axes, bound, accepted): 79 inverse_selected(rank, axes, Algebra.facts(rank, axes, bound, accepted)) 80 81 def Laws.axis_inverse_involution(rank, axes, bound, accepted): 82 inverse_involution(rank, axes, Algebra.facts(rank, axes, bound, accepted)) 83 84 def Laws.axis_inverse_list_composition(A, rank, axes, items, bound, accepted, length): 85 Algebra.inverse_composition(A, rank, axes, items, bound, accepted, length) 86 87 def Laws.axis_inverse_reverse_composition(A, rank, axes, items, bound, accepted, length): 88 reverse_composition(A, rank, axes, items, Algebra.facts_lists(A, rank, axes, items, length, Algebra.facts(rank, axes, bound, accepted))) 89 90 def Laws.axis_inverse_scatter_composition(A, rank, axes, items, bound, accepted, length): 91 Algebra.inverse_scatter_composition(A, rank, axes, items, bound, accepted, length) 92 93 def Laws.axis_coordinate_fit(rank, axes, dimensions, coordinates, bound, accepted, dimensions_length, coordinates_length): 94 coordinate_fit(rank, axes, dimensions, coordinates, dimensions_length, coordinates_length, Algebra.facts(rank, axes, bound, accepted)) 95 96 def Laws.axis_scatter_fit(rank, axes, dimensions, coordinates, bound, accepted, dimensions_length, coordinates_length, fits): 97 Equal.trans(Bool, True{}, Shape.fit(Axis.order(Nat, dimensions, axes), coordinates), Shape.fit(dimensions, Axis.order(Nat, coordinates, Axis.inverse_axes(rank, axes))), fits, 98 Equal.trans(Bool, Shape.fit(Axis.order(Nat, dimensions, axes), coordinates), 99 Shape.fit(Axis.order(Nat, Axis.order(Nat, dimensions, axes), Axis.inverse_axes(rank, axes)), Axis.order(Nat, coordinates, Axis.inverse_axes(rank, axes))), 100 Shape.fit(dimensions, Axis.order(Nat, coordinates, Axis.inverse_axes(rank, axes))), 101 Equal.sym(Bool, Shape.fit(Axis.order(Nat, Axis.order(Nat, dimensions, axes), Axis.inverse_axes(rank, axes)), Axis.order(Nat, coordinates, Axis.inverse_axes(rank, axes))), 102 Shape.fit(Axis.order(Nat, dimensions, axes), coordinates), 103 coordinate_fit(rank, Axis.inverse_axes(rank, axes), Axis.order(Nat, dimensions, axes), coordinates, 104 Algebra.ranked(Nat, rank, axes, dimensions, Algebra.facts_lists(Nat, rank, axes, dimensions, dimensions_length, Algebra.facts(rank, axes, bound, accepted))), 105 coordinates_length, Algebra.facts(rank, Axis.inverse_axes(rank, axes), bound, Algebra.inverse_valid(rank, axes, bound, accepted)))), 106 Equal.cong(List<&2, Nat>, Bool, dims => Shape.fit(dims, Axis.order(Nat, coordinates, Axis.inverse_axes(rank, axes))), 107 Axis.order(Nat, Axis.order(Nat, dimensions, axes), Axis.inverse_axes(rank, axes)), dimensions, 108 Algebra.inverse_composition(Nat, rank, axes, dimensions, bound, accepted, dimensions_length))))