def zeroed_retains

bendtorch-core@0.1.0.0 · src/autograd/broadcast_PROOF.bend:38

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/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwiseProof
import bendtorch-core@0.1.0.0/src/autograd/broadcast.bend as Broadcast
import bendtorch-core@0.1.0.0/src/autograd/broadcast_LAWS.bend as Laws

38def zeroed_retains(input: Core.Dynamic, +target: Shape.Shape, +plan: Shape.BroadcastPlan,
39  result: Result<&2, &1, Core.Error, Core.Tensor<target>>) -> Laws.Retained<input, Broadcast.zeroed(input, target, plan, result)>:
40  match result:
41    case Fail{error}:
42      Laws.Retained{property => {==}}
43    case Done{zeros}:
44      finish_retains(input, Core.Packed{target, zeros}, Elementwise.parallel_allocated(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, Core.new(Shape.output_shape(plan), 0.0)),
45        ElementwiseProof.parallel_allocated_retains(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, Core.new(Shape.output_shape(plan), 0.0)))