|
adamc@193
|
1 (* Copyright (c) 2008, Adam Chlipala
|
|
adamc@193
|
2 *
|
|
adamc@193
|
3 * This work is licensed under a
|
|
adamc@193
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
|
adamc@193
|
5 * Unported License.
|
|
adamc@193
|
6 * The license text is available at:
|
|
adamc@193
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
|
adamc@193
|
8 *)
|
|
adamc@193
|
9
|
|
adamc@193
|
10 (* begin hide *)
|
|
adamc@193
|
11 Require Import List.
|
|
adamc@193
|
12
|
|
adamc@193
|
13 Require Import Tactics DepList.
|
|
adamc@193
|
14
|
|
adamc@193
|
15 Set Implicit Arguments.
|
|
adamc@193
|
16 (* end hide *)
|
|
adamc@193
|
17
|
|
adamc@193
|
18
|
|
adamc@193
|
19 (** %\part{Chapters to be Moved Earlier}
|
|
adamc@193
|
20
|
|
adamc@193
|
21 \chapter{Generic Programming}% *)
|
|
adamc@193
|
22
|
|
adamc@193
|
23 (** TODO: Prose for this chapter *)
|
|
adamc@193
|
24
|
|
adamc@193
|
25
|
|
adamc@193
|
26 (** * Simple Algebraic Datatypes *)
|
|
adamc@193
|
27
|
|
adamc@193
|
28 Record constructor : Type := Con {
|
|
adamc@193
|
29 nonrecursive : Type;
|
|
adamc@193
|
30 recursive : nat
|
|
adamc@193
|
31 }.
|
|
adamc@193
|
32
|
|
adamc@193
|
33 Definition datatype := list constructor.
|
|
adamc@193
|
34
|
|
adamc@193
|
35 Definition Empty_set_dt : datatype := nil.
|
|
adamc@193
|
36 Definition unit_dt : datatype := Con unit 0 :: nil.
|
|
adamc@193
|
37 Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil.
|
|
adamc@193
|
38 Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil.
|
|
adamc@193
|
39 Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil.
|
|
adamc@193
|
40
|
|
adamc@193
|
41 Section tree.
|
|
adamc@193
|
42 Variable A : Type.
|
|
adamc@193
|
43
|
|
adamc@193
|
44 Inductive tree : Type :=
|
|
adamc@193
|
45 | Leaf : A -> tree
|
|
adamc@193
|
46 | Node : tree -> tree -> tree.
|
|
adamc@193
|
47 End tree.
|
|
adamc@193
|
48
|
|
adamc@193
|
49 Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil.
|
|
adamc@193
|
50
|
|
adamc@193
|
51 Section denote.
|
|
adamc@193
|
52 Variable T : Type.
|
|
adamc@193
|
53
|
|
adamc@193
|
54 Definition constructorDenote (c : constructor) :=
|
|
adamc@193
|
55 nonrecursive c -> ilist T (recursive c) -> T.
|
|
adamc@193
|
56
|
|
adamc@193
|
57 Definition datatypeDenote := hlist constructorDenote.
|
|
adamc@193
|
58 End denote.
|
|
adamc@193
|
59
|
|
adamc@193
|
60 Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)).
|
|
adamc@193
|
61 Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)).
|
|
adamc@193
|
62 Notation "[ ! , r # n ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ n)).
|
|
adamc@193
|
63 Notation "[ v , r # n ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ n)).
|
|
adamc@193
|
64
|
|
adamc@193
|
65 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
|
|
adamc@193
|
66 hnil.
|
|
adamc@193
|
67 Definition unit_den : datatypeDenote unit unit_dt :=
|
|
adamc@193
|
68 [!, ! ~> tt] ::: hnil.
|
|
adamc@193
|
69 Definition bool_den : datatypeDenote bool bool_dt :=
|
|
adamc@193
|
70 [!, ! ~> true] ::: [!, ! ~> false] ::: hnil.
|
|
adamc@193
|
71 Definition nat_den : datatypeDenote nat nat_dt :=
|
|
adamc@193
|
72 [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: hnil.
|
|
adamc@193
|
73 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
|
|
adamc@193
|
74 [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: hnil.
|
|
adamc@193
|
75 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
|
|
adamc@193
|
76 [v, ! ~> Leaf v] ::: [!, r # 2 ~> Node (hd r) (hd (tl r))] ::: hnil.
|
