src/tensor/transform_records.bend

bendtorch-core@0.1.0.0 · 29 lines · 3 definitions

1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
4import bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend as Observation
5
6type RetainedFailure<-input: Shape.Shape, -fill: F32, -request: Observation.Request, -code: U32> is Type:
7  RetainedFailure{
8    outcome: {Observation.failure_code(input, request, Core.new(input, fill)) == Some{code} : Maybe<&2, U32>},
9    retained_dimensions: {Observation.kept_dimensions(input, request, Core.new(input, fill)) == Some{Shape.dimensions(input)} : Maybe<&2, List<&2, U32>>},
10    retained_count: {Observation.kept_length(input, request, Core.new(input, fill)) == Some{Shape.logical_numel(Shape.dimensions(input))} : Maybe<&2, Nat>},
11    retained_word_count: {Observation.kept_count(input, request, Core.new(input, fill)) == Some{Shape.count(input)} : Maybe<&2, U32>},
12    retained_value: @+other: U32 -> @inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool} ->
13      {Observation.kept_value(input, request, other, Core.new(input, fill)) == Some{fill} : Maybe<&2, F32>}}
14
15type ReshapeContract<-input: Shape.Shape, -fill: F32, -target: Shape.Shape> is Type:
16  ReshapeContract{
17    outcome: {Observation.reshape_code(input, Shape.dimensions(target), Core.new(input, fill)) == Some{0} : Maybe<&2, U32>},
18    dimensions: {Observation.reshape_dimensions(input, Shape.dimensions(target), Core.new(input, fill)) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>},
19    count: {Observation.reshape_length(input, Shape.dimensions(target), Core.new(input, fill)) == Some{Shape.logical_numel(Shape.dimensions(target))} : Maybe<&2, Nat>},
20    word_count: {Observation.reshape_count(input, Shape.dimensions(target), Core.new(input, fill)) == Some{Shape.count(target)} : Maybe<&2, U32>},
21    value: @+other: U32 -> @inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool} ->
22      {Observation.reshape_value(input, Shape.dimensions(target), other, Core.new(input, fill)) == Some{fill} : Maybe<&2, F32>}}
23
24type ReshapeWrite<-input: Shape.Shape, -fill: F32, -target: Shape.Shape, -index: U32, -value: F32> is Type:
25  ReshapeWrite{
26    written: {Observation.reshape_written(input, index, value, Shape.dimensions(target), index, Core.new(input, fill)) == Some{value} : Maybe<&2, F32>},
27    frame: @+other: U32 -> @inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool} ->
28      @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
29      {Observation.reshape_written(input, index, value, Shape.dimensions(target), other, Core.new(input, fill)) == Some{fill} : Maybe<&2, F32>}}