~/jendhub

def attach_length

bendtorch-core@0.1.0.0 · src/tensor/allocation_PROOF.bend:67

import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationPROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
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/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation

67def attach_length(+shape: Shape.Shape, storage: Storage.Storage, exact: {Lifecycle.logical_length(storage) == Shape.elements(shape) : Nat}) ->
68  {Allocation.tensor_length(shape, Core.attach(shape, storage)) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
69  match storage:
70    case Storage.Empty{}:
71      attach_decided_length(shape, 0n, Shape.bool_case(Nat.is_eq(0n, Shape.elements(shape))), Storage.Empty{}, {==}, natural_equal_true(0n, Shape.elements(shape), exact))
72    case Storage.Owned{+depth, +length, array, balanced, valid}:
73      attach_decided_length(shape, length, Shape.bool_case(Nat.is_eq(length, Shape.elements(shape))), Storage.Owned{depth, length, array, balanced, valid}, {==}, natural_equal_true(length, Shape.elements(shape), exact))

Uses (14)

Used by (1)