def owned_view

bendtorch-core@0.1.0.0 · src/tensor/elementwise_parallel_proof.bend:265

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality

265def owned_view(+shape: Shape.Shape, +depth: Nat, +length: Nat, property: Totality.Property, -array: Array<F32>,
266  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
267  -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
268  {Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}) ==
269    owned_inspect(shape, depth, length, property, array) : Totality.Inspection}:
270  match property:
271    case Totality.Dimensions{}:
272      {==}
273    case Totality.Checked{+index}:
274      {==}
275    case Totality.Raw{+index}:
276      {==}