FoldProof.pair_step_lift: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/contracts/fold_proof.bend as FoldProof Lines 216-242 of bendtorch-core@0.1.0.0/src/tensor/contracts/fold_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/fold_proof.bend&start_line=216&end_line=242 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/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/fold.bend as Fold def pair_step_lift(~O: Data, ~g: O -> F32 -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat, +rest: Nat, +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +cursor: Nat, left_inside: {Nat.is_lt(U32.to_nat(U32.from_nat(ia(plan, cursor))), Shape.logical_numel(Shape.dimensions(left))) == True{} : Bool}, right_inside: {Nat.is_lt(U32.to_nat(U32.from_nat(ib(plan, cursor))), Shape.logical_numel(Shape.dimensions(right))) == True{} : Bool}, -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, F32> -> Type, next: PairStart(~O, ~g, ~P, ~ia, ~ib, rest, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+cursor, Q)) -> PairStart(~O, ~g, ~P, ~ia, ~ib, 1n+rest, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, cursor, Q): +left_seen = List.append(&2, StorageLaws.Op, left_ops, Pointwise.reads(~P, ~ia, plan, cursor)) +right_seen = List.append(&2, StorageLaws.Op, right_ops, Pointwise.reads(~P, ~ib, plan, cursor)) +left_index = U32.from_nat(ia(plan, cursor)) +right_index = U32.from_nat(ib(plan, cursor)) +before = Fold.pair_total(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, cursor) +x = Replayed.value(left, left_fill, left_seen, left_index) left_fits => right_fits => Replayed.read_lift(left, left_fill, left_seen, left_fits, left_index, left_inside, pair => Q(Fold.pair_left(~O, ~g, operation, right_index, left => right => value => Fold.pair_loop(~O, ~g, ~P, ~ia, ~ib, rest, operation, plan, 1n+cursor, left, right, value), Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_seen), right_fits}}, before, Core.read_dynamic_result(left, pair))), left_after => Replayed.read_lift(right, right_fill, right_seen, right_fits, right_index, right_inside, pair => Q(Fold.pair_right(~O, ~g, operation, left => right => value => Fold.pair_loop(~O, ~g, ~P, ~ia, ~ib, rest, operation, plan, 1n+cursor, left, right, value), Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, Replayed.snoc(left_seen, StorageLaws.Read{left_index})), left_after}}, before, x, Core.read_dynamic_result(right, pair))), right_after => pair_shift(~O, ~g, ~P, ~ia, ~ib, rest, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, cursor, Q, next)(left_after, right_after))) Uses (29): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=Op https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/fold.bend&name=pair_left https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/fold.bend&name=pair_loop https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/fold.bend&name=pair_right https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/fold.bend&name=pair_total https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/fold_proof.bend&name=PairStart https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/fold_proof.bend&name=pair_shift https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend&name=reads https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=read_lift https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=snoc https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=storage https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=value https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Error https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=read_dynamic_result