def from_values_contract

bendtorch-core@0.1.0.0 · src/tensor/from_values_contract.bend:357

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
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/allocation_spec.bend as Allocation
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation
import bendtorch-core@0.1.0.0/src/tensor/from_values_records.bend as Laws

357def from_values_contract(+shape: Shape.Shape, +values: List<&2, F32>,
358  counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
359  Laws.FromValuesContract<shape, values>:
360  +counted = counted
361  Laws.FromValuesContract{
362    from_values_lift(shape, values, counted,
363      result => {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, result) == True{} : Bool}, fits => {==}),
364    from_values_lift(shape, values, counted,
365      result => {Observation.dimensions(shape, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}, fits => {==}),
366    from_values_lift(shape, values, counted,
367      result => {Allocation.tensor_length(shape, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
368      fits => Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number},
369        Lifecycle.logical_length(StorageLaws.replay(writes(values, 0n), base(shape, Nil{}))), Shape.logical_numel(Shape.dimensions(shape)),
370        filled_length(shape, values))),
371    from_values_lift(shape, values, counted,
372      result => {Observation.count(shape, result) == Some{Shape.count(shape)} : Maybe<&2, U32>}, fits => {==}),
373    index => inside =>
374      +inside = inside
375      from_values_lift(shape, values, counted,
376        result => {Observation.point(shape, index, result) == List.get(&2, F32, values, U32.to_nat(index)) : Maybe<&2, F32>},
377        fits => filled_value(shape, values, counted, index, inside, fits))}