def allocated_replayed

bendtorch-core@0.1.0.0 · src/tensor/contracts/binary_proofs.bend:438
import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend as BinaryProofs
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
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/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend as Pointwise
import bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast.bend as Broadcast
import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Contracts
import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend as Owned
import bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend as Facts

438# The parallel build on two replayed inputs into an output that `Core.new`
439# allocates: binary_replayed below the planner, which broadcast_to shares.
440def allocated_replayed(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, -P: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type,
441  h: Laws.BinaryWith(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, P)) ->
442  @-lfits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @-rfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} ->
443  P(Elementwise.parallel_allocated(operation, plan, Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}), Core.new(Shape.output_shape(plan), 0.0))):
444  lfits => rfits =>
445    Replayed.new_lift(Shape.output_shape(plan), 0.0, result => P(Elementwise.parallel_allocated(operation, plan, Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}), result)),
446      fo => Owned.created_lift(Shape.count(Shape.output_shape(plan)), 0.0, Conversion.shape_count_within(Shape.output_shape(plan)),
447        s => ((@+left_kept: List<&2, StorageLaws.Op> -> @left_words: {Contracts.words(left, left_fill, left_kept, Shape.logical_numel(Shape.dimensions(left))) == Contracts.words(left, left_fill, left_ops, Shape.logical_numel(Shape.dimensions(left))) : List<&2, F32>} -> @-left_kfits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_kept)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @+right_kept: List<&2, StorageLaws.Op> -> @right_words: {Contracts.words(right, right_fill, right_kept, Shape.logical_numel(Shape.dimensions(right))) == Contracts.words(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))) : List<&2, F32>} -> @-right_kfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_kept)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> @-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), s)) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_kept), left_kfits}}, Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_kept), right_kfits}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), s), ko}}}))) -> @-fo: {Lifecycle.logical_length(s) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} ->
448          P(Elementwise.parallel_allocated(operation, plan, Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}), Done{Core.TTensor{s, fo}}))),
449        zero => ho => fo =>
450          Facts.storage_shift(Shape.output_shape(plan), StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Empty{}), Storage.Empty{}, Owned.replay_empty(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops)),
451            st => k => P(((Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits})), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{st, k}}})),
452            ho(left_ops, {==}, lfits, right_ops, {==}, rfits))(fo),
453        d => fits => f => owned_case(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, planned, lfits, rfits, P, d, fits, f))(
454        left_kept => left_words => left_kfits => right_kept => right_words => right_kfits => ko =>
455          h(left_kept, left_words, left_kfits, right_kept, right_words, right_kfits, Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops),
456            words_cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), Conversion.le_reflexive(Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))))), ko), fo))
def allocated_replayed

Uses (40)

Used by (2)
