def taken

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

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/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

327def taken(dynamic: Core.Dynamic) -> Taken<dynamic, Elementwise.take(dynamic)>:
328  Core.Packed{+shape, Core.TTensor{storage, exact}} = dynamic
329  match storage:
330    case Storage.Empty{}:
331      Taken{0n, Unit{},
332        index => inside => Empty.absurd({Model.observe(F32, 0n, Array.new(F32, 0n, 0.0), Refinement.route(0n, index)) ==
333          Core.checked_observe_dynamic(Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}}, index) : Maybe<&2, F32>},
334          Arith.lt_zero(U32.to_nat(index),
335            %Equal.sym(Nat, 0n, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
336            inside)),
337        property => {==}}
338    case Storage.Owned{+depth, +length, array, balanced, valid}:
339      taken_owned(shape, depth, length, array, Array.clone(F32, array), {==}, balanced, valid, exact)