Mercurial > cpdt > repo

comparison src/Interps.v @ 172:653c03f6061e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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.