def unset_zeros

bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:113

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation
import bendtorch-core@0.1.0.0/src/tensor/construction_contract_PROOF.bend as ConstructionProof
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation
import bendtorch-core@0.1.0.0/src/autograd/gradient_LAWS.bend as Laws

113def unset_zeros(+shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape>>,
114  -same: {result == Core.new(shape, 0.0) : Result<&2, &1, Core.Error, Core.Tensor<shape>>},
115  -done: Allocation.TensorDone<shape, result>) ->
116  Laws.ZerosModel<shape, Core.construct_values(shape, result)>:
117  match result:
118    case Fail{error}:
119      Laws.ZerosModel{
120        {\{Allocation.TensorDone: tensor => equal => Arith.clash(Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Bool,
121          found => Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, found), Fail{error}, Done{tensor},
122          Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Done{tensor}, Fail{error}, equal)))} :
123          Allocation.TensorDone<shape, Fail{error}> -> Empty}(done)}
124    case Done{tensor}:
125      Laws.ZerosModel{({==}, index => inside => Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, tensor, index),
126        Core.read_value(shape, Core.read_flat(shape, tensor, index)), Some{0.0},
127        Equal.sym(Maybe<&2, F32>, Core.read_value(shape, Core.read_flat(shape, tensor, index)), Core.checked_observe(shape, tensor, index),
128          {\{Core.SourceRead: meaning => meaning} : Core.SourceRead<shape, tensor, index> ->
129            {Core.read_value(shape, Core.read_flat(shape, tensor, index)) == Core.checked_observe(shape, tensor, index) : Maybe<&2, F32>}}(
130            Core.source_read_model(shape, tensor, index))),
131        %Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Done{tensor}, Core.new(shape, 0.0), same) :
132          {Observation.point(shape, index, _) == Some{0.0} : Maybe<&2, F32>}
133        ConstructionProof.point_value(shape, 0.0, index, inside)))}