def found_value

bendtorch-core@0.1.0.0 · src/tensor/permute_values.bend:273

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend as FromValues
import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/index_map.bend as IndexMap
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Values
import bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend as PermuteProof

273def found_value(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +values: List<&2, F32>,
274  +counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(input)) : Nat},
275  +index: U32, +mapping: Layout.Mapping<input, axes, plan, index>) ->
276  {Some{Replayed.value(input, 0.0, FromValues.writes(values, 0n), U32.from_nat(source_of(Request{input, axes}, U32.to_nat(index))))} ==
277    Values.listed(values, Values.permute_source(input, axes, index)) : Maybe<&2, F32>}:
278  +found = Layout.source_index(input, axes, plan, index, mapping)
279  +history = FromValues.writes(values, 0n)
280  %Equal.sym(U32, U32.from_nat(U32.to_nat(index)), index, Conversion.word_natural_exact(index)) :
281    {Some{Replayed.value(input, 0.0, history, U32.from_nat(U32.to_nat(Maybe.default(&2, U32, Values.permute_source(input, axes, _), 0))))} ==
282      Values.listed(values, Values.permute_source(input, axes, index)) : Maybe<&2, F32>}
283  %PermuteProof.mapped_index(input, axes, plan, index, mapping) :
284    {Some{Replayed.value(input, 0.0, history, _)} == Values.listed(values, Values.permute_source(input, axes, index)) : Maybe<&2, F32>}
285  %PermuteProof.reference(input, axes, plan, index, mapping) :
286    {Some{Replayed.value(input, 0.0, history, found)} == Values.listed(values, _) : Maybe<&2, F32>}
287  IndexMap.stored_at(input, values, counted, found, PermuteProof.mapped_bound(input, axes, plan, index, mapping))