def fill_model

bendtorch-core@0.1.0.0 · src/tensor/construction_PROOF.bend:477

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/construction_LAWS.bend as Laws

477def fill_model(+values: List<&2, F32>, -shape: Shape.Shape, -original: Core.Tensor<shape>, +cursor: Nat) ->
478  FillOutcome<shape, original, values, cursor, Core.fill_values(values, shape, original, cursor)>:
479  match values:
480    case Nil{}:
481      FillOutcome{(index => offset => at => inside =>
482        Empty.absurd(Core.ObservationChecked(Core.Packed{shape, original}, index) &
483          {Core.checked_observe(shape, original, index) == Laws.list_element(Nil{}, offset) : Maybe<&2, F32>}, lt_zero(offset, inside)),
484        index => earlier => checked => (checked, {==}))}
485    case +value <> +rest:
486      FillOutcome{
487        {\{FillOutcome: meaning => meaning} :
488          FillOutcome<shape, original, value <> rest, cursor,
489            Core.fill_values_decided(shape, cursor, U32.from_nat(cursor), value, original,
490              tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)))> ->
491          FillMeaning(shape, original, value <> rest, cursor, Core.fill_values(value <> rest, shape, original, cursor))}(fill_decision_model(shape, value, rest,
492            cursor, U32.from_nat(cursor), original, Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)),
493            tensor => fill_model(rest, shape, tensor, 1n+cursor)))}