Start of Generic

Makefile

@@ -2,7 +2,7 @@ MODULES_NODOC := Axioms AxiomsImpred Tactics MoreSpecif DepList
 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)

src/Generic.v

+(* 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.

src/Intro.v

@@ -215,6 +215,8 @@ Intensional Transformations & \texttt{Intensional.v} \\
 \hline
 Modeling Impure Languages & \texttt{Impure.v} \\
 \hline
+Generic Programming & \texttt{Generic.v} \\
+\hline
 \end{tabular} \end{center}
 
 % *)

src/toc.html

@@ -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>