Mercurial > cpdt > repo
comparison src/Interps.v @ 172:653c03f6061e
Examples; pair optimization
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 09 Nov 2008 14:24:31 -0500 |
parents | b00b6a9b6b58 |
children | 7fd470d8a788 |
comparison
equal
deleted
inserted
replaced
171:b00b6a9b6b58 | 172:653c03f6061e |
---|---|
64 Infix "+^" := Plus (left associativity, at level 79). | 64 Infix "+^" := Plus (left associativity, at level 79). |
65 | 65 |
66 Infix "@" := App (left associativity, at level 77). | 66 Infix "@" := App (left associativity, at level 77). |
67 Notation "\ x , e" := (Abs (fun x => e)) (at level 78). | 67 Notation "\ x , e" := (Abs (fun x => e)) (at level 78). |
68 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78). | 68 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78). |
69 | |
70 Definition zero : Exp Nat := fun _ => ^0. | |
71 Definition one : Exp Nat := fun _ => ^1. | |
72 Definition zpo : Exp Nat := fun _ => zero _ +^ one _. | |
73 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x. | |
74 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _. | |
75 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => | |
76 \f, \x, #f @ #x. | |
77 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _. | |
69 | 78 |
70 Fixpoint typeDenote (t : type) : Set := | 79 Fixpoint typeDenote (t : type) : Set := |
71 match t with | 80 match t with |
72 | Nat => nat | 81 | Nat => nat |
73 | t1 --> t2 => typeDenote t1 -> typeDenote t2 | 82 | t1 --> t2 => typeDenote t1 -> typeDenote t2 |
83 | App _ _ e1 e2 => (expDenote e1) (expDenote e2) | 92 | App _ _ e1 e2 => (expDenote e1) (expDenote e2) |
84 | Abs _ _ e' => fun x => expDenote (e' x) | 93 | Abs _ _ e' => fun x => expDenote (e' x) |
85 end. | 94 end. |
86 | 95 |
87 Definition ExpDenote t (e : Exp t) := expDenote (e _). | 96 Definition ExpDenote t (e : Exp t) := expDenote (e _). |
97 | |
98 Eval compute in ExpDenote zero. | |
99 Eval compute in ExpDenote one. | |
100 Eval compute in ExpDenote zpo. | |
101 Eval compute in ExpDenote ident. | |
102 Eval compute in ExpDenote app_ident. | |
103 Eval compute in ExpDenote app. | |
104 Eval compute in ExpDenote app_ident'. | |
88 | 105 |
89 Section cfold. | 106 Section cfold. |
90 Variable var : type -> Type. | 107 Variable var : type -> Type. |
91 | 108 |
92 Fixpoint cfold t (e : exp var t) {struct e} : exp var t := | 109 Fixpoint cfold t (e : exp var t) {struct e} : exp var t := |
189 Implicit Arguments Inr [var t1 t2]. | 206 Implicit Arguments Inr [var t1 t2]. |
190 | 207 |
191 Notation "# v" := (Var v) (at level 70). | 208 Notation "# v" := (Var v) (at level 70). |
192 | 209 |
193 Notation "^ n" := (Const n) (at level 70). | 210 Notation "^ n" := (Const n) (at level 70). |
194 Infix "+^" := Plus (left associativity, at level 79). | 211 Infix "+^" := Plus (left associativity, at level 78). |
195 | 212 |
196 Infix "@" := App (left associativity, at level 77). | 213 Infix "@" := App (left associativity, at level 77). |
197 Notation "\ x , e" := (Abs (fun x => e)) (at level 78). | 214 Notation "\ x , e" := (Abs (fun x => e)) (at level 78). |
198 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78). | 215 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78). |
199 | 216 |
201 Notation "#1 e" := (Fst e) (at level 75). | 218 Notation "#1 e" := (Fst e) (at level 75). |
202 Notation "#2 e" := (Snd e) (at level 75). | 219 Notation "#2 e" := (Snd e) (at level 75). |
203 | 220 |
204 Notation "'case' e 'of' x => e1 | y => e2" := (SumCase e (fun x => e1) (fun y => e2)) | 221 Notation "'case' e 'of' x => e1 | y => e2" := (SumCase e (fun x => e1) (fun y => e2)) |
205 (at level 79). | 222 (at level 79). |
223 | |
224 Definition swap : Exp (Nat ** Nat --> Nat ** Nat) := fun _ => | |
225 \p, [#2 #p, #1 #p]. | |
226 Definition zo : Exp (Nat ** Nat) := fun _ => [^0, ^1]. | |
227 Definition swap_zo : Exp (Nat ** Nat) := fun _ => swap _ @ zo _. | |
228 | |
229 Definition natOut : Exp (Nat ++ Nat --> Nat) := fun _ => | |
230 \s, case #s of x => #x | y => #y +^ #y. | |
231 Definition ns1 : Exp (Nat ++ Nat) := fun _ => Inl (^3). | |
232 Definition ns2 : Exp (Nat ++ Nat) := fun _ => Inr (^5). | |
233 Definition natOut_ns1 : Exp Nat := fun _ => natOut _ @ ns1 _. | |
234 Definition natOut_ns2 : Exp Nat := fun _ => natOut _ @ ns2 _. | |
206 | 235 |
207 Fixpoint typeDenote (t : type) : Set := | 236 Fixpoint typeDenote (t : type) : Set := |
208 match t with | 237 match t with |
209 | Nat => nat | 238 | Nat => nat |
210 | t1 --> t2 => typeDenote t1 -> typeDenote t2 | 239 | t1 --> t2 => typeDenote t1 -> typeDenote t2 |
235 end | 264 end |
236 end. | 265 end. |
237 | 266 |
238 Definition ExpDenote t (e : Exp t) := expDenote (e _). | 267 Definition ExpDenote t (e : Exp t) := expDenote (e _). |
239 | 268 |
269 Eval compute in ExpDenote swap. | |
270 Eval compute in ExpDenote zo. | |
271 Eval compute in ExpDenote swap_zo. | |
272 | |
273 Eval compute in ExpDenote natOut. | |
274 Eval compute in ExpDenote ns1. | |
275 Eval compute in ExpDenote ns2. | |
276 Eval compute in ExpDenote natOut_ns1. | |
277 Eval compute in ExpDenote natOut_ns2. | |
278 | |
240 Section cfold. | 279 Section cfold. |
241 Variable var : type -> Type. | 280 Variable var : type -> Type. |
281 | |
282 Definition pairOutType t := | |
283 match t with | |
284 | t1 ** t2 => option (exp var t1 * exp var t2) | |
285 | _ => unit | |
286 end. | |
287 | |
288 Definition pairOutDefault (t : type) : pairOutType t := | |
289 match t return pairOutType t with | |
290 | _ ** _ => None | |
291 | _ => tt | |
292 end. | |
293 | |
294 Definition pairOut t1 t2 (e : exp var (t1 ** t2)) : option (exp var t1 * exp var t2) := | |
295 match e in exp _ t return pairOutType t with | |
296 | Pair _ _ e1 e2 => Some (e1, e2) | |
297 | _ => pairOutDefault _ | |
298 end. | |
242 | 299 |
243 Fixpoint cfold t (e : exp var t) {struct e} : exp var t := | 300 Fixpoint cfold t (e : exp var t) {struct e} : exp var t := |
244 match e in exp _ t return exp _ t with | 301 match e in exp _ t return exp _ t with |
245 | Var _ v => #v | 302 | Var _ v => #v |
246 | 303 |
255 | 312 |
256 | App _ _ e1 e2 => cfold e1 @ cfold e2 | 313 | App _ _ e1 e2 => cfold e1 @ cfold e2 |
257 | Abs _ _ e' => Abs (fun x => cfold (e' x)) | 314 | Abs _ _ e' => Abs (fun x => cfold (e' x)) |
258 | 315 |
259 | Pair _ _ e1 e2 => [cfold e1, cfold e2] | 316 | Pair _ _ e1 e2 => [cfold e1, cfold e2] |
260 | Fst _ _ e' => #1 (cfold e') | 317 | Fst t1 _ e' => |
261 | Snd _ _ e' => #2 (cfold e') | 318 let e'' := cfold e' in |
319 match pairOut e'' with | |
320 | None => #1 e'' | |
321 | Some (e1, _) => e1 | |
322 end | |
323 | Snd _ _ e' => | |
324 let e'' := cfold e' in | |
325 match pairOut e'' with | |
326 | None => #2 e'' | |
327 | Some (_, e2) => e2 | |
328 end | |
262 | 329 |
263 | Inl _ _ e' => Inl (cfold e') | 330 | Inl _ _ e' => Inl (cfold e') |
264 | Inr _ _ e' => Inr (cfold e') | 331 | Inr _ _ e' => Inr (cfold e') |
265 | SumCase _ _ _ e' e1 e2 => | 332 | SumCase _ _ _ e' e1 e2 => |
266 case cfold e' of | 333 case cfold e' of |
269 end. | 336 end. |
270 End cfold. | 337 End cfold. |
271 | 338 |
272 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _). | 339 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _). |
273 | 340 |
341 Section pairs. | |
342 Variables A B : Type. | |
343 | |
344 Variable v1 : A. | |
345 Variable v2 : B. | |
346 Variable v : A * B. | |
347 | |
348 Theorem pair_eta1 : (v1, v2) = v -> v1 = fst v. | |
349 destruct v; crush. | |
350 Qed. | |
351 | |
352 Theorem pair_eta2 : (v1, v2) = v -> v2 = snd v. | |
353 destruct v; crush. | |
354 Qed. | |
355 End pairs. | |
356 | |
357 Hint Resolve pair_eta1 pair_eta2. | |
358 | |
274 Lemma cfold_correct : forall t (e : exp _ t), | 359 Lemma cfold_correct : forall t (e : exp _ t), |
275 expDenote (cfold e) = expDenote e. | 360 expDenote (cfold e) = expDenote e. |
276 induction e; crush; try (ext_eq; crush); | 361 induction e; crush; try (ext_eq; crush); |
277 repeat (match goal with | 362 repeat (match goal with |
278 | [ |- context[cfold ?E] ] => dep_destruct (cfold E) | 363 | [ |- context[cfold ?E] ] => dep_destruct (cfold E) |
279 | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E | 364 | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E |
280 end; crush). | 365 end; crush); eauto. |
281 Qed. | 366 Qed. |
282 | 367 |
283 Theorem Cfold_correct : forall t (E : Exp t), | 368 Theorem Cfold_correct : forall t (E : Exp t), |
284 ExpDenote (Cfold E) = ExpDenote E. | 369 ExpDenote (Cfold E) = ExpDenote E. |
285 unfold ExpDenote, Cfold; intros; apply cfold_correct. | 370 unfold ExpDenote, Cfold; intros; apply cfold_correct. |