spec/lib/common.bend

bend-collections-laws-math@1.0.0.0 · 178 lines · 21 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))