adamc@216
|
1 (* Copyright (c) 2008-2009, Adam Chlipala
|
adamc@175
|
2 *
|
adamc@175
|
3 * This work is licensed under a
|
adamc@175
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
adamc@175
|
5 * Unported License.
|
adamc@175
|
6 * The license text is available at:
|
adamc@175
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
adamc@175
|
8 *)
|
adamc@175
|
9
|
adamc@175
|
10 (* begin hide *)
|
adamc@175
|
11 Require Import String List.
|
adamc@175
|
12
|
adamc@182
|
13 Require Import Axioms Tactics DepList.
|
adamc@175
|
14
|
adamc@175
|
15 Set Implicit Arguments.
|
adamc@175
|
16 (* end hide *)
|
adamc@175
|
17
|
adamc@175
|
18
|
adamc@181
|
19 (** %\chapter{Extensional Transformations}% *)
|
adamc@175
|
20
|
adamc@175
|
21 (** TODO: Prose for this chapter *)
|
adamc@175
|
22
|
adamc@175
|
23
|
adamc@175
|
24 (** * Simply-Typed Lambda Calculus *)
|
adamc@175
|
25
|
adamc@175
|
26 Module STLC.
|
adamc@175
|
27 Module Source.
|
adamc@175
|
28 Inductive type : Type :=
|
adamc@175
|
29 | TNat : type
|
adamc@175
|
30 | Arrow : type -> type -> type.
|
adamc@175
|
31
|
adamc@175
|
32 Notation "'Nat'" := TNat : source_scope.
|
adamc@175
|
33 Infix "-->" := Arrow (right associativity, at level 60) : source_scope.
|
adamc@175
|
34
|
adamc@175
|
35 Open Scope source_scope.
|
adamc@175
|
36 Bind Scope source_scope with type.
|
adamc@175
|
37 Delimit Scope source_scope with source.
|
adamc@175
|
38
|
adamc@175
|
39 Section vars.
|
adamc@175
|
40 Variable var : type -> Type.
|
adamc@175
|
41
|
adamc@175
|
42 Inductive exp : type -> Type :=
|
adamc@175
|
43 | Var : forall t,
|
adamc@175
|
44 var t
|
adamc@175
|
45 -> exp t
|
adamc@175
|
46
|
adamc@175
|
47 | Const : nat -> exp Nat
|
adamc@175
|
48 | Plus : exp Nat -> exp Nat -> exp Nat
|
adamc@175
|
49
|
adamc@175
|
50 | App : forall t1 t2,
|
adamc@175
|
51 exp (t1 --> t2)
|
adamc@175
|
52 -> exp t1
|
adamc@175
|
53 -> exp t2
|
adamc@175
|
54 | Abs : forall t1 t2,
|
adamc@175
|
55 (var t1 -> exp t2)
|
adamc@175
|
56 -> exp (t1 --> t2).
|
adamc@175
|
57 End vars.
|
adamc@175
|
58
|
adamc@175
|
59 Definition Exp t := forall var, exp var t.
|
adamc@175
|
60
|
adamc@175
|
61 Implicit Arguments Var [var t].
|
adamc@175
|
62 Implicit Arguments Const [var].
|
adamc@175
|
63 Implicit Arguments Plus [var].
|
adamc@175
|
64 Implicit Arguments App [var t1 t2].
|
adamc@175
|
65 Implicit Arguments Abs [var t1 t2].
|
adamc@175
|
66
|
adamc@175
|
67 Notation "# v" := (Var v) (at level 70) : source_scope.
|
adamc@175
|
68
|
adamc@175
|
69 Notation "^ n" := (Const n) (at level 70) : source_scope.
|
adamc@175
|
70 Infix "+^" := Plus (left associativity, at level 79) : source_scope.
|
adamc@175
|
71
|
adamc@175
|
72 Infix "@" := App (left associativity, at level 77) : source_scope.
|
adamc@175
|
73 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
|
adamc@175
|
74 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope.
|
adamc@175
|
75
|
adamc@175
|
76 Bind Scope source_scope with exp.
|
adamc@175
|
77
|
adamc@175
|
78 Definition zero : Exp Nat := fun _ => ^0.
|
adamc@175
|
79 Definition one : Exp Nat := fun _ => ^1.
|
adamc@175
|
80 Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
|
adamc@175
|
81 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
|
adamc@175
|
82 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
|
adamc@175
|
83 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
|
adamc@175
|
84 \f, \x, #f @ #x.
|
adamc@175
|
85 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
|
adamc@175
|
86
|
adamc@175
|
87 Fixpoint typeDenote (t : type) : Set :=
|
adamc@175
|
88 match t with
|
adamc@175
|
89 | Nat => nat
|
adamc@175
|
90 | t1 --> t2 => typeDenote t1 -> typeDenote t2
|
adamc@175
|
91 end.
|
adamc@175
|
92
|
adamc@224
|
93 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
|
adamc@224
|
94 match e with
|
adamc@175
|
95 | Var _ v => v
|
adamc@175
|
96
|
adamc@175
|
97 | Const n => n
|
adamc@175
|
98 | Plus e1 e2 => expDenote e1 + expDenote e2
|
adamc@175
|
99
|
adamc@175
|
100 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
|
adamc@175
|
101 | Abs _ _ e' => fun x => expDenote (e' x)
|
adamc@175
|
102 end.
|
adamc@175
|
103
|
adamc@175
|
104 Definition ExpDenote t (e : Exp t) := expDenote (e _).
|
adamc@176
|
105
|
adamc@180
|
106 (* begin thide *)
|
adamc@176
|
107 Section exp_equiv.
|
adamc@176
|
108 Variables var1 var2 : type -> Type.
|
adamc@176
|
109
|
adamc@224
|
110 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type
|
adamc@224
|
111 -> forall t, exp var1 t -> exp var2 t -> Prop :=
|
adamc@181
|
112 | EqVar : forall G t (v1 : var1 t) v2,
|
adamc@176
|
113 In (existT _ t (v1, v2)) G
|
adamc@176
|
114 -> exp_equiv G (#v1) (#v2)
|
adamc@176
|
115
|
adamc@181
|
116 | EqConst : forall G n,
|
adamc@176
|
117 exp_equiv G (^n) (^n)
|
adamc@181
|
118 | EqPlus : forall G x1 y1 x2 y2,
|
adamc@176
|
119 exp_equiv G x1 x2
|
adamc@176
|
120 -> exp_equiv G y1 y2
|
adamc@176
|
121 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
|
adamc@176
|
122
|
adamc@181
|
123 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
|
adamc@176
|
124 exp_equiv G f1 f2
|
adamc@176
|
125 -> exp_equiv G x1 x2
|
adamc@176
|
126 -> exp_equiv G (f1 @ x1) (f2 @ x2)
|
adamc@181
|
127 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
|
adamc@176
|
128 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
|
adamc@176
|
129 -> exp_equiv G (Abs f1) (Abs f2).
|
adamc@176
|
130 End exp_equiv.
|
adamc@176
|
131
|
adamc@176
|
132 Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
|
adamc@176
|
133 exp_equiv nil (E var1) (E var2).
|
adamc@180
|
134 (* end thide *)
|
adamc@175
|
135 End Source.
|
adamc@175
|
136
|
adamc@175
|
137 Module CPS.
|
adamc@175
|
138 Inductive type : Type :=
|
adamc@175
|
139 | TNat : type
|
adamc@175
|
140 | Cont : type -> type
|
adamc@175
|
141 | TUnit : type
|
adamc@175
|
142 | Prod : type -> type -> type.
|
adamc@175
|
143
|
adamc@175
|
144 Notation "'Nat'" := TNat : cps_scope.
|
adamc@175
|
145 Notation "'Unit'" := TUnit : cps_scope.
|
adamc@175
|
146 Notation "t --->" := (Cont t) (at level 61) : cps_scope.
|
adamc@175
|
147 Infix "**" := Prod (right associativity, at level 60) : cps_scope.
|
adamc@175
|
148
|
adamc@175
|
149 Bind Scope cps_scope with type.
|
adamc@175
|
150 Delimit Scope cps_scope with cps.
|
adamc@175
|
151
|
adamc@175
|
152 Section vars.
|
adamc@175
|
153 Variable var : type -> Type.
|
adamc@175
|
154
|
adamc@175
|
155 Inductive prog : Type :=
|
adamc@175
|
156 | PHalt :
|
adamc@175
|
157 var Nat
|
adamc@175
|
158 -> prog
|
adamc@175
|
159 | App : forall t,
|
adamc@175
|
160 var (t --->)
|
adamc@175
|
161 -> var t
|
adamc@175
|
162 -> prog
|
adamc@175
|
163 | Bind : forall t,
|
adamc@175
|
164 primop t
|
adamc@175
|
165 -> (var t -> prog)
|
adamc@175
|
166 -> prog
|
adamc@175
|
167
|
adamc@175
|
168 with primop : type -> Type :=
|
adamc@175
|
169 | Var : forall t,
|
adamc@175
|
170 var t
|
adamc@175
|
171 -> primop t
|
adamc@175
|
172
|
adamc@175
|
173 | Const : nat -> primop Nat
|
adamc@175
|
174 | Plus : var Nat -> var Nat -> primop Nat
|
adamc@175
|
175
|
adamc@175
|
176 | Abs : forall t,
|
adamc@175
|
177 (var t -> prog)
|
adamc@175
|
178 -> primop (t --->)
|
adamc@175
|
179
|
adamc@175
|
180 | Pair : forall t1 t2,
|
adamc@175
|
181 var t1
|
adamc@175
|
182 -> var t2
|
adamc@175
|
183 -> primop (t1 ** t2)
|
adamc@175
|
184 | Fst : forall t1 t2,
|
adamc@175
|
185 var (t1 ** t2)
|
adamc@175
|
186 -> primop t1
|
adamc@175
|
187 | Snd : forall t1 t2,
|
adamc@175
|
188 var (t1 ** t2)
|
adamc@175
|
189 -> primop t2.
|
adamc@175
|
190 End vars.
|
adamc@175
|
191
|
adamc@175
|
192 Implicit Arguments PHalt [var].
|
adamc@175
|
193 Implicit Arguments App [var t].
|
adamc@175
|
194
|
adamc@175
|
195 Implicit Arguments Var [var t].
|
adamc@175
|
196 Implicit Arguments Const [var].
|
adamc@175
|
197 Implicit Arguments Plus [var].
|
adamc@175
|
198 Implicit Arguments Abs [var t].
|
adamc@175
|
199 Implicit Arguments Pair [var t1 t2].
|
adamc@175
|
200 Implicit Arguments Fst [var t1 t2].
|
adamc@175
|
201 Implicit Arguments Snd [var t1 t2].
|
adamc@175
|
202
|
adamc@175
|
203 Notation "'Halt' x" := (PHalt x) (no associativity, at level 75) : cps_scope.
|
adamc@175
|
204 Infix "@@" := App (no associativity, at level 75) : cps_scope.
|
adamc@175
|
205 Notation "x <- p ; e" := (Bind p (fun x => e))
|
adamc@175
|
206 (right associativity, at level 76, p at next level) : cps_scope.
|
adamc@175
|
207 Notation "! <- p ; e" := (Bind p (fun _ => e))
|
adamc@175
|
208 (right associativity, at level 76, p at next level) : cps_scope.
|
adamc@175
|
209
|
adamc@175
|
210 Notation "# v" := (Var v) (at level 70) : cps_scope.
|
adamc@175
|
211
|
adamc@175
|
212 Notation "^ n" := (Const n) (at level 70) : cps_scope.
|
adamc@175
|
213 Infix "+^" := Plus (left associativity, at level 79) : cps_scope.
|
adamc@175
|
214
|
adamc@175
|
215 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : cps_scope.
|
adamc@175
|
216 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : cps_scope.
|
adamc@175
|
217
|
adamc@179
|
218 Notation "[ x1 , x2 ]" := (Pair x1 x2) : cps_scope.
|
adamc@175
|
219 Notation "#1 x" := (Fst x) (at level 72) : cps_scope.
|
adamc@175
|
220 Notation "#2 x" := (Snd x) (at level 72) : cps_scope.
|
adamc@175
|
221
|
adamc@175
|
222 Bind Scope cps_scope with prog primop.
|
adamc@175
|
223
|
adamc@175
|
224 Open Scope cps_scope.
|
adamc@175
|
225
|
adamc@175
|
226 Fixpoint typeDenote (t : type) : Set :=
|
adamc@175
|
227 match t with
|
adamc@175
|
228 | Nat => nat
|
adamc@175
|
229 | t' ---> => typeDenote t' -> nat
|
adamc@175
|
230 | Unit => unit
|
adamc@175
|
231 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
|
adamc@175
|
232 end.
|
adamc@175
|
233
|
adamc@175
|
234 Fixpoint progDenote (e : prog typeDenote) : nat :=
|
adamc@175
|
235 match e with
|
adamc@175
|
236 | PHalt n => n
|
adamc@175
|
237 | App _ f x => f x
|
adamc@175
|
238 | Bind _ p x => progDenote (x (primopDenote p))
|
adamc@175
|
239 end
|
adamc@175
|
240
|
adamc@224
|
241 with primopDenote t (p : primop typeDenote t) : typeDenote t :=
|
adamc@224
|
242 match p with
|
adamc@175
|
243 | Var _ v => v
|
adamc@175
|
244
|
adamc@175
|
245 | Const n => n
|
adamc@175
|
246 | Plus n1 n2 => n1 + n2
|
adamc@175
|
247
|
adamc@175
|
248 | Abs _ e => fun x => progDenote (e x)
|
adamc@175
|
249
|
adamc@175
|
250 | Pair _ _ v1 v2 => (v1, v2)
|
adamc@175
|
251 | Fst _ _ v => fst v
|
adamc@175
|
252 | Snd _ _ v => snd v
|
adamc@175
|
253 end.
|
adamc@175
|
254
|
adamc@175
|
255 Definition Prog := forall var, prog var.
|
adamc@175
|
256 Definition Primop t := forall var, primop var t.
|
adamc@175
|
257 Definition ProgDenote (E : Prog) := progDenote (E _).
|
adamc@175
|
258 Definition PrimopDenote t (P : Primop t) := primopDenote (P _).
|
adamc@175
|
259 End CPS.
|
adamc@175
|
260
|
adamc@175
|
261 Import Source CPS.
|
adamc@175
|
262
|
adamc@180
|
263 (* begin thide *)
|
adamc@175
|
264 Fixpoint cpsType (t : Source.type) : CPS.type :=
|
adamc@175
|
265 match t with
|
adamc@175
|
266 | Nat => Nat%cps
|
adamc@175
|
267 | t1 --> t2 => (cpsType t1 ** (cpsType t2 --->) --->)%cps
|
adamc@175
|
268 end%source.
|
adamc@175
|
269
|
adamc@175
|
270 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
|
adamc@175
|
271
|
adamc@175
|
272 Section cpsExp.
|
adamc@175
|
273 Variable var : CPS.type -> Type.
|
adamc@175
|
274
|
adamc@175
|
275 Import Source.
|
adamc@175
|
276 Open Scope cps_scope.
|
adamc@175
|
277
|
adamc@224
|
278 Fixpoint cpsExp t (e : exp (fun t => var (cpsType t)) t)
|
adamc@175
|
279 : (var (cpsType t) -> prog var) -> prog var :=
|
adamc@224
|
280 match e with
|
adamc@175
|
281 | Var _ v => fun k => k v
|
adamc@175
|
282
|
adamc@175
|
283 | Const n => fun k =>
|
adamc@175
|
284 x <- ^n;
|
adamc@175
|
285 k x
|
adamc@175
|
286 | Plus e1 e2 => fun k =>
|
adamc@175
|
287 x1 <-- e1;
|
adamc@175
|
288 x2 <-- e2;
|
adamc@175
|
289 x <- x1 +^ x2;
|
adamc@175
|
290 k x
|
adamc@175
|
291
|
adamc@175
|
292 | App _ _ e1 e2 => fun k =>
|
adamc@175
|
293 f <-- e1;
|
adamc@175
|
294 x <-- e2;
|
adamc@175
|
295 kf <- \r, k r;
|
adamc@175
|
296 p <- [x, kf];
|
adamc@175
|
297 f @@ p
|
adamc@175
|
298 | Abs _ _ e' => fun k =>
|
adamc@175
|
299 f <- CPS.Abs (var := var) (fun p =>
|
adamc@175
|
300 x <- #1 p;
|
adamc@175
|
301 kf <- #2 p;
|
adamc@175
|
302 r <-- e' x;
|
adamc@175
|
303 kf @@ r);
|
adamc@175
|
304 k f
|
adamc@175
|
305 end
|
adamc@175
|
306
|
adamc@175
|
307 where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
|
adamc@175
|
308 End cpsExp.
|
adamc@175
|
309
|
adamc@175
|
310 Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)) : cps_scope.
|
adamc@175
|
311 Notation "! <-- e1 ; e2" := (cpsExp e1 (fun _ => e2))
|
adamc@175
|
312 (right associativity, at level 76, e1 at next level) : cps_scope.
|
adamc@175
|
313
|
adamc@175
|
314 Implicit Arguments cpsExp [var t].
|
adamc@175
|
315 Definition CpsExp (E : Exp Nat) : Prog :=
|
adamc@175
|
316 fun var => cpsExp (E _) (PHalt (var := _)).
|
adamc@180
|
317 (* end thide *)
|
adamc@175
|
318
|
adamc@175
|
319 Eval compute in CpsExp zero.
|
adamc@175
|
320 Eval compute in CpsExp one.
|
adamc@175
|
321 Eval compute in CpsExp zpo.
|
adamc@175
|
322 Eval compute in CpsExp app_ident.
|
adamc@175
|
323 Eval compute in CpsExp app_ident'.
|
adamc@175
|
324
|
adamc@175
|
325 Eval compute in ProgDenote (CpsExp zero).
|
adamc@175
|
326 Eval compute in ProgDenote (CpsExp one).
|
adamc@175
|
327 Eval compute in ProgDenote (CpsExp zpo).
|
adamc@175
|
328 Eval compute in ProgDenote (CpsExp app_ident).
|
adamc@175
|
329 Eval compute in ProgDenote (CpsExp app_ident').
|
adamc@175
|
330
|
adamc@180
|
331 (* begin thide *)
|
adamc@176
|
332 Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop :=
|
adamc@224
|
333 match t with
|
adamc@176
|
334 | Nat => fun n1 n2 => n1 = n2
|
adamc@176
|
335 | t1 --> t2 => fun f1 f2 =>
|
adamc@176
|
336 forall x1 x2, lr _ x1 x2
|
adamc@176
|
337 -> forall k, exists r,
|
adamc@176
|
338 f2 (x2, k) = k r
|
adamc@176
|
339 /\ lr _ (f1 x1) r
|
adamc@176
|
340 end%source.
|
adamc@176
|
341
|
adamc@176
|
342 Lemma cpsExp_correct : forall G t (e1 : exp _ t) (e2 : exp _ t),
|
adamc@176
|
343 exp_equiv G e1 e2
|
adamc@176
|
344 -> (forall t v1 v2, In (existT _ t (v1, v2)) G -> lr t v1 v2)
|
adamc@176
|
345 -> forall k, exists r,
|
adamc@176
|
346 progDenote (cpsExp e2 k) = progDenote (k r)
|
adamc@176
|
347 /\ lr t (expDenote e1) r.
|
adamc@176
|
348 induction 1; crush; fold typeDenote in *;
|
adamc@176
|
349 repeat (match goal with
|
adamc@176
|
350 | [ H : forall k, exists r, progDenote (cpsExp ?E k) = _ /\ _
|
adamc@176
|
351 |- context[cpsExp ?E ?K] ] =>
|
adamc@176
|
352 generalize (H K); clear H
|
adamc@176
|
353 | [ |- exists r, progDenote (_ ?R) = progDenote (_ r) /\ _ ] =>
|
adamc@176
|
354 exists R
|
adamc@176
|
355 | [ t1 : Source.type |- _ ] =>
|
adamc@176
|
356 match goal with
|
adamc@176
|
357 | [ Hlr : lr t1 ?X1 ?X2, IH : forall v1 v2, _ |- _ ] =>
|
adamc@176
|
358 generalize (IH X1 X2); clear IH; intro IH;
|
adamc@176
|
359 match type of IH with
|
adamc@176
|
360 | ?P -> _ => assert P
|
adamc@176
|
361 end
|
adamc@176
|
362 end
|
adamc@176
|
363 end; crush); eauto.
|
adamc@176
|
364 Qed.
|
adamc@176
|
365
|
adamc@176
|
366 Lemma vars_easy : forall (t : Source.type) (v1 : Source.typeDenote t)
|
adamc@176
|
367 (v2 : typeDenote (cpsType t)),
|
adamc@176
|
368 In
|
adamc@176
|
369 (existT
|
adamc@176
|
370 (fun t0 : Source.type =>
|
adamc@176
|
371 (Source.typeDenote t0 * typeDenote (cpsType t0))%type) t
|
adamc@176
|
372 (v1, v2)) nil -> lr t v1 v2.
|
adamc@176
|
373 crush.
|
adamc@176
|
374 Qed.
|
adamc@176
|
375
|
adamc@176
|
376 Theorem CpsExp_correct : forall (E : Exp Nat),
|
adamc@176
|
377 ProgDenote (CpsExp E) = ExpDenote E.
|
adamc@176
|
378 unfold ProgDenote, CpsExp, ExpDenote; intros;
|
adamc@176
|
379 generalize (cpsExp_correct (e1 := E _) (e2 := E _)
|
adamc@176
|
380 (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush.
|
adamc@176
|
381 Qed.
|
adamc@180
|
382 (* end thide *)
|
adamc@176
|
383
|
adamc@175
|
384 End STLC.
|
adamc@177
|
385
|
adamc@177
|
386
|
adamc@177
|
387 (** * A Pattern Compiler *)
|
adamc@177
|
388
|
adamc@177
|
389 Module PatMatch.
|
adamc@177
|
390 Module Source.
|
adamc@177
|
391 Inductive type : Type :=
|
adamc@177
|
392 | Unit : type
|
adamc@177
|
393 | Arrow : type -> type -> type
|
adamc@177
|
394 | Prod : type -> type -> type
|
adamc@177
|
395 | Sum : type -> type -> type.
|
adamc@177
|
396
|
adamc@177
|
397 Infix "-->" := Arrow (right associativity, at level 61).
|
adamc@177
|
398 Infix "++" := Sum (right associativity, at level 60).
|
adamc@177
|
399 Infix "**" := Prod (right associativity, at level 59).
|
adamc@177
|
400
|
adamc@177
|
401 Inductive pat : type -> list type -> Type :=
|
adamc@177
|
402 | PVar : forall t,
|
adamc@177
|
403 pat t (t :: nil)
|
adamc@177
|
404 | PPair : forall t1 t2 ts1 ts2,
|
adamc@177
|
405 pat t1 ts1
|
adamc@177
|
406 -> pat t2 ts2
|
adamc@177
|
407 -> pat (t1 ** t2) (ts1 ++ ts2)
|
adamc@177
|
408 | PInl : forall t1 t2 ts,
|
adamc@177
|
409 pat t1 ts
|
adamc@177
|
410 -> pat (t1 ++ t2) ts
|
adamc@177
|
411 | PInr : forall t1 t2 ts,
|
adamc@177
|
412 pat t2 ts
|
adamc@177
|
413 -> pat (t1 ++ t2) ts.
|
adamc@177
|
414
|
adamc@177
|
415 Implicit Arguments PVar [t].
|
adamc@177
|
416 Implicit Arguments PInl [t1 t2 ts].
|
adamc@177
|
417 Implicit Arguments PInr [t1 t2 ts].
|
adamc@177
|
418
|
adamc@177
|
419 Notation "##" := PVar (at level 70) : pat_scope.
|
adamc@179
|
420 Notation "[ p1 , p2 ]" := (PPair p1 p2) : pat_scope.
|
adamc@177
|
421 Notation "'Inl' p" := (PInl p) (at level 71) : pat_scope.
|
adamc@177
|
422 Notation "'Inr' p" := (PInr p) (at level 71) : pat_scope.
|
adamc@177
|
423
|
adamc@177
|
424 Bind Scope pat_scope with pat.
|
adamc@177
|
425 Delimit Scope pat_scope with pat.
|
adamc@177
|
426
|
adamc@177
|
427 Section vars.
|
adamc@177
|
428 Variable var : type -> Type.
|
adamc@177
|
429
|
adamc@177
|
430 Inductive exp : type -> Type :=
|
adamc@177
|
431 | Var : forall t,
|
adamc@177
|
432 var t
|
adamc@177
|
433 -> exp t
|
adamc@177
|
434
|
adamc@177
|
435 | EUnit : exp Unit
|
adamc@177
|
436
|
adamc@177
|
437 | App : forall t1 t2,
|
adamc@177
|
438 exp (t1 --> t2)
|
adamc@177
|
439 -> exp t1
|
adamc@177
|
440 -> exp t2
|
adamc@177
|
441 | Abs : forall t1 t2,
|
adamc@177
|
442 (var t1 -> exp t2)
|
adamc@177
|
443 -> exp (t1 --> t2)
|
adamc@177
|
444
|
adamc@177
|
445 | Pair : forall t1 t2,
|
adamc@177
|
446 exp t1
|
adamc@177
|
447 -> exp t2
|
adamc@177
|
448 -> exp (t1 ** t2)
|
adamc@177
|
449
|
adamc@177
|
450 | EInl : forall t1 t2,
|
adamc@177
|
451 exp t1
|
adamc@177
|
452 -> exp (t1 ++ t2)
|
adamc@177
|
453 | EInr : forall t1 t2,
|
adamc@177
|
454 exp t2
|
adamc@177
|
455 -> exp (t1 ++ t2)
|
adamc@177
|
456
|
adamc@177
|
457 | Case : forall t1 t2 (tss : list (list type)),
|
adamc@177
|
458 exp t1
|
adamc@177
|
459 -> (forall ts, member ts tss -> pat t1 ts)
|
adamc@177
|
460 -> (forall ts, member ts tss -> hlist var ts -> exp t2)
|
adamc@177
|
461 -> exp t2
|
adamc@177
|
462 -> exp t2.
|
adamc@177
|
463 End vars.
|
adamc@177
|
464
|
adamc@177
|
465 Definition Exp t := forall var, exp var t.
|
adamc@177
|
466
|
adamc@177
|
467 Implicit Arguments Var [var t].
|
adamc@177
|
468 Implicit Arguments EUnit [var].
|
adamc@177
|
469 Implicit Arguments App [var t1 t2].
|
adamc@177
|
470 Implicit Arguments Abs [var t1 t2].
|
adamc@177
|
471 Implicit Arguments Pair [var t1 t2].
|
adamc@177
|
472 Implicit Arguments EInl [var t1 t2].
|
adamc@177
|
473 Implicit Arguments EInr [var t1 t2].
|
adamc@177
|
474 Implicit Arguments Case [var t1 t2].
|
adamc@177
|
475
|
adamc@177
|
476 Notation "# v" := (Var v) (at level 70) : source_scope.
|
adamc@177
|
477
|
adamc@177
|
478 Notation "()" := EUnit : source_scope.
|
adamc@177
|
479
|
adamc@177
|
480 Infix "@" := App (left associativity, at level 77) : source_scope.
|
adamc@177
|
481 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
|
adamc@177
|
482
|
adamc@179
|
483 Notation "[ x , y ]" := (Pair x y) : source_scope.
|
adamc@177
|
484
|
adamc@177
|
485 Notation "'Inl' e" := (EInl e) (at level 71) : source_scope.
|
adamc@177
|
486 Notation "'Inr' e" := (EInr e) (at level 71) : source_scope.
|
adamc@177
|
487
|
adamc@178
|
488 Delimit Scope source_scope with source.
|
adamc@177
|
489 Bind Scope source_scope with exp.
|
adamc@177
|
490
|
adamc@221
|
491 Local Open Scope source_scope.
|
adamc@177
|
492
|
adamc@177
|
493 Fixpoint typeDenote (t : type) : Set :=
|
adamc@177
|
494 match t with
|
adamc@177
|
495 | Unit => unit
|
adamc@177
|
496 | t1 --> t2 => typeDenote t1 -> typeDenote t2
|
adamc@177
|
497 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
|
adamc@177
|
498 | t1 ++ t2 => (typeDenote t1 + typeDenote t2)%type
|
adamc@177
|
499 end.
|
adamc@177
|
500
|
adamc@224
|
501 Fixpoint patDenote t ts (p : pat t ts)
|
adamc@224
|
502 : typeDenote t -> option (hlist typeDenote ts) :=
|
adamc@224
|
503 match p with
|
adamc@216
|
504 | PVar _ => fun v => Some (v ::: HNil)
|
adamc@177
|
505 | PPair _ _ _ _ p1 p2 => fun v =>
|
adamc@177
|
506 match patDenote p1 (fst v), patDenote p2 (snd v) with
|
adamc@177
|
507 | Some tup1, Some tup2 => Some (happ tup1 tup2)
|
adamc@177
|
508 | _, _ => None
|
adamc@177
|
509 end
|
adamc@177
|
510 | PInl _ _ _ p' => fun v =>
|
adamc@177
|
511 match v with
|
adamc@177
|
512 | inl v' => patDenote p' v'
|
adamc@177
|
513 | _ => None
|
adamc@177
|
514 end
|
adamc@177
|
515 | PInr _ _ _ p' => fun v =>
|
adamc@177
|
516 match v with
|
adamc@177
|
517 | inr v' => patDenote p' v'
|
adamc@177
|
518 | _ => None
|
adamc@177
|
519 end
|
adamc@177
|
520 end.
|
adamc@177
|
521
|
adamc@177
|
522 Section matchesDenote.
|
adamc@177
|
523 Variables t2 : type.
|
adamc@177
|
524 Variable default : typeDenote t2.
|
adamc@177
|
525
|
adamc@177
|
526 Fixpoint matchesDenote (tss : list (list type))
|
adamc@177
|
527 : (forall ts, member ts tss -> option (hlist typeDenote ts))
|
adamc@177
|
528 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
|
adamc@177
|
529 -> typeDenote t2 :=
|
adamc@224
|
530 match tss with
|
adamc@177
|
531 | nil => fun _ _ =>
|
adamc@177
|
532 default
|
adamc@224
|
533 | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss')
|
adamc@224
|
534 -> option (hlist typeDenote ts'))
|
adamc@224
|
535 (bodies : forall ts', member ts' (ts :: tss')
|
adamc@224
|
536 -> hlist typeDenote ts' -> typeDenote t2) =>
|
adamc@216
|
537 match envs _ HFirst with
|
adamc@216
|
538 | None => matchesDenote
|
adamc@216
|
539 (fun _ mem => envs _ (HNext mem))
|
adamc@216
|
540 (fun _ mem => bodies _ (HNext mem))
|
adamc@216
|
541 | Some env => (bodies _ HFirst) env
|
adamc@177
|
542 end
|
adamc@177
|
543 end.
|
adamc@177
|
544 End matchesDenote.
|
adamc@177
|
545
|
adamc@177
|
546 Implicit Arguments matchesDenote [t2 tss].
|
adamc@177
|
547
|
adamc@224
|
548 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
|
adamc@224
|
549 match e with
|
adamc@177
|
550 | Var _ v => v
|
adamc@177
|
551
|
adamc@177
|
552 | EUnit => tt
|
adamc@177
|
553
|
adamc@177
|
554 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
|
adamc@177
|
555 | Abs _ _ e' => fun x => expDenote (e' x)
|
adamc@177
|
556
|
adamc@177
|
557 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
|
adamc@177
|
558
|
adamc@177
|
559 | EInl _ _ e' => inl _ (expDenote e')
|
adamc@177
|
560 | EInr _ _ e' => inr _ (expDenote e')
|
adamc@177
|
561
|
adamc@177
|
562 | Case _ _ _ e ps es def =>
|
adamc@177
|
563 matchesDenote (expDenote def)
|
adamc@177
|
564 (fun _ mem => patDenote (ps _ mem) (expDenote e))
|
adamc@177
|
565 (fun _ mem env => expDenote (es _ mem env))
|
adamc@177
|
566 end.
|
adamc@177
|
567
|
adamc@177
|
568 Definition ExpDenote t (E : Exp t) := expDenote (E _).
|
adamc@177
|
569 End Source.
|
adamc@177
|
570
|
adamc@177
|
571 Import Source.
|
adamc@177
|
572
|
adamc@178
|
573 Module Elab.
|
adamc@177
|
574 Section vars.
|
adamc@177
|
575 Variable var : type -> Type.
|
adamc@177
|
576
|
adamc@177
|
577 Inductive exp : type -> Type :=
|
adamc@177
|
578 | Var : forall t,
|
adamc@177
|
579 var t
|
adamc@177
|
580 -> exp t
|
adamc@177
|
581
|
adamc@177
|
582 | EUnit : exp Unit
|
adamc@177
|
583
|
adamc@177
|
584 | App : forall t1 t2,
|
adamc@177
|
585 exp (t1 --> t2)
|
adamc@177
|
586 -> exp t1
|
adamc@177
|
587 -> exp t2
|
adamc@177
|
588 | Abs : forall t1 t2,
|
adamc@177
|
589 (var t1 -> exp t2)
|
adamc@177
|
590 -> exp (t1 --> t2)
|
adamc@177
|
591
|
adamc@177
|
592 | Pair : forall t1 t2,
|
adamc@177
|
593 exp t1
|
adamc@177
|
594 -> exp t2
|
adamc@177
|
595 -> exp (t1 ** t2)
|
adamc@177
|
596 | Fst : forall t1 t2,
|
adamc@177
|
597 exp (t1 ** t2)
|
adamc@177
|
598 -> exp t1
|
adamc@177
|
599 | Snd : forall t1 t2,
|
adamc@177
|
600 exp (t1 ** t2)
|
adamc@177
|
601 -> exp t2
|
adamc@177
|
602
|
adamc@177
|
603 | EInl : forall t1 t2,
|
adamc@177
|
604 exp t1
|
adamc@177
|
605 -> exp (t1 ++ t2)
|
adamc@177
|
606 | EInr : forall t1 t2,
|
adamc@177
|
607 exp t2
|
adamc@177
|
608 -> exp (t1 ++ t2)
|
adamc@177
|
609 | Case : forall t1 t2 t,
|
adamc@177
|
610 exp (t1 ++ t2)
|
adamc@177
|
611 -> (var t1 -> exp t)
|
adamc@177
|
612 -> (var t2 -> exp t)
|
adamc@177
|
613 -> exp t.
|
adamc@177
|
614 End vars.
|
adamc@177
|
615
|
adamc@177
|
616 Definition Exp t := forall var, exp var t.
|
adamc@177
|
617
|
adamc@177
|
618 Implicit Arguments Var [var t].
|
adamc@177
|
619 Implicit Arguments EUnit [var].
|
adamc@177
|
620 Implicit Arguments App [var t1 t2].
|
adamc@177
|
621 Implicit Arguments Abs [var t1 t2].
|
adamc@177
|
622 Implicit Arguments Pair [var t1 t2].
|
adamc@177
|
623 Implicit Arguments Fst [var t1 t2].
|
adamc@177
|
624 Implicit Arguments Snd [var t1 t2].
|
adamc@177
|
625 Implicit Arguments EInl [var t1 t2].
|
adamc@177
|
626 Implicit Arguments EInr [var t1 t2].
|
adamc@177
|
627 Implicit Arguments Case [var t1 t2 t].
|
adamc@177
|
628
|
adamc@177
|
629
|
adamc@177
|
630 Notation "# v" := (Var v) (at level 70) : elab_scope.
|
adamc@177
|
631
|
adamc@177
|
632 Notation "()" := EUnit : elab_scope.
|
adamc@177
|
633
|
adamc@177
|
634 Infix "@" := App (left associativity, at level 77) : elab_scope.
|
adamc@177
|
635 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : elab_scope.
|
adamc@177
|
636 Notation "\ ? , e" := (Abs (fun _ => e)) (at level 78) : elab_scope.
|
adamc@177
|
637
|
adamc@179
|
638 Notation "[ x , y ]" := (Pair x y) : elab_scope.
|
adamc@177
|
639 Notation "#1 e" := (Fst e) (at level 72) : elab_scope.
|
adamc@177
|
640 Notation "#2 e" := (Snd e) (at level 72) : elab_scope.
|
adamc@177
|
641
|
adamc@177
|
642 Notation "'Inl' e" := (EInl e) (at level 71) : elab_scope.
|
adamc@177
|
643 Notation "'Inr' e" := (EInr e) (at level 71) : elab_scope.
|
adamc@177
|
644
|
adamc@177
|
645 Bind Scope elab_scope with exp.
|
adamc@177
|
646 Delimit Scope elab_scope with elab.
|
adamc@177
|
647
|
adamc@177
|
648 Open Scope elab_scope.
|
adamc@177
|
649
|
adamc@224
|
650 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
|
adamc@224
|
651 match e with
|
adamc@177
|
652 | Var _ v => v
|
adamc@177
|
653
|
adamc@177
|
654 | EUnit => tt
|
adamc@177
|
655
|
adamc@177
|
656 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
|
adamc@177
|
657 | Abs _ _ e' => fun x => expDenote (e' x)
|
adamc@177
|
658
|
adamc@177
|
659 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
|
adamc@177
|
660 | Fst _ _ e' => fst (expDenote e')
|
adamc@177
|
661 | Snd _ _ e' => snd (expDenote e')
|
adamc@177
|
662
|
adamc@177
|
663 | EInl _ _ e' => inl _ (expDenote e')
|
adamc@177
|
664 | EInr _ _ e' => inr _ (expDenote e')
|
adamc@177
|
665 | Case _ _ _ e' e1 e2 =>
|
adamc@177
|
666 match expDenote e' with
|
adamc@177
|
667 | inl v => expDenote (e1 v)
|
adamc@177
|
668 | inr v => expDenote (e2 v)
|
adamc@177
|
669 end
|
adamc@177
|
670 end.
|
adamc@177
|
671
|
adamc@177
|
672 Definition ExpDenote t (E : Exp t) := expDenote (E _).
|
adamc@177
|
673 End Elab.
|
adamc@177
|
674
|
adamc@178
|
675 Import Elab.
|
adamc@178
|
676
|
adamc@178
|
677 Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%source
|
adamc@178
|
678 (right associativity, at level 76, e1 at next level) : source_scope.
|
adamc@178
|
679 Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%elab
|
adamc@178
|
680 (right associativity, at level 76, e1 at next level) : elab_scope.
|
adamc@178
|
681
|
adamc@178
|
682 Section choice_tree.
|
adamc@178
|
683 Open Scope source_scope.
|
adamc@178
|
684
|
adamc@178
|
685 Fixpoint choice_tree var (t : type) (result : Type) : Type :=
|
adamc@178
|
686 match t with
|
adamc@178
|
687 | t1 ** t2 =>
|
adamc@178
|
688 choice_tree var t1
|
adamc@178
|
689 (choice_tree var t2
|
adamc@178
|
690 result)
|
adamc@178
|
691 | t1 ++ t2 =>
|
adamc@178
|
692 choice_tree var t1 result
|
adamc@178
|
693 * choice_tree var t2 result
|
adamc@178
|
694 | t => exp var t -> result
|
adamc@178
|
695 end%type.
|
adamc@178
|
696
|
adamc@224
|
697 Fixpoint merge var t result
|
adamc@178
|
698 : (result -> result -> result)
|
adamc@178
|
699 -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result :=
|
adamc@224
|
700 match t with
|
adamc@178
|
701 | _ ** _ => fun mr ct1 ct2 =>
|
adamc@178
|
702 merge _ _
|
adamc@178
|
703 (merge _ _ mr)
|
adamc@178
|
704 ct1 ct2
|
adamc@178
|
705
|
adamc@178
|
706 | _ ++ _ => fun mr ct1 ct2 =>
|
adamc@178
|
707 (merge var _ mr (fst ct1) (fst ct2),
|
adamc@178
|
708 merge var _ mr (snd ct1) (snd ct2))
|
adamc@178
|
709
|
adamc@178
|
710 | _ => fun mr ct1 ct2 e => mr (ct1 e) (ct2 e)
|
adamc@178
|
711 end.
|
adamc@178
|
712
|
adamc@224
|
713 Fixpoint everywhere var t result
|
adamc@178
|
714 : (exp var t -> result) -> choice_tree var t result :=
|
adamc@224
|
715 match t with
|
adamc@178
|
716 | t1 ** t2 => fun r =>
|
adamc@178
|
717 everywhere (t := t1) (fun e1 =>
|
adamc@178
|
718 everywhere (t := t2) (fun e2 =>
|
adamc@178
|
719 r ([e1, e2])%elab))
|
adamc@178
|
720
|
adamc@178
|
721 | _ ++ _ => fun r =>
|
adamc@178
|
722 (everywhere (fun e => r (Inl e)%elab),
|
adamc@178
|
723 everywhere (fun e => r (Inr e)%elab))
|
adamc@178
|
724
|
adamc@178
|
725 | _ => fun r => r
|
adamc@178
|
726 end.
|
adamc@178
|
727 End choice_tree.
|
adamc@178
|
728
|
adamc@178
|
729 Implicit Arguments merge [var t result].
|
adamc@178
|
730
|
adamc@178
|
731 Section elaborate.
|
adamc@221
|
732 Local Open Scope elab_scope.
|
adamc@178
|
733
|
adamc@224
|
734 Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) :
|
adamc@178
|
735 (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result :=
|
adamc@224
|
736 match p with
|
adamc@178
|
737 | PVar _ => fun succ fail =>
|
adamc@216
|
738 everywhere (fun disc => succ (disc ::: HNil))
|
adamc@178
|
739
|
adamc@178
|
740 | PPair _ _ _ _ p1 p2 => fun succ fail =>
|
adamc@216
|
741 elaboratePat p1
|
adamc@178
|
742 (fun tup1 =>
|
adamc@216
|
743 elaboratePat p2
|
adamc@178
|
744 (fun tup2 =>
|
adamc@178
|
745 succ (happ tup1 tup2))
|
adamc@178
|
746 fail)
|
adamc@178
|
747 (everywhere (fun _ => fail))
|
adamc@178
|
748
|
adamc@178
|
749 | PInl _ _ _ p' => fun succ fail =>
|
adamc@216
|
750 (elaboratePat p' succ fail,
|
adamc@178
|
751 everywhere (fun _ => fail))
|
adamc@178
|
752 | PInr _ _ _ p' => fun succ fail =>
|
adamc@178
|
753 (everywhere (fun _ => fail),
|
adamc@216
|
754 elaboratePat p' succ fail)
|
adamc@178
|
755 end.
|
adamc@178
|
756
|
adamc@178
|
757 Implicit Arguments elaboratePat [var t1 ts result].
|
adamc@178
|
758
|
adamc@224
|
759 Fixpoint letify var t ts : (hlist var ts -> exp var t)
|
adamc@178
|
760 -> hlist (exp var) ts -> exp var t :=
|
adamc@224
|
761 match ts with
|
adamc@216
|
762 | nil => fun f _ => f HNil
|
adamc@216
|
763 | _ :: _ => fun f tup => letify (fun tup' => x <- hhd tup; f (x ::: tup')) (htl tup)
|
adamc@178
|
764 end.
|
adamc@178
|
765
|
adamc@178
|
766 Implicit Arguments letify [var t ts].
|
adamc@178
|
767
|
adamc@178
|
768 Fixpoint expand var result t1 t2
|
adamc@224
|
769 (out : result -> exp var t2)
|
adamc@178
|
770 : forall ct : choice_tree var t1 result,
|
adamc@178
|
771 exp var t1
|
adamc@178
|
772 -> exp var t2 :=
|
adamc@224
|
773 match t1 with
|
adamc@178
|
774 | (_ ** _)%source => fun ct disc =>
|
adamc@178
|
775 expand
|
adamc@178
|
776 (fun ct' => expand out ct' (#2 disc)%source)
|
adamc@178
|
777 ct
|
adamc@178
|
778 (#1 disc)
|
adamc@178
|
779
|
adamc@178
|
780 | (_ ++ _)%source => fun ct disc =>
|
adamc@178
|
781 Case disc
|
adamc@178
|
782 (fun x => expand out (fst ct) (#x))
|
adamc@178
|
783 (fun y => expand out (snd ct) (#y))
|
adamc@178
|
784
|
adamc@178
|
785 | _ => fun ct disc =>
|
adamc@178
|
786 x <- disc; out (ct (#x))
|
adamc@178
|
787 end.
|
adamc@178
|
788
|
adamc@178
|
789 Definition mergeOpt A (o1 o2 : option A) :=
|
adamc@178
|
790 match o1 with
|
adamc@178
|
791 | None => o2
|
adamc@178
|
792 | _ => o1
|
adamc@178
|
793 end.
|
adamc@178
|
794
|
adamc@178
|
795 Import Source.
|
adamc@178
|
796
|
adamc@178
|
797 Fixpoint elaborateMatches var t1 t2
|
adamc@224
|
798 (tss : list (list type))
|
adamc@178
|
799 : (forall ts, member ts tss -> pat t1 ts)
|
adamc@178
|
800 -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2)
|
adamc@178
|
801 -> choice_tree var t1 (option (Elab.exp var t2)) :=
|
adamc@224
|
802 match tss with
|
adamc@178
|
803 | nil => fun _ _ =>
|
adamc@178
|
804 everywhere (fun _ => None)
|
adamc@178
|
805 | ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts')
|
adamc@178
|
806 (es : forall ts', member ts' (ts :: tss') -> hlist var ts' -> Elab.exp var t2) =>
|
adamc@178
|
807 merge (@mergeOpt _)
|
adamc@216
|
808 (elaboratePat (ps _ HFirst)
|
adamc@178
|
809 (fun ts => Some (letify
|
adamc@216
|
810 (fun ts' => es _ HFirst ts')
|
adamc@178
|
811 ts))
|
adamc@178
|
812 None)
|
adamc@216
|
813 (elaborateMatches
|
adamc@216
|
814 (fun _ mem => ps _ (HNext mem))
|
adamc@216
|
815 (fun _ mem => es _ (HNext mem)))
|
adamc@178
|
816 end.
|
adamc@178
|
817
|
adamc@178
|
818 Implicit Arguments elaborateMatches [var t1 t2 tss].
|
adamc@178
|
819
|
adamc@178
|
820 Open Scope cps_scope.
|
adamc@178
|
821
|
adamc@224
|
822 Fixpoint elaborate var t (e : Source.exp var t) : Elab.exp var t :=
|
adamc@224
|
823 match e with
|
adamc@178
|
824 | Var _ v => #v
|
adamc@178
|
825
|
adamc@178
|
826 | EUnit => ()
|
adamc@178
|
827
|
adamc@178
|
828 | App _ _ e1 e2 => elaborate e1 @ elaborate e2
|
adamc@178
|
829 | Abs _ _ e' => \x, elaborate (e' x)
|
adamc@178
|
830
|
adamc@178
|
831 | Pair _ _ e1 e2 => [elaborate e1, elaborate e2]
|
adamc@178
|
832 | EInl _ _ e' => Inl (elaborate e')
|
adamc@178
|
833 | EInr _ _ e' => Inr (elaborate e')
|
adamc@178
|
834
|
adamc@178
|
835 | Case _ _ _ e' ps es def =>
|
adamc@178
|
836 expand
|
adamc@178
|
837 (fun eo => match eo with
|
adamc@178
|
838 | None => elaborate def
|
adamc@178
|
839 | Some e => e
|
adamc@178
|
840 end)
|
adamc@178
|
841 (elaborateMatches ps (fun _ mem env => elaborate (es _ mem env)))
|
adamc@178
|
842 (elaborate e')
|
adamc@178
|
843 end.
|
adamc@178
|
844 End elaborate.
|
adamc@178
|
845
|
adamc@178
|
846 Definition Elaborate t (E : Source.Exp t) : Elab.Exp t :=
|
adamc@178
|
847 fun _ => elaborate (E _).
|
adamc@178
|
848
|
adamc@179
|
849 Fixpoint grab t result : choice_tree typeDenote t result -> typeDenote t -> result :=
|
adamc@224
|
850 match t with
|
adamc@179
|
851 | t1 ** t2 => fun ct v =>
|
adamc@179
|
852 grab t2 _ (grab t1 _ ct (fst v)) (snd v)
|
adamc@179
|
853 | t1 ++ t2 => fun ct v =>
|
adamc@179
|
854 match v with
|
adamc@179
|
855 | inl v' => grab t1 _ (fst ct) v'
|
adamc@179
|
856 | inr v' => grab t2 _ (snd ct) v'
|
adamc@179
|
857 end
|
adamc@179
|
858 | t => fun ct v => ct (#v)%elab
|
adamc@179
|
859 end%source%type.
|
adamc@179
|
860
|
adamc@179
|
861 Implicit Arguments grab [t result].
|
adamc@179
|
862
|
adamc@179
|
863 Ltac my_crush :=
|
adamc@179
|
864 crush;
|
adamc@179
|
865 repeat (match goal with
|
adamc@179
|
866 | [ |- context[match ?E with inl _ => _ | inr _ => _ end] ] =>
|
adamc@179
|
867 destruct E
|
adamc@179
|
868 end; crush).
|
adamc@179
|
869
|
adamc@179
|
870 Lemma expand_grab : forall t2 t1 result
|
adamc@179
|
871 (out : result -> Elab.exp typeDenote t2)
|
adamc@179
|
872 (ct : choice_tree typeDenote t1 result)
|
adamc@179
|
873 (disc : Elab.exp typeDenote t1),
|
adamc@224
|
874 Elab.expDenote (expand out ct disc)
|
adamc@224
|
875 = Elab.expDenote (out (grab ct (Elab.expDenote disc))).
|
adamc@179
|
876 induction t1; my_crush.
|
adamc@179
|
877 Qed.
|
adamc@179
|
878
|
adamc@179
|
879 Lemma recreate_pair : forall t1 t2
|
adamc@179
|
880 (x : Elab.exp typeDenote t1)
|
adamc@179
|
881 (x0 : Elab.exp typeDenote t2)
|
adamc@179
|
882 (v : typeDenote (t1 ** t2)),
|
adamc@179
|
883 expDenote x = fst v
|
adamc@179
|
884 -> expDenote x0 = snd v
|
adamc@179
|
885 -> @eq (typeDenote t1 * typeDenote t2) (expDenote [x, x0]) v.
|
adamc@179
|
886 destruct v; crush.
|
adamc@179
|
887 Qed.
|
adamc@179
|
888
|
adamc@179
|
889 Lemma everywhere_correct : forall t1 result
|
adamc@179
|
890 (succ : Elab.exp typeDenote t1 -> result) disc,
|
adamc@179
|
891 exists disc', grab (everywhere succ) (Elab.expDenote disc) = succ disc'
|
adamc@179
|
892 /\ Elab.expDenote disc' = Elab.expDenote disc.
|
adamc@179
|
893 Hint Resolve recreate_pair.
|
adamc@179
|
894
|
adamc@179
|
895 induction t1; my_crush; eauto; fold choice_tree;
|
adamc@179
|
896 repeat (fold typeDenote in *; crush;
|
adamc@179
|
897 match goal with
|
adamc@179
|
898 | [ IH : forall result succ, _ |- context[grab (everywhere ?S) _] ] =>
|
adamc@179
|
899 generalize (IH _ S); clear IH
|
adamc@179
|
900 | [ e : exp typeDenote (?T ** _), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
|
adamc@179
|
901 generalize (IH (#1 e)); clear IH
|
adamc@179
|
902 | [ e : exp typeDenote (_ ** ?T), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
|
adamc@179
|
903 generalize (IH (#2 e)); clear IH
|
adamc@179
|
904 | [ e : typeDenote ?T, IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
|
adamc@179
|
905 generalize (IH (#e)); clear IH
|
adamc@179
|
906 end; crush); eauto.
|
adamc@179
|
907 Qed.
|
adamc@179
|
908
|
adamc@179
|
909 Lemma merge_correct : forall t result
|
adamc@179
|
910 (ct1 ct2 : choice_tree typeDenote t result)
|
adamc@179
|
911 (mr : result -> result -> result) v,
|
adamc@179
|
912 grab (merge mr ct1 ct2) v = mr (grab ct1 v) (grab ct2 v).
|
adamc@179
|
913 induction t; crush.
|
adamc@179
|
914 Qed.
|
adamc@179
|
915
|
adamc@179
|
916 Lemma everywhere_fail : forall t result
|
adamc@179
|
917 (fail : result) v,
|
adamc@179
|
918 grab (everywhere (fun _ : Elab.exp typeDenote t => fail)) v = fail.
|
adamc@179
|
919 induction t; crush.
|
adamc@179
|
920 Qed.
|
adamc@179
|
921
|
adamc@179
|
922 Lemma elaboratePat_correct : forall t1 ts (p : pat t1 ts)
|
adamc@179
|
923 result (succ : hlist (Elab.exp typeDenote) ts -> result)
|
adamc@179
|
924 (fail : result) v env,
|
adamc@179
|
925 patDenote p v = Some env
|
adamc@216
|
926 -> exists env', grab (elaboratePat p succ fail) v = succ env'
|
adamc@179
|
927 /\ env = hmap Elab.expDenote env'.
|
adamc@179
|
928 Hint Resolve hmap_happ.
|
adamc@179
|
929
|
adamc@179
|
930 induction p; crush; fold choice_tree;
|
adamc@179
|
931 repeat (match goal with
|
adamc@179
|
932 | [ |- context[grab (everywhere ?succ) ?v] ] =>
|
adamc@179
|
933 generalize (everywhere_correct succ (#v)%elab)
|
adamc@179
|
934
|
adamc@224
|
935 | [ H : forall result succ fail, _
|
adamc@224
|
936 |- context[grab (elaboratePat _ ?S ?F) ?V] ] =>
|
adamc@179
|
937 generalize (H _ S F V); clear H
|
adamc@179
|
938 | [ H1 : context[match ?E with Some _ => _ | None => _ end],
|
adamc@216
|
939 H2 : forall env, ?E = Some env -> _ |- _ ] =>
|
adamc@216
|
940 destruct E
|
adamc@179
|
941 | [ H : forall env, Some ?E = Some env -> _ |- _ ] =>
|
adamc@179
|
942 generalize (H _ (refl_equal _)); clear H
|
adamc@179
|
943 end; crush); eauto.
|
adamc@179
|
944 Qed.
|
adamc@179
|
945
|
adamc@179
|
946 Lemma elaboratePat_fails : forall t1 ts (p : pat t1 ts)
|
adamc@179
|
947 result (succ : hlist (Elab.exp typeDenote) ts -> result)
|
adamc@179
|
948 (fail : result) v,
|
adamc@179
|
949 patDenote p v = None
|
adamc@216
|
950 -> grab (elaboratePat p succ fail) v = fail.
|
adamc@179
|
951 Hint Resolve everywhere_fail.
|
adamc@179
|
952
|
adamc@179
|
953 induction p; try solve [ crush ];
|
adamc@179
|
954 simpl; fold choice_tree; intuition; simpl in *;
|
adamc@179
|
955 repeat match goal with
|
adamc@179
|
956 | [ IH : forall result succ fail v, patDenote ?P v = _ -> _
|
adamc@216
|
957 |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
|
adamc@179
|
958 generalize (IH _ S F V); clear IH; intro IH;
|
adamc@179
|
959 generalize (elaboratePat_correct P S F V); intros;
|
adamc@179
|
960 destruct (patDenote P V); try discriminate
|
adamc@179
|
961 | [ H : forall env, Some _ = Some env -> _ |- _ ] =>
|
adamc@179
|
962 destruct (H _ (refl_equal _)); clear H; intuition
|
adamc@179
|
963 | [ H : _ |- _ ] => rewrite H; intuition
|
adamc@224
|
964 | [ |- context[match ?v with inl _ => _ | inr _ => _ end] ] =>
|
adamc@224
|
965 destruct v; auto
|
adamc@179
|
966 end.
|
adamc@179
|
967 Qed.
|
adamc@179
|
968
|
adamc@179
|
969 Implicit Arguments letify [var t ts].
|
adamc@179
|
970
|
adamc@179
|
971 Lemma letify_correct : forall t ts (f : hlist typeDenote ts -> Elab.exp typeDenote t)
|
adamc@179
|
972 (env : hlist (Elab.exp typeDenote) ts),
|
adamc@179
|
973 Elab.expDenote (letify f env)
|
adamc@179
|
974 = Elab.expDenote (f (hmap Elab.expDenote env)).
|
adamc@216
|
975 induction ts; crush; dep_destruct env; crush.
|
adamc@179
|
976 Qed.
|
adamc@179
|
977
|
adamc@179
|
978 Theorem elaborate_correct : forall t (e : Source.exp typeDenote t),
|
adamc@179
|
979 Elab.expDenote (elaborate e) = Source.expDenote e.
|
adamc@179
|
980 Hint Rewrite expand_grab merge_correct letify_correct : cpdt.
|
adamc@179
|
981 Hint Rewrite everywhere_fail elaboratePat_fails using assumption : cpdt.
|
adamc@179
|
982
|
adamc@179
|
983 induction e; crush; try (ext_eq; crush);
|
adamc@179
|
984 match goal with
|
adamc@179
|
985 | [ tss : list (list type) |- _ ] =>
|
adamc@179
|
986 induction tss; crush;
|
adamc@179
|
987 match goal with
|
adamc@216
|
988 | [ |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
|
adamc@179
|
989 case_eq (patDenote P V); [intros env Heq;
|
adamc@179
|
990 destruct (elaboratePat_correct P S F _ Heq); crush;
|
adamc@179
|
991 match goal with
|
adamc@179
|
992 | [ H : _ |- _ ] => rewrite <- H; crush
|
adamc@179
|
993 end
|
adamc@179
|
994 | crush ]
|
adamc@179
|
995 end
|
adamc@179
|
996 end.
|
adamc@179
|
997 Qed.
|
adamc@179
|
998
|
adamc@179
|
999 Theorem Elaborate_correct : forall t (E : Source.Exp t),
|
adamc@179
|
1000 Elab.ExpDenote (Elaborate E) = Source.ExpDenote E.
|
adamc@179
|
1001 unfold Elab.ExpDenote, Elaborate, Source.ExpDenote;
|
adamc@179
|
1002 intros; apply elaborate_correct.
|
adamc@179
|
1003 Qed.
|
adamc@179
|
1004
|
adamc@177
|
1005 End PatMatch.
|
adamc@181
|
1006
|
adamc@181
|
1007
|
adamc@181
|
1008 (** * Exercises *)
|
adamc@181
|
1009
|
adamc@181
|
1010 (** %\begin{enumerate}%#<ol>#
|
adamc@181
|
1011
|
adamc@181
|
1012 %\item%#<li># When in the last chapter we implemented constant folding for simply-typed lambda calculus, it may have seemed natural to try applying beta reductions. This would have been a lot more trouble than is apparent at first, because we would have needed to convince Coq that our normalizing function always terminated.
|
adamc@181
|
1013
|
adamc@181
|
1014 It might also seem that beta reduction is a lost cause because we have no effective way of substituting in the [exp] type; we only managed to write a substitution function for the parametric [Exp] type. This is not as big of a problem as it seems. For instance, for the language we built by extending simply-typed lambda calculus with products and sums, it also appears that we need substitution for simplifying [case] expressions whose discriminees are known to be [inl] or [inr], but the function is still implementable.
|
adamc@181
|
1015
|
adamc@200
|
1016 For this exercise, extend the products and sums constant folder from the last chapter so that it simplifies [case] expressions as well, by checking if the discriminee is a known [inl] or known [inr]. Also extend the correctness theorem to apply to your new definition. You will probably want to assert an axiom relating to an expression equivalence relation like the one defined in this chapter. Any such axiom should only mention syntax; it should not mention any compilation or denotation functions. Following the format of the axiom from the last chapter is the safest bet to avoid proving a worthless theorem.
|
adamc@181
|
1017 #</li>#
|
adamc@181
|
1018
|
adamc@181
|
1019 #</ol>#%\end{enumerate}% *)
|