src/storage/main.bend
bendtorch-core@0.1.0.0 · 127 lines · 18 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
3import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayModel
4import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
5import bendtorch-core@0.1.0.0/src/storage/certificates.bend as Certificates
6
7type Error is Data:
8 TooLarge{}
9 OutOfBounds{}
10 InvalidIndex{}
11
12def bounds(+d: Nat, +n: Nat) -> Bool:
13 Bool.and(Nat.is_le(d, 20n), Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d))))
14
15type Storage is Type:
16 Empty{}
17 Owned{depth: Nat, length: Nat, array: Array<F32>,
18 -balanced: Model.Balanced(F32, depth, array),
19 -bounds: {bounds(depth, length) == True{} : Bool}}
20
21def depth_seek(fuel: Nat, +n: Nat, +depth: Nat, +capacity: Nat, done: Bool) -> Nat & Nat:
22 match fuel done:
23 case 0n _:
24 (depth, capacity)
25 case 1n+p True{}:
26 (depth, capacity)
27 case 1n+p False{}:
28 +next = Nat.add(capacity, capacity)
29 depth_seek(p, n, 1n+depth, next, Nat.is_le(n, next))
30
31def allocate(+d: Nat, +n: Nat, +value: F32, valid: Bool,
32 -decision: {valid == bounds(d, n) : Bool}) -> Result<&2, &1, Error, Storage>:
33 match valid:
34 case False{}:
35 Fail{TooLarge{}}
36 case True{}:
37 Done{Owned{d, n, Array.new(F32, d, value), ArrayModel.new_balanced(F32, d, value),
38 Equal.sym(Bool, True{}, bounds(d, n), decision)}}
39
40def allocate_at(+n: Nat, value: F32, metadata: Nat & Nat) -> Result<&2, &1, Error, Storage>:
41 (d0, capacity) = metadata
42 +d = d0
43 allocate(d, n, value, bounds(d, n), {==})
44
45def new_checked(+n: Nat, value: F32, allowed: Bool) -> Result<&2, &1, Error, Storage>:
46 match n allowed:
47 case 0n _:
48 Done{Empty{}}
49 case 1n+p False{}:
50 Fail{TooLarge{}}
51 case 1n+p True{}:
52 allocate_at(n, value, depth_seek(20n, n, 0n, 1n, Nat.is_le(n, 1n)))
53
54def new(+n: U32, value: F32) -> Result<&2, &1, Error, Storage>:
55 new_checked(U32.to_nat(n), value, U32.is_le(n, 1048576))
56
57def index_matches(+d: Nat, +n: Nat, +i: U32) -> Bool:
58 +offset = Model.offset(d, Refinement.route(d, i))
59 Bool.and(Nat.is_eq(offset, U32.to_nat(i)), Nat.is_lt(offset, n))
60
61def finish_read(+d: Nat, n: Nat, -original: Array<F32>, -i: U32,
62 result: Array<F32> & F32, -exact: {result == Array.get(F32, original, i) : Array<F32> & F32},
63 -balanced: Model.Balanced(F32, d, original), -valid: {bounds(d, n) == True{} : Bool}) ->
64 Storage & Result<&2, &2, Error, F32>:
65 (array, value) = result
66 (Owned{d, n, array, Certificates.get_result(F32, d, original, i, (array, value), exact, balanced), valid}, Done{value})
67
68def get_checked(+d: Nat, +n: Nat, array: Array<F32>, +i: U32, allowed: Bool,
69 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
70 -balanced: Model.Balanced(F32, d, array), -valid: {bounds(d, n) == True{} : Bool}) ->
71 Storage & Result<&2, &2, Error, F32>:
72 match allowed:
73 case False{}:
74 (Owned{d, n, array, balanced, valid}, Fail{OutOfBounds{}})
75 case True{}:
76 finish_read(d, n, array, i, Array.get(F32, array, i), {==}, balanced, valid)
77
78def get(storage: Storage, +i: U32) -> Storage & Result<&2, &2, Error, F32>:
79 match storage:
80 case Empty{}:
81 (Empty{}, Fail{OutOfBounds{}})
82 case Owned{+d, +n, array, balanced, valid}:
83 get_checked(d, n, array, i, Nat.is_lt(U32.to_nat(i), n), {==}, balanced, valid)
84
85def finish_write(+d: Nat, n: Nat, -original: Array<F32>, -i: U32, -value: F32,
86 array: Array<F32>, -exact: {array == Array.set(F32, original, i, value) : Array<F32>},
87 -balanced: Model.Balanced(F32, d, original), -valid: {bounds(d, n) == True{} : Bool}) ->
88 Storage & Result<&2, &2, Error, Unit>:
89 (Owned{d, n, array, Certificates.set_result(F32, d, original, i, value, array, exact, balanced), valid}, Done{Unit{}})
90
91def set_checked(+d: Nat, +n: Nat, array: Array<F32>, +i: U32, value: F32, allowed: Bool,
92 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
93 -balanced: Model.Balanced(F32, d, array), -valid: {bounds(d, n) == True{} : Bool}) ->
94 Storage & Result<&2, &2, Error, Unit>:
95 match allowed:
96 case False{}:
97 (Owned{d, n, array, balanced, valid}, Fail{OutOfBounds{}})
98 case True{}:
99 finish_write(d, n, array, i, value, Array.set(F32, array, i, value), {==}, balanced, valid)
100
101def set(storage: Storage, +i: U32, value: F32) -> Storage & Result<&2, &2, Error, Unit>:
102 match storage:
103 case Empty{}:
104 (Empty{}, Fail{OutOfBounds{}})
105 case Owned{+d, +n, array, balanced, valid}:
106 set_checked(d, n, array, i, value, Nat.is_lt(U32.to_nat(i), n), {==}, balanced, valid)
107
108def finish_clone(+d: Nat, +n: Nat, -original: Array<F32>, pair: Array<F32> & Array<F32>,
109 -exact: {pair == Array.clone(F32, original) : Array<F32> & Array<F32>},
110 -balanced: Model.Balanced(F32, d, original), -valid: {bounds(d, n) == True{} : Bool}) -> Storage & Storage:
111 (first, second) = pair
112 (Owned{d, n, first, Certificates.clone_first(F32, d, original, (first, second), exact, balanced), valid},
113 Owned{d, n, second, Certificates.clone_second(F32, d, original, (first, second), exact, balanced), valid})
114
115def clone(storage: Storage) -> Storage & Storage:
116 match storage:
117 case Empty{}:
118 (Empty{}, Empty{})
119 case Owned{+d, +n, array, balanced, valid}:
120 finish_clone(d, n, array, Array.clone(F32, array), {==}, balanced, valid)
121
122def length(storage: Storage) -> Storage & Nat:
123 match storage:
124 case Empty{}:
125 (Empty{}, 0n)
126 case Owned{+d, +n, array, balanced, valid}:
127 (Owned{d, n, array, balanced, valid}, n)