~/jendhub

def filled_value

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

import bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend as FromValuesContract
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/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation
import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads

332def filled_value(+shape: Shape.Shape, +values: List<&2, F32>,
333  +counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
334  +index: U32, +inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
335  -fits: {Lifecycle.logical_length(StorageLaws.replay(writes(values, 0n), base(shape, Nil{}))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
336  {Observation.point(shape, index, Done{Core.TTensor{StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), fits}}) ==
337    List.get(&2, F32, values, U32.to_nat(index)) : Maybe<&2, F32>}:
338  Equal.trans(Maybe<&2, F32>,
339    Observation.point(shape, index, Done{Core.TTensor{StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), fits}}),
340    Lifecycle.read_value(Storage.get(StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), index)),
341    List.get(&2, F32, values, U32.to_nat(index)),
342    Core.read_result_value(shape, StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), fits, index,
343      Storage.get(StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), index), {==}),
344    Equal.trans(Maybe<&2, F32>,
345      Lifecycle.read_value(Storage.get(StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), index)),
346      Some{StorageLaws.expected(writes(values, 0n), U32.to_nat(Shape.count(shape)), index, 0.0)},
347      List.get(&2, F32, values, U32.to_nat(index)),
348      Reads.stored_value(StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), index,
349        StorageLaws.expected(writes(values, 0n), U32.to_nat(Shape.count(shape)), index, 0.0),
350        StorageLaws.replay_get(Shape.count(shape), 0.0, writes(values, 0n), index, Conversion.shape_count_within(shape),
351          Reads.word_inside(shape, index, inside))),
352      written_at(values, 0n, Shape.count(shape), index, 0.0, U32.to_nat(index), start_room(shape, values, counted), {==},
353        %Equal.sym(Nat, List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), counted) :
354          {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
355        inside)))

Uses (33)

Used by (1)