1module Std.List
2
3import Std.Foundation
4
5-- Structural lists (Language Platform PRD §28.2 Collections, LP-802).
6--
7-- This is the small structural sequence: cheap to build, cheap to walk, and
8-- shared rather than copied — appending to a list keeps the original intact
9-- because the tail is shared, which is the sharing property §28.4 requires.
10-- Iteration is deterministic by construction: a list has one order, the one
11-- it was built in.
12--
13-- Asymptotic contract (§28.4 requires it to be explicit):
14-- stdListCons O(1)
15-- stdListHead O(1)
16-- stdListLength O(n)
17-- stdListAppend O(n) in the left list, sharing the right one
18-- stdListReverse O(n)
19-- stdListMap O(n)
20-- stdListFold O(n)
21-- stdListFoldFromHead O(n)
22-- stdListZipWith O(min(n, m))
23-- stdListIndex O(i)
24family StdList : Type 0
25parameter erased stdListElement : Type 0
26constructor StdListEmpty
27constructor StdListCons
28field unrestricted stdListHeadValue : stdListElement
29recursive unrestricted stdListTailValue
30
31end-family
32
33-- The number of elements.
34def stdListLength =
35 (lambda erased element : Type 0 .
36 (lambda unrestricted values : (family StdList element) .
37 (eliminate
38 StdList
39 (lambda unrestricted current : (family StdList element) . Nat)
40 values
41 (branch StdListEmpty . zero)
42 (branch StdListCons head tail induction . (succ induction)))))
43
44-- The first element, or the supplied default for an empty list.
45def stdListHeadOr =
46 (lambda erased element : Type 0 .
47 (lambda unrestricted fallback : element .
48 (lambda unrestricted values : (family StdList element) .
49 (eliminate
50 StdList
51 (lambda unrestricted current : (family StdList element) . element)
52 values
53 (branch StdListEmpty . fallback)
54 (branch StdListCons head tail induction . head)))))
55
56-- The first element as an option, so the empty case is visible in the type.
57def stdListHead =
58 (lambda erased element : Type 0 .
59 (lambda unrestricted values : (family StdList element) .
60 (eliminate
61 StdList
62 (lambda unrestricted current : (family StdList element) . (family StdOption element))
63 values
64 (branch StdListEmpty . (constructor StdOption StdNone element))
65 (branch StdListCons head tail induction . (constructor StdOption StdSome element head)))))
66
67-- Everything after the first element; the empty list has an empty tail.
68def stdListTail =
69 (lambda erased element : Type 0 .
70 (lambda unrestricted values : (family StdList element) .
71 (eliminate
72 StdList
73 (lambda unrestricted current : (family StdList element) . (family StdList element))
74 values
75 (branch StdListEmpty . (constructor StdList StdListEmpty element))
76 (branch StdListCons head tail induction . tail))))
77
78-- Is the list empty?
79def stdListIsEmpty =
80 (lambda erased element : Type 0 .
81 (lambda unrestricted values : (family StdList element) .
82 (eliminate
83 StdList
84 (lambda unrestricted current : (family StdList element) . (family StdBool))
85 values
86 (branch StdListEmpty . (constructor StdBool StdTrue))
87 (branch StdListCons head tail induction . (constructor StdBool StdFalse)))))
88
89-- The left list followed by the right one. The right list is SHARED, not
90-- copied: only the left spine is rebuilt.
91def stdListAppend =
92 (lambda erased element : Type 0 .
93 (lambda unrestricted left : (family StdList element) .
94 (lambda unrestricted right : (family StdList element) .
95 (eliminate
96 StdList
97 (lambda unrestricted current : (family StdList element) . (family StdList element))
98 left
99 (branch StdListEmpty . right)
100 (branch
101 StdListCons
102 head
103 tail
104 induction
105 .
106 (constructor StdList StdListCons element head induction))))))
107
108-- The list in the opposite order.
109def stdListReverse =
110 (lambda erased element : Type 0 .
111 (lambda unrestricted values : (family StdList element) .
112 (app
113 (eliminate
114 StdList
115 (lambda unrestricted current : (family StdList element) .
116 (pi unrestricted accumulator : (family StdList element) . (family StdList element)))
117 values
118 (branch
119 StdListEmpty
120 .
121 (lambda unrestricted accumulator : (family StdList element) . accumulator))
122 (branch
123 StdListCons
124 head
125 tail
126 induction
127 .
128 (lambda unrestricted accumulator : (family StdList element) .
129 (induction (constructor StdList StdListCons element head accumulator)))))
130 (constructor StdList StdListEmpty element))))
131
132-- Every element transformed, in order.
133def stdListMap =
134 (lambda erased element : Type 0 .
135 (lambda erased target : Type 0 .
136 (lambda unrestricted transform : (pi unrestricted value : element . target) .
137 (lambda unrestricted values : (family StdList element) .
138 (eliminate
139 StdList
140 (lambda unrestricted current : (family StdList element) . (family StdList target))
141 values
142 (branch StdListEmpty . (constructor StdList StdListEmpty target))
143 (branch
144 StdListCons
145 head
146 tail
147 induction
148 .
149 (constructor StdList StdListCons target (transform head) induction)))))))
150
151-- Fold from the right: `stdListFold f z [a, b] = f a (f b z)`.
152def stdListFold =
153 (lambda erased element : Type 0 .
154 (lambda erased accumulator : Type 0 .
155 (lambda unrestricted step : (pi unrestricted value : element . (pi unrestricted carried : accumulator . accumulator)) .
156 (lambda unrestricted initial : accumulator .
157 (lambda unrestricted values : (family StdList element) .
158 (eliminate
159 StdList
160 (lambda unrestricted current : (family StdList element) . accumulator)
161 values
162 (branch StdListEmpty . initial)
163 (branch StdListCons head tail induction . (step head induction))))))))
164
165-- Fold from the head: `step (... (step (step initial x0) x1) ...) xn`.
166-- stdListFold visits the LAST element first (its step sees the folded tail);
167-- this visits the FIRST element first and threads the accumulator forward,
168-- which is the order a floating-point accumulation or a reverse-time pass over
169-- a newest-first history must respect (the results differ when the step does
170-- not associate, e.g. f32 addition). The list is eliminated into a function of
171-- the accumulator, so the recursion is still structural.
172def stdListFoldFromHead =
173 (lambda erased element : Type 0 .
174 (lambda erased accumulator : Type 0 .
175 (lambda unrestricted step : (pi unrestricted carried : accumulator . (pi unrestricted value : element . accumulator)) .
176 (lambda unrestricted initial : accumulator .
177 (lambda unrestricted values : (family StdList element) .
178 (app
179 (eliminate
180 StdList
181 (lambda unrestricted current : (family StdList element) . (pi unrestricted carried : accumulator . accumulator))
182 values
183 (branch StdListEmpty . (lambda unrestricted carried : accumulator . carried))
184 (branch StdListCons head tail induction .
185 (lambda unrestricted carried : accumulator . (induction (step carried head)))))
186 initial))))))
187
188-- Combine two lists position by position, keeping their order; the result is
189-- as long as the SHORTER list (the rest of the longer one is dropped -- callers
190-- that need equal lengths must establish them). The left list is eliminated
191-- into a function of the right one, so both spines are walked together.
192def stdListZipWith =
193 (lambda erased left : Type 0 .
194 (lambda erased right : Type 0 .
195 (lambda erased result : Type 0 .
196 (lambda unrestricted combine : (pi unrestricted l : left . (pi unrestricted r : right . result)) .
197 (lambda unrestricted lefts : (family StdList left) .
198 (lambda unrestricted rights : (family StdList right) .
199 (app
200 (eliminate
201 StdList
202 (lambda unrestricted current : (family StdList left) .
203 (pi unrestricted others : (family StdList right) . (family StdList result)))
204 lefts
205 (branch StdListEmpty .
206 (lambda unrestricted others : (family StdList right) . (constructor StdList StdListEmpty result)))
207 (branch StdListCons head tail induction .
208 (lambda unrestricted others : (family StdList right) .
209 (eliminate
210 StdList
211 (lambda unrestricted inner : (family StdList right) . (family StdList result))
212 others
213 (branch StdListEmpty . (constructor StdList StdListEmpty result))
214 (branch StdListCons otherHead otherTail otherInduction .
215 (constructor StdList StdListCons result (combine head otherHead) (induction otherTail)))))))
216 rights)))))))
217
218-- The first `count` elements (all of them when the list is shorter); the
219-- structural recursion is on the count, the list is eliminated one cell at a
220-- time under it (Language & Testing Evolution L5: shrinkers halve lists).
221def stdListTake =
222 (lambda erased element : Type 0 .
223 (lambda unrestricted count : Nat .
224 (lambda unrestricted values : (family StdList element) .
225 (app
226 (nat-eliminate
227 (lambda unrestricted current : Nat .
228 (pi unrestricted remaining : (family StdList element) . (family StdList element)))
229 (lambda unrestricted remaining : (family StdList element) .
230 (constructor StdList StdListEmpty element))
231 (lambda unrestricted predecessor : Nat .
232 (lambda unrestricted induction : (pi unrestricted remaining : (family StdList element) . (family StdList element)) .
233 (lambda unrestricted remaining : (family StdList element) .
234 (eliminate
235 StdList
236 (lambda unrestricted current : (family StdList element) .
237 (family StdList element))
238 remaining
239 (branch StdListEmpty . (constructor StdList StdListEmpty element))
240 (branch
241 StdListCons
242 head
243 tail
244 tailInduction
245 .
246 (constructor StdList StdListCons element head (induction tail)))))))
247 count)
248 values))))
249
250-- Everything after the first `count` elements.
251def stdListDrop =
252 (lambda erased element : Type 0 .
253 (lambda unrestricted count : Nat .
254 (lambda unrestricted values : (family StdList element) .
255 (app
256 (nat-eliminate
257 (lambda unrestricted current : Nat .
258 (pi unrestricted remaining : (family StdList element) . (family StdList element)))
259 (lambda unrestricted remaining : (family StdList element) . remaining)
260 (lambda unrestricted predecessor : Nat .
261 (lambda unrestricted induction : (pi unrestricted remaining : (family StdList element) . (family StdList element)) .
262 (lambda unrestricted remaining : (family StdList element) .
263 (eliminate
264 StdList
265 (lambda unrestricted current : (family StdList element) .
266 (family StdList element))
267 remaining
268 (branch StdListEmpty . (constructor StdList StdListEmpty element))
269 (branch StdListCons head tail tailInduction . (induction tail))))))
270 count)
271 values))))
272
273-- The element at a position, as an option: an index past the end is absent,
274-- never an error and never a wrong element.
275def stdListIndex =
276 (lambda erased element : Type 0 .
277 (lambda unrestricted values : (family StdList element) .
278 (lambda unrestricted position : Nat .
279 (app
280 (eliminate
281 StdList
282 (lambda unrestricted current : (family StdList element) .
283 (pi unrestricted remaining : Nat . (family StdOption element)))
284 values
285 (branch
286 StdListEmpty
287 .
288 (lambda unrestricted remaining : Nat . (constructor StdOption StdNone element)))
289 (branch
290 StdListCons
291 head
292 tail
293 induction
294 .
295 (lambda unrestricted remaining : Nat .
296 (nat-eliminate
297 (lambda unrestricted current : Nat . (family StdOption element))
298 (constructor StdOption StdSome element head)
299 (lambda unrestricted predecessor : Nat .
300 (lambda unrestricted inner : (family StdOption element) .
301 (induction predecessor)))
302 remaining))))
303 position))))
304
305-- A list of the naturals below a bound, in increasing order: `[0, 1, ..., n-1]`.
306def stdListNaturalsBelow =
307 (lambda unrestricted bound : Nat .
308 (nat-eliminate
309 (lambda unrestricted current : Nat . (family StdList Nat))
310 (constructor StdList StdListEmpty Nat)
311 (lambda unrestricted predecessor : Nat .
312 (lambda unrestricted induction : (family StdList Nat) .
313 (stdListAppend
314 Nat
315 induction
316 (constructor StdList StdListCons Nat predecessor (constructor StdList StdListEmpty Nat)))))
317 bound))
318
319-- Structural equality of two lists of naturals: same length, same elements in
320-- the same order. The first list is eliminated into a FUNCTION of the second,
321-- so the recursion walks both spines together. A proof about two computed
322-- lists states this closed verdict rather than an equation between them: an
323-- equation between two lists built by the same builder is compared
324-- symbolically first (the builders' element functions, under a binder),
325-- which costs far more than computing them (Proof.CheckedHMMATile's instance
326-- words: 580 s against 34 s).
327def stdListNaturalEqual =
328 (lambda unrestricted expected : (family StdList Nat) .
329 (lambda unrestricted actual : (family StdList Nat) .
330 (app
331 (eliminate
332 StdList
333 (lambda unrestricted current : (family StdList Nat) .
334 (pi unrestricted other : (family StdList Nat) . (family StdBool)))
335 expected
336 (branch
337 StdListEmpty
338 .
339 (lambda unrestricted other : (family StdList Nat) . (stdListIsEmpty Nat other)))
340 (branch
341 StdListCons
342 head
343 tail
344 induction
345 .
346 (lambda unrestricted other : (family StdList Nat) .
347 (eliminate
348 StdList
349 (lambda unrestricted current : (family StdList Nat) . (family StdBool))
350 other
351 (branch StdListEmpty . (constructor StdBool StdFalse))
352 (branch
353 StdListCons
354 otherHead
355 otherTail
356 otherInduction
357 .
358 (stdBoolAnd
359 (stdOrderIsEqual (stdOrderCompareNatural head otherHead))
360 (induction otherTail)))))))
361 actual)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.