src/tensor/core.bend
bendtorch-core@0.1.0.0 · 587 lines · 94 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
4import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
5import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
6
7type Error is Data:
8 ShapeError{error: Shape.Error}
9 StorageError{error: Storage.Error}
10 ValueCountMismatch{}
11 StorageLengthMismatch{}
12
13type 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
17type Dynamic is Type:
18 Packed{shape: Shape.Shape, tensor: Tensor<shape>}
19
20def pack(shape: Shape.Shape, tensor: Tensor<shape>) -> Dynamic:
21 Packed{shape, tensor}
22
23def shape(dynamic: Dynamic) -> Dynamic & Shape.Shape:
24 match dynamic:
25 case Packed{+shape, tensor}:
26 (Packed{shape, tensor}, shape)
27
28def count(dynamic: Dynamic) -> Dynamic & U32:
29 match dynamic:
30 case Packed{+shape, tensor}:
31 (Packed{shape, tensor}, Shape.count(shape))
32
33def logical_length(-shape: Shape.Shape, tensor: Tensor<shape>) -> Nat:
34 TTensor{storage, exact} = tensor
35 Lifecycle.logical_length(storage)
36
37def observe(-shape: Shape.Shape, tensor: Tensor<shape>, index: U32) -> Maybe<&2, F32>:
38 TTensor{storage, exact} = tensor
39 Lifecycle.observe(storage, index)
40
41def observe_dynamic(dynamic: Dynamic, index: U32) -> Maybe<&2, F32>:
42 Packed{shape, tensor} = dynamic
43 observe(shape, tensor, index)
44
45def 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
54type LengthValid<-shape: Shape.Shape, -tensor: Tensor<shape>> is Data:
55 LengthValid{-exact: {logical_length(shape, tensor) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}}
56
57def 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
70def 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
80def attach(+shape: Shape.Shape, storage: Storage.Storage) -> Result<&2, &1, Error, Tensor<shape>>:
81 attach_length(shape, storage, Storage.length(storage), {==})
82
83def 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
91def new(+shape: Shape.Shape, fill: F32) -> Result<&2, &1, Error, Tensor<shape>>:
92 new_result(shape, Storage.new(Shape.count(shape), fill))
93
94def 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
101def 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
108def 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
121def 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
125def 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
132def 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
136type 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
140def 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
146def 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
149def 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
153def 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
157type 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
161def 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
170def 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
180def 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
192type 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
195def 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
203def 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
207def 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
211def 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
219type 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
223def 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
231def 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
235def 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
248def 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
253def 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
267type 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
270def 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
284type 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
287type 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
291def 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
297def 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
300def 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
308def 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
312def 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
320def 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
324def 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
340def 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
344def 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
354def 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
358def 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
367def 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
376def 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
386def 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
390def 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
398def 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
407def 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
411def 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
418def 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
426def construct(+dimensions: List<&2, U32>, values: List<&2, F32>) -> Result<&2, &1, Error, Dynamic>:
427 construct_shape(dimensions, values, Shape.construct(dimensions))
428
429def 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
436def 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
443def 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
448def 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
452type 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
456def 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
462def dynamic_read_certificate(original: Dynamic, +index: U32) -> DynamicRead<original, index>:
463 dynamic_read_certificate_pair(original, index, read_dynamic(original, index), {==})
464
465def dynamic_read_value(pair: Dynamic & Result<&2, &2, Error, F32>) -> Maybe<&2, F32>:
466 (dynamic, result) = pair
467 result_value(result)
468
469def checked_observe_dynamic(dynamic: Dynamic, index: U32) -> Maybe<&2, F32>:
470 Packed{shape, tensor} = dynamic
471 checked_observe(shape, tensor, index)
472
473def 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
478type 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
481def 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
488def 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
492def 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
496def 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
501type 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
505def 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
512def 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
516type 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
520def 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
528def 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
536def 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
553def 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
558def 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
562def 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
566def clone_dynamic(dynamic: Dynamic) -> Dynamic & Dynamic:
567 Packed{+shape, tensor} = dynamic
568 clone_dynamic_result(shape, clone(shape, tensor))
569
570def 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
574def 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