type SoleContract

bendtorch-core@0.1.0.0 · src/autograd/tensor_backward_LAWS.bend:141

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward

141# What a VJP that sends one contribution promises: it goes to node a, it has
142# the target's dimensions, and every in-bounds index i holds cell(i).
143type SoleContract<-a: Nat, -target: Shape.Shape, -cell: Nat -> F32, -pass: Backward.Pass> is Type:
144  SoleContract{
145    target_id: {sole_target(sole(pass)) == Some{a} : Maybe<&2, Nat>},
146    dimensions: {sole_dimensions(sole(pass)) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>},
147    value: @+index: U32 -> @inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool} ->
148      {sole_point(sole(pass), index) == Some{cell(U32.to_nat(index))} : Maybe<&2, F32>}}