def cloned_meaning

bendtorch-core@0.1.0.0 · src/tensor/permute_build_proof.bend:433

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Values
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/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
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/transforms.bend as Transforms

433# The copy from an owned source, whatever the clone hands out.
434def cloned_meaning(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +d: Nat, +n: Nat,
435  -valid: {Storage.bounds(d, n) == True{} : Bool}, -exact: {n == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat},
436  +ds: Nat, +ns: Nat, -a: Array<F32>, pair: Array<F32> & Array<F32>, -same: {pair == Array.clone(F32, a) : Array<F32> & Array<F32>},
437  -b: Model.Balanced(F32, ds, a), -ok: {Storage.bounds(ds, ns) == True{} : Bool},
438  -fits: {Lifecycle.logical_length(Storage.Owned{ds, ns, a, b, ok}) == Shape.logical_numel(Shape.dimensions(input)) : Nat}) ->
439  Transforms.LoopMeaning(input, axes, plan, Core.TTensor{Storage.Owned{ds, ns, a, b, ok}, fits}, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))),
440    Transforms.built_cloned(input, axes, plan, d, n, valid, exact, ds, ns, a, pair, same, b, ok, fits)):
441  (kept, copy) = pair
442  -kept_a = {\{Fact: q => q} : Fact<{Pair.fst(Array<F32>, Array<F32>, (kept, copy)) == a : Array<F32>}> -> {kept == a : Array<F32>}}(
443    clone_first(ds, a, (kept, copy), same, b))
444  -copy_a = {\{Fact: q => q} : Fact<{Pair.snd(Array<F32>, Array<F32>, (kept, copy)) == a : Array<F32>}> -> {copy == a : Array<F32>}}(
445    clone_second(ds, a, (kept, copy), same, b))
446  -bc = {\{Fact: q => q} : Fact<Model.Balanced(F32, ds, copy)> -> Model.Balanced(F32, ds, copy)}(balanced_along(ds, copy, a, copy_a, b))
447  Transforms.Prefix{
448    other => Equal.cong(Array<F32>, Maybe<&2, F32>, x => Lifecycle.observe_allowed(ds, ns, x, other, Nat.is_lt(U32.to_nat(other), ns)), kept, a, kept_a),
449    other => earlier => word_below(Layout.output(input, axes, plan), other, earlier),
450    other => earlier => Route.index_matched(d, n, U32.from_nat(other), valid, length_below(Layout.output(input, axes, plan), n, exact, other, earlier)),
451    other => earlier => Equal.trans(Maybe<&2, F32>,
452      Lifecycle.checked_observe_array(d, n, Build.build(d, Build.Request{input, axes}, n, copy), U32.from_nat(other)),
453      Some{Refinement.second(F32, Array.get(F32, a, U32.from_nat(Values.permute_source_index(input, axes, other))))},
454      Transforms.expected_output(input, axes, plan, Core.TTensor{Storage.Owned{ds, ns, a, b, ok}, fits}, U32.from_nat(other)),
455      Equal.trans(Maybe<&2, F32>,
456        Lifecycle.checked_observe_array(d, n, Build.build(d, Build.Request{input, axes}, n, copy), U32.from_nat(other)),
457        Some{Refinement.second(F32, Array.get(F32, copy, U32.from_nat(Values.permute_source_index(input, axes, other))))}, Some{Refinement.second(F32, Array.get(F32, a, U32.from_nat(Values.permute_source_index(input, axes, other))))},
458        {\{Fact: q => q} : Fact<{Lifecycle.checked_observe_array(d, n, Build.build(d, Build.Request{input, axes}, n, copy), U32.from_nat(other)) ==
459          Some{Refinement.second(F32, Array.get(F32, copy, U32.from_nat(Values.permute_source_index(input, axes, other))))} : Maybe<&2, F32>}> ->
460          {Lifecycle.checked_observe_array(d, n, Build.build(d, Build.Request{input, axes}, n, copy), U32.from_nat(other)) ==
461            Some{Refinement.second(F32, Array.get(F32, copy, U32.from_nat(Values.permute_source_index(input, axes, other))))} : Maybe<&2, F32>}}(
462          output_word(input, axes, plan, d, n, valid, exact, ds, copy, bc, other, earlier)),
463        Equal.cong(Array<F32>, Maybe<&2, F32>, x => Some{Refinement.second(F32, Array.get(F32, x, U32.from_nat(Values.permute_source_index(input, axes, other))))}, copy, a, copy_a)),
464      Equal.sym(Maybe<&2, F32>, Transforms.expected_output(input, axes, plan, Core.TTensor{Storage.Owned{ds, ns, a, b, ok}, fits}, U32.from_nat(other)),
465        Some{Refinement.second(F32, Array.get(F32, a, U32.from_nat(Values.permute_source_index(input, axes, other))))},
466        {\{Fact: q => q} : Fact<{Transforms.expected_mapped(input, axes, plan, U32.from_nat(other), Core.TTensor{Storage.Owned{ds, ns, a, b, ok}, fits},
467          Layout.map_index(input, axes, plan, U32.from_nat(other))) == Some{Refinement.second(F32, Array.get(F32, a, U32.from_nat(Values.permute_source_index(input, axes, other))))} : Maybe<&2, F32>}> ->
468          {Transforms.expected_mapped(input, axes, plan, U32.from_nat(other), Core.TTensor{Storage.Owned{ds, ns, a, b, ok}, fits},
469            Layout.map_index(input, axes, plan, U32.from_nat(other))) == Some{Refinement.second(F32, Array.get(F32, a, U32.from_nat(Values.permute_source_index(input, axes, other))))} : Maybe<&2, F32>}}(
470          expected_word(input, axes, plan, other, ds, ns, a, b, ok, fits, fits, Layout.map_index(input, axes, plan, U32.from_nat(other)),
471            mapping_done(input, axes, plan, U32.from_nat(other),
472              %Equal.sym(Nat, U32.to_nat(U32.from_nat(other)), other, word_below(Layout.output(input, axes, plan), other, earlier)) : {Nat.is_lt(_, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))) == True{} : Bool}
473              earlier)))))}