Mercurial > cpdt > repo

comparison src/Generic.v @ 198:a35eaec19781

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Templatize Generic
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Nov 2008 14:21:38 -0500
parents f6293ba66559
children f8bcd33bdd91
comparison
equal deleted inserted replaced
197:f6293ba66559 198:a35eaec19781
23 (** TODO: Prose for this chapter *) 23 (** TODO: Prose for this chapter *)
24 24
25 25
26 (** * Reflecting Datatype Definitions *) 26 (** * Reflecting Datatype Definitions *)
27 27
28 (* EX: Define a reflected representation of simple algebraic datatypes. *)
29
30 (* begin thide *)
28 Record constructor : Type := Con { 31 Record constructor : Type := Con {
29 nonrecursive : Type; 32 nonrecursive : Type;
30 recursive : nat 33 recursive : nat
31 }. 34 }.
32 35
35 Definition Empty_set_dt : datatype := nil. 38 Definition Empty_set_dt : datatype := nil.
36 Definition unit_dt : datatype := Con unit 0 :: nil. 39 Definition unit_dt : datatype := Con unit 0 :: nil.
37 Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil. 40 Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil.
38 Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil. 41 Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil.
39 Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil. 42 Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil.
43 (* end thide *)
40 44
41 Section tree. 45 Section tree.
42 Variable A : Type. 46 Variable A : Type.
43 47
44 Inductive tree : Type := 48 Inductive tree : Type :=
45 | Leaf : A -> tree 49 | Leaf : A -> tree
46 | Node : tree -> tree -> tree. 50 | Node : tree -> tree -> tree.
47 End tree. 51 End tree.
48 52
53 (* begin thide *)
49 Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil. 54 Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil.
50 55
51 Section denote. 56 Section denote.
52 Variable T : Type. 57 Variable T : Type.
53 58
54 Definition constructorDenote (c : constructor) := 59 Definition constructorDenote (c : constructor) :=
55 nonrecursive c -> ilist T (recursive c) -> T. 60 nonrecursive c -> ilist T (recursive c) -> T.
56 61
57 Definition datatypeDenote := hlist constructorDenote. 62 Definition datatypeDenote := hlist constructorDenote.
58 End denote. 63 End denote.
64 (* end thide *)
59 65
60 Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)). 66 Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)).
61 Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)). 67 Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)).
62 Notation "[ ! , r # n ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ n)). 68 Notation "[ ! , r # n ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ n)).
63 Notation "[ v , r # n ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ n)). 69 Notation "[ v , r # n ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ n)).
64 70
71 (* begin thide *)
65 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt := 72 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
66 hnil. 73 hnil.
67 Definition unit_den : datatypeDenote unit unit_dt := 74 Definition unit_den : datatypeDenote unit unit_dt :=
68 [!, ! ~> tt] ::: hnil. 75 [!, ! ~> tt] ::: hnil.
69 Definition bool_den : datatypeDenote bool bool_dt := 76 Definition bool_den : datatypeDenote bool bool_dt :=
72 [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: hnil. 79 [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: hnil.
73 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) := 80 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
74 [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: hnil. 81 [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: hnil.
75 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) := 82 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
76 [v, ! ~> Leaf v] ::: [!, r # 2 ~> Node (hd r) (hd (tl r))] ::: hnil. 83 [v, ! ~> Leaf v] ::: [!, r # 2 ~> Node (hd r) (hd (tl r))] ::: hnil.
84 (* end thide *)
77 85
78 86
79 (** * Recursive Definitions *) 87 (** * Recursive Definitions *)
80 88
89 (* EX: Define a generic [size] function. *)
90
91 (* begin thide *)
81 Definition fixDenote (T : Type) (dt : datatype) := 92 Definition fixDenote (T : Type) (dt : datatype) :=
82 forall (R : Type), datatypeDenote R dt -> (T -> R). 93 forall (R : Type), datatypeDenote R dt -> (T -> R).
83 94
84 Definition size T dt (fx : fixDenote T dt) : T -> nat := 95 Definition size T dt (fx : fixDenote T dt) : T -> nat :=
85 fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt). 96 fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt).
119 match t with 130 match t with
120 | Leaf x => (fst cases) x inil 131 | Leaf x => (fst cases) x inil
121 | Node t1 t2 => (fst (snd cases)) tt (icons (F t1) (icons (F t2) inil)) 132 | Node t1 t2 => (fst (snd cases)) tt (icons (F t1) (icons (F t2) inil))
122 end. 133 end.
123 Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A). 134 Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A).
135 (* end thide *)
124 136
125 137
126 (** ** Pretty-Printing *) 138 (** ** Pretty-Printing *)
127 139
140 (* EX: Define a generic pretty-printing function. *)
141
142 (* begin thide *)
128 Record print_constructor (c : constructor) : Type := PI { 143 Record print_constructor (c : constructor) : Type := PI {
129 printName : string; 144 printName : string;
130 printNonrec : nonrecursive c -> string 145 printNonrec : nonrecursive c -> string
131 }. 146 }.
132 147
138 153
139 Definition print T dt (pr : print_datatype dt) (fx : fixDenote T dt) : T -> string := 154 Definition print T dt (pr : print_datatype dt) (fx : fixDenote T dt) : T -> string :=
140 fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string) 155 fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string)
141 (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x 156 (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x
142 ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr). 157 ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr).
158 (* end thide *)
143 159
144 Eval compute in print hnil Empty_set_fix. 160 Eval compute in print hnil Empty_set_fix.
145 Eval compute in print (^ "tt" (fun _ => "") ::: hnil) unit_fix. 161 Eval compute in print (^ "tt" (fun _ => "") ::: hnil) unit_fix.
146 Eval compute in print (^ "true" (fun _ => "") 162 Eval compute in print (^ "true" (fun _ => "")
147 ::: ^ "false" (fun _ => "") 163 ::: ^ "false" (fun _ => "")
165 ::: hnil) (@tree_fix A). 181 ::: hnil) (@tree_fix A).
166 182
167 183
168 (** ** Mapping *) 184 (** ** Mapping *)
169 185
186 (* EX: Define a generic [map] function. *)
187
188 (* begin thide *)
170 Definition map T dt (dd : datatypeDenote T dt) (fx : fixDenote T dt) (f : T -> T) : T -> T := 189 Definition map T dt (dd : datatypeDenote T dt) (fx : fixDenote T dt) (f : T -> T) : T -> T :=
171 fx T (hmap (B1 := constructorDenote T) (B2 := constructorDenote T) 190 fx T (hmap (B1 := constructorDenote T) (B2 := constructorDenote T)
172 (fun _ c x r => f (c x r)) dd). 191 (fun _ c x r => f (c x r)) dd).
192 (* end thide *)
173 193
174 Eval compute in map Empty_set_den Empty_set_fix. 194 Eval compute in map Empty_set_den Empty_set_fix.
175 Eval compute in map unit_den unit_fix. 195 Eval compute in map unit_den unit_fix.
176 Eval compute in map bool_den bool_fix. 196 Eval compute in map bool_den bool_fix.
177 Eval compute in map nat_den nat_fix. 197 Eval compute in map nat_den nat_fix.
184 Eval simpl in map_nat S 2. 204 Eval simpl in map_nat S 2.
185 205
186 206
187 (** * Proving Theorems about Recursive Definitions *) 207 (** * Proving Theorems about Recursive Definitions *)
188 208
209 (* begin thide *)
189 Section ok. 210 Section ok.
190 Variable T : Type. 211 Variable T : Type.
191 Variable dt : datatype. 212 Variable dt : datatype.
192 213
193 Variable dd : datatypeDenote T dt. 214 Variable dd : datatypeDenote T dt.
213 Lemma foldr_plus : forall n (ils : ilist nat n), 234 Lemma foldr_plus : forall n (ils : ilist nat n),
214 foldr plus 1 ils > 0. 235 foldr plus 1 ils > 0.
215 induction n; crush. 236 induction n; crush.
216 generalize (IHn b); crush. 237 generalize (IHn b); crush.
217 Qed. 238 Qed.
239 (* end thide *)
218 240
219 Theorem size_positive : forall T dt 241 Theorem size_positive : forall T dt
220 (dd : datatypeDenote T dt) (fx : fixDenote T dt) 242 (dd : datatypeDenote T dt) (fx : fixDenote T dt)
221 (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx) 243 (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
222 (v : T), 244 (v : T),
223 size fx v > 0. 245 size fx v > 0.
246 (* begin thide *)
224 Hint Rewrite hget_hmake : cpdt. 247 Hint Rewrite hget_hmake : cpdt.
225 Hint Resolve foldr_plus. 248 Hint Resolve foldr_plus.
226 249
227 unfold size; intros; pattern v; apply dok; crush. 250 unfold size; intros; pattern v; apply dok; crush.
228 Qed. 251 Qed.
252 (* end thide *)
229 253
230 Theorem map_id : forall T dt 254 Theorem map_id : forall T dt
231 (dd : datatypeDenote T dt) (fx : fixDenote T dt) 255 (dd : datatypeDenote T dt) (fx : fixDenote T dt)
232 (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx) 256 (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
233 (v : T), 257 (v : T),
234 map dd fx (fun x => x) v = v. 258 map dd fx (fun x => x) v = v.
259 (* begin thide *)
235 Hint Rewrite hget_hmap : cpdt. 260 Hint Rewrite hget_hmap : cpdt.
236 261
237 unfold map; intros; pattern v; apply dok; crush. 262 unfold map; intros; pattern v; apply dok; crush.
238 match goal with 263 match goal with
239 | [ |- hget _ _ _ ?R1 = hget _ _ _ ?R2 ] => replace R1 with R2 264 | [ |- hget _ _ _ ?R1 = hget _ _ _ ?R2 ] => replace R1 with R2
246 unfold icons. 271 unfold icons.
247 f_equal. 272 f_equal.
248 apply IHn; crush. 273 apply IHn; crush.
249 apply (H (Some i0)). 274 apply (H (Some i0)).
250 Qed. 275 Qed.
276 (* end thide *)