def fill_advance

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

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

278def fill_advance(-shape: Shape.Shape, +value: F32, +rest: List<&2, F32>, +cursor: Nat,
279  -original: Core.Tensor<shape>, -written: Core.Tensor<shape>,
280  result: Result<&2, &1, Core.Error, Core.Tensor<shape>>, -point: Written<shape, original, written, cursor, value>,
281  -next: FillMeaning(shape, written, rest, 1n+cursor, result)) -> FillOutcome<shape, original, value <> rest, cursor, result>:
282  match result:
283    case Fail{error}:
284      FillOutcome{Unit{}}
285    case Done{tensor}:
286      FillOutcome{
287        (index => offset => at => inside =>
288          {\{Written: observed => before =>
289            {\{Tuple: mapping => after => fill_elements_advance(shape, value, rest, cursor, written, tensor,
290              observed, mapping, after, index, offset, at, inside)} :
291              (FillElements(shape, rest, 1n+cursor, tensor) & FillFrame(shape, written, 1n+cursor, tensor)) ->
292                (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
293                  {Core.checked_observe(shape, tensor, index) == Laws.list_element(value <> rest, offset) : Maybe<&2, F32>})}(next)
294          } : Written<shape, original, written, cursor, value> ->
295            (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
296              {Core.checked_observe(shape, tensor, index) == Laws.list_element(value <> rest, offset) : Maybe<&2, F32>})}(point),
297          index => earlier => checked =>
298            {\{Written: observed => before =>
299              {\{Tuple: mapping => after => fill_frame_advance(shape, original, written, tensor, cursor, before, after, index, earlier, checked)} :
300                (FillElements(shape, rest, 1n+cursor, tensor) & FillFrame(shape, written, 1n+cursor, tensor)) ->
301                  (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
302                    {Core.checked_observe(shape, tensor, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>})}(next)
303            } : Written<shape, original, written, cursor, value> ->
304              (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
305                {Core.checked_observe(shape, tensor, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>})}(point))}