PermuteValues.empty_lift: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/permute_values.bend as PermuteValues Lines 183-208 of bendtorch-core@0.1.0.0/src/tensor/permute_values.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&start_line=183&end_line=208 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/storage/arith.bend as Arith 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/layout.bend as Layout import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms 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/index_map.bend as IndexMap import bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend as Facts import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend as Owned import bendtorch-core@0.1.0.0/src/storage/model.bend as Model import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore # With no output cell the input has none either: both are empty, and the # copy hands the source back as it is. def empty_lift(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +fill: F32, +ops: List<&2, StorageLaws.Op>, +zero: {U32.to_nat(Shape.count(Layout.output(input, axes, plan))) == 0n : Nat}, -Q: Core.Tensor & Result<&2, &1, Transforms.Error, Core.Dynamic> -> Type, -fo: {Lifecycle.logical_length(Storage.Empty{}) == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat}) -> @-sf: {Lifecycle.logical_length(Replayed.storage(input, fill, ops)) == Shape.logical_numel(Shape.dimensions(input)) : Nat} -> Kept(input, axes, plan, Q, Replayed.storage(input, fill, ops), StorageLaws.replay(IndexMap.writes(~Request, ~source_of, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Request{input, axes}, input, fill, ops), Storage.Empty{})) -> Packed(input, axes, plan, Q, Replayed.storage(input, fill, ops), sf, Storage.Empty{}, fo): Owned.created_lift(Shape.count(input), fill, Conversion.shape_count_within(input), s => (@-sf: {Lifecycle.logical_length(StorageLaws.replay(ops, s)) == Shape.logical_numel(Shape.dimensions(input)) : Nat} -> Kept(input, axes, plan, Q, StorageLaws.replay(ops, s), StorageLaws.replay(IndexMap.writes(~Request, ~source_of, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Request{input, axes}, input, fill, ops), Storage.Empty{})) -> Packed(input, axes, plan, Q, StorageLaws.replay(ops, s), sf, Storage.Empty{}, fo)), nothing => sf => hyp => Facts.storage_shift(input, StorageLaws.step(StorageLaws.replay(ops, Storage.Empty{}), StorageLaws.First{}), StorageLaws.replay(ops, Storage.Empty{}), Equal.trans(Storage.Storage, StorageLaws.step(StorageLaws.replay(ops, Storage.Empty{}), StorageLaws.First{}), Storage.Empty{}, StorageLaws.replay(ops, Storage.Empty{}), Equal.cong(Storage.Storage, Storage.Storage, st => StorageLaws.step(st, StorageLaws.First{}), StorageLaws.replay(ops, Storage.Empty{}), Storage.Empty{}, Owned.replay_empty(ops)), Equal.sym(Storage.Storage, StorageLaws.replay(ops, Storage.Empty{}), Storage.Empty{}, Owned.replay_empty(ops))), st => k => Packed(input, axes, plan, Q, st, k, Storage.Empty{}, fo), k => Facts.storage_shift(Layout.output(input, axes, plan), StorageLaws.replay(IndexMap.writes(~Request, ~source_of, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Request{input, axes}, input, fill, ops), Storage.Empty{}), Storage.Empty{}, Owned.replay_empty(IndexMap.writes(~Request, ~source_of, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Request{input, axes}, input, fill, ops)), st => ko => Packed(input, axes, plan, Q, StorageLaws.step(StorageLaws.replay(ops, Storage.Empty{}), StorageLaws.First{}), k, st, ko), ko => hyp(k, ko))(fo))(sf), d => fits => f => Empty.absurd(@-sf: {Lifecycle.logical_length(StorageLaws.replay(ops, Storage.Owned{d, U32.to_nat(Shape.count(input)), Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f})) == Shape.logical_numel(Shape.dimensions(input)) : Nat} -> Kept(input, axes, plan, Q, StorageLaws.replay(ops, Storage.Owned{d, U32.to_nat(Shape.count(input)), Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f}), StorageLaws.replay(IndexMap.writes(~Request, ~source_of, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Request{input, axes}, input, fill, ops), Storage.Empty{})) -> Packed(input, axes, plan, Q, StorageLaws.replay(ops, Storage.Owned{d, U32.to_nat(Shape.count(input)), Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f}), sf, Storage.Empty{}, fo), Arith.lt_zero(0n, %Equal.trans(Nat, U32.to_nat(Shape.count(input)), U32.to_nat(Shape.count(Layout.output(input, axes, plan))), 0n, Equal.sym(Nat, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), U32.to_nat(Shape.count(input)), count_same(input, axes, plan)), zero) : {Nat.is_lt(0n, _) == True{} : Bool} Arith.and_left(Nat.is_lt(0n, U32.to_nat(Shape.count(input))), Nat.is_le(U32.to_nat(Shape.count(input)), Model.capacity(d)), Arith.and_right(Nat.is_le(d, 20n), Bool.and(Nat.is_lt(0n, U32.to_nat(Shape.count(input))), Nat.is_le(U32.to_nat(Shape.count(input)), Model.capacity(d))), fits))))) Uses (46): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.new https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans 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=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le 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 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=count 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/storage/LAWS.bend&name=replay https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=step https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_left https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_right https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=lt_zero https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/array.bend&name=new_balanced https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=Storage https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=capacity https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend&name=created_lift https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend&name=replay_empty https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend&name=storage_shift 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/core.bend&name=Dynamic 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/index_map.bend&name=writes https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=Plan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=output https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=logical_length https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=Kept https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=Packed https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=Request https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=count_same https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=source_of https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=Error https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=shape_count_within