def cloned_lift

bendtorch-core@0.1.0.0 · src/tensor/permute_values.bend:147

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/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/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/api.bend as Api

147def cloned_lift(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +fill: F32, +ops: List<&2, StorageLaws.Op>,
148  +d: Nat, -f: {Storage.bounds(d, U32.to_nat(Shape.count(Layout.output(input, axes, plan)))) == True{} : Bool}, -fo: {U32.to_nat(Shape.count(Layout.output(input, axes, plan))) == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat},
149  +ds: Nat, -b: Model.Balanced(F32, ds, Api.arr(Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)), -f2: {Storage.bounds(ds, U32.to_nat(Shape.count(input))) == True{} : Bool},
150  pair: Array<F32> & Array<F32>, -same: {pair == Array.clone(F32, Api.arr(Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)) : Array<F32> & Array<F32>},
151  -sf: {Lifecycle.logical_length(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}) == Shape.logical_numel(Shape.dimensions(input)) : Nat},
152  -Q: Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic> -> Type,
153  hyp: @-kf: {Lifecycle.logical_length(StorageLaws.owner(Storage.Storage, Storage.finish_clone(ds, U32.to_nat(Shape.count(input)), Api.arr(Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill), pair, same, b, f2))) == Shape.logical_numel(Shape.dimensions(input)) : Nat} ->
154    Packed(input, axes, plan, Q, StorageLaws.owner(Storage.Storage, Storage.finish_clone(ds, U32.to_nat(Shape.count(input)), Api.arr(Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill), pair, same, b, f2)), kf,
155      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))), Pair.snd(Array<F32>, Array<F32>, pair)),
156        Build.balanced(d, Build.Request{input, axes}, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Pair.snd(Array<F32>, Array<F32>, pair)), f}, fo)) ->
157  Q(Transforms.copy_pack(input, axes, plan, Transforms.built_cloned(input, axes, plan, d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), f, fo, ds, U32.to_nat(Shape.count(input)), Api.arr(Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill), pair, same, b, f2, sf))):
158  (kept, copy) = pair
159  hyp(sf)