def BinaryWith

bendtorch-core@0.1.0.0 · src/tensor/contracts/binary_LAWS.bend:26

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Contracts

26# What the transport form of binary_replayed asks of P: P holds for both
27# inputs, replayed with any histories that keep their words, next to the
28# output replayed over +0.0 with any history whose words are `cells`.
29def BinaryWith(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
30  +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
31  +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>,
32  -P: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type) -> Type:
33  @+left_kept: List<&2, StorageLaws.Op> ->
34  @left_words: {Contracts.words(left, left_fill, left_kept, Shape.logical_numel(Shape.dimensions(left))) ==
35    Contracts.words(left, left_fill, left_ops, Shape.logical_numel(Shape.dimensions(left))) : List<&2, F32>} ->
36  @-left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_kept)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} ->
37  @+right_kept: List<&2, StorageLaws.Op> ->
38  @right_words: {Contracts.words(right, right_fill, right_kept, Shape.logical_numel(Shape.dimensions(right))) ==
39    Contracts.words(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))) : List<&2, F32>} ->
40  @-right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_kept)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} ->
41  @+output_ops: List<&2, StorageLaws.Op> ->
42  @values: {Contracts.words(Shape.output_shape(plan), 0.0, output_ops, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) ==
43    cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops,
44      Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) : List<&2, F32>} ->
45  @-output_fits: {Lifecycle.logical_length(Replayed.storage(Shape.output_shape(plan), 0.0, output_ops)) ==
46    Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} ->
47    P(((Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_kept), left_fits}},
48      Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_kept), right_fits}}),
49      Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{Replayed.storage(Shape.output_shape(plan), 0.0, output_ops), output_fits}}}))