def parallel_success

bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:421

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/storage/main.bend as Storage
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/autograd/reduce.bend as Reduce
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as Laws

421def parallel_success(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan,
422  result: Result<&2, &1, Core.Error, Core.Tensor<target>>, -done: Allocation.TensorDone<target, result>) ->
423  Laws.Success<Reduce.parallel_allocated(Core.Packed{shape, tensor}, target, plan, result)>:
424  match result:
425    case Fail{error}:
426      Laws.Success{Empty.absurd({False{} == True{} : Bool},
427        {\{Allocation.TensorDone: tensor => same => Arith.clash(Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<target>>, Bool,
428          found => Result.is_done(&2, &1, Core.Error, Core.Tensor<target>, found), Fail{error}, Done{tensor},
429          Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<target>>, Done{tensor}, Fail{error}, same)))} :
430          Allocation.TensorDone<target, Fail{error}> -> Empty}(done))}
431    case Done{Core.TTensor{storage, exact}}:
432      match storage:
433        case Storage.Empty{}:
434          Laws.Success{{==}}
435        case Storage.Owned{+depth, +length, array, balanced, valid}:
436          indexed_success(shape, tensor, target, plan, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, depth, length,
437            valid, exact, Shape.index_map(plan))