adamc@193: (* Copyright (c) 2008, Adam Chlipala
adamc@193:  * 
adamc@193:  * This work is licensed under a
adamc@193:  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@193:  * Unported License.
adamc@193:  * The license text is available at:
adamc@193:  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@193:  *)
adamc@193: 
adamc@193: (* begin hide *)
adamc@193: Require Import List.
adamc@193: 
adamc@193: Require Import Tactics DepList.
adamc@193: 
adamc@193: Set Implicit Arguments.
adamc@193: (* end hide *)
adamc@193: 
adamc@193: 
adamc@193: (** %\part{Chapters to be Moved Earlier}
adamc@193: 
adamc@193: \chapter{Generic Programming}% *)
adamc@193: 
adamc@193: (** TODO: Prose for this chapter *)
adamc@193: 
adamc@193: 
adamc@193: (** * Simple Algebraic Datatypes *)
adamc@193: 
adamc@193: Record constructor : Type := Con {
adamc@193:   nonrecursive : Type;
adamc@193:   recursive : nat
adamc@193: }.
adamc@193: 
adamc@193: Definition datatype := list constructor.
adamc@193: 
adamc@193: Definition Empty_set_dt : datatype := nil.
adamc@193: Definition unit_dt : datatype := Con unit 0 :: nil.
adamc@193: Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil.
adamc@193: Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil.
adamc@193: Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil.
adamc@193: 
adamc@193: Section tree.
adamc@193:   Variable A : Type.
adamc@193: 
adamc@193:   Inductive tree : Type :=
adamc@193:   | Leaf : A -> tree
adamc@193:   | Node : tree -> tree -> tree.
adamc@193: End tree.
adamc@193: 
adamc@193: Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil.
adamc@193: 
adamc@193: Section denote.
adamc@193:   Variable T : Type.
adamc@193: 
adamc@193:   Definition constructorDenote (c : constructor) :=
adamc@193:     nonrecursive c -> ilist T (recursive c) -> T.
adamc@193: 
adamc@193:   Definition datatypeDenote := hlist constructorDenote.
adamc@193: End denote.
adamc@193: 
adamc@193: Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)).
adamc@193: Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)).
adamc@193: Notation "[ ! , r # n ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ n)).
adamc@193: Notation "[ v , r # n ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ n)).
adamc@193: 
adamc@193: Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
adamc@193:   hnil.
adamc@193: Definition unit_den : datatypeDenote unit unit_dt :=
adamc@193:   [!, ! ~> tt] ::: hnil.
adamc@193: Definition bool_den : datatypeDenote bool bool_dt :=
adamc@193:   [!, ! ~> true] ::: [!, ! ~> false] ::: hnil.
adamc@193: Definition nat_den : datatypeDenote nat nat_dt :=
adamc@193:   [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: hnil.
adamc@193: Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
adamc@193:   [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: hnil.
adamc@193: Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
adamc@193:   [v, ! ~> Leaf v] ::: [!, r # 2 ~> Node (hd r) (hd (tl r))] ::: hnil.