Mercurial > cpdt > repo
comparison src/DataStruct.v @ 463:218361342cd2
Proofreading pass through Chapter 17
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 29 Aug 2012 17:03:19 -0400 |
parents | b1fead9f68f2 |
children | 1fd4109f7b31 |
comparison
equal
deleted
inserted
replaced
462:d7a73ab1df7b | 463:218361342cd2 |
---|---|
207 | 207 |
208 (* begin thide *) | 208 (* begin thide *) |
209 Variable elm : A. | 209 Variable elm : A. |
210 | 210 |
211 Inductive member : list A -> Type := | 211 Inductive member : list A -> Type := |
212 | MFirst : forall ls, member (elm :: ls) | 212 | HFirst : forall ls, member (elm :: ls) |
213 | MNext : forall x ls, member ls -> member (x :: ls). | 213 | HNext : forall x ls, member ls -> member (x :: ls). |
214 | 214 |
215 (** Because the element [elm] that we are "searching for" in a list does not change across the constructors of [member], we simplify our definitions by making [elm] a local variable. In the definition of [member], we say that [elm] is found in any list that begins with [elm], and, if removing the first element of a list leaves [elm] present, then [elm] is present in the original list, too. The form looks much like a predicate for list membership, but we purposely define [member] in [Type] so that we may decompose its values to guide computations. | 215 (** Because the element [elm] that we are "searching for" in a list does not change across the constructors of [member], we simplify our definitions by making [elm] a local variable. In the definition of [member], we say that [elm] is found in any list that begins with [elm], and, if removing the first element of a list leaves [elm] present, then [elm] is present in the original list, too. The form looks much like a predicate for list membership, but we purposely define [member] in [Type] so that we may decompose its values to guide computations. |
216 | 216 |
217 We can use [member] to adapt our definition of [get] to [hlist]s. The same basic [match] tricks apply. In the [HCons] case, we form a two-element convoy, passing both the data element [x] and the recursor for the sublist [mls'] to the result of the inner [match]. We did not need to do that in [get]'s definition because the types of list elements were not dependent there. *) | 217 We can use [member] to adapt our definition of [get] to [hlist]s. The same basic [match] tricks apply. In the [HCons] case, we form a two-element convoy, passing both the data element [x] and the recursor for the sublist [mls'] to the result of the inner [match]. We did not need to do that in [get]'s definition because the types of list elements were not dependent there. *) |
218 | 218 |
221 | HNil => fun mem => | 221 | HNil => fun mem => |
222 match mem in member ls' return (match ls' with | 222 match mem in member ls' return (match ls' with |
223 | nil => B elm | 223 | nil => B elm |
224 | _ :: _ => unit | 224 | _ :: _ => unit |
225 end) with | 225 end) with |
226 | MFirst _ => tt | 226 | HFirst _ => tt |
227 | MNext _ _ _ => tt | 227 | HNext _ _ _ => tt |
228 end | 228 end |
229 | HCons _ _ x mls' => fun mem => | 229 | HCons _ _ x mls' => fun mem => |
230 match mem in member ls' return (match ls' with | 230 match mem in member ls' return (match ls' with |
231 | nil => Empty_set | 231 | nil => Empty_set |
232 | x' :: ls'' => | 232 | x' :: ls'' => |
233 B x' -> (member ls'' -> B elm) | 233 B x' -> (member ls'' -> B elm) |
234 -> B elm | 234 -> B elm |
235 end) with | 235 end) with |
236 | MFirst _ => fun x _ => x | 236 | HFirst _ => fun x _ => x |
237 | MNext _ _ mem' => fun _ get_mls' => get_mls' mem' | 237 | HNext _ _ mem' => fun _ get_mls' => get_mls' mem' |
238 end x (hget mls') | 238 end x (hget mls') |
239 end. | 239 end. |
240 (* end thide *) | 240 (* end thide *) |
241 End hlist. | 241 End hlist. |
242 | 242 |
243 (* begin thide *) | 243 (* begin thide *) |
244 Implicit Arguments HNil [A B]. | 244 Implicit Arguments HNil [A B]. |
245 Implicit Arguments HCons [A B x ls]. | 245 Implicit Arguments HCons [A B x ls]. |
246 | 246 |
247 Implicit Arguments MFirst [A elm ls]. | 247 Implicit Arguments HFirst [A elm ls]. |
248 Implicit Arguments MNext [A elm x ls]. | 248 Implicit Arguments HNext [A elm x ls]. |
249 (* end thide *) | 249 (* end thide *) |
250 | 250 |
251 (** By putting the parameters [A] and [B] in [Type], we allow some very higher-order uses. For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *) | 251 (** By putting the parameters [A] and [B] in [Type], we allow some very higher-order uses. For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *) |
252 | 252 |
253 Definition someTypes : list Set := nat :: bool :: nil. | 253 Definition someTypes : list Set := nat :: bool :: nil. |
255 (* begin thide *) | 255 (* begin thide *) |
256 | 256 |
257 Example someValues : hlist (fun T : Set => T) someTypes := | 257 Example someValues : hlist (fun T : Set => T) someTypes := |
258 HCons 5 (HCons true HNil). | 258 HCons 5 (HCons true HNil). |
259 | 259 |
260 Eval simpl in hget someValues MFirst. | 260 Eval simpl in hget someValues HFirst. |
261 (** %\vspace{-.15in}% [[ | 261 (** %\vspace{-.15in}% [[ |
262 = 5 | 262 = 5 |
263 : (fun T : Set => T) nat | 263 : (fun T : Set => T) nat |
264 ]] | 264 ]] |
265 *) | 265 *) |
266 | 266 |
267 Eval simpl in hget someValues (MNext MFirst). | 267 Eval simpl in hget someValues (HNext HFirst). |
268 (** %\vspace{-.15in}% [[ | 268 (** %\vspace{-.15in}% [[ |
269 = true | 269 = true |
270 : (fun T : Set => T) bool | 270 : (fun T : Set => T) bool |
271 ]] | 271 ]] |
272 *) | 272 *) |
332 = tt | 332 = tt |
333 : typeDenote Unit | 333 : typeDenote Unit |
334 ]] | 334 ]] |
335 *) | 335 *) |
336 | 336 |
337 Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) HNil. | 337 Eval simpl in expDenote (Abs (dom := Unit) (Var HFirst)) HNil. |
338 (** %\vspace{-.15in}% [[ | 338 (** %\vspace{-.15in}% [[ |
339 = fun x : unit => x | 339 = fun x : unit => x |
340 : typeDenote (Arrow Unit Unit) | 340 : typeDenote (Arrow Unit Unit) |
341 ]] | 341 ]] |
342 *) | 342 *) |
343 | 343 |
344 Eval simpl in expDenote (Abs (dom := Unit) | 344 Eval simpl in expDenote (Abs (dom := Unit) |
345 (Abs (dom := Unit) (Var (MNext MFirst)))) HNil. | 345 (Abs (dom := Unit) (Var (HNext HFirst)))) HNil. |
346 (** %\vspace{-.15in}% [[ | 346 (** %\vspace{-.15in}% [[ |
347 = fun x _ : unit => x | 347 = fun x _ : unit => x |
348 : typeDenote (Arrow Unit (Arrow Unit Unit)) | 348 : typeDenote (Arrow Unit (Arrow Unit Unit)) |
349 ]] | 349 ]] |
350 *) | 350 *) |
351 | 351 |
352 Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) HNil. | 352 Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var HFirst))) HNil. |
353 (** %\vspace{-.15in}% [[ | 353 (** %\vspace{-.15in}% [[ |
354 = fun _ x0 : unit => x0 | 354 = fun _ x0 : unit => x0 |
355 : typeDenote (Arrow Unit (Arrow Unit Unit)) | 355 : typeDenote (Arrow Unit (Arrow Unit Unit)) |
356 ]] | 356 ]] |
357 *) | 357 *) |
358 | 358 |
359 Eval simpl in expDenote (App (Abs (Var MFirst)) Const) HNil. | 359 Eval simpl in expDenote (App (Abs (Var HFirst)) Const) HNil. |
360 (** %\vspace{-.15in}% [[ | 360 (** %\vspace{-.15in}% [[ |
361 = tt | 361 = tt |
362 : typeDenote Unit | 362 : typeDenote Unit |
363 ]] | 363 ]] |
364 *) | 364 *) |