type ReshapeContract

bendtorch-core@0.1.0.0 · src/tensor/transform_records.bend:15

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend as Observation

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>}}