def reshape_contract

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads
import bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend as Observation
import bendtorch-core@0.1.0.0/src/tensor/transform_records.bend as Laws

183def reshape_contract(+input: Shape.Shape, +fill: F32, +target: Shape.Shape, same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}) -> Laws.ReshapeContract<input, fill, target>:
184  +same = same
185  Laws.ReshapeContract{
186    reshape_outcome(input, fill, target, same),
187    reshape_dimensions(input, fill, target, same),
188    reshape_length(input, fill, target, same),
189    reshape_count(input, fill, target, same),
190    other => inside => Reads.new_lift(input, fill, result => {Observation.reshape_value(input, Shape.dimensions(target), other, result) == Some{fill} : Maybe<&2, F32>},
191      valid => reshape_value_done(input, fill, target, valid, other, same, inside))}