Mercurial > cpdt > repo
comparison src/DataStruct.v @ 457:b1fead9f68f2
Proofreading pass through Chapter 11
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Tue, 28 Aug 2012 15:53:21 -0400 |
parents | df0a45de158a |
children | 218361342cd2 |
comparison
equal
deleted
inserted
replaced
456:848bf35f7f6c | 457:b1fead9f68f2 |
---|---|
195 | 195 |
196 (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B].%\index{Gallina terms!hlist}% *) | 196 (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B].%\index{Gallina terms!hlist}% *) |
197 | 197 |
198 (* begin thide *) | 198 (* begin thide *) |
199 Inductive hlist : list A -> Type := | 199 Inductive hlist : list A -> Type := |
200 | MNil : hlist nil | 200 | HNil : hlist nil |
201 | MCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls). | 201 | HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls). |
202 | 202 |
203 (** We can implement a variant of the last section's [get] function for [hlist]s. To get the dependent typing to work out, we will need to index our element selectors by the types of data that they point to.%\index{Gallina terms!member}% *) | 203 (** We can implement a variant of the last section's [get] function for [hlist]s. To get the dependent typing to work out, we will need to index our element selectors by the types of data that they point to.%\index{Gallina terms!member}% *) |
204 | 204 |
205 (* end thide *) | 205 (* end thide *) |
206 (* EX: Define an analogue to [get] for [hlist]s. *) | 206 (* EX: Define an analogue to [get] for [hlist]s. *) |
212 | MFirst : forall ls, member (elm :: ls) | 212 | MFirst : forall ls, member (elm :: ls) |
213 | MNext : forall x ls, member ls -> member (x :: ls). | 213 | MNext : 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 [MCons] 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 |
219 Fixpoint hget ls (mls : hlist ls) : member ls -> B elm := | 219 Fixpoint hget ls (mls : hlist ls) : member ls -> B elm := |
220 match mls with | 220 match mls with |
221 | MNil => 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 | MFirst _ => tt |
227 | MNext _ _ _ => tt | 227 | MNext _ _ _ => tt |
228 end | 228 end |
229 | MCons _ _ 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 |
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 MNil [A B]. | 244 Implicit Arguments HNil [A B]. |
245 Implicit Arguments MCons [A B x ls]. | 245 Implicit Arguments HCons [A B x ls]. |
246 | 246 |
247 Implicit Arguments MFirst [A elm ls]. | 247 Implicit Arguments MFirst [A elm ls]. |
248 Implicit Arguments MNext [A elm x ls]. | 248 Implicit Arguments MNext [A elm x ls]. |
249 (* end thide *) | 249 (* end thide *) |
250 | 250 |
253 Definition someTypes : list Set := nat :: bool :: nil. | 253 Definition someTypes : list Set := nat :: bool :: nil. |
254 | 254 |
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 MCons 5 (MCons true MNil). | 258 HCons 5 (HCons true HNil). |
259 | 259 |
260 Eval simpl in hget someValues MFirst. | 260 Eval simpl in hget someValues MFirst. |
261 (** %\vspace{-.15in}% [[ | 261 (** %\vspace{-.15in}% [[ |
262 = 5 | 262 = 5 |
263 : (fun T : Set => T) nat | 263 : (fun T : Set => T) nat |
272 *) | 272 *) |
273 | 273 |
274 (** We can also build indexed lists of pairs in this way. *) | 274 (** We can also build indexed lists of pairs in this way. *) |
275 | 275 |
276 Example somePairs : hlist (fun T : Set => T * T)%type someTypes := | 276 Example somePairs : hlist (fun T : Set => T * T)%type someTypes := |
277 MCons (1, 2) (MCons (true, false) MNil). | 277 HCons (1, 2) (HCons (true, false) HNil). |
278 | 278 |
279 (** There are many more useful applications of heterogeneous lists, based on different choices of the first argument to [hlist]. *) | 279 (** There are many more useful applications of heterogeneous lists, based on different choices of the first argument to [hlist]. *) |
280 | 280 |
281 (* end thide *) | 281 (* end thide *) |
282 | 282 |
309 match t with | 309 match t with |
310 | Unit => unit | 310 | Unit => unit |
311 | Arrow t1 t2 => typeDenote t1 -> typeDenote t2 | 311 | Arrow t1 t2 => typeDenote t1 -> typeDenote t2 |
312 end. | 312 end. |
313 | 313 |
314 (** Now it is straightforward to write an expression interpreter. The type of the function, [expDenote], tells us that we translate expressions into functions from properly typed environments to final values. An environment for a free variable list [ts] is simply a [hlist typeDenote ts]. That is, for each free variable, the heterogeneous list that is the environment must have a value of the variable's associated type. We use [hget] to implement the [Var] case, and we use [MCons] to extend the environment in the [Abs] case. *) | 314 (** Now it is straightforward to write an expression interpreter. The type of the function, [expDenote], tells us that we translate expressions into functions from properly typed environments to final values. An environment for a free variable list [ts] is simply a [hlist typeDenote ts]. That is, for each free variable, the heterogeneous list that is the environment must have a value of the variable's associated type. We use [hget] to implement the [Var] case, and we use [HCons] to extend the environment in the [Abs] case. *) |
315 | 315 |
316 (* EX: Define an interpreter for [exp]s. *) | 316 (* EX: Define an interpreter for [exp]s. *) |
317 | 317 |
318 (* begin thide *) | 318 (* begin thide *) |
319 Fixpoint expDenote ts t (e : exp ts t) : hlist typeDenote ts -> typeDenote t := | 319 Fixpoint expDenote ts t (e : exp ts t) : hlist typeDenote ts -> typeDenote t := |
320 match e with | 320 match e with |
321 | Const _ => fun _ => tt | 321 | Const _ => fun _ => tt |
322 | 322 |
323 | Var _ _ mem => fun s => hget s mem | 323 | Var _ _ mem => fun s => hget s mem |
324 | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s) | 324 | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s) |
325 | Abs _ _ _ e' => fun s => fun x => expDenote e' (MCons x s) | 325 | Abs _ _ _ e' => fun s => fun x => expDenote e' (HCons x s) |
326 end. | 326 end. |
327 | 327 |
328 (** Like for previous examples, our interpreter is easy to run with [simpl]. *) | 328 (** Like for previous examples, our interpreter is easy to run with [simpl]. *) |
329 | 329 |
330 Eval simpl in expDenote Const MNil. | 330 Eval simpl in expDenote Const HNil. |
331 (** %\vspace{-.15in}% [[ | 331 (** %\vspace{-.15in}% [[ |
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)) MNil. | 337 Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) 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)))) MNil. | 345 (Abs (dom := Unit) (Var (MNext MFirst)))) 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))) MNil. | 352 Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) 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) MNil. | 359 Eval simpl in expDenote (App (Abs (Var MFirst)) Const) HNil. |
360 (** %\vspace{-.15in}% [[ | 360 (** %\vspace{-.15in}% [[ |
361 = tt | 361 = tt |
362 : typeDenote Unit | 362 : typeDenote Unit |
363 ]] | 363 ]] |
364 *) | 364 *) |