spec/lib/common.bend
bend-collections-laws-containers@1.0.0.0 · 178 lines · 0 definitions
1import 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.
7def 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).
19def 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
27def 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
36def 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
45def high(k: Nat, +n: Nat) -> Nat:
46 match k:
47 case 0n:
48 n
49 case 1n+p:
50 high(p, half(n))
51
52def 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
60def fits(+k: Nat, +n: Nat) -> Bool:
61 Nat.is_eq(high(k, n), 0n)
62
63def 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.
71def 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).
81def 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
90def 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
97def 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
108def 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
119def 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
126def 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
133def 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
140def 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
147def 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
154def 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
163def 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
173def 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))