def written_projection

bendtorch-core@0.1.0.0 · src/tensor/reshape_contract.bend:142

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/storage/LAWS.bend as StorageLaws
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/transform_observation.bend as Observation

142def written_projection(+input: Shape.Shape, +target: Shape.Shape, -original: Storage.Storage,
143  -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +index: U32, +value: F32, +other: U32, +same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat},
144  pair: Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
145  -equal: {pair == Storage.set(original, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}) ->
146  {Observation.reshape_written_pair(input, Shape.dimensions(target), other, Core.write_result(input, original, valid, index, value, pair, equal)) ==
147    Lifecycle.read_value(Storage.get(StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, pair), other)) : Maybe<&2, F32>}:
148  (storage, result) = pair
149  reshaped_value(input, target, storage,
150    Equal.trans(Nat, Lifecycle.logical_length(storage), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(input)),
151      %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, (storage, result), Storage.set(original, index, value), equal) :
152        {Lifecycle.retained_write(_) == Lifecycle.logical_length(original) : Nat}
153      Lifecycle.set_length(original, index, value), valid),
154    other, same)