1	import Base
2	
3	# Shared specification mathematics. Pure list/number definitions, written
4	# independently of every implementation module (imports only Base).
5	
6	# 2^k as a natural number.
7	def pow2(k: Nat) -> Nat:
8	  match k:
9	    case 0n:
10	      1n
11	    case 1n+p:
12	      Nat.double(pow2(p))
13	
14	# Widths without powers: x * 2^k, n div 2^k and n mod 2^k by k doublings or
15	# halvings, and "n fits k bits". A literal 2^32 or 2^64 is beyond what the
16	# proof checker expands, so the fixed-width specifications (spec/math/generic,
17	# instances, w64) state widths through these; for a symbolic k they equal the
18	# pow2 forms (proofs/math/typed/width.bend).
19	def shift(k: Nat, +x: Nat) -> Nat:
20	  match k:
21	    case 0n:
22	      x
23	    case 1n+p:
24	      Nat.double(shift(p, x))
25	
26	# n div 2 and n mod 2, structurally
27	def half(n: Nat) -> Nat:
28	  match n:
29	    case 0n:
30	      0n
31	    case 1n:
32	      0n
33	    case 2n+q:
34	      1n+half(q)
35	
36	def bit(n: Nat) -> Nat:
37	  match n:
38	    case 0n:
39	      0n
40	    case 1n:
41	      1n
42	    case 2n+q:
43	      bit(q)
44	
45	def high(k: Nat, +n: Nat) -> Nat:
46	  match k:
47	    case 0n:
48	      n
49	    case 1n+p:
50	      high(p, half(n))
51	
52	def low(k: Nat, +n: Nat) -> Nat:
53	  match k:
54	    case 0n:
55	      0n
56	    case 1n+p:
57	      Nat.add(bit(n), Nat.double(low(p, half(n))))
58	
59	# n < 2^k
60	def fits(+k: Nat, +n: Nat) -> Bool:
61	  Nat.is_eq(high(k, n), 0n)
62	
63	def length(-A: Data, xs: List<&2, A>) -> Nat:
64	  match xs:
65	    case Nil{}:
66	      0n
67	    case Con{h, t}:
68	      1n+length(A, t)
69	
70	# Element i, if any.
71	def nth(-A: Data, xs: List<&2, A>, i: Nat) -> Maybe<&2, A>:
72	  match xs i:
73	    case Nil{} _:
74	      None{}
75	    case Con{h, t} 0n:
76	      Some{h}
77	    case Con{h, t} 1n+p:
78	      nth(A, t, p)
79	
80	# Replace element i (no change when i is out of range).
81	def update(-A: Data, xs: List<&2, A>, i: Nat, x: A) -> List<&2, A>:
82	  match xs i:
83	    case Nil{} _:
84	      Nil{}
85	    case Con{h, t} 0n:
86	      Con{x, t}
87	    case Con{h, t} 1n+p:
88	      Con{h, update(A, t, p, x)}
89	
90	def snoc(-A: Data, xs: List<&2, A>, x: A) -> List<&2, A>:
91	  match xs:
92	    case Nil{}:
93	      Con{x, Nil{}}
94	    case Con{h, t}:
95	      Con{h, snoc(A, t, x)}
96	
97	def last(-A: Data, xs: List<&2, A>) -> Maybe<&2, A>:
98	  match xs:
99	    case Nil{}:
100	      None{}
101	    case Con{h, t}:
102	      match t:
103	        case Nil{}:
104	          Some{h}
105	        case Con{h2, t2}:
106	          last(A, Con{h2, t2})
107	
108	def init(-A: Data, xs: List<&2, A>) -> List<&2, A>:
109	  match xs:
110	    case Nil{}:
111	      Nil{}
112	    case Con{h, t}:
113	      match t:
114	        case Nil{}:
115	          Nil{}
116	        case Con{h2, t2}:
117	          Con{h, init(A, Con{h2, t2})}
118	
119	def head(-A: Data, xs: List<&2, A>) -> Maybe<&2, A>:
120	  match xs:
121	    case Nil{}:
122	      None{}
123	    case Con{h, t}:
124	      Some{h}
125	
126	def tail(-A: Data, xs: List<&2, A>) -> List<&2, A>:
127	  match xs:
128	    case Nil{}:
129	      Nil{}
130	    case Con{h, t}:
131	      t
132	
133	def append(-A: Data, xs: List<&2, A>, ys: List<&2, A>) -> List<&2, A>:
134	  match xs:
135	    case Nil{}:
136	      ys
137	    case Con{h, t}:
138	      Con{h, append(A, t, ys)}
139	
140	def reverse(-A: Data, xs: List<&2, A>) -> List<&2, A>:
141	  match xs:
142	    case Nil{}:
143	      Nil{}
144	    case Con{h, t}:
145	      snoc(A, reverse(A, t), h)
146	
147	def replicate(-A: Data, n: Nat, +x: A) -> List<&2, A>:
148	  match n:
149	    case 0n:
150	      Nil{}
151	    case 1n+p:
152	      Con{x, replicate(A, p, x)}
153	
154	def take(-A: Data, xs: List<&2, A>, n: Nat) -> List<&2, A>:
155	  match xs n:
156	    case Nil{} _:
157	      Nil{}
158	    case Con{h, t} 0n:
159	      Nil{}
160	    case Con{h, t} 1n+p:
161	      Con{h, take(A, t, p)}
162	
163	def drop(-A: Data, xs: List<&2, A>, n: Nat) -> List<&2, A>:
164	  match xs n:
165	    case Nil{} _:
166	      Nil{}
167	    case Con{h, t} 0n:
168	      Con{h, t}
169	    case Con{h, t} 1n+p:
170	      drop(A, t, p)
171	
172	# membership of a natural number in a list of them
173	def memn(+s: Nat, xs: List<&2, Nat>) -> Bool:
174	  match xs:
175	    case Nil{}:
176	      False{}
177	    case Con{+x, t}:
178	      Bool.or(Nat.is_eq(x, s), memn(s, t))