# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1227900098 18000
# Node ID a35eaec19781a97ebda5e21f0e5c96e4e34f7ff5
# Parent  f6293ba665592441a11cc24b78dc1656e23bcbf5
Templatize Generic

diff -r f6293ba66559 -r a35eaec19781 src/Generic.v
--- a/src/Generic.v	Fri Nov 28 14:10:23 2008 -0500
+++ b/src/Generic.v	Fri Nov 28 14:21:38 2008 -0500
@@ -25,6 +25,9 @@
 
 (** * Reflecting Datatype Definitions *)
 
+(* EX: Define a reflected representation of simple algebraic datatypes. *)
+
+(* begin thide *)
 Record constructor : Type := Con {
   nonrecursive : Type;
   recursive : nat
@@ -37,6 +40,7 @@
 Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil.
 Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil.
 Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil.
+(* end thide *)
 
 Section tree.
   Variable A : Type.
@@ -46,6 +50,7 @@
   | Node : tree -> tree -> tree.
 End tree.
 
+(* begin thide *)
 Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil.
 
 Section denote.
@@ -56,12 +61,14 @@
 
   Definition datatypeDenote := hlist constructorDenote.
 End denote.
+(* end thide *)
 
 Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)).
 Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)).
 Notation "[ ! , r # n ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ n)).
 Notation "[ v , r # n ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ n)).
 
+(* begin thide *)
 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
   hnil.
 Definition unit_den : datatypeDenote unit unit_dt :=
@@ -74,10 +81,14 @@
   [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: hnil.
 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
   [v, ! ~> Leaf v] ::: [!, r # 2 ~> Node (hd r) (hd (tl r))] ::: hnil.
+(* end thide *)
 
 
 (** * Recursive Definitions *)
 
+(* EX: Define a generic [size] function. *)
+
+(* begin thide *)
 Definition fixDenote (T : Type) (dt : datatype) :=
   forall (R : Type), datatypeDenote R dt -> (T -> R).
 
@@ -121,10 +132,14 @@
       | Node t1 t2 => (fst (snd cases)) tt (icons (F t1) (icons (F t2) inil))
     end.
 Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A).
+(* end thide *)
 
 
 (** ** Pretty-Printing *)
 
+(* EX: Define a generic pretty-printing function. *)
+
+(* begin thide *)
 Record print_constructor (c : constructor) : Type := PI {
   printName : string;
   printNonrec : nonrecursive c -> string
@@ -140,6 +155,7 @@
   fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string)
     (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x
       ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr).
+(* end thide *)
 
 Eval compute in print hnil Empty_set_fix.
 Eval compute in print (^ "tt" (fun _ => "") ::: hnil) unit_fix.
@@ -167,9 +183,13 @@
 
 (** ** Mapping *)
 
+(* EX: Define a generic [map] function. *)
+
+(* begin thide *)
 Definition map T dt (dd : datatypeDenote T dt) (fx : fixDenote T dt) (f : T -> T) : T -> T :=
   fx T (hmap (B1 := constructorDenote T) (B2 := constructorDenote T)
     (fun _ c x r => f (c x r)) dd).
+(* end thide *)
 
 Eval compute in map Empty_set_den Empty_set_fix.
 Eval compute in map unit_den unit_fix.
@@ -186,6 +206,7 @@
 
 (** * Proving Theorems about Recursive Definitions *)
 
+(* begin thide *)
 Section ok.
   Variable T : Type.
   Variable dt : datatype.
@@ -215,23 +236,27 @@
   induction n; crush.
   generalize (IHn b); crush.
 Qed.
+(* end thide *)
 
 Theorem size_positive : forall T dt
   (dd : datatypeDenote T dt) (fx : fixDenote T dt)
   (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
   (v : T),
   size fx v > 0.
+(* begin thide *)
   Hint Rewrite hget_hmake : cpdt.
   Hint Resolve foldr_plus.
  
   unfold size; intros; pattern v; apply dok; crush.
 Qed.
+(* end thide *)
 
 Theorem map_id : forall T dt
   (dd : datatypeDenote T dt) (fx : fixDenote T dt)
   (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
   (v : T),
   map dd fx (fun x => x) v = v.
+(* begin thide *)
   Hint Rewrite hget_hmap : cpdt.
 
   unfold map; intros; pattern v; apply dok; crush.
@@ -248,3 +273,4 @@
   apply IHn; crush.
   apply (H (Some i0)).
 Qed.
+(* end thide *)