1	# Vec: a growable array. push is amortized O(1): a full buffer doubles.
2	#
3	# get, set and pop are one Array access. An index at or past the length
4	# answers None (get, pop) or leaves the vector as it was (set).
5	import Base
6	
7	type Vec<-T: Data> is Type:
8	  VNil{}
9	  Vec{len: U32, buf: Array<T>}
10	
11	def Vec.new(~T: Data) -> Vec<T>:
12	  VNil{}
13	
14	def Vec.len(~T: Data, v: Vec<T>) -> Vec<T> & U32:
15	  match v:
16	    case VNil{}:
17	      (VNil{}, 0)
18	    case Vec{+n, buf}:
19	      (Vec{n, buf}, n)
20	
21	def Vec.copy(
22	  ~T: Data, fuel: Nat, +i: U32, dst: Array<T>, r: Array<T> & T
23	) -> Array<T>:
24	  match fuel:
25	    case 0n:
26	      dst
27	    case 1n+p:
28	      (src, x) = r
29	      +j = U32.inc(i)
30	      Vec.copy(~T, p, j, Array.set(T, dst, i, x), Array.get(T, src, j))
31	
32	def Vec.push.grow(
33	  ~T: Data, full: Bool, +n: U32, +x: T, buf: Array<T>, +cap: U32
34	) -> Vec<T>:
35	  match full:
36	    case False{}:
37	      Vec{U32.inc(n), Array.set(T, buf, n, x)}
38	    case True{}:
39	      # Every slot of big starts as x, so slot n needs no write.
40	      big = Array.new(T, 1n+U32.log2(cap), x)
41	      Vec{U32.inc(n), Vec.copy(~T, U32.to_nat(n), 0, big, Array.get(T, buf, 0))}
42	
43	def Vec.push.at(~T: Data, +n: U32, +x: T, bc: Array<T> & U32) -> Vec<T>:
44	  (buf, +cap) = bc
45	  Vec.push.grow(~T, U32.is_eq(n, cap), n, x, buf, cap)
46	
47	def Vec.push(~T: Data, v: Vec<T>, +x: T) -> Vec<T>:
48	  match v:
49	    case VNil{}:
50	      Vec{1, ALeaf{x}}
51	    case Vec{+n, buf}:
52	      Vec.push.at(~T, n, x, Array.size(T, buf))
53	
54	def Vec.get.fin(~T: Data, n: U32, r: Array<T> & T) -> Vec<T> & Maybe<&2, T>:
55	  (buf, x) = r
56	  (Vec{n, buf}, Some{x})
57	
58	def Vec.get.if(
59	  ~T: Data, ok: Bool, +n: U32, buf: Array<T>, +i: U32
60	) -> Vec<T> & Maybe<&2, T>:
61	  match ok:
62	    case True{}:
63	      Vec.get.fin(~T, n, Array.get(T, buf, i))
64	    case False{}:
65	      (Vec{n, buf}, None{})
66	
67	def Vec.get(~T: Data, v: Vec<T>, +i: U32) -> Vec<T> & Maybe<&2, T>:
68	  match v:
69	    case VNil{}:
70	      (VNil{}, None{})
71	    case Vec{+n, buf}:
72	      Vec.get.if(~T, U32.is_lt(i, n), n, buf, i)
73	
74	def Vec.set.if(
75	  ~T: Data, ok: Bool, n: U32, buf: Array<T>, i: U32, x: T
76	) -> Vec<T>:
77	  match ok:
78	    case True{}:
79	      Vec{n, Array.set(T, buf, i, x)}
80	    case False{}:
81	      Vec{n, buf}
82	
83	def Vec.set(~T: Data, v: Vec<T>, +i: U32, x: T) -> Vec<T>:
84	  match v:
85	    case VNil{}:
86	      VNil{}
87	    case Vec{+n, buf}:
88	      Vec.set.if(~T, U32.is_lt(i, n), n, buf, i, x)
89	
90	def Vec.pop.if(
91	  ~T: Data, empty: Bool, +n: U32, buf: Array<T>
92	) -> Vec<T> & Maybe<&2, T>:
93	  match empty:
94	    case True{}:
95	      (Vec{n, buf}, None{})
96	    case False{}:
97	      +m = (n - 1 : U32)
98	      Vec.get.fin(~T, m, Array.get(T, buf, m))
99	
100	# The last element, and the vector without it. The buffer keeps its size.
101	def Vec.pop(~T: Data, v: Vec<T>) -> Vec<T> & Maybe<&2, T>:
102	  match v:
103	    case VNil{}:
104	      (VNil{}, None{})
105	    case Vec{+n, buf}:
106	      Vec.pop.if(~T, U32.is_zero(n), n, buf)
107	
108	def Vec.to_list.go(
109	  ~T: Data, fuel: Nat, +i: U32, acc: List<&2, T>, r: Array<T> & T
110	) -> List<&2, T>:
111	  match fuel:
112	    case 0n:
113	      acc
114	    case 1n+p:
115	      (buf, x) = r
116	      +j = (i - 1 : U32)
117	      Vec.to_list.go(~T, p, j, x <> acc, Array.get(T, buf, j))
118	
119	# The elements, first to last.
120	def Vec.to_list(~T: Data, v: Vec<T>) -> List<&2, T>:
121	  match v:
122	    case VNil{}:
123	      Nil{}
124	    case Vec{+n, buf}:
125	      +last = (n - 1 : U32)
126	      Vec.to_list.go(~T, U32.to_nat(n), last, Nil{}, Array.get(T, buf, last))
127	
128	def Vec.from_list.go(~T: Data, xs: List<&2, T>, v: Vec<T>) -> Vec<T>:
129	  match xs:
130	    case Nil{}:
131	      v
132	    case h <> t:
133	      Vec.from_list.go(~T, t, Vec.push(~T, v, h))
134	
135	def Vec.from_list(~T: Data, xs: List<&2, T>) -> Vec<T>:
136	  Vec.from_list.go(~T, xs, VNil{})