def attached_length

bendtorch-core@0.1.0.0 · src/tensor/construction_contract_PROOF.bend:237

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
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_PROOF.bend as AllocationProof
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation

237def attached_length(+shape: Shape.Shape, +index: U32, +length: Nat,
238  decision: Shape.BoolCase<Nat.is_eq(length, Shape.elements(shape))>, storage: Storage.Storage,
239  -exact: {Lifecycle.logical_length(storage) == length : Nat}, counted: {length == Shape.elements(shape) : Nat},
240  kept: {Lifecycle.retained_read(Storage.get(storage, index)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
241  {Observation.after_length(shape, index, Core.attach_decided(shape, storage, length, exact, decision)) ==
242    Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
243  match decision:
244    case Shape.BFalse{no}:
245      Empty.absurd({None{} == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
246        Nats.contradiction(Nat.is_eq(length, Shape.elements(shape)), AllocationProof.natural_equal_true(length, Shape.elements(shape), counted), no))
247    case Shape.BTrue{yes}:
248      Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number},
249        Observation.after_length_pair(shape, Core.read_flat(shape,
250          Core.TTensor{storage, Equal.trans(Nat, Lifecycle.logical_length(storage), length, Shape.logical_numel(Shape.dimensions(shape)), exact,
251            Equal.trans(Nat, length, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)),
252              Lifecycle.natural_equal(length, Shape.elements(shape), yes), Shape.elements_exact(shape)))}, index)),
253        Shape.logical_numel(Shape.dimensions(shape)),
254        Equal.trans(Nat,
255          Observation.after_length_pair(shape, Core.read_flat(shape,
256            Core.TTensor{storage, Equal.trans(Nat, Lifecycle.logical_length(storage), length, Shape.logical_numel(Shape.dimensions(shape)), exact,
257              Equal.trans(Nat, length, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)),
258                Lifecycle.natural_equal(length, Shape.elements(shape), yes), Shape.elements_exact(shape)))}, index)),
259          Lifecycle.retained_read(Storage.get(storage, index)), Shape.logical_numel(Shape.dimensions(shape)),
260          length_projection(shape, storage,
261            Equal.trans(Nat, Lifecycle.logical_length(storage), length, Shape.logical_numel(Shape.dimensions(shape)), exact,
262              Equal.trans(Nat, length, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)),
263                Lifecycle.natural_equal(length, Shape.elements(shape), yes), Shape.elements_exact(shape))),
264            index, Storage.get(storage, index), {==}), kept))