1	import Base
2	import ./model.bend as Model
3	import ./array.bend as ArrayModel
4	import ./refinement.bend as Refinement
5	import ./certificates.bend as Certificates
6	
7	type Error is Data:
8	  TooLarge{}
9	  OutOfBounds{}
10	  InvalidIndex{}
11	
12	def 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	
15	type 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	
21	def 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	
31	def 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	
40	def 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	
45	def 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	
54	def new(+n: U32, value: F32) -> Result<&2, &1, Error, Storage>:
55	  new_checked(U32.to_nat(n), value, U32.is_le(n, 1048576))
56	
57	def 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	
61	def 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	
68	def 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	
78	def 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	
85	def 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	
91	def 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	
101	def 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	
108	def 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	
115	def 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	
122	def 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)