law copy_value_mapping

bendtorch-core@0.1.0.0 · src/tensor/transform_LAWS.bend:152

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model

152law copy_value_mapping:
153  for -input: Shape.Shape
154  for -axes: List<&2, U32>
155  for +plan: Layout.Plan<input, axes>
156  for +depth: Nat
157  for +length: Nat
158  for array: Array<F32>
159  for +index: U32
160  for source: Core.Tensor<input>
161  for +value: F32
162  for balanced: Model.Balanced(F32, depth, array)
163  for -valid: {Storage.bounds(depth, length) == True{} : Bool}
164  for -exact: {length == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat}
165  for allowed: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}
166  for matched: {Storage.index_matches(depth, length, index) == True{} : Bool}
167  {Transforms.copy_observe(input, axes, plan,
168    Transforms.copy_read(input, axes, plan, index, source => target => (source, Done{target}),
169      Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, (source, Done{value})), index) == Some{value} : Maybe<&2, F32>}