def clone_owned_meaning
bendtorch-core@0.1.0.0 · src/tensor/construction_PROOF.bend:88
import bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend as ConstructionPROOF
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/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/clone.bend as Clone
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/construction_LAWS.bend as Laws
88def clone_owned_meaning(-shape: Shape.Shape, +depth: Nat, +length: Nat, -array: Array<F32>,
89 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
90 -length_exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
91 Laws.CloneMeaning<shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}>:
92 Laws.CloneMeaning{
93 index => Equal.trans(Maybe<&2, F32>,
94 Laws.clone_first_checked(shape, Core.clone(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}), index),
95 Lifecycle.checked_observe(Pair.fst(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
96 Lifecycle.checked_observe_array(depth, length, array, index),
97 clone_first_checked_view(shape, Storage.Owned{depth, length, array, balanced, valid}, length_exact, index,
98 Storage.clone(Storage.Owned{depth, length, array, balanced, valid}), {==}),
99 Equal.trans(Maybe<&2, F32>,
100 Lifecycle.checked_observe(Pair.fst(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
101 Lifecycle.checked_observe_array(depth, length, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, array)), index),
102 Lifecycle.checked_observe_array(depth, length, array, index),
103 storage_clone_first_checked_view(depth, length, array, index, Array.clone(F32, array), {==}, balanced, valid),
104 Equal.cong(Array<F32>, Maybe<&2, F32>, a => Lifecycle.checked_observe_array(depth, length, a, index),
105 Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, array)), array, Clone.first_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced))))),
106 index => Equal.trans(Maybe<&2, F32>,
107 Laws.clone_second_checked(shape, Core.clone(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}), index),
108 Lifecycle.checked_observe(Pair.snd(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
109 Lifecycle.checked_observe_array(depth, length, array, index),
110 clone_second_checked_view(shape, Storage.Owned{depth, length, array, balanced, valid}, length_exact, index,
111 Storage.clone(Storage.Owned{depth, length, array, balanced, valid}), {==}),
112 Equal.trans(Maybe<&2, F32>,
113 Lifecycle.checked_observe(Pair.snd(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
114 Lifecycle.checked_observe_array(depth, length, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, array)), index),
115 Lifecycle.checked_observe_array(depth, length, array, index),
116 storage_clone_second_checked_view(depth, length, array, index, Array.clone(F32, array), {==}, balanced, valid),
117 Equal.cong(Array<F32>, Maybe<&2, F32>, a => Lifecycle.checked_observe_array(depth, length, a, index),
118 Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, array)), array, Clone.second_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced))))),
119 index => Equal.trans(Maybe<&2, F32>,
120 Laws.clone_first_model(shape, Core.clone(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}), index),
121 Lifecycle.observe(Pair.fst(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
122 Model.observe(F32, depth, array, Refinement.route(depth, index)),
123 clone_first_model_view(shape, Storage.Owned{depth, length, array, balanced, valid}, length_exact, index,
124 Storage.clone(Storage.Owned{depth, length, array, balanced, valid}), {==}),
125 Equal.trans(Maybe<&2, F32>,
126 Lifecycle.observe(Pair.fst(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
127 Model.observe(F32, depth, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, array)), Refinement.route(depth, index)),
128 Model.observe(F32, depth, array, Refinement.route(depth, index)),
129 storage_clone_first_model_view(depth, length, array, index, Array.clone(F32, array), {==}, balanced, valid),
130 Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, depth, a, Refinement.route(depth, index)),
131 Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, array)), array, Clone.first_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced))))),
132 index => Equal.trans(Maybe<&2, F32>,
133 Laws.clone_second_model(shape, Core.clone(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}), index),
134 Lifecycle.observe(Pair.snd(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
135 Model.observe(F32, depth, array, Refinement.route(depth, index)),
136 clone_second_model_view(shape, Storage.Owned{depth, length, array, balanced, valid}, length_exact, index,
137 Storage.clone(Storage.Owned{depth, length, array, balanced, valid}), {==}),
138 Equal.trans(Maybe<&2, F32>,
139 Lifecycle.observe(Pair.snd(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
140 Model.observe(F32, depth, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, array)), Refinement.route(depth, index)),
141 Model.observe(F32, depth, array, Refinement.route(depth, index)),
142 storage_clone_second_model_view(depth, length, array, index, Array.clone(F32, array), {==}, balanced, valid),
143 Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, depth, a, Refinement.route(depth, index)),
144 Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, array)), array, Clone.second_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced)))))}