# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1227884156 18000
# Node ID 8e9499e27b6c3d27d8c8f3941c8cb9a4430264b7
# Parent  32ce9b28d7e78f72c8c1a0cc4393efd0bd2a7e1b
Start of Generic

diff -r 32ce9b28d7e7 -r 8e9499e27b6c Makefile
--- a/Makefile	Tue Nov 18 13:09:09 2008 -0500
+++ b/Makefile	Fri Nov 28 09:55:56 2008 -0500
@@ -2,7 +2,7 @@
 MODULES_PROSE := Intro
 MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset \
 	MoreDep DataStruct Equality Match Reflection Firstorder Hoas Interps \
-	Extensional Intensional Impure
+	Extensional Intensional Impure Generic
 MODULES_DOC   := $(MODULES_PROSE) $(MODULES_CODE)
 MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
 VS            := $(MODULES:%=src/%.v)
diff -r 32ce9b28d7e7 -r 8e9499e27b6c src/Generic.v
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Generic.v	Fri Nov 28 09:55:56 2008 -0500
@@ -0,0 +1,76 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * 
+ * This work is licensed under a
+ * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
+ * Unported License.
+ * The license text is available at:
+ *   http://creativecommons.org/licenses/by-nc-nd/3.0/
+ *)
+
+(* begin hide *)
+Require Import List.
+
+Require Import Tactics DepList.
+
+Set Implicit Arguments.
+(* end hide *)
+
+
+(** %\part{Chapters to be Moved Earlier}
+
+\chapter{Generic Programming}% *)
+
+(** TODO: Prose for this chapter *)
+
+
+(** * Simple Algebraic Datatypes *)
+
+Record constructor : Type := Con {
+  nonrecursive : Type;
+  recursive : nat
+}.
+
+Definition datatype := list constructor.
+
+Definition Empty_set_dt : datatype := nil.
+Definition unit_dt : datatype := Con unit 0 :: nil.
+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.
+
+Section tree.
+  Variable A : Type.
+
+  Inductive tree : Type :=
+  | Leaf : A -> tree
+  | Node : tree -> tree -> tree.
+End tree.
+
+Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil.
+
+Section denote.
+  Variable T : Type.
+
+  Definition constructorDenote (c : constructor) :=
+    nonrecursive c -> ilist T (recursive c) -> T.
+
+  Definition datatypeDenote := hlist constructorDenote.
+End denote.
+
+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)).
+
+Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
+  hnil.
+Definition unit_den : datatypeDenote unit unit_dt :=
+  [!, ! ~> tt] ::: hnil.
+Definition bool_den : datatypeDenote bool bool_dt :=
+  [!, ! ~> true] ::: [!, ! ~> false] ::: hnil.
+Definition nat_den : datatypeDenote nat nat_dt :=
+  [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: hnil.
+Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
+  [!, ! ~> 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.
diff -r 32ce9b28d7e7 -r 8e9499e27b6c src/Intro.v
--- a/src/Intro.v	Tue Nov 18 13:09:09 2008 -0500
+++ b/src/Intro.v	Fri Nov 28 09:55:56 2008 -0500
@@ -215,6 +215,8 @@
 \hline
 Modeling Impure Languages & \texttt{Impure.v} \\
 \hline
+Generic Programming & \texttt{Generic.v} \\
+\hline
 \end{tabular} \end{center}
 
 % *)
diff -r 32ce9b28d7e7 -r 8e9499e27b6c src/toc.html
--- a/src/toc.html	Tue Nov 18 13:09:09 2008 -0500
+++ b/src/toc.html	Fri Nov 28 09:55:56 2008 -0500
@@ -21,5 +21,6 @@
 <li><a href="Extensional.html">Extensional Transformations</a>
 <li><a href="Intensional.html">Intensional Transformations</a>
 <li><a href="Impure.html">Modeling Impure Languages</a>
+<li><a href="Generic.html">Generic Programming</a>
 
 </body></html>