Mercurial > cpdt > repo

comparison src/Generic.v @ 359:059c51227e69

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak Generic templating
author Adam Chlipala <adam@chlipala.net>
date Tue, 01 Nov 2011 12:34:00 -0400
parents 6cc9a3bbc2c6
children e0d91bcf70ec
comparison
equal deleted inserted replaced
358:6cc9a3bbc2c6 359:059c51227e69
231 (* end thide *) 231 (* end thide *)
232 232
233 233
234 (** ** Pretty-Printing *) 234 (** ** Pretty-Printing *)
235 235
236 (* EX: Define a generic pretty-printing function. *)
237
238 (** It is also useful to do generic pretty-printing of datatype values, rendering them as human-readable strings. To do so, we will need a bit of metadata for each constructor. Specifically, we need the name to print for the constructor and the function to use to render its non-recursive arguments. Everything else can be done generically. *) 236 (** It is also useful to do generic pretty-printing of datatype values, rendering them as human-readable strings. To do so, we will need a bit of metadata for each constructor. Specifically, we need the name to print for the constructor and the function to use to render its non-recursive arguments. Everything else can be done generically. *)
239 237
240 (* begin thide *)
241 Record print_constructor (c : constructor) : Type := PI { 238 Record print_constructor (c : constructor) : Type := PI {
242 printName : string; 239 printName : string;
243 printNonrec : nonrecursive c -> string 240 printNonrec : nonrecursive c -> string
244 }. 241 }.
245 242
268 265
269 Definition print T dt (pr : print_datatype dt) (fx : fixDenote T dt) : T -> string := 266 Definition print T dt (pr : print_datatype dt) (fx : fixDenote T dt) : T -> string :=
270 fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string) 267 fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string)
271 (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x 268 (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x
272 ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr). 269 ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr).
273 (* end thide *)
274 270
275 (** Some simple tests establish that [print] gets the job done. *) 271 (** Some simple tests establish that [print] gets the job done. *)
276 272
277 Eval compute in print HNil Empty_set_fix. 273 Eval compute in print HNil Empty_set_fix.
278 (** %\vspace{-.15in}% [[ 274 (** %\vspace{-.15in}% [[
367 (** Some of these simplified terms seem overly complex because we have turned off simplification of calls to [append], which is what uses of the [++] operator desugar to. Selective [++] simplification would combine adjacent string literals, yielding more or less the code we would write manually to implement this printing scheme. *) 363 (** Some of these simplified terms seem overly complex because we have turned off simplification of calls to [append], which is what uses of the [++] operator desugar to. Selective [++] simplification would combine adjacent string literals, yielding more or less the code we would write manually to implement this printing scheme. *)
368 364
369 365
370 (** ** Mapping *) 366 (** ** Mapping *)
371 367
372 (* EX: Define a generic [map] function. *)
373
374 (** By this point, we have developed enough machinery that it is old hat to define a generic function similar to the list [map] function. *) 368 (** By this point, we have developed enough machinery that it is old hat to define a generic function similar to the list [map] function. *)
375 369
376 (* begin thide *)
377 Definition map T dt (dd : datatypeDenote T dt) (fx : fixDenote T dt) (f : T -> T) 370 Definition map T dt (dd : datatypeDenote T dt) (fx : fixDenote T dt) (f : T -> T)
378 : T -> T := 371 : T -> T :=
379 fx T (hmap (B1 := constructorDenote T) (B2 := constructorDenote T) 372 fx T (hmap (B1 := constructorDenote T) (B2 := constructorDenote T)
380 (fun _ c x r => f (c x r)) dd). 373 (fun _ c x r => f (c x r)) dd).
381 (* end thide *)
382 374
383 Eval compute in map Empty_set_den Empty_set_fix. 375 Eval compute in map Empty_set_den Empty_set_fix.
384 (** %\vspace{-.15in}% [[ 376 (** %\vspace{-.15in}% [[
385 = fun (_ : Empty_set -> Empty_set) (emp : Empty_set) => 377 = fun (_ : Empty_set -> Empty_set) (emp : Empty_set) =>
386 match emp return Empty_set with 378 match emp return Empty_set with
468 460
469 (** * Proving Theorems about Recursive Definitions *) 461 (** * Proving Theorems about Recursive Definitions *)
470 462
471 (** We would like to be able to prove theorems about our generic functions. To do so, we need to establish additional well-formedness properties that must hold of pieces of evidence. *) 463 (** We would like to be able to prove theorems about our generic functions. To do so, we need to establish additional well-formedness properties that must hold of pieces of evidence. *)
472 464
473 (* begin thide *)
474 Section ok. 465 Section ok.
475 Variable T : Type. 466 Variable T : Type.
476 Variable dt : datatype. 467 Variable dt : datatype.
477 468
478 Variable dd : datatypeDenote T dt. 469 Variable dd : datatypeDenote T dt.
502 493
503 End ok. 494 End ok.
504 495
505 (** We are now ready to prove that the [size] function we defined earlier always returns positive results. First, we establish a simple lemma. *) 496 (** We are now ready to prove that the [size] function we defined earlier always returns positive results. First, we establish a simple lemma. *)
506 497
498 (* begin thide *)
507 Lemma foldr_plus : forall n (ils : ilist nat n), 499 Lemma foldr_plus : forall n (ils : ilist nat n),
508 foldr plus 1 ils > 0. 500 foldr plus 1 ils > 0.
509 induction ils; crush. 501 induction ils; crush.
510 Qed. 502 Qed.
511 (* end thide *) 503 (* end thide *)