Mercurial > cpdt > repo
comparison src/Extensional.v @ 256:4293dd6912cd
Prosified Extensional
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 16 Dec 2009 15:31:54 -0500 |
parents | 0400fa005d5a |
children | 108ec446fbaf |
comparison
equal
deleted
inserted
replaced
255:05250878e4ca | 256:4293dd6912cd |
---|---|
16 (* end hide *) | 16 (* end hide *) |
17 | 17 |
18 | 18 |
19 (** %\chapter{Extensional Transformations}% *) | 19 (** %\chapter{Extensional Transformations}% *) |
20 | 20 |
21 (** TODO: Prose for this chapter *) | 21 (** Last chapter's constant folding example was particularly easy to verify, because that transformation used the same source and target language. In this chapter, we verify a different translation, illustrating the added complexities in translating between languages. |
22 | 22 |
23 | 23 Program transformations can be classified as %\textit{%#<i>#intensional#</i>#%}%, when they require some notion of inequality between variables; or %\textit{%#<i>#extensional#</i>#%}%, otherwise. This chapter's example is extensional, and the next chapter deals with the trickier intensional case. *) |
24 (** * Simply-Typed Lambda Calculus *) | 24 |
25 | 25 |
26 Module STLC. | 26 (** * CPS Conversion for Simply-Typed Lambda Calculus *) |
27 Module Source. | 27 |
28 Inductive type : Type := | 28 (** A convenient method for compiling functional programs begins with conversion to %\textit{%#<i>#continuation-passing style#</i>#%}%, or CPS. In this restricted form, function calls never return; instead, we pass explicit return pointers, much as in assembly language. Additionally, we make order of evaluation explicit, breaking complex expressions into sequences of primitive operations. |
29 | TNat : type | 29 |
30 | Arrow : type -> type -> type. | 30 Our translation will operate over the same source language that we used in the first part of last chapter, so we omit most of the language definition. However, we do make one significant change: since we will be working with multiple languages that involve similar constructs, we use Coq's %\textit{%#<i>#notation scope#</i>#%}% mechanism to disambiguate. For instance, the span of code dealing with type notations looks like this: *) |
31 | 31 |
32 Notation "'Nat'" := TNat : source_scope. | 32 (* begin hide *) |
33 Infix "-->" := Arrow (right associativity, at level 60) : source_scope. | 33 Module Source. |
34 | 34 Inductive type : Type := |
35 Open Scope source_scope. | 35 | TNat : type |
36 Bind Scope source_scope with type. | 36 | Arrow : type -> type -> type. |
37 Delimit Scope source_scope with source. | 37 (* end hide *) |
38 | 38 |
39 Section vars. | 39 Notation "'Nat'" := TNat : source_scope. |
40 Variable var : type -> Type. | 40 Infix "-->" := Arrow (right associativity, at level 60) : source_scope. |
41 | 41 |
42 Inductive exp : type -> Type := | 42 Open Scope source_scope. |
43 | Var : forall t, | 43 Bind Scope source_scope with type. |
44 var t | 44 Delimit Scope source_scope with source. |
45 -> exp t | 45 |
46 | 46 (** We explicitly place our notations inside a scope named [source_scope], and we associate a delimiting key [source] with [source_scope]. Without further commands, our notations would only be used in expressions like [(...)%source]. We also open our scope locally within this module, so that we avoid repeating [%source] in many places. Further, we %\textit{%#<i>#bind#</i>#%}% our scope to [type]. In some circumstances where Coq is able to infer that some subexpression has type [type], that subexpression will automatically be parsed in [source_scope]. *) |
47 | Const : nat -> exp Nat | 47 |
48 | Plus : exp Nat -> exp Nat -> exp Nat | 48 (* begin hide *) |
49 | 49 Section vars. |
50 | App : forall t1 t2, | 50 Variable var : type -> Type. |
51 exp (t1 --> t2) | 51 |
52 -> exp t1 | 52 Inductive exp : type -> Type := |
53 -> exp t2 | 53 | Var : forall t, |
54 | Abs : forall t1 t2, | 54 var t |
55 (var t1 -> exp t2) | 55 -> exp t |
56 -> exp (t1 --> t2). | 56 |
57 End vars. | 57 | Const : nat -> exp Nat |
58 | 58 | Plus : exp Nat -> exp Nat -> exp Nat |
59 Definition Exp t := forall var, exp var t. | 59 |
60 | 60 | App : forall t1 t2, |
61 Implicit Arguments Var [var t]. | 61 exp (t1 --> t2) |
62 Implicit Arguments Const [var]. | 62 -> exp t1 |
63 Implicit Arguments Plus [var]. | 63 -> exp t2 |
64 Implicit Arguments App [var t1 t2]. | 64 | Abs : forall t1 t2, |
65 Implicit Arguments Abs [var t1 t2]. | 65 (var t1 -> exp t2) |
66 | 66 -> exp (t1 --> t2). |
67 Notation "# v" := (Var v) (at level 70) : source_scope. | 67 End vars. |
68 | 68 |
69 Notation "^ n" := (Const n) (at level 70) : source_scope. | 69 Definition Exp t := forall var, exp var t. |
70 Infix "+^" := Plus (left associativity, at level 79) : source_scope. | 70 |
71 | 71 Implicit Arguments Var [var t]. |
72 Infix "@" := App (left associativity, at level 77) : source_scope. | 72 Implicit Arguments Const [var]. |
73 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope. | 73 Implicit Arguments Plus [var]. |
74 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope. | 74 Implicit Arguments App [var t1 t2]. |
75 | 75 Implicit Arguments Abs [var t1 t2]. |
76 Bind Scope source_scope with exp. | 76 |
77 | 77 Notation "# v" := (Var v) (at level 70) : source_scope. |
78 Definition zero : Exp Nat := fun _ => ^0. | 78 |
79 Definition one : Exp Nat := fun _ => ^1. | 79 Notation "^ n" := (Const n) (at level 70) : source_scope. |
80 Definition zpo : Exp Nat := fun _ => zero _ +^ one _. | 80 Infix "+^" := Plus (left associativity, at level 79) : source_scope. |
81 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x. | 81 |
82 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _. | 82 Infix "@" := App (left associativity, at level 77) : source_scope. |
83 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => | 83 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope. |
84 \f, \x, #f @ #x. | 84 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope. |
85 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _. | 85 |
86 | 86 Bind Scope source_scope with exp. |
87 Fixpoint typeDenote (t : type) : Set := | 87 |
88 match t with | 88 Definition zero : Exp Nat := fun _ => ^0. |
89 | Nat => nat | 89 Definition one : Exp Nat := fun _ => ^1. |
90 | t1 --> t2 => typeDenote t1 -> typeDenote t2 | 90 Definition zpo : Exp Nat := fun _ => zero _ +^ one _. |
91 end. | 91 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x. |
92 | 92 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _. |
93 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t := | 93 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => |
94 match e with | 94 \f, \x, #f @ #x. |
95 | Var _ v => v | 95 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _. |
96 | 96 |
97 | Const n => n | 97 Fixpoint typeDenote (t : type) : Set := |
98 | Plus e1 e2 => expDenote e1 + expDenote e2 | 98 match t with |
99 | 99 | Nat => nat |
100 | App _ _ e1 e2 => (expDenote e1) (expDenote e2) | 100 | t1 --> t2 => typeDenote t1 -> typeDenote t2 |
101 | Abs _ _ e' => fun x => expDenote (e' x) | 101 end. |
102 end. | 102 |
103 | 103 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t := |
104 Definition ExpDenote t (e : Exp t) := expDenote (e _). | 104 match e with |
105 | Var _ v => v | |
106 | |
107 | Const n => n | |
108 | Plus e1 e2 => expDenote e1 + expDenote e2 | |
109 | |
110 | App _ _ e1 e2 => (expDenote e1) (expDenote e2) | |
111 | Abs _ _ e' => fun x => expDenote (e' x) | |
112 end. | |
113 | |
114 Definition ExpDenote t (e : Exp t) := expDenote (e _). | |
115 (* end hide *) | |
116 | |
117 (** The other critical new ingredient is a generalization of the [Closed] relation from two chapters ago. The new relation [exp_equiv] characters when two expressions may be considered syntactically equal. We need to be able to handle cases where each expression uses a different [var] type. Intuitively, we will want to compare expressions that use their variables to store source-level and target-level values. We express pairs of equivalent variables using a list parameter to the relation; variable expressions will be considered equivalent if and only if their variables belong to this list. The rule for function abstraction extends the list in a higher-order way. The remaining rules just implement the obvious congruence over expressions. *) | |
105 | 118 |
106 (* begin thide *) | 119 (* begin thide *) |
107 Section exp_equiv. | 120 Section exp_equiv. |
108 Variables var1 var2 : type -> Type. | 121 Variables var1 var2 : type -> Type. |
109 | 122 |
110 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type | 123 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type |
111 -> forall t, exp var1 t -> exp var2 t -> Prop := | 124 -> forall t, exp var1 t -> exp var2 t -> Prop := |
112 | EqVar : forall G t (v1 : var1 t) v2, | 125 | EqVar : forall G t (v1 : var1 t) v2, |
113 In (existT _ t (v1, v2)) G | 126 In (existT _ t (v1, v2)) G |
114 -> exp_equiv G (#v1) (#v2) | 127 -> exp_equiv G (#v1) (#v2) |
115 | 128 |
116 | EqConst : forall G n, | 129 | EqConst : forall G n, |
117 exp_equiv G (^n) (^n) | 130 exp_equiv G (^n) (^n) |
118 | EqPlus : forall G x1 y1 x2 y2, | 131 | EqPlus : forall G x1 y1 x2 y2, |
119 exp_equiv G x1 x2 | 132 exp_equiv G x1 x2 |
120 -> exp_equiv G y1 y2 | 133 -> exp_equiv G y1 y2 |
121 -> exp_equiv G (x1 +^ y1) (x2 +^ y2) | 134 -> exp_equiv G (x1 +^ y1) (x2 +^ y2) |
122 | 135 |
123 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2, | 136 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2, |
124 exp_equiv G f1 f2 | 137 exp_equiv G f1 f2 |
125 -> exp_equiv G x1 x2 | 138 -> exp_equiv G x1 x2 |
126 -> exp_equiv G (f1 @ x1) (f2 @ x2) | 139 -> exp_equiv G (f1 @ x1) (f2 @ x2) |
127 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2, | 140 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2, |
128 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2)) | 141 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2)) |
129 -> exp_equiv G (Abs f1) (Abs f2). | 142 -> exp_equiv G (Abs f1) (Abs f2). |
130 End exp_equiv. | 143 End exp_equiv. |
131 | 144 |
132 Axiom Exp_equiv : forall t (E : Exp t) var1 var2, | 145 (** It turns out that, for any parametric expression [E], any two instantiations of [E] with particular [var] types must be equivalent, with respect to an empty variable list. The parametricity of Gallina guarantees this, in much the same way that it guaranteed the truth of the axiom about [Closed]. Thus, we assert an analogous axiom here. *) |
133 exp_equiv nil (E var1) (E var2). | 146 |
147 Axiom Exp_equiv : forall t (E : Exp t) var1 var2, | |
148 exp_equiv nil (E var1) (E var2). | |
134 (* end thide *) | 149 (* end thide *) |
135 End Source. | 150 End Source. |
136 | 151 |
137 Module CPS. | 152 (** Now we need to define the CPS language, where binary function types are replaced with unary continuation types, and we add product types because they will be useful in our translation. *) |
138 Inductive type : Type := | 153 |
139 | TNat : type | 154 Module CPS. |
140 | Cont : type -> type | 155 Inductive type : Type := |
141 | TUnit : type | 156 | TNat : type |
142 | Prod : type -> type -> type. | 157 | Cont : type -> type |
143 | 158 | Prod : type -> type -> type. |
144 Notation "'Nat'" := TNat : cps_scope. | 159 |
145 Notation "'Unit'" := TUnit : cps_scope. | 160 Notation "'Nat'" := TNat : cps_scope. |
146 Notation "t --->" := (Cont t) (at level 61) : cps_scope. | 161 Notation "t --->" := (Cont t) (at level 61) : cps_scope. |
147 Infix "**" := Prod (right associativity, at level 60) : cps_scope. | 162 Infix "**" := Prod (right associativity, at level 60) : cps_scope. |
148 | 163 |
149 Bind Scope cps_scope with type. | 164 Bind Scope cps_scope with type. |
150 Delimit Scope cps_scope with cps. | 165 Delimit Scope cps_scope with cps. |
151 | 166 |
152 Section vars. | 167 Section vars. |
153 Variable var : type -> Type. | 168 Variable var : type -> Type. |
154 | 169 |
155 Inductive prog : Type := | 170 (** A CPS program is a series of bindings of primitive operations (primops), followed by either a halt with a final program result or by a call to a continuation. The arguments to these program-ending operations are enforced to be variables. To use the values of compound expressions instead, those expressions must be decomposed into bindings of primops. The primop language itself similarly forces variables for all arguments besides bodies of function abstractions. *) |
156 | PHalt : | 171 |
157 var Nat | 172 Inductive prog : Type := |
158 -> prog | 173 | PHalt : |
159 | App : forall t, | 174 var Nat |
160 var (t --->) | 175 -> prog |
161 -> var t | 176 | App : forall t, |
162 -> prog | 177 var (t --->) |
163 | Bind : forall t, | 178 -> var t |
164 primop t | 179 -> prog |
165 -> (var t -> prog) | 180 | Bind : forall t, |
166 -> prog | 181 primop t |
167 | 182 -> (var t -> prog) |
168 with primop : type -> Type := | 183 -> prog |
169 | Var : forall t, | 184 |
170 var t | 185 with primop : type -> Type := |
171 -> primop t | 186 | Const : nat -> primop Nat |
172 | 187 | Plus : var Nat -> var Nat -> primop Nat |
173 | Const : nat -> primop Nat | 188 |
174 | Plus : var Nat -> var Nat -> primop Nat | 189 | Abs : forall t, |
175 | 190 (var t -> prog) |
176 | Abs : forall t, | 191 -> primop (t --->) |
177 (var t -> prog) | 192 |
178 -> primop (t --->) | 193 | Pair : forall t1 t2, |
179 | 194 var t1 |
180 | Pair : forall t1 t2, | 195 -> var t2 |
181 var t1 | 196 -> primop (t1 ** t2) |
182 -> var t2 | 197 | Fst : forall t1 t2, |
183 -> primop (t1 ** t2) | 198 var (t1 ** t2) |
184 | Fst : forall t1 t2, | 199 -> primop t1 |
185 var (t1 ** t2) | 200 | Snd : forall t1 t2, |
186 -> primop t1 | 201 var (t1 ** t2) |
187 | Snd : forall t1 t2, | 202 -> primop t2. |
188 var (t1 ** t2) | 203 End vars. |
189 -> primop t2. | 204 |
190 End vars. | 205 Implicit Arguments PHalt [var]. |
191 | 206 Implicit Arguments App [var t]. |
192 Implicit Arguments PHalt [var]. | 207 |
193 Implicit Arguments App [var t]. | 208 Implicit Arguments Const [var]. |
194 | 209 Implicit Arguments Plus [var]. |
195 Implicit Arguments Var [var t]. | 210 Implicit Arguments Abs [var t]. |
196 Implicit Arguments Const [var]. | 211 Implicit Arguments Pair [var t1 t2]. |
197 Implicit Arguments Plus [var]. | 212 Implicit Arguments Fst [var t1 t2]. |
198 Implicit Arguments Abs [var t]. | 213 Implicit Arguments Snd [var t1 t2]. |
199 Implicit Arguments Pair [var t1 t2]. | 214 |
200 Implicit Arguments Fst [var t1 t2]. | 215 Notation "'Halt' x" := (PHalt x) (no associativity, at level 75) : cps_scope. |
201 Implicit Arguments Snd [var t1 t2]. | 216 Infix "@@" := App (no associativity, at level 75) : cps_scope. |
202 | 217 Notation "x <- p ; e" := (Bind p (fun x => e)) |
203 Notation "'Halt' x" := (PHalt x) (no associativity, at level 75) : cps_scope. | 218 (right associativity, at level 76, p at next level) : cps_scope. |
204 Infix "@@" := App (no associativity, at level 75) : cps_scope. | 219 Notation "! <- p ; e" := (Bind p (fun _ => e)) |
205 Notation "x <- p ; e" := (Bind p (fun x => e)) | 220 (right associativity, at level 76, p at next level) : cps_scope. |
206 (right associativity, at level 76, p at next level) : cps_scope. | 221 |
207 Notation "! <- p ; e" := (Bind p (fun _ => e)) | 222 Notation "^ n" := (Const n) (at level 70) : cps_scope. |
208 (right associativity, at level 76, p at next level) : cps_scope. | 223 Infix "+^" := Plus (left associativity, at level 79) : cps_scope. |
209 | 224 |
210 Notation "# v" := (Var v) (at level 70) : cps_scope. | 225 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : cps_scope. |
211 | 226 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : cps_scope. |
212 Notation "^ n" := (Const n) (at level 70) : cps_scope. | 227 |
213 Infix "+^" := Plus (left associativity, at level 79) : cps_scope. | 228 Notation "[ x1 , x2 ]" := (Pair x1 x2) : cps_scope. |
214 | 229 Notation "#1 x" := (Fst x) (at level 72) : cps_scope. |
215 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : cps_scope. | 230 Notation "#2 x" := (Snd x) (at level 72) : cps_scope. |
216 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : cps_scope. | 231 |
217 | 232 Bind Scope cps_scope with prog primop. |
218 Notation "[ x1 , x2 ]" := (Pair x1 x2) : cps_scope. | 233 |
219 Notation "#1 x" := (Fst x) (at level 72) : cps_scope. | 234 Open Scope cps_scope. |
220 Notation "#2 x" := (Snd x) (at level 72) : cps_scope. | 235 |
221 | 236 (** In interpreting types, we treat continuations as functions with codomain [nat], choosing [nat] as our arbitrary program result type. *) |
222 Bind Scope cps_scope with prog primop. | 237 |
223 | 238 Fixpoint typeDenote (t : type) : Set := |
224 Open Scope cps_scope. | 239 match t with |
225 | 240 | Nat => nat |
226 Fixpoint typeDenote (t : type) : Set := | 241 | t' ---> => typeDenote t' -> nat |
227 match t with | 242 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type |
228 | Nat => nat | 243 end. |
229 | t' ---> => typeDenote t' -> nat | 244 |
230 | Unit => unit | 245 (** A mutually-recursive definition establishes the meanings of programs and primops. *) |
231 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type | 246 |
232 end. | 247 Fixpoint progDenote (e : prog typeDenote) : nat := |
233 | 248 match e with |
234 Fixpoint progDenote (e : prog typeDenote) : nat := | 249 | PHalt n => n |
235 match e with | 250 | App _ f x => f x |
236 | PHalt n => n | 251 | Bind _ p x => progDenote (x (primopDenote p)) |
237 | App _ f x => f x | 252 end |
238 | Bind _ p x => progDenote (x (primopDenote p)) | 253 |
239 end | 254 with primopDenote t (p : primop typeDenote t) : typeDenote t := |
240 | 255 match p with |
241 with primopDenote t (p : primop typeDenote t) : typeDenote t := | 256 | Const n => n |
242 match p with | 257 | Plus n1 n2 => n1 + n2 |
243 | Var _ v => v | 258 |
244 | 259 | Abs _ e => fun x => progDenote (e x) |
245 | Const n => n | 260 |
246 | Plus n1 n2 => n1 + n2 | 261 | Pair _ _ v1 v2 => (v1, v2) |
247 | 262 | Fst _ _ v => fst v |
248 | Abs _ e => fun x => progDenote (e x) | 263 | Snd _ _ v => snd v |
249 | 264 end. |
250 | Pair _ _ v1 v2 => (v1, v2) | 265 |
251 | Fst _ _ v => fst v | 266 Definition Prog := forall var, prog var. |
252 | Snd _ _ v => snd v | 267 Definition Primop t := forall var, primop var t. |
253 end. | 268 Definition ProgDenote (E : Prog) := progDenote (E _). |
254 | 269 Definition PrimopDenote t (P : Primop t) := primopDenote (P _). |
255 Definition Prog := forall var, prog var. | 270 End CPS. |
256 Definition Primop t := forall var, primop var t. | 271 |
257 Definition ProgDenote (E : Prog) := progDenote (E _). | 272 Import Source CPS. |
258 Definition PrimopDenote t (P : Primop t) := primopDenote (P _). | 273 |
259 End CPS. | 274 (** The translation itself begins with a type-level compilation function. We change every function into a continuation whose argument is a pair, consisting of the translation of the original argument and of an explicit return pointer. *) |
260 | |
261 Import Source CPS. | |
262 | 275 |
263 (* begin thide *) | 276 (* begin thide *) |
264 Fixpoint cpsType (t : Source.type) : CPS.type := | 277 Fixpoint cpsType (t : Source.type) : CPS.type := |
265 match t with | 278 match t with |
266 | Nat => Nat%cps | 279 | Nat => Nat%cps |
267 | t1 --> t2 => (cpsType t1 ** (cpsType t2 --->) --->)%cps | 280 | t1 --> t2 => (cpsType t1 ** (cpsType t2 --->) --->)%cps |
268 end%source. | 281 end%source. |
269 | 282 |
270 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level). | 283 (** Now we can define the expression translation. The notation [x <-- e1; e2] stands for translating source-level expression [e1], binding [x] to the CPS-level result of running the translated program, and then evaluating CPS-level expression [e2] in that context. *) |
271 | 284 |
272 Section cpsExp. | 285 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level). |
273 Variable var : CPS.type -> Type. | 286 |
274 | 287 Section cpsExp. |
275 Import Source. | 288 Variable var : CPS.type -> Type. |
276 Open Scope cps_scope. | 289 |
277 | 290 Import Source. |
278 Fixpoint cpsExp t (e : exp (fun t => var (cpsType t)) t) | 291 Open Scope cps_scope. |
279 : (var (cpsType t) -> prog var) -> prog var := | 292 |
280 match e with | 293 (** We implement a well-known variety of higher-order, one-pass CPS translation. The translation [cpsExp] is parameterized not only by the expression [e] to translate, but also by a meta-level continuation. The idea is that [cpsExp] evaluates the translation of [e] and calls the continuation on the result. With this convention, [cpsExp] itself is a natural match for the notation we just reserved. *) |
281 | Var _ v => fun k => k v | 294 |
282 | 295 Fixpoint cpsExp t (e : exp (fun t => var (cpsType t)) t) |
283 | Const n => fun k => | 296 : (var (cpsType t) -> prog var) -> prog var := |
284 x <- ^n; | 297 match e with |
285 k x | 298 | Var _ v => fun k => k v |
286 | Plus e1 e2 => fun k => | 299 |
287 x1 <-- e1; | 300 | Const n => fun k => |
288 x2 <-- e2; | 301 x <- ^n; |
289 x <- x1 +^ x2; | 302 k x |
290 k x | 303 | Plus e1 e2 => fun k => |
291 | 304 x1 <-- e1; |
292 | App _ _ e1 e2 => fun k => | 305 x2 <-- e2; |
293 f <-- e1; | 306 x <- x1 +^ x2; |
294 x <-- e2; | 307 k x |
295 kf <- \r, k r; | 308 |
296 p <- [x, kf]; | 309 | App _ _ e1 e2 => fun k => |
297 f @@ p | 310 f <-- e1; |
298 | Abs _ _ e' => fun k => | 311 x <-- e2; |
299 f <- CPS.Abs (var := var) (fun p => | 312 kf <- \r, k r; |
300 x <- #1 p; | 313 p <- [x, kf]; |
301 kf <- #2 p; | 314 f @@ p |
302 r <-- e' x; | 315 | Abs _ _ e' => fun k => |
303 kf @@ r); | 316 f <- CPS.Abs (var := var) (fun p => |
304 k f | 317 x <- #1 p; |
305 end | 318 kf <- #2 p; |
306 | 319 r <-- e' x; |
307 where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)). | 320 kf @@ r); |
308 End cpsExp. | 321 k f |
309 | 322 end |
310 Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)) : cps_scope. | 323 |
311 Notation "! <-- e1 ; e2" := (cpsExp e1 (fun _ => e2)) | 324 where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)). |
312 (right associativity, at level 76, e1 at next level) : cps_scope. | 325 End cpsExp. |
313 | 326 |
314 Implicit Arguments cpsExp [var t]. | 327 (** Since notations do not survive the closing of sections, we redefine the notation associated with [cpsExp]. *) |
315 Definition CpsExp (E : Exp Nat) : Prog := | 328 |
316 fun var => cpsExp (E _) (PHalt (var := _)). | 329 Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)) : cps_scope. |
330 | |
331 Implicit Arguments cpsExp [var t]. | |
332 | |
333 (** We wrap [cpsExp] into the parametric version [CpsExp], passing an always-halt continuation at the root of the recursion. *) | |
334 | |
335 Definition CpsExp (E : Exp Nat) : Prog := | |
336 fun _ => cpsExp (E _) (PHalt (var := _)). | |
317 (* end thide *) | 337 (* end thide *) |
318 | 338 |
319 Eval compute in CpsExp zero. | 339 Eval compute in CpsExp zero. |
320 Eval compute in CpsExp one. | 340 (** %\vspace{-.15in}% [[ |
321 Eval compute in CpsExp zpo. | 341 = fun var : type -> Type => x <- ^0; Halt x |
322 Eval compute in CpsExp app_ident. | 342 : Prog |
323 Eval compute in CpsExp app_ident'. | 343 ]] *) |
324 | 344 |
325 Eval compute in ProgDenote (CpsExp zero). | 345 Eval compute in CpsExp one. |
326 Eval compute in ProgDenote (CpsExp one). | 346 (** %\vspace{-.15in}% [[ |
327 Eval compute in ProgDenote (CpsExp zpo). | 347 = fun var : type -> Type => x <- ^1; Halt x |
328 Eval compute in ProgDenote (CpsExp app_ident). | 348 : Prog |
329 Eval compute in ProgDenote (CpsExp app_ident'). | 349 ]] *) |
350 | |
351 Eval compute in CpsExp zpo. | |
352 (** %\vspace{-.15in}% [[ | |
353 = fun var : type -> Type => x <- ^0; x0 <- ^1; x1 <- (x +^ x0); Halt x1 | |
354 : Prog | |
355 ]] *) | |
356 | |
357 Eval compute in CpsExp app_ident. | |
358 (** %\vspace{-.15in}% [[ | |
359 = fun var : type -> Type => | |
360 f <- (\ p, x <- #1 p; kf <- #2 p; kf @@ x); | |
361 x <- ^0; | |
362 x0 <- ^1; x1 <- (x +^ x0); kf <- (\ r, Halt r); p <- [x1, kf]; f @@ p | |
363 : Prog | |
364 ]] *) | |
365 | |
366 Eval compute in CpsExp app_ident'. | |
367 (** %\vspace{-.15in}% [[ | |
368 = fun var : type -> Type => | |
369 f <- | |
370 (\ p, | |
371 x <- #1 p; | |
372 kf <- #2 p; | |
373 f <- | |
374 (\ p0, | |
375 x0 <- #1 p0; | |
376 kf0 <- #2 p0; kf1 <- (\ r, kf0 @@ r); p1 <- [x0, kf1]; x @@ p1); | |
377 kf @@ f); | |
378 f0 <- (\ p, x <- #1 p; kf <- #2 p; kf @@ x); | |
379 kf <- | |
380 (\ r, | |
381 x <- ^0; | |
382 x0 <- ^1; | |
383 x1 <- (x +^ x0); kf <- (\ r0, Halt r0); p <- [x1, kf]; r @@ p); | |
384 p <- [f0, kf]; f @@ p | |
385 : Prog | |
386 ]] *) | |
387 | |
388 Eval compute in ProgDenote (CpsExp zero). | |
389 (** %\vspace{-.15in}% [[ | |
390 = 0 | |
391 : nat | |
392 ]] *) | |
393 | |
394 Eval compute in ProgDenote (CpsExp one). | |
395 (** %\vspace{-.15in}% [[ | |
396 = 1 | |
397 : nat | |
398 ]] *) | |
399 | |
400 Eval compute in ProgDenote (CpsExp zpo). | |
401 (** %\vspace{-.15in}% [[ | |
402 = 1 | |
403 : nat | |
404 ]] *) | |
405 | |
406 Eval compute in ProgDenote (CpsExp app_ident). | |
407 (** %\vspace{-.15in}% [[ | |
408 = 1 | |
409 : nat | |
410 ]] *) | |
411 | |
412 Eval compute in ProgDenote (CpsExp app_ident'). | |
413 (** %\vspace{-.15in}% [[ | |
414 = 1 | |
415 : nat | |
416 ]] *) | |
417 | |
418 | |
419 (** Our main inductive lemma about [cpsExp] needs a notion of compatibility between source-level and CPS-level values. We express compatibility with a %\textit{%#<i>#logical relation#</i>#%}%; that is, we define a binary relation by recursion on type structure, and the function case of the relation considers functions related if they map related arguments to related results. In detail, the function case is slightly more complicated, since it must deal with our continuation-based calling convention. *) | |
330 | 420 |
331 (* begin thide *) | 421 (* begin thide *) |
332 Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop := | 422 Fixpoint lr (t : Source.type) |
333 match t with | 423 : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop := |
334 | Nat => fun n1 n2 => n1 = n2 | 424 match t with |
335 | t1 --> t2 => fun f1 f2 => | 425 | Nat => fun n1 n2 => n1 = n2 |
336 forall x1 x2, lr _ x1 x2 | 426 | t1 --> t2 => fun f1 f2 => |
337 -> forall k, exists r, | 427 forall x1 x2, lr _ x1 x2 |
338 f2 (x2, k) = k r | 428 -> forall k, exists r, |
339 /\ lr _ (f1 x1) r | 429 f2 (x2, k) = k r |
340 end%source. | 430 /\ lr _ (f1 x1) r |
341 | 431 end%source. |
342 Lemma cpsExp_correct : forall G t (e1 : exp _ t) (e2 : exp _ t), | 432 |
343 exp_equiv G e1 e2 | 433 (** The main lemma is now easily stated and proved. The most surprising aspect of the statement is the presence of %\textit{%#<i>#two#</i>#%}% versions of the expression to be compiled. The first, [e1], uses a [var] choice that makes it a suitable argument to [expDenote]. The second expression, [e2], uses a [var] choice that makes its compilation, [cpsExp e2 k], a suitable argument to [progDenote]. We use [exp_equiv] to assert that [e1] and [e2] have the same underlying structure, up to a variable correspondence list [G]. A hypothesis about [G] ensures that all of its pairs of variables belong to the logical relation [lr]. We also use [lr], in concert with some quantification over continuations and program results, in the conclusion of the lemma. |
344 -> (forall t v1 v2, In (existT _ t (v1, v2)) G -> lr t v1 v2) | 434 |
345 -> forall k, exists r, | 435 The lemma's proof should be unsurprising by now. It uses our standard bag of Ltac tricks to help out with quantifier instantiation; [crush] and [eauto] can handle the rest. *) |
346 progDenote (cpsExp e2 k) = progDenote (k r) | 436 |
347 /\ lr t (expDenote e1) r. | 437 Lemma cpsExp_correct : forall G t (e1 : exp _ t) (e2 : exp _ t), |
348 induction 1; crush; fold typeDenote in *; | 438 exp_equiv G e1 e2 |
349 repeat (match goal with | 439 -> (forall t v1 v2, In (existT _ t (v1, v2)) G -> lr t v1 v2) |
350 | [ H : forall k, exists r, progDenote (cpsExp ?E k) = _ /\ _ | 440 -> forall k, exists r, |
441 progDenote (cpsExp e2 k) = progDenote (k r) | |
442 /\ lr t (expDenote e1) r. | |
443 induction 1; crush; | |
444 repeat (match goal with | |
445 | [ H : forall k, exists r, progDenote (cpsExp ?E k) = _ /\ _ | |
351 |- context[cpsExp ?E ?K] ] => | 446 |- context[cpsExp ?E ?K] ] => |
352 generalize (H K); clear H | 447 generalize (H K); clear H |
353 | [ |- exists r, progDenote (_ ?R) = progDenote (_ r) /\ _ ] => | 448 | [ |- exists r, progDenote (_ ?R) = progDenote (_ r) /\ _ ] => |
354 exists R | 449 exists R |
355 | [ t1 : Source.type |- _ ] => | 450 | [ t1 : Source.type |- _ ] => |
356 match goal with | 451 match goal with |
357 | [ Hlr : lr t1 ?X1 ?X2, IH : forall v1 v2, _ |- _ ] => | 452 | [ Hlr : lr t1 ?X1 ?X2, IH : forall v1 v2, _ |- _ ] => |
358 generalize (IH X1 X2); clear IH; intro IH; | 453 generalize (IH X1 X2); clear IH; intro IH; |
359 match type of IH with | 454 match type of IH with |
360 | ?P -> _ => assert P | 455 | ?P -> _ => assert P |
361 end | 456 end |
362 end | 457 end |
363 end; crush); eauto. | 458 end; crush); eauto. |
364 Qed. | 459 Qed. |
365 | 460 |
366 Lemma vars_easy : forall (t : Source.type) (v1 : Source.typeDenote t) | 461 (** A simple lemma establishes the degenerate case of [cpsExp_correct]'s hypothesis about [G]. *) |
367 (v2 : typeDenote (cpsType t)), | 462 |
368 In | 463 Lemma vars_easy : forall t v1 v2, |
369 (existT | 464 In (existT (fun t0 => (Source.typeDenote t0 * typeDenote (cpsType t0))%type) t |
370 (fun t0 : Source.type => | 465 (v1, v2)) nil -> lr t v1 v2. |
371 (Source.typeDenote t0 * typeDenote (cpsType t0))%type) t | 466 crush. |
372 (v1, v2)) nil -> lr t v1 v2. | 467 Qed. |
373 crush. | 468 |
374 Qed. | 469 (** A manual application of [cpsExp_correct] proves a version applicable to [CpsExp]. This is where we use the axiom [Exp_equiv]. *) |
375 | 470 |
376 Theorem CpsExp_correct : forall (E : Exp Nat), | 471 Theorem CpsExp_correct : forall (E : Exp Nat), |
377 ProgDenote (CpsExp E) = ExpDenote E. | 472 ProgDenote (CpsExp E) = ExpDenote E. |
378 unfold ProgDenote, CpsExp, ExpDenote; intros; | 473 unfold ProgDenote, CpsExp, ExpDenote; intros; |
379 generalize (cpsExp_correct (e1 := E _) (e2 := E _) | 474 generalize (cpsExp_correct (e1 := E _) (e2 := E _) |
380 (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush. | 475 (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush. |
381 Qed. | 476 Qed. |
382 (* end thide *) | 477 (* end thide *) |
383 | |
384 End STLC. | |
385 | 478 |
386 | 479 |
387 (** * Exercises *) | 480 (** * Exercises *) |
388 | 481 |
389 (** %\begin{enumerate}%#<ol># | 482 (** %\begin{enumerate}%#<ol># |