PermuteValues.run_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 210-238 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=210&end_line=238 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/tensor/permute_build.bend as Build 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 import bendtorch-core@0.1.0.0/src/storage/api.bend as Api def run_lift(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +fill: F32, +ops: List<&2, StorageLaws.Op>, -Q: Core.Tensor & Result<&2, &1, Transforms.Error, Core.Dynamic> -> Type, h: Final(input, axes, plan, fill, ops, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), pair => Q(Transforms.copy_pack(input, axes, plan, pair))), -source_fits: {Lifecycle.logical_length(Replayed.storage(input, fill, ops)) == Shape.logical_numel(Shape.dimensions(input)) : Nat}) -> Q(Transforms.copy_allocated(input, axes, plan, Core.TTensor{Replayed.storage(input, fill, ops), source_fits}, Core.new(Layout.output(input, axes, plan), 0.0))): Replayed.new_lift(Layout.output(input, axes, plan), 0.0, result => Q(Transforms.copy_allocated(input, axes, plan, Core.TTensor{Replayed.storage(input, fill, ops), source_fits}, result)), target_fits => Owned.created_lift(Shape.count(Layout.output(input, axes, plan)), 0.0, Conversion.shape_count_within(Layout.output(input, axes, plan)), s => (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), s)) -> @-fo: {Lifecycle.logical_length(s) == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat} -> Q(Transforms.copy_pack(input, axes, plan, Transforms.built(input, axes, plan, Core.TTensor{Replayed.storage(input, fill, ops), source_fits}, Core.TTensor{s, fo})))), zero => hyp => fo => empty_lift(input, axes, plan, fill, ops, zero, Q, fo)(source_fits, hyp), d => fits => f => hyp => fo => +positive = Arith.and_left(Nat.is_lt(0n, U32.to_nat(Shape.count(Layout.output(input, axes, plan)))), Nat.is_le(U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Model.capacity(d)), Arith.and_right(Nat.is_le(d, 20n), Bool.and(Nat.is_lt(0n, U32.to_nat(Shape.count(Layout.output(input, axes, plan)))), Nat.is_le(U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Model.capacity(d))), fits)) Facts.input_lift(input, fill, ops, %count_same(input, axes, plan) : {Nat.is_lt(0n, _) == True{} : Bool} positive, st => (@-sf: {Lifecycle.logical_length(st) == Shape.logical_numel(Shape.dimensions(input)) : Nat} -> Kept(input, axes, plan, Q, st, StorageLaws.replay(IndexMap.writes(~Request, ~source_of, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Request{input, axes}, input, fill, ops), Storage.Owned{d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f})) -> Q(Transforms.copy_pack(input, axes, plan, Transforms.built_owned(input, axes, plan, d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), f, fo, Core.TTensor{st, sf})))), ds => fits_s => b => f2 => sf => hyp2 => cloned_lift(input, axes, plan, fill, ops, d, f, fo, ds, b, f2, Array.clone(F32, Api.arr(Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)), {==}, sf, Q, kf => 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.Owned{d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), Storage.Owned{d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Build.build(d, Build.Request{input, axes}, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)), Build.balanced(d, Build.Request{input, axes}, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)), f}, made(input, axes, plan, fill, ops, d, fits, f, ds, fits_s), st => ko => Packed(input, axes, plan, Q, StorageLaws.step(Storage.Owned{ds, U32.to_nat(Shape.count(input)), Api.arr(Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill), b, f2}, StorageLaws.First{}), kf, st, ko), ko => hyp2(kf, ko))(fo)))(source_fits, hyp))( kf => ko => Facts.storage_shift(input, kept_source(input, fill, ops), StorageLaws.step(Replayed.storage(input, fill, ops), StorageLaws.First{}), Replayed.replay_snoc(ops, StorageLaws.First{}, input, fill), st => k => Packed(input, axes, plan, Q, st, k, StorageLaws.replay(IndexMap.writes(~Request, ~source_of, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Request{input, axes}, input, fill, ops), StorageLaws.created(Shape.count(Layout.output(input, axes, plan)), 0.0)), ko), k => h(k, ko))(kf), target_fits)) Uses (61): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.clone 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=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=created 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/api.bend&name=Effect https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=arr 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/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=norm https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend&name=input_lift 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=new_lift https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=replay_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/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/core.bend&name=new 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_build.bend&name=Request https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=balanced https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=build https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=Final 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=cloned_lift 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=empty_lift https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=kept_source https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=made 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/transforms.bend&name=built https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=built_owned https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=copy_allocated https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=copy_pack https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=shape_count_within