Mercurial > cpdt > repo

comparison src/OpSem.v @ 262:de53c8bcfa8d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
OpSem code
author Adam Chlipala <adamc@hcoop.net>
date Mon, 28 Dec 2009 12:35:44 -0500
parents src/Impure.v@2a34c4dc6a10
children af6f6d8dcfe7
comparison
equal deleted inserted replaced
261:0a644d7004d5 262:de53c8bcfa8d
1 (* Copyright (c) 2008-2009, Adam Chlipala
2 *
3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License.
6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *)
9
10 (* begin hide *)
11 Require Import Arith List.
12
13 Require Import Tactics.
14
15 Set Implicit Arguments.
16 (* end hide *)
17
18
19 (** %\chapter{Higher-Order Operational Semantics}% *)
20
21 (** * Closure Heaps *)
22
23 Section lookup.
24 Variable A : Type.
25
26 Fixpoint lookup (ls : list A) (n : nat) : option A :=
27 match ls with
28 | nil => None
29 | v :: ls' => if eq_nat_dec n (length ls') then Some v else lookup ls' n
30 end.
31
32 Definition extends (ls1 ls2 : list A) := exists ls, ls2 = ls ++ ls1.
33
34 Infix "##" := lookup (left associativity, at level 1).
35 Infix "~>" := extends (no associativity, at level 80).
36
37 Theorem lookup1 : forall x ls,
38 (x :: ls) ## (length ls) = Some x.
39 crush; match goal with
40 | [ |- context[if ?E then _ else _] ] => destruct E
41 end; crush.
42 Qed.
43
44 Theorem extends_refl : forall ls, ls ~> ls.
45 exists nil; reflexivity.
46 Qed.
47
48 Theorem extends1 : forall v ls, ls ~> v :: ls.
49 intros; exists (v :: nil); reflexivity.
50 Qed.
51
52 Theorem extends_trans : forall ls1 ls2 ls3,
53 ls1 ~> ls2
54 -> ls2 ~> ls3
55 -> ls1 ~> ls3.
56 intros ? ? ? [l1 ?] [l2 ?]; exists (l2 ++ l1); crush.
57 Qed.
58
59 Lemma lookup_contra : forall n v ls,
60 ls ## n = Some v
61 -> n >= length ls
62 -> False.
63 induction ls; crush;
64 match goal with
65 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
66 end; crush.
67 Qed.
68
69 Hint Resolve lookup_contra.
70
71 Theorem extends_lookup : forall ls1 ls2 n v,
72 ls1 ~> ls2
73 -> ls1 ## n = Some v
74 -> ls2 ## n = Some v.
75 intros ? ? ? ? [l ?]; crush; induction l; crush;
76 match goal with
77 | [ |- context[if ?E then _ else _] ] => destruct E
78 end; crush; elimtype False; eauto.
79 Qed.
80 End lookup.
81
82 Infix "##" := lookup (left associativity, at level 1).
83 Infix "~>" := extends (no associativity, at level 80).
84
85 Hint Resolve lookup1 extends_refl extends1 extends_trans extends_lookup.
86
87
88 (** * Languages and Translation *)
89
90 Module Source.
91 Section exp.
92 Variable var : Type.
93
94 Inductive exp : Type :=
95 | Var : var -> exp
96 | App : exp -> exp -> exp
97 | Abs : (var -> exp) -> exp
98 | Bool : bool -> exp.
99 End exp.
100
101 Implicit Arguments Bool [var].
102
103 Definition Exp := forall var, exp var.
104
105 Inductive val : Set :=
106 | VFun : nat -> val
107 | VBool : bool -> val.
108
109 Definition closure := val -> exp val.
110 Definition closures := list closure.
111
112 Inductive eval : closures -> exp val -> closures -> val -> Prop :=
113 | EvVar : forall cs v,
114 eval cs (Var v) cs v
115
116 | EvApp : forall cs1 e1 e2 cs2 v1 c cs3 v2 cs4 v3,
117 eval cs1 e1 cs2 (VFun v1)
118 -> eval cs2 e2 cs3 v2
119 -> cs2 ## v1 = Some c
120 -> eval cs3 (c v2) cs4 v3
121 -> eval cs1 (App e1 e2) cs4 v3
122
123 | EvAbs : forall cs c,
124 eval cs (Abs c) (c :: cs) (VFun (length cs))
125
126 | EvBool : forall cs b,
127 eval cs (Bool b) cs (VBool b).
128
129 Definition Eval (cs1 : closures) (E : Exp) (cs2 : closures) (v : val) := eval cs1 (E _) cs2 v.
130
131 Section exp_equiv.
132 Variables var1 var2 : Type.
133
134 Inductive exp_equiv : list (var1 * var2) -> exp var1 -> exp var2 -> Prop :=
135 | EqVar : forall G v1 v2,
136 In (v1, v2) G
137 -> exp_equiv G (Var v1) (Var v2)
138
139 | EqApp : forall G f1 x1 f2 x2,
140 exp_equiv G f1 f2
141 -> exp_equiv G x1 x2
142 -> exp_equiv G (App f1 x1) (App f2 x2)
143 | EqAbs : forall G f1 f2,
144 (forall v1 v2, exp_equiv ((v1, v2) :: G) (f1 v1) (f2 v2))
145 -> exp_equiv G (Abs f1) (Abs f2)
146
147 | EqBool : forall G b,
148 exp_equiv G (Bool b) (Bool b).
149 End exp_equiv.
150
151 Definition Wf (E : Exp) := forall var1 var2, exp_equiv nil (E var1) (E var2).
152 End Source.
153
154 Module CPS.
155 Section exp.
156 Variable var : Type.
157
158 Inductive prog : Type :=
159 | Halt : var -> prog
160 | App : var -> var -> prog
161 | Bind : primop -> (var -> prog) -> prog
162
163 with primop : Type :=
164 | Abs : (var -> prog) -> primop
165
166 | Bool : bool -> primop
167
168 | Pair : var -> var -> primop
169 | Fst : var -> primop
170 | Snd : var -> primop.
171 End exp.
172
173 Implicit Arguments Bool [var].
174
175 Notation "x <- p ; e" := (Bind p (fun x => e))
176 (right associativity, at level 76, p at next level).
177
178 Definition Prog := forall var, prog var.
179 Definition Primop := forall var, primop var.
180
181 Inductive val : Type :=
182 | VFun : nat -> val
183 | VBool : bool -> val
184 | VPair : val -> val -> val.
185 Definition closure := val -> prog val.
186 Definition closures := list closure.
187
188 Inductive eval : closures -> prog val -> val -> Prop :=
189 | EvHalt : forall cs v,
190 eval cs (Halt v) v
191
192 | EvApp : forall cs n v2 c v3,
193 cs ## n = Some c
194 -> eval cs (c v2) v3
195 -> eval cs (App (VFun n) v2) v3
196
197 | EvBind : forall cs1 p e cs2 v1 v2,
198 evalP cs1 p cs2 v1
199 -> eval cs2 (e v1) v2
200 -> eval cs1 (Bind p e) v2
201
202 with evalP : closures -> primop val -> closures -> val -> Prop :=
203 | EvAbs : forall cs c,
204 evalP cs (Abs c) (c :: cs) (VFun (length cs))
205
206 | EvPair : forall cs v1 v2,
207 evalP cs (Pair v1 v2) cs (VPair v1 v2)
208 | EvFst : forall cs v1 v2,
209 evalP cs (Fst (VPair v1 v2)) cs v1
210 | EvSnd : forall cs v1 v2,
211 evalP cs (Snd (VPair v1 v2)) cs v2
212
213 | EvBool : forall cs b,
214 evalP cs (Bool b) cs (VBool b).
215
216 Definition Eval (cs : closures) (P : Prog) (v : val) := eval cs (P _) v.
217 End CPS.
218
219 Import Source CPS.
220
221 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
222
223 Section cpsExp.
224 Variable var : Type.
225
226 Import Source.
227
228 Fixpoint cpsExp (e : exp var)
229 : (var -> prog var) -> prog var :=
230 match e with
231 | Var v => fun k => k v
232
233 | App e1 e2 => fun k =>
234 f <-- e1;
235 x <-- e2;
236 kf <- CPS.Abs k;
237 p <- Pair x kf;
238 CPS.App f p
239 | Abs e' => fun k =>
240 f <- CPS.Abs (var := var) (fun p =>
241 x <- Fst p;
242 kf <- Snd p;
243 r <-- e' x;
244 CPS.App kf r);
245 k f
246
247 | Bool b => fun k =>
248 x <- CPS.Bool b;
249 k x
250 end
251
252 where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
253 End cpsExp.
254
255 Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
256
257 Definition CpsExp (E : Exp) : Prog := fun _ => cpsExp (E _) (Halt (var := _)).
258
259
260 (** * Correctness Proof *)
261
262 Definition cpsFunc var (e' : var -> Source.exp var) :=
263 fun p : var =>
264 x <- Fst p;
265 kf <- Snd p;
266 r <-- e' x;
267 CPS.App kf r.
268
269 Section cr.
270 Variable s1 : Source.closures.
271 Variable s2 : CPS.closures.
272
273 Import Source.
274
275 Inductive cr : Source.val -> CPS.val -> Prop :=
276 | CrFun : forall l1 l2 G f1 f2,
277 (forall x1 x2, exp_equiv ((x1, x2) :: G) (f1 x1) (f2 x2))
278 -> (forall x1 x2, In (x1, x2) G -> cr x1 x2)
279 -> s1 ## l1 = Some f1
280 -> s2 ## l2 = Some (cpsFunc f2)
281 -> cr (Source.VFun l1) (CPS.VFun l2)
282
283 | CrBool : forall b,
284 cr (Source.VBool b) (CPS.VBool b).
285 End cr.
286
287 Notation "s1 & s2 |-- v1 ~~ v2" := (cr s1 s2 v1 v2) (no associativity, at level 70).
288
289 Hint Constructors cr.
290
291 Lemma eval_monotone : forall cs1 e cs2 v,
292 Source.eval cs1 e cs2 v
293 -> cs1 ~> cs2.
294 induction 1; crush; eauto.
295 Qed.
296
297 Lemma cr_monotone : forall cs1 cs2 cs1' cs2',
298 cs1 ~> cs1'
299 -> cs2 ~> cs2'
300 -> forall v1 v2, cs1 & cs2 |-- v1 ~~ v2
301 -> cs1' & cs2' |-- v1 ~~ v2.
302 induction 3; crush; eauto.
303 Qed.
304
305 Hint Resolve eval_monotone cr_monotone.
306
307 Lemma push : forall G s1 s2 v1' v2',
308 (forall v1 v2, In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2)
309 -> s1 & s2 |-- v1' ~~ v2'
310 -> (forall v1 v2, (v1', v2') = (v1, v2) \/ In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2).
311 crush.
312 Qed.
313
314 Hint Resolve push.
315
316 Ltac evalOne :=
317 match goal with
318 | [ |- CPS.eval ?cs ?e ?v ] =>
319 let e := eval hnf in e in
320 change (CPS.eval cs e v);
321 econstructor; [ solve [ eauto ] | ]
322 end.
323
324 Hint Constructors evalP.
325 Hint Extern 1 (CPS.eval _ _ _) => evalOne; repeat evalOne.
326
327 Lemma cpsExp_correct : forall s1 e1 s1' r1,
328 Source.eval s1 e1 s1' r1
329 -> forall G (e2 : exp CPS.val),
330 exp_equiv G e1 e2
331 -> forall s2,
332 (forall v1 v2, In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2)
333 -> forall k, exists s2', exists r2,
334 (forall r, CPS.eval s2' (k r2) r
335 -> CPS.eval s2 (cpsExp e2 k) r)
336 /\ s1' & s2' |-- r1 ~~ r2
337 /\ s2 ~> s2'.
338 induction 1; inversion 1; crush;
339 repeat (match goal with
340 | [ H : _ & _ |-- Source.VFun _ ~~ _ |- _ ] => inversion H; clear H
341 | [ H1 : ?E = _, H2 : ?E = _ |- _ ] => rewrite H1 in H2; clear H1
342 | [ H : forall G e2, exp_equiv G ?E e2 -> _ |- _ ] =>
343 match goal with
344 | [ _ : Source.eval ?CS E _ _, _ : Source.eval _ ?E' ?CS _,
345 _ : forall G e2, exp_equiv G ?E' e2 -> _ |- _ ] => fail 1
346 | _ => match goal with
347 | [ k : val -> prog val, _ : _ & ?cs |-- _ ~~ _, _ : context[VFun] |- _ ] =>
348 guess (k :: cs) H
349 | _ => guess tt H
350 end
351 end
352 end; crush); eauto 13.
353 Qed.
354
355 Lemma CpsExp_correct : forall E cs b,
356 Source.Eval nil E cs (Source.VBool b)
357 -> Wf E
358 -> CPS.Eval nil (CpsExp E) (CPS.VBool b).
359 Hint Constructors CPS.eval.
360
361 unfold Source.Eval, CPS.Eval, CpsExp; intros ? ? ? H1 H2;
362 generalize (cpsExp_correct H1 (H2 _ _) (s2 := nil)
363 (fun _ _ pf => match pf with end) (Halt (var := _))); crush;
364 match goal with
365 | [ H : _ & _ |-- _ ~~ _ |- _ ] => inversion H
366 end; crush.
367 Qed.