def written_model

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

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/core_PROOF.bend as CoreProof

403def written_model(-shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, +cursor: Nat,
404  +index: U32, +value: F32, -unit: Unit, -converted: {U32.to_nat(index) == cursor : Nat},
405  -meaning: Core.CheckedUpdateMeaning(shape, original, index, value, (tensor, Done{unit}))) -> Written<shape, original, tensor, cursor, value>:
406  Written{
407    other => at =>
408      {\{Tuple: checked => rest =>
409        {\{Tuple: observed => frame => written_point(shape, tensor, cursor, index, value, converted, checked, observed, other, at)} :
410          ({Core.checked_observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>} &
411            (@+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{shape, original}, other) ->
412              @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
413                Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
414                  {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})) ->
415          (Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
416            {Core.checked_observe(shape, tensor, other) == Some{value} : Maybe<&2, F32>})}(rest)
417      } : Core.CheckedUpdateMeaning(shape, original, index, value, (tensor, Done{unit})) ->
418        (Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
419          {Core.checked_observe(shape, tensor, other) == Some{value} : Maybe<&2, F32>})}(meaning),
420    other => earlier => before_checked =>
421      {\{Tuple: checked => rest =>
422        {\{Tuple: observed => frame => frame(other)(before_checked)(
423          %Equal.sym(Nat, U32.to_nat(index), cursor, converted) : {Nat.is_eq(_, U32.to_nat(other)) == False{} : Bool}
424          CoreProof.lt_big_small_different(U32.to_nat(other), cursor, earlier))} :
425          ({Core.checked_observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>} &
426            (@+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{shape, original}, other) ->
427              @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
428                Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
429                  {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})) ->
430          (Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
431            {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})}(rest)
432      } : Core.CheckedUpdateMeaning(shape, original, index, value, (tensor, Done{unit})) ->
433        (Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
434          {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})}(meaning)}