Mercurial > cpdt > repo
comparison src/Generic.v @ 488:31258618ef73
Incorporate feedback from Nathan Collins
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 08 Jan 2013 14:38:56 -0500 |
| parents | f38a3af9dd17 |
| children | 04177dd1b133 |
comparison
equal
deleted
inserted
replaced
| 487:8bfb27cf0121 | 488:31258618ef73 |
|---|---|
| 24 | 24 |
| 25 Generic programming can often be very useful in Coq developments, so we devote this chapter to studying it. In a proof assistant, there is the new possibility of generic proofs about generic programs, which we also devote some space to. *) | 25 Generic programming can often be very useful in Coq developments, so we devote this chapter to studying it. In a proof assistant, there is the new possibility of generic proofs about generic programs, which we also devote some space to. *) |
| 26 | 26 |
| 27 (** * Reifying Datatype Definitions *) | 27 (** * Reifying Datatype Definitions *) |
| 28 | 28 |
| 29 (** The key to generic programming with dependent types is%\index{universe types}% _universe types_. This concept should not be confused with the idea of _universes_ from the metatheory of CIC and related languages. Rather, the idea of universe types is to define inductive types that provide _syntactic representations_ of Coq types. We cannot directly write CIC programs that do case analysis on types, but we _can_ case analyze on reified syntactic versions of those types. | 29 (** The key to generic programming with dependent types is%\index{universe types}% _universe types_. This concept should not be confused with the idea of _universes_ from the metatheory of CIC and related languages, which we will study in more detail in the next chapter. Rather, the idea of universe types is to define inductive types that provide _syntactic representations_ of Coq types. We cannot directly write CIC programs that do case analysis on types, but we _can_ case analyze on reified syntactic versions of those types. |
| 30 | 30 |
| 31 Thus, to begin, we must define a syntactic representation of some class of datatypes. In this chapter, our running example will have to do with basic algebraic datatypes, of the kind found in ML and Haskell, but without additional bells and whistles like type parameters and mutually recursive definitions. | 31 Thus, to begin, we must define a syntactic representation of some class of datatypes. In this chapter, our running example will have to do with basic algebraic datatypes, of the kind found in ML and Haskell, but without additional bells and whistles like type parameters and mutually recursive definitions. |
| 32 | 32 |
| 33 The first step is to define a representation for constructors of our datatypes. We use the [Record] command as a shorthand for defining an inductive type with a single constructor, plus projection functions for pulling out any of the named arguments to that constructor. *) | 33 The first step is to define a representation for constructors of our datatypes. We use the [Record] command as a shorthand for defining an inductive type with a single constructor, plus projection functions for pulling out any of the named arguments to that constructor. *) |
| 34 | 34 |
| 136 The function [hmake] is a kind of [map] alternative that goes from a regular [list] to an [hlist]. We can use it to define a generic size function that counts the number of constructors used to build a value in a datatype. *) | 136 The function [hmake] is a kind of [map] alternative that goes from a regular [list] to an [hlist]. We can use it to define a generic size function that counts the number of constructors used to build a value in a datatype. *) |
| 137 | 137 |
| 138 Definition size T dt (fx : fixDenote T dt) : T -> nat := | 138 Definition size T dt (fx : fixDenote T dt) : T -> nat := |
| 139 fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt). | 139 fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt). |
| 140 | 140 |
| 141 (** Our definition is parameterized over a recursion scheme [fx]. We instantiate [fx] by passing it the function result type and a set of function cases, where we build the latter with [hmake]. The function argument to [hmake] takes three arguments: the representation of a constructor, its non-recursive arguments, and the results of recursive calls on all of its recursive arguments. We only need the recursive call results here, so we call them [r] and bind the other two inputs with wildcards. The actual case body is simple: we add together the recursive call results and increment the result by one (to account for the current constructor). This [foldr] function is an [hlist]-specific version defined in the [DepList] module. | 141 (** Our definition is parameterized over a recursion scheme [fx]. We instantiate [fx] by passing it the function result type and a set of function cases, where we build the latter with [hmake]. The function argument to [hmake] takes three arguments: the representation of a constructor, its non-recursive arguments, and the results of recursive calls on all of its recursive arguments. We only need the recursive call results here, so we call them [r] and bind the other two inputs with wildcards. The actual case body is simple: we add together the recursive call results and increment the result by one (to account for the current constructor). This [foldr] function is an [ilist]-specific version defined in the [DepList] module. |
| 142 | 142 |
| 143 It is instructive to build [fixDenote] values for our example types and see what specialized [size] functions result from them. *) | 143 It is instructive to build [fixDenote] values for our example types and see what specialized [size] functions result from them. *) |
| 144 | 144 |
| 145 Definition Empty_set_fix : fixDenote Empty_set Empty_set_dt := | 145 Definition Empty_set_fix : fixDenote Empty_set Empty_set_dt := |
| 146 fun R _ emp => match emp with end. | 146 fun R _ emp => match emp with end. |
| 290 Eval compute in print (^ "true" (fun _ => "") | 290 Eval compute in print (^ "true" (fun _ => "") |
| 291 ::: ^ "false" (fun _ => "") | 291 ::: ^ "false" (fun _ => "") |
| 292 ::: HNil) bool_fix. | 292 ::: HNil) bool_fix. |
| 293 (** %\vspace{-.15in}% [[ | 293 (** %\vspace{-.15in}% [[ |
| 294 = fun b : bool => if b then "true()" else "false()" | 294 = fun b : bool => if b then "true()" else "false()" |
| 295 : bool -> s | 295 : bool -> string |
| 296 ]] | 296 ]] |
| 297 *) | 297 *) |
| 298 | 298 |
| 299 Definition print_nat := print (^ "O" (fun _ => "") | 299 Definition print_nat := print (^ "O" (fun _ => "") |
| 300 ::: ^ "S" (fun _ => "") | 300 ::: ^ "S" (fun _ => "") |
| 654 (* begin thide *) | 654 (* begin thide *) |
| 655 Definition pred' := pred. | 655 Definition pred' := pred. |
| 656 (* end thide *) | 656 (* end thide *) |
| 657 (* end hide *) | 657 (* end hide *) |
| 658 | 658 |
| 659 (** The base case is discharged automatically, and the inductive case looks like this, where [H] is the outer IH (for induction over [T] values) and [IHn] is the inner IH (for induction over the recursive arguments). | 659 (** The base case is discharged automatically, and the inductive case looks like this, where [H] is the outer IH (for induction over [T] values) and [IHr] is the inner IH (for induction over the recursive arguments). |
| 660 [[ | 660 [[ |
| 661 H : forall i : fin (S n), | 661 H : forall i : fin (S n), |
| 662 fx T | 662 fx T |
| 663 (hmap | 663 (hmap |
| 664 (fun (x : constructor) (c : constructorDenote T x) | 664 (fun (x : constructor) (c : constructorDenote T x) |