def empty_lift

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

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

183# With no output cell the input has none either: both are empty, and the
184# copy hands the source back as it is.
185def empty_lift(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +fill: F32, +ops: List<&2, StorageLaws.Op>,
186  +zero: {U32.to_nat(Shape.count(Layout.output(input, axes, plan))) == 0n : Nat}, -Q: Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic> -> Type,
187  -fo: {Lifecycle.logical_length(Storage.Empty{}) == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat}) ->
188  @-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{})) ->
189    Packed(input, axes, plan, Q, Replayed.storage(input, fill, ops), sf, Storage.Empty{}, fo):
190  Owned.created_lift(Shape.count(input), fill, Conversion.shape_count_within(input),
191    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{})) ->
192      Packed(input, axes, plan, Q, StorageLaws.replay(ops, s), sf, Storage.Empty{}, fo)),
193    nothing => sf => hyp =>
194      Facts.storage_shift(input, StorageLaws.step(StorageLaws.replay(ops, Storage.Empty{}), StorageLaws.First{}), StorageLaws.replay(ops, Storage.Empty{}),
195        Equal.trans(Storage.Storage, StorageLaws.step(StorageLaws.replay(ops, Storage.Empty{}), StorageLaws.First{}), Storage.Empty{}, StorageLaws.replay(ops, Storage.Empty{}),
196          Equal.cong(Storage.Storage, Storage.Storage, st => StorageLaws.step(st, StorageLaws.First{}), StorageLaws.replay(ops, Storage.Empty{}), Storage.Empty{}, Owned.replay_empty(ops)),
197          Equal.sym(Storage.Storage, StorageLaws.replay(ops, Storage.Empty{}), Storage.Empty{}, Owned.replay_empty(ops))),
198        st => k => Packed(input, axes, plan, Q, st, k, Storage.Empty{}, fo),
199        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)),
200          st => ko => Packed(input, axes, plan, Q, StorageLaws.step(StorageLaws.replay(ops, Storage.Empty{}), StorageLaws.First{}), k, st, ko),
201          ko => hyp(k, ko))(fo))(sf),
202    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} ->
203      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{})) ->
204        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),
205      Arith.lt_zero(0n,
206        %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}
207        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)),
208          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)))))