type BroadcastToContract

bendtorch-core@0.1.0.0 · src/autograd/broadcast_pointwise_LAWS.bend:35

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/autograd/broadcast.bend as Broadcast

35# What broadcast_to promises, stated only through the result: it succeeds
36# with the target's dimensions, every in-bounds output index i holds cell(i),
37# and the returned input still holds every word.
38type BroadcastToContract<-target: Shape.Shape, -input: Shape.Shape, -cell: Nat -> F32, -word: U32 -> F32,
39  -result: Core.Dynamic & Result<&2, &1, Broadcast.Error, Core.Dynamic>> is Type:
40  BroadcastToContract{
41    successful: {succeeded(result) == True{} : Bool},
42    dimensions: {output_dimensions(result) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>},
43    value: @+index: U32 -> @inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool} ->
44      {output_point(result, index) == Some{cell(U32.to_nat(index))} : Maybe<&2, F32>},
45    kept: @+other: U32 -> @inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool} ->
46      {input_point(result, other) == Some{word(other)} : Maybe<&2, F32>}}