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-- stdListIndex O(i)
22family StdList : Type 0
23parameter erased stdListElement : Type 0
24constructor StdListEmpty
25constructor StdListCons
26field unrestricted stdListHeadValue : stdListElement
27recursive unrestricted stdListTailValue
28
29end-family
30
31-- The number of elements.
32def stdListLength =
33 (lambda erased element : Type 0 .
34 (lambda unrestricted values : (family StdList element) .
35 (eliminate
36 StdList
37 (lambda unrestricted current : (family StdList element) . Nat)
38 values
39 (branch StdListEmpty . zero)
40 (branch StdListCons head tail induction . (succ induction)))))
41
42-- The first element, or the supplied default for an empty list.
43def stdListHeadOr =
44 (lambda erased element : Type 0 .
45 (lambda unrestricted fallback : element .
46 (lambda unrestricted values : (family StdList element) .
47 (eliminate
48 StdList
49 (lambda unrestricted current : (family StdList element) . element)
50 values
51 (branch StdListEmpty . fallback)
52 (branch StdListCons head tail induction . head)))))
53
54-- The first element as an option, so the empty case is visible in the type.
55def stdListHead =
56 (lambda erased element : Type 0 .
57 (lambda unrestricted values : (family StdList element) .
58 (eliminate
59 StdList
60 (lambda unrestricted current : (family StdList element) . (family StdOption element))
61 values
62 (branch StdListEmpty . (constructor StdOption StdNone element))
63 (branch StdListCons head tail induction . (constructor StdOption StdSome element head)))))
64
65-- Everything after the first element; the empty list has an empty tail.
66def stdListTail =
67 (lambda erased element : Type 0 .
68 (lambda unrestricted values : (family StdList element) .
69 (eliminate
70 StdList
71 (lambda unrestricted current : (family StdList element) . (family StdList element))
72 values
73 (branch StdListEmpty . (constructor StdList StdListEmpty element))
74 (branch StdListCons head tail induction . tail))))
75
76-- Is the list empty?
77def stdListIsEmpty =
78 (lambda erased element : Type 0 .
79 (lambda unrestricted values : (family StdList element) .
80 (eliminate
81 StdList
82 (lambda unrestricted current : (family StdList element) . (family StdBool))
83 values
84 (branch StdListEmpty . (constructor StdBool StdTrue))
85 (branch StdListCons head tail induction . (constructor StdBool StdFalse)))))
86
87-- The left list followed by the right one. The right list is SHARED, not
88-- copied: only the left spine is rebuilt.
89def stdListAppend =
90 (lambda erased element : Type 0 .
91 (lambda unrestricted left : (family StdList element) .
92 (lambda unrestricted right : (family StdList element) .
93 (eliminate
94 StdList
95 (lambda unrestricted current : (family StdList element) . (family StdList element))
96 left
97 (branch StdListEmpty . right)
98 (branch
99 StdListCons
100 head
101 tail
102 induction
103 .
104 (constructor StdList StdListCons element head induction))))))
105
106-- The list in the opposite order.
107def stdListReverse =
108 (lambda erased element : Type 0 .
109 (lambda unrestricted values : (family StdList element) .
110 (app
111 (eliminate
112 StdList
113 (lambda unrestricted current : (family StdList element) .
114 (pi unrestricted accumulator : (family StdList element) . (family StdList element)))
115 values
116 (branch
117 StdListEmpty
118 .
119 (lambda unrestricted accumulator : (family StdList element) . accumulator))
120 (branch
121 StdListCons
122 head
123 tail
124 induction
125 .
126 (lambda unrestricted accumulator : (family StdList element) .
127 (induction (constructor StdList StdListCons element head accumulator)))))
128 (constructor StdList StdListEmpty element))))
129
130-- Every element transformed, in order.
131def stdListMap =
132 (lambda erased element : Type 0 .
133 (lambda erased target : Type 0 .
134 (lambda unrestricted transform : (pi unrestricted value : element . target) .
135 (lambda unrestricted values : (family StdList element) .
136 (eliminate
137 StdList
138 (lambda unrestricted current : (family StdList element) . (family StdList target))
139 values
140 (branch StdListEmpty . (constructor StdList StdListEmpty target))
141 (branch
142 StdListCons
143 head
144 tail
145 induction
146 .
147 (constructor StdList StdListCons target (transform head) induction)))))))
148
149-- Fold from the right: `stdListFold f z [a, b] = f a (f b z)`.
150def stdListFold =
151 (lambda erased element : Type 0 .
152 (lambda erased accumulator : Type 0 .
153 (lambda unrestricted step : (pi unrestricted value : element . (pi unrestricted carried : accumulator . accumulator)) .
154 (lambda unrestricted initial : accumulator .
155 (lambda unrestricted values : (family StdList element) .
156 (eliminate
157 StdList
158 (lambda unrestricted current : (family StdList element) . accumulator)
159 values
160 (branch StdListEmpty . initial)
161 (branch StdListCons head tail induction . (step head induction))))))))
162
163-- The first `count` elements (all of them when the list is shorter); the
164-- structural recursion is on the count, the list is eliminated one cell at a
165-- time under it (Language & Testing Evolution L5: shrinkers halve lists).
166def stdListTake =
167 (lambda erased element : Type 0 .
168 (lambda unrestricted count : Nat .
169 (lambda unrestricted values : (family StdList element) .
170 (app
171 (nat-eliminate
172 (lambda unrestricted current : Nat .
173 (pi unrestricted remaining : (family StdList element) . (family StdList element)))
174 (lambda unrestricted remaining : (family StdList element) .
175 (constructor StdList StdListEmpty element))
176 (lambda unrestricted predecessor : Nat .
177 (lambda unrestricted induction : (pi unrestricted remaining : (family StdList element) . (family StdList element)) .
178 (lambda unrestricted remaining : (family StdList element) .
179 (eliminate
180 StdList
181 (lambda unrestricted current : (family StdList element) .
182 (family StdList element))
183 remaining
184 (branch StdListEmpty . (constructor StdList StdListEmpty element))
185 (branch
186 StdListCons
187 head
188 tail
189 tailInduction
190 .
191 (constructor StdList StdListCons element head (induction tail)))))))
192 count)
193 values))))
194
195-- Everything after the first `count` elements.
196def stdListDrop =
197 (lambda erased element : Type 0 .
198 (lambda unrestricted count : Nat .
199 (lambda unrestricted values : (family StdList element) .
200 (app
201 (nat-eliminate
202 (lambda unrestricted current : Nat .
203 (pi unrestricted remaining : (family StdList element) . (family StdList element)))
204 (lambda unrestricted remaining : (family StdList element) . remaining)
205 (lambda unrestricted predecessor : Nat .
206 (lambda unrestricted induction : (pi unrestricted remaining : (family StdList element) . (family StdList element)) .
207 (lambda unrestricted remaining : (family StdList element) .
208 (eliminate
209 StdList
210 (lambda unrestricted current : (family StdList element) .
211 (family StdList element))
212 remaining
213 (branch StdListEmpty . (constructor StdList StdListEmpty element))
214 (branch StdListCons head tail tailInduction . (induction tail))))))
215 count)
216 values))))
217
218-- The element at a position, as an option: an index past the end is absent,
219-- never an error and never a wrong element.
220def stdListIndex =
221 (lambda erased element : Type 0 .
222 (lambda unrestricted values : (family StdList element) .
223 (lambda unrestricted position : Nat .
224 (app
225 (eliminate
226 StdList
227 (lambda unrestricted current : (family StdList element) .
228 (pi unrestricted remaining : Nat . (family StdOption element)))
229 values
230 (branch
231 StdListEmpty
232 .
233 (lambda unrestricted remaining : Nat . (constructor StdOption StdNone element)))
234 (branch
235 StdListCons
236 head
237 tail
238 induction
239 .
240 (lambda unrestricted remaining : Nat .
241 (nat-eliminate
242 (lambda unrestricted current : Nat . (family StdOption element))
243 (constructor StdOption StdSome element head)
244 (lambda unrestricted predecessor : Nat .
245 (lambda unrestricted inner : (family StdOption element) .
246 (induction predecessor)))
247 remaining))))
248 position))))
249
250-- A list of the naturals below a bound, in increasing order: `[0, 1, ..., n-1]`.
251def stdListNaturalsBelow =
252 (lambda unrestricted bound : Nat .
253 (nat-eliminate
254 (lambda unrestricted current : Nat . (family StdList Nat))
255 (constructor StdList StdListEmpty Nat)
256 (lambda unrestricted predecessor : Nat .
257 (lambda unrestricted induction : (family StdList Nat) .
258 (stdListAppend
259 Nat
260 induction
261 (constructor StdList StdListCons Nat predecessor (constructor StdList StdListEmpty Nat)))))
262 bound))
263
264-- Structural equality of two lists of naturals: same length, same elements in
265-- the same order. The first list is eliminated into a FUNCTION of the second,
266-- so the recursion walks both spines together. A proof about two computed
267-- lists states this closed verdict rather than an equation between them: an
268-- equation between two lists built by the same builder is compared
269-- symbolically first (the builders' element functions, under a binder),
270-- which costs far more than computing them (Proof.CheckedHMMATile's instance
271-- words: 580 s against 34 s).
272def stdListNaturalEqual =
273 (lambda unrestricted expected : (family StdList Nat) .
274 (lambda unrestricted actual : (family StdList Nat) .
275 (app
276 (eliminate
277 StdList
278 (lambda unrestricted current : (family StdList Nat) .
279 (pi unrestricted other : (family StdList Nat) . (family StdBool)))
280 expected
281 (branch
282 StdListEmpty
283 .
284 (lambda unrestricted other : (family StdList Nat) . (stdListIsEmpty Nat other)))
285 (branch
286 StdListCons
287 head
288 tail
289 induction
290 .
291 (lambda unrestricted other : (family StdList Nat) .
292 (eliminate
293 StdList
294 (lambda unrestricted current : (family StdList Nat) . (family StdBool))
295 other
296 (branch StdListEmpty . (constructor StdBool StdFalse))
297 (branch
298 StdListCons
299 otherHead
300 otherTail
301 otherInduction
302 .
303 (stdBoolAnd
304 (stdOrderIsEqual (stdOrderCompareNatural head otherHead))
305 (induction otherTail)))))))
306 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.