PermuteBuildProof.cloned_meaning: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend as PermuteBuildProof Lines 433-473 of bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&start_line=433&end_line=473 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 # The copy from an owned source, whatever the clone hands out. def cloned_meaning(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +d: Nat, +n: Nat, -valid: {Storage.bounds(d, n) == True{} : Bool}, -exact: {n == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat}, +ds: Nat, +ns: Nat, -a: Array, pair: Array & Array, -same: {pair == Array.clone(F32, a) : Array & Array}, -b: Model.Balanced(F32, ds, a), -ok: {Storage.bounds(ds, ns) == True{} : Bool}, -fits: {Lifecycle.logical_length(Storage.Owned{ds, ns, a, b, ok}) == Shape.logical_numel(Shape.dimensions(input)) : Nat}) -> 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))), Transforms.built_cloned(input, axes, plan, d, n, valid, exact, ds, ns, a, pair, same, b, ok, fits)): (kept, copy) = pair -kept_a = {\{Fact: q => q} : Fact<{Pair.fst(Array, Array, (kept, copy)) == a : Array}> -> {kept == a : Array}}( clone_first(ds, a, (kept, copy), same, b)) -copy_a = {\{Fact: q => q} : Fact<{Pair.snd(Array, Array, (kept, copy)) == a : Array}> -> {copy == a : Array}}( clone_second(ds, a, (kept, copy), same, b)) -bc = {\{Fact: q => q} : Fact -> Model.Balanced(F32, ds, copy)}(balanced_along(ds, copy, a, copy_a, b)) Transforms.Prefix{ other => Equal.cong(Array, Maybe<&2, F32>, x => Lifecycle.observe_allowed(ds, ns, x, other, Nat.is_lt(U32.to_nat(other), ns)), kept, a, kept_a), other => earlier => word_below(Layout.output(input, axes, plan), other, earlier), other => earlier => Route.index_matched(d, n, U32.from_nat(other), valid, length_below(Layout.output(input, axes, plan), n, exact, other, earlier)), other => earlier => Equal.trans(Maybe<&2, F32>, Lifecycle.checked_observe_array(d, n, Build.build(d, Build.Request{input, axes}, n, copy), U32.from_nat(other)), Some{Refinement.second(F32, Array.get(F32, a, U32.from_nat(Values.permute_source_index(input, axes, other))))}, Transforms.expected_output(input, axes, plan, Core.TTensor{Storage.Owned{ds, ns, a, b, ok}, fits}, U32.from_nat(other)), Equal.trans(Maybe<&2, F32>, Lifecycle.checked_observe_array(d, n, Build.build(d, Build.Request{input, axes}, n, copy), U32.from_nat(other)), 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))))}, {\{Fact: q => q} : Fact<{Lifecycle.checked_observe_array(d, n, Build.build(d, Build.Request{input, axes}, n, copy), U32.from_nat(other)) == Some{Refinement.second(F32, Array.get(F32, copy, U32.from_nat(Values.permute_source_index(input, axes, other))))} : Maybe<&2, F32>}> -> {Lifecycle.checked_observe_array(d, n, Build.build(d, Build.Request{input, axes}, n, copy), U32.from_nat(other)) == Some{Refinement.second(F32, Array.get(F32, copy, U32.from_nat(Values.permute_source_index(input, axes, other))))} : Maybe<&2, F32>}}( output_word(input, axes, plan, d, n, valid, exact, ds, copy, bc, other, earlier)), Equal.cong(Array, 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)), 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)), Some{Refinement.second(F32, Array.get(F32, a, U32.from_nat(Values.permute_source_index(input, axes, other))))}, {\{Fact: q => q} : Fact<{Transforms.expected_mapped(input, axes, plan, U32.from_nat(other), Core.TTensor{Storage.Owned{ds, ns, a, b, ok}, fits}, 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>}> -> {Transforms.expected_mapped(input, axes, plan, U32.from_nat(other), Core.TTensor{Storage.Owned{ds, ns, a, b, ok}, fits}, 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>}}( expected_word(input, axes, plan, other, ds, ns, a, b, ok, fits, fits, Layout.map_index(input, axes, plan, U32.from_nat(other)), mapping_done(input, axes, plan, U32.from_nat(other), %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} earlier)))))} Uses (51): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.clone https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=Storage https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=bounds https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Balanced https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=second https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/route.bend&name=index_matched https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=Plan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=map_index https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=output https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=checked_observe_array https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=logical_length https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=observe_allowed https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=permute_source_index https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=Request https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=build https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=Fact https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=balanced_along https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=clone_first https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=clone_second https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=expected_word https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=length_below https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=mapping_done https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=output_word https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=word_below https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=LoopMeaning https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=Prefix https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=built_cloned https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=expected_mapped https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=expected_output