1	import Base
2	import ../shape/core.bend as Shape
3	import ../storage/main.bend as Storage
4	import ../storage/model.bend as Model
5	import ./lifecycle.bend as Lifecycle
6	
7	type Error is Data:
8	  ShapeError{error: Shape.Error}
9	  StorageError{error: Storage.Error}
10	  ValueCountMismatch{}
11	  StorageLengthMismatch{}
12	
13	type Tensor<-shape: Shape.Shape> is Type:
14	  TTensor{storage: Storage.Storage,
15	    -length_exact: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}}
16	
17	type Dynamic is Type:
18	  Packed{shape: Shape.Shape, tensor: Tensor<shape>}
19	
20	def pack(shape: Shape.Shape, tensor: Tensor<shape>) -> Dynamic:
21	  Packed{shape, tensor}
22	
23	def shape(dynamic: Dynamic) -> Dynamic & Shape.Shape:
24	  match dynamic:
25	    case Packed{+shape, tensor}:
26	      (Packed{shape, tensor}, shape)
27	
28	def count(dynamic: Dynamic) -> Dynamic & U32:
29	  match dynamic:
30	    case Packed{+shape, tensor}:
31	      (Packed{shape, tensor}, Shape.count(shape))
32	
33	def logical_length(-shape: Shape.Shape, tensor: Tensor<shape>) -> Nat:
34	  TTensor{storage, exact} = tensor
35	  Lifecycle.logical_length(storage)
36	
37	def observe(-shape: Shape.Shape, tensor: Tensor<shape>, index: U32) -> Maybe<&2, F32>:
38	  TTensor{storage, exact} = tensor
39	  Lifecycle.observe(storage, index)
40	
41	def observe_dynamic(dynamic: Dynamic, index: U32) -> Maybe<&2, F32>:
42	  Packed{shape, tensor} = dynamic
43	  observe(shape, tensor, index)
44	
45	def ObservationChecked(dynamic: Dynamic, -index: U32) -> Data:
46	  Packed{shape, tensor} = dynamic
47	  TTensor{storage, exact} = tensor
48	  match storage:
49	    case Storage.Empty{}:
50	      Empty
51	    case Storage.Owned{+depth, +length, array, balanced, valid}:
52	      {Storage.index_matches(depth, length, index) == True{} : Bool}
53	
54	type LengthValid<-shape: Shape.Shape, -tensor: Tensor<shape>> is Data:
55	  LengthValid{-exact: {logical_length(shape, tensor) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}}
56	
57	def attach_decided(+shape: Shape.Shape, storage: Storage.Storage, +n: Nat,
58	  -exact: {Lifecycle.logical_length(storage) == n : Nat},
59	  decision: Shape.BoolCase<Nat.is_eq(n, Shape.elements(shape))>) ->
60	  Result<&2, &1, Error, Tensor<shape>>:
61	  match decision:
62	    case Shape.BFalse{equal}:
63	      Fail{StorageLengthMismatch{}}
64	    case Shape.BTrue{equal}:
65	      Done{TTensor{storage, Equal.trans(Nat, Lifecycle.logical_length(storage), n,
66	        Shape.logical_numel(Shape.dimensions(shape)), exact,
67	        Equal.trans(Nat, n, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)),
68	          Lifecycle.natural_equal(n, Shape.elements(shape), equal), Shape.elements_exact(shape)))}}
69	
70	def attach_length(+shape: Shape.Shape, -original: Storage.Storage, pair: Storage.Storage & Nat,
71	  -same: {pair == Storage.length(original) : Storage.Storage & Nat}) ->
72	  Result<&2, &1, Error, Tensor<shape>>:
73	  (storage, +n) = pair
74	  attach_decided(shape, storage, n,
75	    %Equal.sym(Storage.Storage & Nat, (storage, n), Storage.length(original), same) :
76	      {Lifecycle.length_owner(_) == Lifecycle.length_value(_) : Nat}
77	    Lifecycle.length_exact(original),
78	    Shape.bool_case(Nat.is_eq(n, Shape.elements(shape))))
79	
80	def attach(+shape: Shape.Shape, storage: Storage.Storage) -> Result<&2, &1, Error, Tensor<shape>>:
81	  attach_length(shape, storage, Storage.length(storage), {==})
82	
83	def new_result(+shape: Shape.Shape, result: Result<&2, &1, Storage.Error, Storage.Storage>) ->
84	  Result<&2, &1, Error, Tensor<shape>>:
85	  match result:
86	    case Fail{error}:
87	      Fail{StorageError{error}}
88	    case Done{storage}:
89	      attach(shape, storage)
90	
91	def new(+shape: Shape.Shape, fill: F32) -> Result<&2, &1, Error, Tensor<shape>>:
92	  new_result(shape, Storage.new(Shape.count(shape), fill))
93	
94	def storage_read_error(result: Result<&2, &2, Storage.Error, F32>) -> Result<&2, &2, Error, F32>:
95	  match result:
96	    case Fail{error}:
97	      Fail{StorageError{error}}
98	    case Done{value}:
99	      Done{value}
100	
101	def storage_write_error(result: Result<&2, &2, Storage.Error, Unit>) -> Result<&2, &2, Error, Unit>:
102	  match result:
103	    case Fail{error}:
104	      Fail{StorageError{error}}
105	    case Done{value}:
106	      Done{value}
107	
108	def read_result(-shape: Shape.Shape, -original: Storage.Storage,
109	  -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +i: U32,
110	  pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>,
111	  -same: {pair == Storage.get(original, i) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}) ->
112	  Tensor<shape> & Result<&2, &2, Error, F32>:
113	  (storage, result) = pair
114	  tensor : Tensor<shape> = TTensor{storage, Equal.trans(Nat, Lifecycle.logical_length(storage), Lifecycle.logical_length(original),
115	    Shape.logical_numel(Shape.dimensions(shape)),
116	    %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, (storage, result), Storage.get(original, i), same) :
117	      {Lifecycle.retained_read(_) == Lifecycle.logical_length(original) : Nat}
118	    Lifecycle.get_length(original, i), valid)}
119	  (tensor, storage_read_error(result))
120	
121	def read_flat(-shape: Shape.Shape, tensor: Tensor<shape>, +i: U32) -> Tensor<shape> & Result<&2, &2, Error, F32>:
122	  TTensor{storage, valid} = tensor
123	  read_result(shape, storage, valid, i, Storage.get(storage, i), {==})
124	
125	def result_value(result: Result<&2, &2, Error, F32>) -> Maybe<&2, F32>:
126	  match result:
127	    case Fail{error}:
128	      None{}
129	    case Done{value}:
130	      Some{value}
131	
132	def read_value(-shape: Shape.Shape, pair: Tensor<shape> & Result<&2, &2, Error, F32>) -> Maybe<&2, F32>:
133	  (tensor, result) = pair
134	  result_value(result)
135	
136	type Read<-shape: Shape.Shape, -original: Tensor<shape>, -index: U32> is Type:
137	  Read{tensor: Tensor<shape>, result: Result<&2, &2, Error, F32>,
138	    exact: {(tensor, result) == read_flat(shape, original, index) : Tensor<shape> & Result<&2, &2, Error, F32>}}
139	
140	def read_certificate_pair(-shape: Shape.Shape, -original: Tensor<shape>, -index: U32,
141	  pair: Tensor<shape> & Result<&2, &2, Error, F32>,
142	  exact: {pair == read_flat(shape, original, index) : Tensor<shape> & Result<&2, &2, Error, F32>}) -> Read<shape, original, index>:
143	  (tensor, result) = pair
144	  Read{tensor, result, exact}
145	
146	def read_certificate(-shape: Shape.Shape, original: Tensor<shape>, +index: U32) -> Read<shape, original, index>:
147	  read_certificate_pair(shape, original, index, read_flat(shape, original, index), {==})
148	
149	def certificate_value(-shape: Shape.Shape, -original: Tensor<shape>, -index: U32, certificate: Read<shape, original, index>) -> Maybe<&2, F32>:
150	  Read{tensor, result, exact} = certificate
151	  result_value(result)
152	
153	def checked_observe(-shape: Shape.Shape, tensor: Tensor<shape>, index: U32) -> Maybe<&2, F32>:
154	  TTensor{storage, exact} = tensor
155	  Lifecycle.checked_observe(storage, index)
156	
157	type ObservationModel<-shape: Shape.Shape, -original: Tensor<shape>, -index: U32,
158	  -checked: ObservationChecked(Packed{shape, original}, index)> is Data:
159	  ObservationModel{-equal: {checked_observe(shape, original, index) == observe(shape, original, index) : Maybe<&2, F32>}}
160	
161	def owned_observation_model(-shape: Shape.Shape, +depth: Nat, +length: Nat, -array: Array<F32>, +index: U32,
162	  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
163	  -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
164	  -checked: {Storage.index_matches(depth, length, index) == True{} : Bool},
165	  certificate: Lifecycle.ArrayObservationModel<depth, length, array, index, checked>) ->
166	  ObservationModel<shape, TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index, checked>:
167	  Lifecycle.ArrayObservationModel{equal} = certificate
168	  ObservationModel{equal}
169	
170	def observation_model(-shape: Shape.Shape, original: Tensor<shape>, +index: U32,
171	  +checked: ObservationChecked(Packed{shape, original}, index)) -> ObservationModel<shape, original, index, checked>:
172	  TTensor{storage, exact} = original
173	  match storage:
174	    case Storage.Empty{}:
175	      match checked:
176	    case Storage.Owned{+depth, +length, array, balanced, valid}:
177	      owned_observation_model(shape, depth, length, array, index, balanced, valid, exact, checked,
178	        Lifecycle.array_observation_model(depth, length, array, index, checked))
179	
180	def read_result_value(-shape: Shape.Shape, -original: Storage.Storage,
181	  -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32,
182	  pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>,
183	  -same: {pair == Storage.get(original, index) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}) ->
184	  {read_value(shape, read_result(shape, original, valid, index, pair, same)) == Lifecycle.read_value(pair) : Maybe<&2, F32>}:
185	  (storage, result) = pair
186	  match result:
187	    case Fail{error}:
188	      {==}
189	    case Done{value}:
190	      {==}
191	
192	type SourceRead<-shape: Shape.Shape, -original: Tensor<shape>, -index: U32> is Data:
193	  SourceRead{-meaning: {read_value(shape, read_flat(shape, original, index)) == checked_observe(shape, original, index) : Maybe<&2, F32>}}
194	
195	def storage_read_source(-shape: Shape.Shape, -storage: Storage.Storage,
196	  -valid: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32,
197	  certificate: Lifecycle.StorageReadModel<storage, index>) -> SourceRead<shape, TTensor{storage, valid}, index>:
198	  Lifecycle.StorageReadModel{meaning} = certificate
199	  SourceRead{Equal.trans(Maybe<&2, F32>, read_value(shape, read_flat(shape, TTensor{storage, valid}, index)),
200	    Lifecycle.read_value(Storage.get(storage, index)), Lifecycle.checked_observe(storage, index),
201	    read_result_value(shape, storage, valid, index, Storage.get(storage, index), {==}), meaning)}
202	
203	def source_read_model(-shape: Shape.Shape, original: Tensor<shape>, +index: U32) -> SourceRead<shape, original, index>:
204	  TTensor{storage, valid} = original
205	  storage_read_source(shape, storage, valid, index, Lifecycle.storage_read_model(storage, index))
206	
207	def retained_read_observe(-shape: Shape.Shape, pair: Tensor<shape> & Result<&2, &2, Error, F32>, index: U32) -> Maybe<&2, F32>:
208	  (tensor, result) = pair
209	  checked_observe(shape, tensor, index)
210	
211	def read_result_keeps_projection(-shape: Shape.Shape, -original: Storage.Storage,
212	  -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +other: U32,
213	  pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>,
214	  -same: {pair == Storage.get(original, index) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}) ->
215	  {retained_read_observe(shape, read_result(shape, original, valid, index, pair, same), other) == Lifecycle.retained_observe(pair, other) : Maybe<&2, F32>}:
216	  (storage, result) = pair
217	  {==}
218	
219	type SourceReadKeeps<-shape: Shape.Shape, -original: Tensor<shape>, -index: U32> is Data:
220	  SourceReadKeeps{-kept: @+other: U32 ->
221	    {retained_read_observe(shape, read_flat(shape, original, index), other) == checked_observe(shape, original, other) : Maybe<&2, F32>}}
222	
223	def storage_read_keeps_source(-shape: Shape.Shape, -storage: Storage.Storage,
224	  -valid: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32,
225	  certificate: Lifecycle.StorageReadKeeps<storage, index>) -> SourceReadKeeps<shape, TTensor{storage, valid}, index>:
226	  Lifecycle.StorageReadKeeps{kept} = certificate
227	  SourceReadKeeps{other => Equal.trans(Maybe<&2, F32>, retained_read_observe(shape, read_flat(shape, TTensor{storage, valid}, index), other),
228	    Lifecycle.retained_observe(Storage.get(storage, index), other), Lifecycle.checked_observe(storage, other),
229	    read_result_keeps_projection(shape, storage, valid, index, other, Storage.get(storage, index), {==}), kept(other))}
230	
231	def source_read_keeps(-shape: Shape.Shape, original: Tensor<shape>, +index: U32) -> SourceReadKeeps<shape, original, index>:
232	  TTensor{storage, valid} = original
233	  storage_read_keeps_source(shape, storage, valid, index, Lifecycle.storage_read_keeps(storage, index))
234	
235	def write_result(-shape: Shape.Shape, -original: Storage.Storage,
236	  -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +i: U32, +value: F32,
237	  pair: Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
238	  -same: {pair == Storage.set(original, i, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}) ->
239	  Tensor<shape> & Result<&2, &2, Error, Unit>:
240	  (storage, result) = pair
241	  tensor : Tensor<shape> = TTensor{storage, Equal.trans(Nat, Lifecycle.logical_length(storage), Lifecycle.logical_length(original),
242	    Shape.logical_numel(Shape.dimensions(shape)),
243	    %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, (storage, result), Storage.set(original, i, value), same) :
244	      {Lifecycle.retained_write(_) == Lifecycle.logical_length(original) : Nat}
245	    Lifecycle.set_length(original, i, value), valid)}
246	  (tensor, storage_write_error(result))
247	
248	def write_flat(-shape: Shape.Shape, tensor: Tensor<shape>, +i: U32, +value: F32) ->
249	  Tensor<shape> & Result<&2, &2, Error, Unit>:
250	  TTensor{storage, valid} = tensor
251	  write_result(shape, storage, valid, i, value, Storage.set(storage, i, value), {==})
252	
253	def UpdateMeaning(-shape: Shape.Shape, -original: Tensor<shape>, +index: U32, +value: F32,
254	  pair: Tensor<shape> & Result<&2, &2, Error, Unit>) -> Type:
255	  (tensor, result) = pair
256	  match result:
257	    case Fail{error}:
258	      Unit
259	    case Done{unit}:
260	      ObservationChecked(Packed{shape, tensor}, index) &
261	        ({observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>} &
262	          (@+other: U32 -> @checked: ObservationChecked(Packed{shape, original}, other) ->
263	            @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
264	              ObservationChecked(Packed{shape, tensor}, other) &
265	                {observe(shape, tensor, other) == observe(shape, original, other) : Maybe<&2, F32>}))
266	
267	type UpdateModel<-shape: Shape.Shape, -original: Tensor<shape>, -index: U32, -value: F32> is Data:
268	  UpdateModel{-meaning: UpdateMeaning(shape, original, index, value, write_flat(shape, original, index, value))}
269	
270	def CheckedUpdateMeaning(-shape: Shape.Shape, -original: Tensor<shape>, +index: U32, +value: F32,
271	  pair: Tensor<shape> & Result<&2, &2, Error, Unit>) -> Type:
272	  (tensor, result) = pair
273	  match result:
274	    case Fail{error}:
275	      Unit
276	    case Done{unit}:
277	      ObservationChecked(Packed{shape, tensor}, index) &
278	        ({checked_observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>} &
279	          (@+other: U32 -> @checked: ObservationChecked(Packed{shape, original}, other) ->
280	            @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
281	              ObservationChecked(Packed{shape, tensor}, other) &
282	                {checked_observe(shape, tensor, other) == checked_observe(shape, original, other) : Maybe<&2, F32>}))
283	
284	type CheckedUpdateModel<-shape: Shape.Shape, -original: Tensor<shape>, -index: U32, -value: F32> is Data:
285	  CheckedUpdateModel{-meaning: CheckedUpdateMeaning(shape, original, index, value, write_flat(shape, original, index, value))}
286	
287	type Write<-shape: Shape.Shape, -original: Tensor<shape>, -index: U32, -value: F32> is Type:
288	  Write{tensor: Tensor<shape>, result: Result<&2, &2, Error, Unit>,
289	    exact: {(tensor, result) == write_flat(shape, original, index, value) : Tensor<shape> & Result<&2, &2, Error, Unit>}}
290	
291	def write_certificate_pair(-shape: Shape.Shape, -original: Tensor<shape>, -index: U32, -value: F32,
292	  pair: Tensor<shape> & Result<&2, &2, Error, Unit>,
293	  exact: {pair == write_flat(shape, original, index, value) : Tensor<shape> & Result<&2, &2, Error, Unit>}) -> Write<shape, original, index, value>:
294	  (tensor, result) = pair
295	  Write{tensor, result, exact}
296	
297	def write_certificate(-shape: Shape.Shape, original: Tensor<shape>, +index: U32, +value: F32) -> Write<shape, original, index, value>:
298	  write_certificate_pair(shape, original, index, value, write_flat(shape, original, index, value), {==})
299	
300	def read_coordinate_result(+shape: Shape.Shape, tensor: Tensor<shape>, result: Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>) ->
301	  Tensor<shape> & Result<&2, &2, Error, F32>:
302	  match result:
303	    case Fail{error}:
304	      (tensor, Fail{ShapeError{error}})
305	    case Done{index}:
306	      read_flat(shape, tensor, Shape.index_value(shape, index))
307	
308	def read_coordinate(+shape: Shape.Shape, tensor: Tensor<shape>, coordinates: List<&2, U32>) ->
309	  Tensor<shape> & Result<&2, &2, Error, F32>:
310	  read_coordinate_result(shape, tensor, Shape.flatten_checked(shape, coordinates))
311	
312	def write_coordinate_result(+shape: Shape.Shape, tensor: Tensor<shape>, value: F32,
313	  result: Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>) -> Tensor<shape> & Result<&2, &2, Error, Unit>:
314	  match result:
315	    case Fail{error}:
316	      (tensor, Fail{ShapeError{error}})
317	    case Done{index}:
318	      write_flat(shape, tensor, Shape.index_value(shape, index), value)
319	
320	def write_coordinate(+shape: Shape.Shape, tensor: Tensor<shape>, coordinates: List<&2, U32>, value: F32) ->
321	  Tensor<shape> & Result<&2, &2, Error, Unit>:
322	  write_coordinate_result(shape, tensor, value, Shape.flatten_checked(shape, coordinates))
323	
324	def clone_result(-shape: Shape.Shape, -original: Storage.Storage,
325	  -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
326	  pair: Storage.Storage & Storage.Storage,
327	  -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) -> Tensor<shape> & Tensor<shape>:
328	  (first, second) = pair
329	  (TTensor{first, Equal.trans(Nat, Lifecycle.logical_length(first), Lifecycle.logical_length(original),
330	    Shape.logical_numel(Shape.dimensions(shape)),
331	    %Equal.sym(Storage.Storage & Storage.Storage, (first, second), Storage.clone(original), same) :
332	      {Lifecycle.first_length(_) == Lifecycle.logical_length(original) : Nat}
333	    Lifecycle.clone_first_length(original), valid)},
334	  TTensor{second, Equal.trans(Nat, Lifecycle.logical_length(second), Lifecycle.logical_length(original),
335	    Shape.logical_numel(Shape.dimensions(shape)),
336	    %Equal.sym(Storage.Storage & Storage.Storage, (first, second), Storage.clone(original), same) :
337	      {Lifecycle.second_length(_) == Lifecycle.logical_length(original) : Nat}
338	    Lifecycle.clone_second_length(original), valid)})
339	
340	def clone(-shape: Shape.Shape, tensor: Tensor<shape>) -> Tensor<shape> & Tensor<shape>:
341	  TTensor{storage, valid} = tensor
342	  clone_result(shape, storage, valid, Storage.clone(storage), {==})
343	
344	def length_result(-shape: Shape.Shape, -original: Storage.Storage,
345	  -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
346	  pair: Storage.Storage & Nat, -same: {pair == Storage.length(original) : Storage.Storage & Nat}) -> Tensor<shape> & Nat:
347	  (storage, n) = pair
348	  (TTensor{storage, Equal.trans(Nat, Lifecycle.logical_length(storage), Lifecycle.logical_length(original),
349	    Shape.logical_numel(Shape.dimensions(shape)),
350	    %Equal.sym(Storage.Storage & Nat, (storage, n), Storage.length(original), same) :
351	      {Lifecycle.length_owner(_) == Lifecycle.logical_length(original) : Nat}
352	    Lifecycle.length_preserved(original), valid)}, n)
353	
354	def length(-shape: Shape.Shape, tensor: Tensor<shape>) -> Tensor<shape> & Nat:
355	  TTensor{storage, valid} = tensor
356	  length_result(shape, storage, valid, Storage.length(storage), {==})
357	
358	def fill_values_step(-shape: Shape.Shape, rec: Tensor<shape> -> Result<&2, &1, Error, Tensor<shape>>,
359	  pair: Tensor<shape> & Result<&2, &2, Error, Unit>) -> Result<&2, &1, Error, Tensor<shape>>:
360	  (tensor, result) = pair
361	  match result:
362	    case Fail{error}:
363	      Fail{error}
364	    case Done{unit}:
365	      rec(tensor)
366	
367	def fill_values_decided(-shape: Shape.Shape, +cursor: Nat, +index: U32, value: F32,
368	  tensor: Tensor<shape>, rec: Tensor<shape> -> Result<&2, &1, Error, Tensor<shape>>,
369	  decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>) -> Result<&2, &1, Error, Tensor<shape>>:
370	  match decision:
371	    case Shape.BFalse{equal}:
372	      Fail{StorageError{Storage.InvalidIndex{}}}
373	    case Shape.BTrue{equal}:
374	      fill_values_step(shape, rec, write_flat(shape, tensor, index, value))
375	
376	def fill_values(values: List<&2, F32>, -shape: Shape.Shape, tensor: Tensor<shape>, +cursor: Nat) ->
377	  Result<&2, &1, Error, Tensor<shape>>:
378	  match values:
379	    case Nil{}:
380	      Done{tensor}
381	    case value <> rest:
382	      +index = U32.from_nat(cursor)
383	      fill_values_decided(shape, cursor, index, value, tensor,
384	        tensor => fill_values(rest, shape, tensor, 1n+cursor), Shape.bool_case(Nat.is_eq(U32.to_nat(index), cursor)))
385	
386	def fill_values_word(values: List<&2, F32>, -shape: Shape.Shape, tensor: Tensor<shape>, index: U32) ->
387	  Result<&2, &1, Error, Tensor<shape>>:
388	  fill_values(values, shape, tensor, U32.to_nat(index))
389	
390	def from_values_new(-shape: Shape.Shape, values: List<&2, F32>, result: Result<&2, &1, Error, Tensor<shape>>) ->
391	  Result<&2, &1, Error, Tensor<shape>>:
392	  match result:
393	    case Fail{error}:
394	      Fail{error}
395	    case Done{tensor}:
396	      fill_values(values, shape, tensor, 0n)
397	
398	def from_values_counted(+shape: Shape.Shape, +values: List<&2, F32>,
399	  decision: Shape.BoolCase<Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape))>) ->
400	  Result<&2, &1, Error, Tensor<shape>>:
401	  match decision:
402	    case Shape.BFalse{equal}:
403	      Fail{ValueCountMismatch{}}
404	    case Shape.BTrue{equal}:
405	      from_values_new(shape, values, new(shape, 0.0))
406	
407	def from_values(+shape: Shape.Shape, +values: List<&2, F32>) -> Result<&2, &1, Error, Tensor<shape>>:
408	  from_values_counted(shape, values,
409	    Shape.bool_case(Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape))))
410	
411	def construct_values(+shape: Shape.Shape, result: Result<&2, &1, Error, Tensor<shape>>) -> Result<&2, &1, Error, Dynamic>:
412	  match result:
413	    case Fail{error}:
414	      Fail{error}
415	    case Done{tensor}:
416	      Done{pack(shape, tensor)}
417	
418	def construct_shape(-dimensions: List<&2, U32>, values: List<&2, F32>, result: Shape.ConstructResult<dimensions>) ->
419	  Result<&2, &1, Error, Dynamic>:
420	  match result:
421	    case Shape.SError{error}:
422	      Fail{ShapeError{error}}
423	    case Shape.SBuilt{+shape, preserved}:
424	      construct_values(shape, from_values(shape, values))
425	
426	def construct(+dimensions: List<&2, U32>, values: List<&2, F32>) -> Result<&2, &1, Error, Dynamic>:
427	  construct_shape(dimensions, values, Shape.construct(dimensions))
428	
429	def ConstructionDimensions(+dimensions: List<&2, U32>, result: Result<&2, &1, Error, Dynamic>) -> Type:
430	  match result:
431	    case Fail{error}:
432	      Unit
433	    case Done{Packed{+shape, tensor}}:
434	      {Shape.dimensions(shape) == dimensions : List<&2, U32>}
435	
436	def ValuesCount(+shape: Shape.Shape, +values: List<&2, F32>, result: Result<&2, &1, Error, Tensor<shape>>) -> Type:
437	  match result:
438	    case Fail{error}:
439	      Unit
440	    case Done{tensor}:
441	      {Shape.logical_numel(Shape.dimensions(shape)) == List.length(&2, F32, values) : Nat}
442	
443	def read_dynamic_result(+shape: Shape.Shape, pair: Tensor<shape> & Result<&2, &2, Error, F32>) ->
444	  Dynamic & Result<&2, &2, Error, F32>:
445	  (tensor, result) = pair
446	  (Packed{shape, tensor}, result)
447	
448	def read_dynamic(dynamic: Dynamic, index: U32) -> Dynamic & Result<&2, &2, Error, F32>:
449	  Packed{+shape, tensor} = dynamic
450	  read_dynamic_result(shape, read_flat(shape, tensor, index))
451	
452	type DynamicRead<-original: Dynamic, -index: U32> is Type:
453	  DynamicRead{dynamic: Dynamic, result: Result<&2, &2, Error, F32>,
454	    exact: {(dynamic, result) == read_dynamic(original, index) : Dynamic & Result<&2, &2, Error, F32>}}
455	
456	def dynamic_read_certificate_pair(-original: Dynamic, -index: U32,
457	  pair: Dynamic & Result<&2, &2, Error, F32>,
458	  exact: {pair == read_dynamic(original, index) : Dynamic & Result<&2, &2, Error, F32>}) -> DynamicRead<original, index>:
459	  (dynamic, result) = pair
460	  DynamicRead{dynamic, result, exact}
461	
462	def dynamic_read_certificate(original: Dynamic, +index: U32) -> DynamicRead<original, index>:
463	  dynamic_read_certificate_pair(original, index, read_dynamic(original, index), {==})
464	
465	def dynamic_read_value(pair: Dynamic & Result<&2, &2, Error, F32>) -> Maybe<&2, F32>:
466	  (dynamic, result) = pair
467	  result_value(result)
468	
469	def checked_observe_dynamic(dynamic: Dynamic, index: U32) -> Maybe<&2, F32>:
470	  Packed{shape, tensor} = dynamic
471	  checked_observe(shape, tensor, index)
472	
473	def dynamic_result_value(+shape: Shape.Shape, pair: Tensor<shape> & Result<&2, &2, Error, F32>) ->
474	  {dynamic_read_value(read_dynamic_result(shape, pair)) == read_value(shape, pair) : Maybe<&2, F32>}:
475	  (tensor, result) = pair
476	  {==}
477	
478	type DynamicSourceRead<-original: Dynamic, -index: U32> is Data:
479	  DynamicSourceRead{-meaning: {dynamic_read_value(read_dynamic(original, index)) == checked_observe_dynamic(original, index) : Maybe<&2, F32>}}
480	
481	def dynamic_read_source(+shape: Shape.Shape, -tensor: Tensor<shape>, +index: U32, certificate: SourceRead<shape, tensor, index>) ->
482	  DynamicSourceRead<Packed{shape, tensor}, index>:
483	  SourceRead{meaning} = certificate
484	  DynamicSourceRead{Equal.trans(Maybe<&2, F32>, dynamic_read_value(read_dynamic(Packed{shape, tensor}, index)),
485	    read_value(shape, read_flat(shape, tensor, index)), checked_observe(shape, tensor, index),
486	    dynamic_result_value(shape, read_flat(shape, tensor, index)), meaning)}
487	
488	def dynamic_source_read_model(original: Dynamic, +index: U32) -> DynamicSourceRead<original, index>:
489	  Packed{+shape, tensor} = original
490	  dynamic_read_source(shape, tensor, index, source_read_model(shape, tensor, index))
491	
492	def retained_dynamic_observe(pair: Dynamic & Result<&2, &2, Error, F32>, index: U32) -> Maybe<&2, F32>:
493	  (dynamic, result) = pair
494	  checked_observe_dynamic(dynamic, index)
495	
496	def dynamic_keeps_projection(+shape: Shape.Shape, pair: Tensor<shape> & Result<&2, &2, Error, F32>, +other: U32) ->
497	  {retained_dynamic_observe(read_dynamic_result(shape, pair), other) == retained_read_observe(shape, pair, other) : Maybe<&2, F32>}:
498	  (tensor, result) = pair
499	  {==}
500	
501	type DynamicSourceReadKeeps<-original: Dynamic, -index: U32> is Data:
502	  DynamicSourceReadKeeps{-kept: @+other: U32 ->
503	    {retained_dynamic_observe(read_dynamic(original, index), other) == checked_observe_dynamic(original, other) : Maybe<&2, F32>}}
504	
505	def dynamic_read_keeps_source(+shape: Shape.Shape, -tensor: Tensor<shape>, +index: U32, certificate: SourceReadKeeps<shape, tensor, index>) ->
506	  DynamicSourceReadKeeps<Packed{shape, tensor}, index>:
507	  SourceReadKeeps{kept} = certificate
508	  DynamicSourceReadKeeps{other => Equal.trans(Maybe<&2, F32>, retained_dynamic_observe(read_dynamic(Packed{shape, tensor}, index), other),
509	    retained_read_observe(shape, read_flat(shape, tensor, index), other), checked_observe(shape, tensor, other),
510	    dynamic_keeps_projection(shape, read_flat(shape, tensor, index), other), kept(other))}
511	
512	def dynamic_source_read_keeps(original: Dynamic, +index: U32) -> DynamicSourceReadKeeps<original, index>:
513	  Packed{+shape, tensor} = original
514	  dynamic_read_keeps_source(shape, tensor, index, source_read_keeps(shape, tensor, index))
515	
516	type ReadInfo<-original: Dynamic, -index: U32> is Type:
517	  ReadInfo{owner: Dynamic, same: {owner == original : Dynamic},
518	    source: DynamicSourceRead<original, index>, keeps: DynamicSourceReadKeeps<original, index>}
519	
520	def owned_read_source(-shape: Shape.Shape, +depth: Nat, +length: Nat, -array: Array<F32>, +index: U32,
521	  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
522	  -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
523	  SourceRead<shape, TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index>:
524	  storage_read_source(shape, Storage.Owned{depth, length, array, balanced, valid}, exact, index,
525	    Lifecycle.read_checked_storage(depth, length, array, index, balanced, valid,
526	      Lifecycle.read_checked_model(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid)))
527	
528	def owned_read_keeps(-shape: Shape.Shape, +depth: Nat, +length: Nat, -array: Array<F32>, +index: U32,
529	  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
530	  -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
531	  SourceReadKeeps<shape, TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index>:
532	  storage_read_keeps_source(shape, Storage.Owned{depth, length, array, balanced, valid}, exact, index,
533	    Lifecycle.read_checked_storage_keeps(depth, length, array, index, balanced, valid,
534	      Lifecycle.read_checked_keeps(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid)))
535	
536	def read_info(original: Dynamic, +index: U32) -> ReadInfo<original, index>:
537	  Packed{+shape, tensor} = original
538	  TTensor{storage, exact} = tensor
539	  match storage:
540	    case Storage.Empty{}:
541	      ReadInfo{Packed{shape, TTensor{Storage.Empty{}, exact}}, {==},
542	        dynamic_read_source(shape, TTensor{Storage.Empty{}, exact}, index,
543	          storage_read_source(shape, Storage.Empty{}, exact, index, Lifecycle.StorageReadModel{{==}})),
544	        dynamic_read_keeps_source(shape, TTensor{Storage.Empty{}, exact}, index,
545	          storage_read_keeps_source(shape, Storage.Empty{}, exact, index, Lifecycle.StorageReadKeeps{other => {==}}))}
546	    case Storage.Owned{+depth, +length, array, balanced, valid}:
547	      ReadInfo{Packed{shape, TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, {==},
548	        dynamic_read_source(shape, TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index,
549	          owned_read_source(shape, depth, length, array, index, balanced, valid, exact)),
550	        dynamic_read_keeps_source(shape, TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index,
551	          owned_read_keeps(shape, depth, length, array, index, balanced, valid, exact))}
552	
553	def write_dynamic_result(+shape: Shape.Shape, pair: Tensor<shape> & Result<&2, &2, Error, Unit>) ->
554	  Dynamic & Result<&2, &2, Error, Unit>:
555	  (tensor, result) = pair
556	  (Packed{shape, tensor}, result)
557	
558	def write_dynamic(dynamic: Dynamic, index: U32, value: F32) -> Dynamic & Result<&2, &2, Error, Unit>:
559	  Packed{+shape, tensor} = dynamic
560	  write_dynamic_result(shape, write_flat(shape, tensor, index, value))
561	
562	def clone_dynamic_result(+shape: Shape.Shape, pair: Tensor<shape> & Tensor<shape>) -> Dynamic & Dynamic:
563	  (first, second) = pair
564	  (Packed{shape, first}, Packed{shape, second})
565	
566	def clone_dynamic(dynamic: Dynamic) -> Dynamic & Dynamic:
567	  Packed{+shape, tensor} = dynamic
568	  clone_dynamic_result(shape, clone(shape, tensor))
569	
570	def write_observe(-shape: Shape.Shape, pair: Tensor<shape> & Result<&2, &2, Error, Unit>, index: U32) -> Maybe<&2, F32>:
571	  (tensor, result) = pair
572	  observe(shape, tensor, index)
573	
574	def error_code(error: Error) -> U32:
575	  match error:
576	    case ShapeError{error}:
577	      Shape.error_code(error)
578	    case StorageError{Storage.TooLarge{}}:
579	      7
580	    case StorageError{Storage.OutOfBounds{}}:
581	      8
582	    case StorageError{Storage.InvalidIndex{}}:
583	      9
584	    case ValueCountMismatch{}:
585	      10
586	    case StorageLengthMismatch{}:
587	      11