Mercurial > cpdt > repo

comparison src/Generic.v @ 216:d1464997078d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Switch DepList to inductive, not recursive, types
author Adam Chlipala <adamc@hcoop.net>
date Wed, 11 Nov 2009 14:28:47 -0500
parents f8bcd33bdd91
children dbac52f5bce1
comparison
equal deleted inserted replaced
215:f8bcd33bdd91 216:d1464997078d
1 (* Copyright (c) 2008, Adam Chlipala 1 (* Copyright (c) 2008-2009, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
68 Notation "[ ! , r # n ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ n)). 68 Notation "[ ! , r # n ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ n)).
69 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)).
70 70
71 (* begin thide *) 71 (* begin thide *)
72 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt := 72 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
73 hnil. 73 HNil.
74 Definition unit_den : datatypeDenote unit unit_dt := 74 Definition unit_den : datatypeDenote unit unit_dt :=
75 [!, ! ~> tt] ::: hnil. 75 [!, ! ~> tt] ::: HNil.
76 Definition bool_den : datatypeDenote bool bool_dt := 76 Definition bool_den : datatypeDenote bool bool_dt :=
77 [!, ! ~> true] ::: [!, ! ~> false] ::: hnil. 77 [!, ! ~> true] ::: [!, ! ~> false] ::: HNil.
78 Definition nat_den : datatypeDenote nat nat_dt := 78 Definition nat_den : datatypeDenote nat nat_dt :=
79 [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: hnil. 79 [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: HNil.
80 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) := 80 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
81 [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: hnil. 81 [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: HNil.
82 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) := 82 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
83 [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 *) 84 (* end thide *)
85 85
86 86
87 (** * Recursive Definitions *) 87 (** * Recursive Definitions *)
88 88
98 Definition Empty_set_fix : fixDenote Empty_set Empty_set_dt := 98 Definition Empty_set_fix : fixDenote Empty_set Empty_set_dt :=
99 fun R _ emp => match emp with end. 99 fun R _ emp => match emp with end.
100 Eval compute in size Empty_set_fix. 100 Eval compute in size Empty_set_fix.
101 101
102 Definition unit_fix : fixDenote unit unit_dt := 102 Definition unit_fix : fixDenote unit unit_dt :=
103 fun R cases _ => (fst cases) tt inil. 103 fun R cases _ => (hhd cases) tt INil.
104 Eval compute in size unit_fix. 104 Eval compute in size unit_fix.
105 105
106 Definition bool_fix : fixDenote bool bool_dt := 106 Definition bool_fix : fixDenote bool bool_dt :=
107 fun R cases b => if b 107 fun R cases b => if b
108 then (fst cases) tt inil 108 then (hhd cases) tt INil
109 else (fst (snd cases)) tt inil. 109 else (hhd (htl cases)) tt INil.
110 Eval compute in size bool_fix. 110 Eval compute in size bool_fix.
111 111
112 Definition nat_fix : fixDenote nat nat_dt := 112 Definition nat_fix : fixDenote nat nat_dt :=
113 fun R cases => fix F (n : nat) : R := 113 fun R cases => fix F (n : nat) : R :=
114 match n with 114 match n with
115 | O => (fst cases) tt inil 115 | O => (hhd cases) tt INil
116 | S n' => (fst (snd cases)) tt (icons (F n') inil) 116 | S n' => (hhd (htl cases)) tt (ICons (F n') INil)
117 end. 117 end.
118 Eval cbv beta iota delta -[plus] in size nat_fix. 118 Eval cbv beta iota delta -[plus] in size nat_fix.
119 119
120 Definition list_fix (A : Type) : fixDenote (list A) (list_dt A) := 120 Definition list_fix (A : Type) : fixDenote (list A) (list_dt A) :=
121 fun R cases => fix F (ls : list A) : R := 121 fun R cases => fix F (ls : list A) : R :=
122 match ls with 122 match ls with
123 | nil => (fst cases) tt inil 123 | nil => (hhd cases) tt INil
124 | x :: ls' => (fst (snd cases)) x (icons (F ls') inil) 124 | x :: ls' => (hhd (htl cases)) x (ICons (F ls') INil)
125 end. 125 end.
126 Eval cbv beta iota delta -[plus] in fun A => size (@list_fix A). 126 Eval cbv beta iota delta -[plus] in fun A => size (@list_fix A).
127 127
128 Definition tree_fix (A : Type) : fixDenote (tree A) (tree_dt A) := 128 Definition tree_fix (A : Type) : fixDenote (tree A) (tree_dt A) :=
129 fun R cases => fix F (t : tree A) : R := 129 fun R cases => fix F (t : tree A) : R :=
130 match t with 130 match t with
131 | Leaf x => (fst cases) x inil 131 | Leaf x => (hhd cases) x INil
132 | Node t1 t2 => (fst (snd cases)) tt (icons (F t1) (icons (F t2) inil)) 132 | Node t1 t2 => (hhd (htl cases)) tt (ICons (F t1) (ICons (F t2) INil))
133 end. 133 end.
134 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 *) 135 (* end thide *)
136 136
137 137
155 fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string) 155 fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string)
156 (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x 156 (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x
157 ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr). 157 ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr).
158 (* end thide *) 158 (* end thide *)
159 159
160 Eval compute in print hnil Empty_set_fix. 160 Eval compute in print HNil Empty_set_fix.
161 Eval compute in print (^ "tt" (fun _ => "") ::: hnil) unit_fix. 161 Eval compute in print (^ "tt" (fun _ => "") ::: HNil) unit_fix.
162 Eval compute in print (^ "true" (fun _ => "") 162 Eval compute in print (^ "true" (fun _ => "")
163 ::: ^ "false" (fun _ => "") 163 ::: ^ "false" (fun _ => "")
164 ::: hnil) bool_fix. 164 ::: HNil) bool_fix.
165 165
166 Definition print_nat := print (^ "O" (fun _ => "") 166 Definition print_nat := print (^ "O" (fun _ => "")
167 ::: ^ "S" (fun _ => "") 167 ::: ^ "S" (fun _ => "")
168 ::: hnil) nat_fix. 168 ::: HNil) nat_fix.
169 Eval cbv beta iota delta -[append] in print_nat. 169 Eval cbv beta iota delta -[append] in print_nat.
170 Eval simpl in print_nat 0. 170 Eval simpl in print_nat 0.
171 Eval simpl in print_nat 1. 171 Eval simpl in print_nat 1.
172 Eval simpl in print_nat 2. 172 Eval simpl in print_nat 2.
173 173
174 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) => 174 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
175 print (^ "nil" (fun _ => "") 175 print (^ "nil" (fun _ => "")
176 ::: ^ "cons" pr 176 ::: ^ "cons" pr
177 ::: hnil) (@list_fix A). 177 ::: HNil) (@list_fix A).
178 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) => 178 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
179 print (^ "Leaf" pr 179 print (^ "Leaf" pr
180 ::: ^ "Node" (fun _ => "") 180 ::: ^ "Node" (fun _ => "")
181 ::: hnil) (@tree_fix A). 181 ::: HNil) (@tree_fix A).
182 182
183 183
184 (** ** Mapping *) 184 (** ** Mapping *)
185 185
186 (* EX: Define a generic [map] function. *) 186 (* EX: Define a generic [map] function. *)
223 223
224 Definition fixDenoteOk := 224 Definition fixDenoteOk :=
225 forall (R : Type) (cases : datatypeDenote R dt) 225 forall (R : Type) (cases : datatypeDenote R dt)
226 c (m : member c dt) 226 c (m : member c dt)
227 (x : nonrecursive c) (r : ilist T (recursive c)), 227 (x : nonrecursive c) (r : ilist T (recursive c)),
228 fx R cases ((hget dd m) x r) 228 fx cases ((hget dd m) x r)
229 = (hget cases m) x (imap (fx R cases) r). 229 = (hget cases m) x (imap (fx cases) r).
230 End ok. 230 End ok.
231 231
232 Implicit Arguments datatypeDenoteOk [T dt]. 232 Implicit Arguments datatypeDenoteOk [T dt].
233 233
234 Lemma foldr_plus : forall n (ils : ilist nat n), 234 Lemma foldr_plus : forall n (ils : ilist nat n),
235 foldr plus 1 ils > 0. 235 foldr plus 1 ils > 0.
236 induction n; crush. 236 induction ils; crush.
237 generalize (IHn b); crush.
238 Qed. 237 Qed.
239 (* end thide *) 238 (* end thide *)
240 239
241 Theorem size_positive : forall T dt 240 Theorem size_positive : forall T dt
242 (dd : datatypeDenote T dt) (fx : fixDenote T dt) 241 (dd : datatypeDenote T dt) (fx : fixDenote T dt)
263 match goal with 262 match goal with
264 | [ |- hget _ _ _ ?R1 = hget _ _ _ ?R2 ] => replace R1 with R2 263 | [ |- hget _ _ _ ?R1 = hget _ _ _ ?R2 ] => replace R1 with R2
265 end; crush. 264 end; crush.
266 265
267 induction (recursive c); crush. 266 induction (recursive c); crush.
268 destruct r; reflexivity. 267 dep_destruct r; reflexivity.
269 destruct r; crush. 268 dep_destruct r; crush.
270 rewrite (H None). 269 rewrite (H First).
271 unfold icons.
272 f_equal. 270 f_equal.
273 apply IHn; crush. 271 apply IHn; crush.
274 apply (H (Some i0)). 272 apply (H (Next i)).
275 Qed. 273 Qed.
276 (* end thide *) 274 (* end thide *)