src/tensor/lifecycle.bend
bendtorch-core@0.1.0.0 · 329 lines · 45 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
3import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
4import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
5import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
6
7def logical_length(storage: Storage.Storage) -> Nat:
8 match storage:
9 case Storage.Empty{}:
10 0n
11 case Storage.Owned{d, n, array, balanced, valid}:
12 n
13
14def retained_read(result: Storage.Storage & Result<&2, &2, Storage.Error, F32>) -> Nat:
15 (storage, value) = result
16 logical_length(storage)
17
18def retained_write(result: Storage.Storage & Result<&2, &2, Storage.Error, Unit>) -> Nat:
19 (storage, value) = result
20 logical_length(storage)
21
22def finish_read_length(+d: Nat, +n: Nat, -original: Array<F32>, +i: U32,
23 result: Array<F32> & F32, -exact: {result == Array.get(F32, original, i) : Array<F32> & F32},
24 -balanced: Model.Balanced(F32, d, original), -valid: {Storage.bounds(d, n) == True{} : Bool}) ->
25 {retained_read(Storage.finish_read(d, n, original, i, result, exact, balanced, valid)) == n : Nat}:
26 (array, value) = result
27 {==}
28
29def get_checked_length(+d: Nat, +n: Nat, array: Array<F32>, +i: U32, allowed: Bool,
30 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
31 -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool}) ->
32 {retained_read(Storage.get_checked(d, n, array, i, allowed, decision, balanced, valid)) == n : Nat}:
33 match allowed:
34 case False{}:
35 {==}
36 case True{}:
37 finish_read_length(d, n, array, i, Array.get(F32, array, i), {==}, balanced, valid)
38
39def get_length(storage: Storage.Storage, +i: U32) ->
40 {retained_read(Storage.get(storage, i)) == logical_length(storage) : Nat}:
41 match storage:
42 case Storage.Empty{}:
43 {==}
44 case Storage.Owned{+d, +n, array, balanced, valid}:
45 get_checked_length(d, n, array, i, Nat.is_lt(U32.to_nat(i), n), {==}, balanced, valid)
46
47def set_checked_length(+d: Nat, +n: Nat, array: Array<F32>, +i: U32, +value: F32, allowed: Bool,
48 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
49 -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool}) ->
50 {retained_write(Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid)) == n : Nat}:
51 match allowed:
52 case False{}:
53 {==}
54 case True{}:
55 {==}
56
57def set_length(storage: Storage.Storage, +i: U32, +value: F32) ->
58 {retained_write(Storage.set(storage, i, value)) == logical_length(storage) : Nat}:
59 match storage:
60 case Storage.Empty{}:
61 {==}
62 case Storage.Owned{+d, +n, array, balanced, valid}:
63 set_checked_length(d, n, array, i, value, Nat.is_lt(U32.to_nat(i), n), {==}, balanced, valid)
64
65def first_length(pair: Storage.Storage & Storage.Storage) -> Nat:
66 (first, second) = pair
67 logical_length(first)
68
69def second_length(pair: Storage.Storage & Storage.Storage) -> Nat:
70 (first, second) = pair
71 logical_length(second)
72
73def finish_clone_first(+d: Nat, +n: Nat, -original: Array<F32>, pair: Array<F32> & Array<F32>,
74 -exact: {pair == Array.clone(F32, original) : Array<F32> & Array<F32>},
75 -balanced: Model.Balanced(F32, d, original), -valid: {Storage.bounds(d, n) == True{} : Bool}) ->
76 {first_length(Storage.finish_clone(d, n, original, pair, exact, balanced, valid)) == n : Nat}:
77 (first, second) = pair
78 {==}
79
80def finish_clone_second(+d: Nat, +n: Nat, -original: Array<F32>, pair: Array<F32> & Array<F32>,
81 -exact: {pair == Array.clone(F32, original) : Array<F32> & Array<F32>},
82 -balanced: Model.Balanced(F32, d, original), -valid: {Storage.bounds(d, n) == True{} : Bool}) ->
83 {second_length(Storage.finish_clone(d, n, original, pair, exact, balanced, valid)) == n : Nat}:
84 (first, second) = pair
85 {==}
86
87def clone_first_length(storage: Storage.Storage) ->
88 {first_length(Storage.clone(storage)) == logical_length(storage) : Nat}:
89 match storage:
90 case Storage.Empty{}:
91 {==}
92 case Storage.Owned{+d, +n, array, balanced, valid}:
93 finish_clone_first(d, n, array, Array.clone(F32, array), {==}, balanced, valid)
94
95def clone_second_length(storage: Storage.Storage) ->
96 {second_length(Storage.clone(storage)) == logical_length(storage) : Nat}:
97 match storage:
98 case Storage.Empty{}:
99 {==}
100 case Storage.Owned{+d, +n, array, balanced, valid}:
101 finish_clone_second(d, n, array, Array.clone(F32, array), {==}, balanced, valid)
102
103def length_owner(pair: Storage.Storage & Nat) -> Nat:
104 (storage, n) = pair
105 logical_length(storage)
106
107def length_value(pair: Storage.Storage & Nat) -> Nat:
108 (storage, n) = pair
109 n
110
111def length_exact(storage: Storage.Storage) ->
112 {length_owner(Storage.length(storage)) == length_value(Storage.length(storage)) : Nat}:
113 match storage:
114 case Storage.Empty{}:
115 {==}
116 case Storage.Owned{d, n, array, balanced, valid}:
117 {==}
118
119def length_preserved(storage: Storage.Storage) ->
120 {length_owner(Storage.length(storage)) == logical_length(storage) : Nat}:
121 match storage:
122 case Storage.Empty{}:
123 {==}
124 case Storage.Owned{d, n, array, balanced, valid}:
125 {==}
126
127def IsTrue(value: Bool) -> Data:
128 match value:
129 case True{}:
130 Unit
131 case False{}:
132 Empty
133
134def false_true(equal: {True{} == False{} : Bool}) -> Empty:
135 %equal : IsTrue(_)
136 Unit{}
137
138def natural_equal(+a: Nat, +b: Nat, equal: {True{} == Nat.is_eq(a, b) : Bool}) -> {a == b : Nat}:
139 match a b:
140 case 0n 0n:
141 {==}
142 case 0n 1n+q:
143 Empty.absurd({0n == 1n+q : Nat}, false_true(equal))
144 case 1n+p 0n:
145 Empty.absurd({1n+p == 0n : Nat}, false_true(equal))
146 case 1n+p 1n+q:
147 Equal.cong(Nat, Nat, x => 1n+x, p, q, natural_equal(p, q, equal))
148
149def observe(storage: Storage.Storage, +index: U32) -> Maybe<&2, F32>:
150 match storage:
151 case Storage.Empty{}:
152 None{}
153 case Storage.Owned{+d, n, array, balanced, valid}:
154 Model.observe(F32, d, array, Refinement.route(d, index))
155
156def read_value(pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>) -> Maybe<&2, F32>:
157 (storage, result) = pair
158 match result:
159 case Fail{error}:
160 None{}
161 case Done{value}:
162 Some{value}
163
164def observe_index(+depth: Nat, -length: Nat, array: Array<F32>, +index: U32, matched: Bool) -> Maybe<&2, F32>:
165 match matched:
166 case False{}:
167 None{}
168 case True{}:
169 Model.observe(F32, depth, array, Refinement.route(depth, index))
170
171def observe_allowed(+depth: Nat, +length: Nat, array: Array<F32>, +index: U32, allowed: Bool) -> Maybe<&2, F32>:
172 match allowed:
173 case False{}:
174 None{}
175 case True{}:
176 observe_index(depth, length, array, index, Storage.index_matches(depth, length, index))
177
178def checked_observe(storage: Storage.Storage, +index: U32) -> Maybe<&2, F32>:
179 match storage:
180 case Storage.Empty{}:
181 None{}
182 case Storage.Owned{+depth, +length, array, balanced, valid}:
183 observe_allowed(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length))
184
185def finish_read_value(-depth: Nat, -length: Nat, -original: Array<F32>, -index: U32,
186 pair: Array<F32> & F32, -exact: {pair == Array.get(F32, original, index) : Array<F32> & F32},
187 -balanced: Model.Balanced(F32, depth, original), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
188 {read_value(Storage.finish_read(depth, length, original, index, pair, exact, balanced, valid)) ==
189 Some{Refinement.second(F32, pair)} : Maybe<&2, F32>}:
190 (array, value) = pair
191 {==}
192
193type ReadCheckedModel<-depth: Nat, -length: Nat, -array: Array<F32>, -index: U32, -allowed: Bool,
194 -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
195 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}> is Data:
196 ReadCheckedModel{-meaning: {read_value(Storage.get_checked(depth, length, array, index, allowed, decision, balanced, valid)) ==
197 observe_allowed(depth, length, array, index, allowed) : Maybe<&2, F32>}}
198
199def read_checked_model(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32, allowed: Bool,
200 -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
201 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
202 ReadCheckedModel<depth, length, array, index, allowed, decision, balanced, valid>:
203 match allowed:
204 case False{}:
205 ReadCheckedModel{{==}}
206 case True{}:
207 ReadCheckedModel{
208 %Route.index_complete(depth, length, index, valid,
209 Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), length), decision)) :
210 {read_value(Storage.finish_read(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid)) ==
211 observe_index(depth, length, array, index, _) : Maybe<&2, F32>}
212 Equal.trans(Maybe<&2, F32>,
213 read_value(Storage.finish_read(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid)),
214 Some{Refinement.second(F32, Array.get(F32, array, index))}, Model.observe(F32, depth, array, Refinement.route(depth, index)),
215 finish_read_value(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid),
216 Refinement.law_get_refines(F32, depth, array, index, balanced))}
217
218type StorageReadModel<-original: Storage.Storage, -index: U32> is Data:
219 StorageReadModel{-meaning: {read_value(Storage.get(original, index)) == checked_observe(original, index) : Maybe<&2, F32>}}
220
221def read_checked_storage(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32,
222 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
223 certificate: ReadCheckedModel<depth, length, array, index, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid>) ->
224 StorageReadModel<Storage.Owned{depth, length, array, balanced, valid}, index>:
225 ReadCheckedModel{meaning} = certificate
226 StorageReadModel{meaning}
227
228def storage_read_model(original: Storage.Storage, +index: U32) -> StorageReadModel<original, index>:
229 match original:
230 case Storage.Empty{}:
231 StorageReadModel{{==}}
232 case Storage.Owned{+depth, +length, array, balanced, valid}:
233 read_checked_storage(depth, length, array, index, balanced, valid,
234 read_checked_model(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid))
235
236def checked_observe_array(+depth: Nat, +length: Nat, array: Array<F32>, +index: U32) -> Maybe<&2, F32>:
237 observe_allowed(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length))
238
239def retained_observe(pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>, index: U32) -> Maybe<&2, F32>:
240 (storage, result) = pair
241 checked_observe(storage, index)
242
243def finish_read_observe(+depth: Nat, +length: Nat, -original: Array<F32>, -index: U32, +other: U32,
244 pair: Array<F32> & F32, -exact: {pair == Array.get(F32, original, index) : Array<F32> & F32},
245 -balanced: Model.Balanced(F32, depth, original), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
246 {retained_observe(Storage.finish_read(depth, length, original, index, pair, exact, balanced, valid), other) ==
247 checked_observe_array(depth, length, Refinement.first(F32, pair), other) : Maybe<&2, F32>}:
248 (array, value) = pair
249 {==}
250
251type ReadCheckedKeeps<-depth: Nat, -length: Nat, -array: Array<F32>, -index: U32, -allowed: Bool,
252 -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
253 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}> is Data:
254 ReadCheckedKeeps{-kept: @+other: U32 ->
255 {retained_observe(Storage.get_checked(depth, length, array, index, allowed, decision, balanced, valid), other) ==
256 checked_observe_array(depth, length, array, other) : Maybe<&2, F32>}}
257
258def read_checked_keeps(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32, allowed: Bool,
259 -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
260 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
261 ReadCheckedKeeps<depth, length, array, index, allowed, decision, balanced, valid>:
262 match allowed:
263 case False{}:
264 ReadCheckedKeeps{other => {==}}
265 case True{}:
266 ReadCheckedKeeps{other => Equal.trans(Maybe<&2, F32>,
267 retained_observe(Storage.finish_read(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid), other),
268 checked_observe_array(depth, length, Refinement.first(F32, Array.get(F32, array, index)), other),
269 checked_observe_array(depth, length, array, other),
270 finish_read_observe(depth, length, array, index, other, Array.get(F32, array, index), {==}, balanced, valid),
271 Equal.cong(Array<F32>, Maybe<&2, F32>, a => checked_observe_array(depth, length, a, other),
272 Refinement.first(F32, Array.get(F32, array, index)), array, Refinement.law_get_retains(F32, depth, array, index, balanced)))}
273
274type StorageReadKeeps<-original: Storage.Storage, -index: U32> is Data:
275 StorageReadKeeps{-kept: @+other: U32 ->
276 {retained_observe(Storage.get(original, index), other) == checked_observe(original, other) : Maybe<&2, F32>}}
277
278def read_checked_storage_keeps(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32,
279 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
280 certificate: ReadCheckedKeeps<depth, length, array, index, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid>) ->
281 StorageReadKeeps<Storage.Owned{depth, length, array, balanced, valid}, index>:
282 ReadCheckedKeeps{kept} = certificate
283 StorageReadKeeps{kept}
284
285def storage_read_keeps(original: Storage.Storage, +index: U32) -> StorageReadKeeps<original, index>:
286 match original:
287 case Storage.Empty{}:
288 StorageReadKeeps{other => {==}}
289 case Storage.Owned{+depth, +length, array, balanced, valid}:
290 read_checked_storage_keeps(depth, length, array, index, balanced, valid,
291 read_checked_keeps(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid))
292
293def and_left_true(+left: Bool, +right: Bool, equal: {Bool.and(left, right) == True{} : Bool}) -> {left == True{} : Bool}:
294 match left:
295 case False{}:
296 Empty.absurd({False{} == True{} : Bool}, false_true(Equal.sym(Bool, False{}, True{}, equal)))
297 case True{}:
298 {==}
299
300def and_right_true(+left: Bool, +right: Bool, equal: {Bool.and(left, right) == True{} : Bool}) -> {right == True{} : Bool}:
301 match left:
302 case False{}:
303 Empty.absurd({right == True{} : Bool}, false_true(Equal.sym(Bool, False{}, True{}, equal)))
304 case True{}:
305 equal
306
307def checked_index_allowed(+depth: Nat, +length: Nat, +index: U32,
308 +checked: {Storage.index_matches(depth, length, index) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}:
309 %natural_equal(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index),
310 Equal.sym(Bool, Nat.is_eq(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index)), True{},
311 and_left_true(Nat.is_eq(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index)),
312 Nat.is_lt(Model.offset(depth, Refinement.route(depth, index)), length), checked))) :
313 {Nat.is_lt(_, length) == True{} : Bool}
314 and_right_true(Nat.is_eq(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index)),
315 Nat.is_lt(Model.offset(depth, Refinement.route(depth, index)), length), checked)
316
317type ArrayObservationModel<-depth: Nat, -length: Nat, -array: Array<F32>, -index: U32,
318 -checked: {Storage.index_matches(depth, length, index) == True{} : Bool}> is Data:
319 ArrayObservationModel{-equal: {checked_observe_array(depth, length, array, index) ==
320 Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}}
321
322def array_observation_model(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32,
323 +checked: {Storage.index_matches(depth, length, index) == True{} : Bool}) -> ArrayObservationModel<depth, length, array, index, checked>:
324 ArrayObservationModel{
325 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), length), True{}, checked_index_allowed(depth, length, index, checked)) :
326 {observe_allowed(depth, length, array, index, _) == Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}
327 %Equal.sym(Bool, Storage.index_matches(depth, length, index), True{}, checked) :
328 {observe_index(depth, length, array, index, _) == Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}
329 {==}}