1	import Base
2	import ./nat.bend as Nat
3	
4	# vec.bend: lists whose length is part of their type.
5	#
6	#   import ./vec.bend as Vec
7	#
8	# Vec(A, n) is computed from n: Unit at 0n, a pair of an A and a
9	# Vec(A, p) at 1n+p. Matching on n tells the checker the vector's shape,
10	# so zip_with has no length-mismatch case and get has no out-of-bounds
11	# case: at n = 0n its bound Nat.LT(i, 0n) is Empty.
12	#
13	# Indexing is O(i) and every element is a separate pair. For large numeric
14	# data use Array.
15	
16	def Vec(-A: Data, n: Nat) -> Data:
17	  match n:
18	    case 0n:
19	      Unit
20	    case 1n+p:
21	      Sigma<&2, &2, A, _ => Vec(A, p)>
22	
23	# a list as a Vec of its own length
24	def from_list(-A: Data, xs: List<&2, A>) -> Vec(A, List.length(&2, A, xs)):
25	  match xs:
26	    case Nil{}:
27	      Unit{}
28	    case h <> t:
29	      (h, from_list(A, t))
30	
31	def get(-A: Data, n: Nat, v: Vec(A, n), i: Nat, lt: Nat.LT(i, n)) -> A:
32	  match n:
33	    case 0n:
34	      match lt:
35	    case 1n+p:
36	      (h, t) = v
37	      match i:
38	        case 0n:
39	          h
40	        case 1n+j:
41	          get(A, p, t, j, lt)
42	
43	def zip_with(~A: Data, ~B: Data, ~C: Data, ~f: A -> B -> C, n: Nat, xs: Vec(A, n), ys: Vec(B, n)) -> Vec(C, n):
44	  match n:
45	    case 0n:
46	      Unit{}
47	    case 1n+p:
48	      (x, xt) = xs
49	      (y, yt) = ys
50	      (f(x, y), zip_with(~A, ~B, ~C, ~f, p, xt, yt))
51	
52	def foldr(~A: Data, ~B: Data, ~f: A -> B -> B, n: Nat, v: Vec(A, n), z: B) -> B:
53	  match n:
54	    case 0n:
55	      z
56	    case 1n+p:
57	      (h, t) = v
58	      f(h, foldr(~A, ~B, ~f, p, t, z))