def taken_owned

bendtorch-core@0.1.0.0 · src/tensor/elementwise_parallel_proof.bend:290

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
import bendtorch-core@0.1.0.0/src/storage/certificates.bend as Certificates
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/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality

290def taken_owned(+shape: Shape.Shape, +depth: Nat, +length: Nat, -array: Array<F32>, pair: Array<F32> & Array<F32>,
291  -same: {pair == Array.clone(F32, array) : Array<F32> & Array<F32>}, -balanced: Model.Balanced(F32, depth, array),
292  -valid: {Storage.bounds(depth, length) == True{} : Bool}, -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
293  Taken<Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}},
294    Elementwise.take_owned(shape, depth, length, array, pair, same, balanced, valid, exact)>:
295  (kept, copy) = pair
296  -kept_same = {\{Fact: p => p} : Fact<({Pair.fst(Array<F32>, Array<F32>, (kept, copy)) == array : Array<F32>})> -> {kept == array : Array<F32>}}(
297    clone_first(depth, array, array, (kept, copy), same, {==}, balanced))
298  -copy_same = {\{Fact: p => p} : Fact<({Pair.snd(Array<F32>, Array<F32>, (kept, copy)) == array : Array<F32>})> -> {copy == array : Array<F32>}}(
299    clone_second(depth, array, array, (kept, copy), same, {==}, balanced))
300  Taken{depth,
301    {\{Fact: p => p} : Fact<(Model.Balanced(F32, depth, copy))> -> Model.Balanced(F32, depth, copy)}(transport_balanced(depth, copy, array, copy_same, balanced)),
302    index => inside => Equal.trans(Maybe<&2, F32>, Model.observe(F32, depth, copy, Refinement.route(depth, index)),
303      Model.observe(F32, depth, array, Refinement.route(depth, index)),
304      Lifecycle.observe_allowed(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length)),
305      Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, depth, a, Refinement.route(depth, index)), copy, array, copy_same),
306      Equal.sym(Maybe<&2, F32>, Lifecycle.observe_allowed(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length)),
307        Model.observe(F32, depth, array, Refinement.route(depth, index)),
308        observe_allowed_equal(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length),
309          %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
310          inside,
311          Equal.sym(Bool, True{}, Storage.index_matches(depth, length, index),
312            Route.index_complete(depth, length, index, valid,
313              %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
314              inside))))),
315    property => Equal.trans(Totality.Inspection,
316      Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, kept,
317        Certificates.clone_first(F32, depth, array, (kept, copy), same, balanced), valid}, exact}}),
318      owned_inspect(shape, depth, length, property, kept),
319      Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}),
320      owned_view(shape, depth, length, property, kept, Certificates.clone_first(F32, depth, array, (kept, copy), same, balanced), valid, exact),
321      Equal.trans(Totality.Inspection, owned_inspect(shape, depth, length, property, kept), owned_inspect(shape, depth, length, property, array),
322        Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}),
323        Equal.cong(Array<F32>, Totality.Inspection, a => owned_inspect(shape, depth, length, property, a), kept, array, kept_same),
324        Equal.sym(Totality.Inspection, Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}),
325          owned_inspect(shape, depth, length, property, array), owned_view(shape, depth, length, property, array, balanced, valid, exact))))}