src/tensor/permute_contract.bend
bendtorch-core@0.1.0.0 · 241 lines · 16 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/LAWS.bend as ShapeLaws
4import bendtorch-core@0.1.0.0/src/shape/PROOF.bend as ShapeProof
5import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
6import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
7import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
8import bendtorch-core@0.1.0.0/src/storage/PROOF.bend as StorageProof
9import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
10import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
11import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
12import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
13import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as Transpose
14import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
15import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof
16import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
17import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads
18import bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend as Observation
19import bendtorch-core@0.1.0.0/src/tensor/transform_records.bend as Laws
20
21def retained_code(+input: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +request: Observation.Request, +error: Transforms.Error,
22 failed: {Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request) == (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}) ->
23 {Observation.failure_code(input, request, Done{Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}}) == Some{Transforms.error_code(error)} : Maybe<&2, U32>}:
24 Equal.cong(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Maybe<&2, U32>, pair => Some{Observation.failure_code_pair(input, pair)},
25 Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request), (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}), failed)
26
27def retained_dimensions(+input: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +request: Observation.Request, +error: Transforms.Error,
28 failed: {Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request) == (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}) ->
29 {Observation.kept_dimensions(input, request, Done{Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}}) == Some{Shape.dimensions(input)} : Maybe<&2, List<&2, U32>>}:
30 Equal.cong(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Maybe<&2, List<&2, U32>>, pair => Observation.kept_dimensions_pair(input, pair),
31 Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request), (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}), failed)
32
33def retained_length(+input: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +request: Observation.Request, +error: Transforms.Error,
34 failed: {Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request) == (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}) ->
35 {Observation.kept_length(input, request, Done{Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}}) == Some{Shape.logical_numel(Shape.dimensions(input))} : Maybe<&2, Nat>}:
36 Equal.trans(Maybe<&2, Nat>, Some{Observation.kept_length_pair(input, Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request))},
37 Some{Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill))}, Some{Shape.logical_numel(Shape.dimensions(input))},
38 Equal.cong(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Maybe<&2, Nat>, pair => Some{Observation.kept_length_pair(input, pair)},
39 Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request), (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}), failed),
40 Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number}, Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)), Shape.logical_numel(Shape.dimensions(input)), Reads.created_exact(input, fill)))
41
42def retained_count(+input: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +request: Observation.Request, +error: Transforms.Error,
43 failed: {Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request) == (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}) ->
44 {Observation.kept_count(input, request, Done{Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}}) == Some{Shape.count(input)} : Maybe<&2, U32>}:
45 Equal.cong(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Maybe<&2, U32>, pair => Observation.kept_count_pair(input, pair),
46 Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request), (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}), failed)
47
48def retained_value(+input: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +request: Observation.Request, +error: Transforms.Error, +other: U32,
49 inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool}, failed: {Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request) == (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}) ->
50 {Observation.kept_value(input, request, other, Done{Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}}) == Some{fill} : Maybe<&2, F32>}:
51 Equal.trans(Maybe<&2, F32>, Observation.kept_value_pair(input, other, Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request)),
52 Observation.kept_value_pair(input, other, (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error})), Some{fill},
53 Equal.cong(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Maybe<&2, F32>, pair => Observation.kept_value_pair(input, other, pair),
54 Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request), (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}), failed),
55 Reads.read_point_done(input, fill, valid, other, inside))
56
57def ranked_failure(+input: Shape.Shape, +axes: List<&2, U32>,
58 decision: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))>,
59 wrong: {Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) == False{} : Bool}) ->
60 {Layout.plan_ranked(input, axes, decision) == Fail{Layout.AxesLengthMismatch{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
61 match decision:
62 case Shape.BFalse{no}:
63 {==}
64 case Shape.BTrue{yes}:
65 Empty.absurd({Layout.plan_ranked(input, axes, Shape.BTrue{yes}) == Fail{Layout.AxesLengthMismatch{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
66 Nats.contradiction(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), yes,
67 Equal.sym(Bool, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), False{}, wrong)))
68
69def ranked_pass(+input: Shape.Shape, +axes: List<&2, U32>,
70 decision: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))>,
71 ranked: {Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) == True{} : Bool}) ->
72 {Layout.plan_ranked(input, axes, decision) == Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))) : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
73 match decision:
74 case Shape.BFalse{no}:
75 Empty.absurd({Layout.plan_ranked(input, axes, Shape.BFalse{no}) == Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))) : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
76 Nats.contradiction(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))),
77 Equal.sym(Bool, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), True{}, ranked), no))
78 case Shape.BTrue{yes}:
79 {==}
80
81def bounded_failure(+input: Shape.Shape, +axes: List<&2, U32>, decision: Shape.BoolCase<Layout.bounded(axes, Shape.rank(input))>,
82 outside: {Layout.bounded(axes, Shape.rank(input)) == False{} : Bool}) ->
83 {Layout.plan_bounded(input, axes, decision) == Fail{Layout.AxisOutOfBounds{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
84 match decision:
85 case Shape.BFalse{no}:
86 {==}
87 case Shape.BTrue{yes}:
88 Empty.absurd({Layout.plan_bounded(input, axes, Shape.BTrue{yes}) == Fail{Layout.AxisOutOfBounds{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
89 Nats.contradiction(Layout.bounded(axes, Shape.rank(input)), yes, Equal.sym(Bool, Layout.bounded(axes, Shape.rank(input)), False{}, outside)))
90
91def bounded_pass(+input: Shape.Shape, +axes: List<&2, U32>, decision: Shape.BoolCase<Layout.bounded(axes, Shape.rank(input))>,
92 bounded: {Layout.bounded(axes, Shape.rank(input)) == True{} : Bool}) ->
93 {Layout.plan_bounded(input, axes, decision) == Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))) : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
94 match decision:
95 case Shape.BFalse{no}:
96 Empty.absurd({Layout.plan_bounded(input, axes, Shape.BFalse{no}) == Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))) : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
97 Nats.contradiction(Layout.bounded(axes, Shape.rank(input)), Equal.sym(Bool, Layout.bounded(axes, Shape.rank(input)), True{}, bounded), no))
98 case Shape.BTrue{yes}:
99 {==}
100
101def unique_failure(+input: Shape.Shape, +axes: List<&2, U32>, decision: Shape.BoolCase<Layout.unique(axes)>,
102 duplicate: {Layout.unique(axes) == False{} : Bool}) ->
103 {Layout.plan_unique(input, axes, decision) == Fail{Layout.DuplicateAxis{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
104 match decision:
105 case Shape.BFalse{no}:
106 {==}
107 case Shape.BTrue{yes}:
108 Empty.absurd({Layout.plan_unique(input, axes, Shape.BTrue{yes}) == Fail{Layout.DuplicateAxis{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
109 Nats.contradiction(Layout.unique(axes), yes, Equal.sym(Bool, Layout.unique(axes), False{}, duplicate)))
110
111def planned_failure(+input: Shape.Shape, -tensor: Core.Tensor<input>, +axes: List<&2, U32>, -error: Layout.Error,
112 planned: {Layout.permutation(input, axes) == Fail{error} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}) ->
113 {Observation.apply(input, tensor, Observation.Permute{axes}) == (tensor, Fail{Transforms.LayoutError{error}}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}:
114 Equal.cong(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, result => Transforms.copy_planned(input, axes, tensor, result),
115 Layout.permutation(input, axes), Fail{error}, planned)
116
117def transpose_failure(+input: Shape.Shape, -tensor: Core.Tensor<input>, +a: U32, +b: U32,
118 decision: Shape.BoolCase<Transpose.valid(input, a, b)>, outside: {Transpose.valid(input, a, b) == False{} : Bool}) ->
119 {Transforms.transpose_decided(input, tensor, a, b, decision) == (tensor, Fail{Transforms.LayoutError{Layout.AxisOutOfBounds{}}}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}:
120 match decision:
121 case Shape.BFalse{no}:
122 {==}
123 case Shape.BTrue{yes}:
124 Empty.absurd({Transforms.transpose_decided(input, tensor, a, b, Shape.BTrue{yes}) == (tensor, Fail{Transforms.LayoutError{Layout.AxisOutOfBounds{}}}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>},
125 Nats.contradiction(Transpose.valid(input, a, b), yes, Equal.sym(Bool, Transpose.valid(input, a, b), False{}, outside)))
126
127def permute_rank_mismatch(+input: Shape.Shape, +fill: F32, +axes: List<&2, U32>, wrong: {Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) == False{} : Bool}) -> Laws.RetainedFailure<input, fill, Observation.Permute{axes}, 12>:
128 +wrong = wrong
129 Laws.RetainedFailure{
130 Reads.new_lift(input, fill, result => {Observation.failure_code(input, Observation.Permute{axes}, result) == Some{12} : Maybe<&2, U32>},
131 valid => retained_code(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxesLengthMismatch{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxesLengthMismatch{}, ranked_failure(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), wrong)))),
132 Reads.new_lift(input, fill, result => {Observation.kept_dimensions(input, Observation.Permute{axes}, result) == Some{Shape.dimensions(input)} : Maybe<&2, List<&2, U32>>},
133 valid => retained_dimensions(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxesLengthMismatch{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxesLengthMismatch{}, ranked_failure(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), wrong)))),
134 Reads.new_lift(input, fill, result => {Observation.kept_length(input, Observation.Permute{axes}, result) == Some{Shape.logical_numel(Shape.dimensions(input))} : Maybe<&2, Nat>},
135 valid => retained_length(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxesLengthMismatch{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxesLengthMismatch{}, ranked_failure(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), wrong)))),
136 Reads.new_lift(input, fill, result => {Observation.kept_count(input, Observation.Permute{axes}, result) == Some{Shape.count(input)} : Maybe<&2, U32>},
137 valid => retained_count(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxesLengthMismatch{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxesLengthMismatch{}, ranked_failure(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), wrong)))),
138 other => inside => Reads.new_lift(input, fill, result => {Observation.kept_value(input, Observation.Permute{axes}, other, result) == Some{fill} : Maybe<&2, F32>},
139 valid => retained_value(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxesLengthMismatch{}}, other, inside, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxesLengthMismatch{}, ranked_failure(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), wrong))))}
140
141def permute_axis_out_of_bounds(+input: Shape.Shape, +fill: F32, +axes: List<&2, U32>, ranked: {Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) == True{} : Bool},
142 outside: {Layout.bounded(axes, Shape.rank(input)) == False{} : Bool}) -> Laws.RetainedFailure<input, fill, Observation.Permute{axes}, 13>:
143 +ranked = ranked
144 +outside = outside
145 Laws.RetainedFailure{
146 Reads.new_lift(input, fill, result => {Observation.failure_code(input, Observation.Permute{axes}, result) == Some{13} : Maybe<&2, U32>},
147 valid => retained_code(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxisOutOfBounds{},
148 Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
149 Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.AxisOutOfBounds{}},
150 ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
151 bounded_failure(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), outside))))),
152 Reads.new_lift(input, fill, result => {Observation.kept_dimensions(input, Observation.Permute{axes}, result) == Some{Shape.dimensions(input)} : Maybe<&2, List<&2, U32>>},
153 valid => retained_dimensions(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxisOutOfBounds{},
154 Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
155 Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.AxisOutOfBounds{}},
156 ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
157 bounded_failure(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), outside))))),
158 Reads.new_lift(input, fill, result => {Observation.kept_length(input, Observation.Permute{axes}, result) == Some{Shape.logical_numel(Shape.dimensions(input))} : Maybe<&2, Nat>},
159 valid => retained_length(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxisOutOfBounds{},
160 Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
161 Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.AxisOutOfBounds{}},
162 ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
163 bounded_failure(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), outside))))),
164 Reads.new_lift(input, fill, result => {Observation.kept_count(input, Observation.Permute{axes}, result) == Some{Shape.count(input)} : Maybe<&2, U32>},
165 valid => retained_count(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxisOutOfBounds{},
166 Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
167 Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.AxisOutOfBounds{}},
168 ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
169 bounded_failure(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), outside))))),
170 other => inside => Reads.new_lift(input, fill, result => {Observation.kept_value(input, Observation.Permute{axes}, other, result) == Some{fill} : Maybe<&2, F32>},
171 valid => retained_value(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, other, inside, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxisOutOfBounds{},
172 Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
173 Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.AxisOutOfBounds{}},
174 ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
175 bounded_failure(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), outside)))))}
176
177def permute_duplicate_axis(+input: Shape.Shape, +fill: F32, +axes: List<&2, U32>, ranked: {Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) == True{} : Bool},
178 bounded: {Layout.bounded(axes, Shape.rank(input)) == True{} : Bool}, duplicate: {Layout.unique(axes) == False{} : Bool}) -> Laws.RetainedFailure<input, fill, Observation.Permute{axes}, 14>:
179 +ranked = ranked
180 +bounded = bounded
181 +duplicate = duplicate
182 Laws.RetainedFailure{
183 Reads.new_lift(input, fill, result => {Observation.failure_code(input, Observation.Permute{axes}, result) == Some{14} : Maybe<&2, U32>},
184 valid => retained_code(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.DuplicateAxis{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.DuplicateAxis{},
185 Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
186 Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.DuplicateAxis{}},
187 ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
188 Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))),
189 Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))), Fail{Layout.DuplicateAxis{}},
190 bounded_pass(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), bounded),
191 unique_failure(input, axes, Shape.bool_case(Layout.unique(axes)), duplicate)))))),
192 Reads.new_lift(input, fill, result => {Observation.kept_dimensions(input, Observation.Permute{axes}, result) == Some{Shape.dimensions(input)} : Maybe<&2, List<&2, U32>>},
193 valid => retained_dimensions(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.DuplicateAxis{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.DuplicateAxis{},
194 Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
195 Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.DuplicateAxis{}},
196 ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
197 Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))),
198 Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))), Fail{Layout.DuplicateAxis{}},
199 bounded_pass(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), bounded),
200 unique_failure(input, axes, Shape.bool_case(Layout.unique(axes)), duplicate)))))),
201 Reads.new_lift(input, fill, result => {Observation.kept_length(input, Observation.Permute{axes}, result) == Some{Shape.logical_numel(Shape.dimensions(input))} : Maybe<&2, Nat>},
202 valid => retained_length(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.DuplicateAxis{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.DuplicateAxis{},
203 Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
204 Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.DuplicateAxis{}},
205 ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
206 Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))),
207 Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))), Fail{Layout.DuplicateAxis{}},
208 bounded_pass(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), bounded),
209 unique_failure(input, axes, Shape.bool_case(Layout.unique(axes)), duplicate)))))),
210 Reads.new_lift(input, fill, result => {Observation.kept_count(input, Observation.Permute{axes}, result) == Some{Shape.count(input)} : Maybe<&2, U32>},
211 valid => retained_count(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.DuplicateAxis{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.DuplicateAxis{},
212 Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
213 Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.DuplicateAxis{}},
214 ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
215 Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))),
216 Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))), Fail{Layout.DuplicateAxis{}},
217 bounded_pass(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), bounded),
218 unique_failure(input, axes, Shape.bool_case(Layout.unique(axes)), duplicate)))))),
219 other => inside => Reads.new_lift(input, fill, result => {Observation.kept_value(input, Observation.Permute{axes}, other, result) == Some{fill} : Maybe<&2, F32>},
220 valid => retained_value(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.DuplicateAxis{}}, other, inside, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.DuplicateAxis{},
221 Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
222 Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.DuplicateAxis{}},
223 ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
224 Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))),
225 Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))), Fail{Layout.DuplicateAxis{}},
226 bounded_pass(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), bounded),
227 unique_failure(input, axes, Shape.bool_case(Layout.unique(axes)), duplicate))))))}
228
229def transpose_out_of_bounds(+input: Shape.Shape, +fill: F32, +a: U32, +b: U32, outside: {Transpose.valid(input, a, b) == False{} : Bool}) -> Laws.RetainedFailure<input, fill, Observation.Transpose{a, b}, 13>:
230 +outside = outside
231 Laws.RetainedFailure{
232 Reads.new_lift(input, fill, result => {Observation.failure_code(input, Observation.Transpose{a, b}, result) == Some{13} : Maybe<&2, U32>},
233 valid => retained_code(input, fill, valid, Observation.Transpose{a, b}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, transpose_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, a, b, Shape.bool_case(Transpose.valid(input, a, b)), outside))),
234 Reads.new_lift(input, fill, result => {Observation.kept_dimensions(input, Observation.Transpose{a, b}, result) == Some{Shape.dimensions(input)} : Maybe<&2, List<&2, U32>>},
235 valid => retained_dimensions(input, fill, valid, Observation.Transpose{a, b}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, transpose_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, a, b, Shape.bool_case(Transpose.valid(input, a, b)), outside))),
236 Reads.new_lift(input, fill, result => {Observation.kept_length(input, Observation.Transpose{a, b}, result) == Some{Shape.logical_numel(Shape.dimensions(input))} : Maybe<&2, Nat>},
237 valid => retained_length(input, fill, valid, Observation.Transpose{a, b}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, transpose_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, a, b, Shape.bool_case(Transpose.valid(input, a, b)), outside))),
238 Reads.new_lift(input, fill, result => {Observation.kept_count(input, Observation.Transpose{a, b}, result) == Some{Shape.count(input)} : Maybe<&2, U32>},
239 valid => retained_count(input, fill, valid, Observation.Transpose{a, b}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, transpose_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, a, b, Shape.bool_case(Transpose.valid(input, a, b)), outside))),
240 other => inside => Reads.new_lift(input, fill, result => {Observation.kept_value(input, Observation.Transpose{a, b}, other, result) == Some{fill} : Maybe<&2, F32>},
241 valid => retained_value(input, fill, valid, Observation.Transpose{a, b}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, other, inside, transpose_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, a, b, Shape.bool_case(Transpose.valid(input, a, b)), outside)))}