def IndependentMapping

bendtorch-core@0.1.0.0 · src/tensor/core_LAWS.bend:11

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/projection_LAWS.bend as Projection

11def IndependentMapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, -left: Core.Dynamic, -right: Core.Dynamic,
12  result: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>) -> Type:
13  (inputs, outcome) = result
14  match outcome:
15    case Fail{error}:
16      Unit
17    case Done{output}:
18      @+index: U32 -> @inside: Shape.LT(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) ->
19        {Core.observe_dynamic(output, index) == Projection.specified_expected(operation, left, right, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}