adamc@175
|
1 (* Copyright (c) 2008, 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@177
|
13 Require Import AxiomsImpred Tactics DepList.
|
adamc@175
|
14
|
adamc@175
|
15 Set Implicit Arguments.
|
adamc@175
|
16 (* end hide *)
|
adamc@175
|
17
|
adamc@175
|
18
|
adamc@175
|
19 (** %\chapter{Certifying 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@175
|
93 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
|
adamc@175
|
94 match e in (exp _ t) return (typeDenote t) 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@176
|
106 Section exp_equiv.
|
adamc@176
|
107 Variables var1 var2 : type -> Type.
|
adamc@176
|
108
|
adamc@176
|
109 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop :=
|
adamc@176
|
110 | EqEVar : forall G t (v1 : var1 t) v2,
|
adamc@176
|
111 In (existT _ t (v1, v2)) G
|
adamc@176
|
112 -> exp_equiv G (#v1) (#v2)
|
adamc@176
|
113
|
adamc@176
|
114 | EqEConst : forall G n,
|
adamc@176
|
115 exp_equiv G (^n) (^n)
|
adamc@176
|
116 | EqEPlus : forall G x1 y1 x2 y2,
|
adamc@176
|
117 exp_equiv G x1 x2
|
adamc@176
|
118 -> exp_equiv G y1 y2
|
adamc@176
|
119 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
|
adamc@176
|
120
|
adamc@176
|
121 | EqEApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
|
adamc@176
|
122 exp_equiv G f1 f2
|
adamc@176
|
123 -> exp_equiv G x1 x2
|
adamc@176
|
124 -> exp_equiv G (f1 @ x1) (f2 @ x2)
|
adamc@176
|
125 | EqEAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
|
adamc@176
|
126 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
|
adamc@176
|
127 -> exp_equiv G (Abs f1) (Abs f2).
|
adamc@176
|
128 End exp_equiv.
|
adamc@176
|
129
|
adamc@176
|
130 Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
|
adamc@176
|
131 exp_equiv nil (E var1) (E var2).
|
adamc@175
|
132 End Source.
|
adamc@175
|
133
|
adamc@175
|
134 Module CPS.
|
adamc@175
|
135 Inductive type : Type :=
|
adamc@175
|
136 | TNat : type
|
adamc@175
|
137 | Cont : type -> type
|
adamc@175
|
138 | TUnit : type
|
adamc@175
|
139 | Prod : type -> type -> type.
|
adamc@175
|
140
|
adamc@175
|
141 Notation "'Nat'" := TNat : cps_scope.
|
adamc@175
|
142 Notation "'Unit'" := TUnit : cps_scope.
|
adamc@175
|
143 Notation "t --->" := (Cont t) (at level 61) : cps_scope.
|
adamc@175
|
144 Infix "**" := Prod (right associativity, at level 60) : cps_scope.
|
adamc@175
|
145
|
adamc@175
|
146 Bind Scope cps_scope with type.
|
adamc@175
|
147 Delimit Scope cps_scope with cps.
|
adamc@175
|
148
|
adamc@175
|
149 Section vars.
|
adamc@175
|
150 Variable var : type -> Type.
|
adamc@175
|
151
|
adamc@175
|
152 Inductive prog : Type :=
|
adamc@175
|
153 | PHalt :
|
adamc@175
|
154 var Nat
|
adamc@175
|
155 -> prog
|
adamc@175
|
156 | App : forall t,
|
adamc@175
|
157 var (t --->)
|
adamc@175
|
158 -> var t
|
adamc@175
|
159 -> prog
|
adamc@175
|
160 | Bind : forall t,
|
adamc@175
|
161 primop t
|
adamc@175
|
162 -> (var t -> prog)
|
adamc@175
|
163 -> prog
|
adamc@175
|
164
|
adamc@175
|
165 with primop : type -> Type :=
|
adamc@175
|
166 | Var : forall t,
|
adamc@175
|
167 var t
|
adamc@175
|
168 -> primop t
|
adamc@175
|
169
|
adamc@175
|
170 | Const : nat -> primop Nat
|
adamc@175
|
171 | Plus : var Nat -> var Nat -> primop Nat
|
adamc@175
|
172
|
adamc@175
|
173 | Abs : forall t,
|
adamc@175
|
174 (var t -> prog)
|
adamc@175
|
175 -> primop (t --->)
|
adamc@175
|
176
|
adamc@175
|
177 | Pair : forall t1 t2,
|
adamc@175
|
178 var t1
|
adamc@175
|
179 -> var t2
|
adamc@175
|
180 -> primop (t1 ** t2)
|
adamc@175
|
181 | Fst : forall t1 t2,
|
adamc@175
|
182 var (t1 ** t2)
|
adamc@175
|
183 -> primop t1
|
adamc@175
|
184 | Snd : forall t1 t2,
|
adamc@175
|
185 var (t1 ** t2)
|
adamc@175
|
186 -> primop t2.
|
adamc@175
|
187 End vars.
|
adamc@175
|
188
|
adamc@175
|
189 Implicit Arguments PHalt [var].
|
adamc@175
|
190 Implicit Arguments App [var t].
|
adamc@175
|
191
|
adamc@175
|
192 Implicit Arguments Var [var t].
|
adamc@175
|
193 Implicit Arguments Const [var].
|
adamc@175
|
194 Implicit Arguments Plus [var].
|
adamc@175
|
195 Implicit Arguments Abs [var t].
|
adamc@175
|
196 Implicit Arguments Pair [var t1 t2].
|
adamc@175
|
197 Implicit Arguments Fst [var t1 t2].
|
adamc@175
|
198 Implicit Arguments Snd [var t1 t2].
|
adamc@175
|
199
|
adamc@175
|
200 Notation "'Halt' x" := (PHalt x) (no associativity, at level 75) : cps_scope.
|
adamc@175
|
201 Infix "@@" := App (no associativity, at level 75) : cps_scope.
|
adamc@175
|
202 Notation "x <- p ; e" := (Bind p (fun x => e))
|
adamc@175
|
203 (right associativity, at level 76, p at next level) : cps_scope.
|
adamc@175
|
204 Notation "! <- p ; e" := (Bind p (fun _ => e))
|
adamc@175
|
205 (right associativity, at level 76, p at next level) : cps_scope.
|
adamc@175
|
206
|
adamc@175
|
207 Notation "# v" := (Var v) (at level 70) : cps_scope.
|
adamc@175
|
208
|
adamc@175
|
209 Notation "^ n" := (Const n) (at level 70) : cps_scope.
|
adamc@175
|
210 Infix "+^" := Plus (left associativity, at level 79) : cps_scope.
|
adamc@175
|
211
|
adamc@175
|
212 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : cps_scope.
|
adamc@175
|
213 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : cps_scope.
|
adamc@175
|
214
|
adamc@175
|
215 Notation "[ x1 , x2 ]" := (Pair x1 x2) (at level 73) : cps_scope.
|
adamc@175
|
216 Notation "#1 x" := (Fst x) (at level 72) : cps_scope.
|
adamc@175
|
217 Notation "#2 x" := (Snd x) (at level 72) : cps_scope.
|
adamc@175
|
218
|
adamc@175
|
219 Bind Scope cps_scope with prog primop.
|
adamc@175
|
220
|
adamc@175
|
221 Open Scope cps_scope.
|
adamc@175
|
222
|
adamc@175
|
223 Fixpoint typeDenote (t : type) : Set :=
|
adamc@175
|
224 match t with
|
adamc@175
|
225 | Nat => nat
|
adamc@175
|
226 | t' ---> => typeDenote t' -> nat
|
adamc@175
|
227 | Unit => unit
|
adamc@175
|
228 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
|
adamc@175
|
229 end.
|
adamc@175
|
230
|
adamc@175
|
231 Fixpoint progDenote (e : prog typeDenote) : nat :=
|
adamc@175
|
232 match e with
|
adamc@175
|
233 | PHalt n => n
|
adamc@175
|
234 | App _ f x => f x
|
adamc@175
|
235 | Bind _ p x => progDenote (x (primopDenote p))
|
adamc@175
|
236 end
|
adamc@175
|
237
|
adamc@175
|
238 with primopDenote t (p : primop typeDenote t) {struct p} : typeDenote t :=
|
adamc@175
|
239 match p in (primop _ t) return (typeDenote t) with
|
adamc@175
|
240 | Var _ v => v
|
adamc@175
|
241
|
adamc@175
|
242 | Const n => n
|
adamc@175
|
243 | Plus n1 n2 => n1 + n2
|
adamc@175
|
244
|
adamc@175
|
245 | Abs _ e => fun x => progDenote (e x)
|
adamc@175
|
246
|
adamc@175
|
247 | Pair _ _ v1 v2 => (v1, v2)
|
adamc@175
|
248 | Fst _ _ v => fst v
|
adamc@175
|
249 | Snd _ _ v => snd v
|
adamc@175
|
250 end.
|
adamc@175
|
251
|
adamc@175
|
252 Definition Prog := forall var, prog var.
|
adamc@175
|
253 Definition Primop t := forall var, primop var t.
|
adamc@175
|
254 Definition ProgDenote (E : Prog) := progDenote (E _).
|
adamc@175
|
255 Definition PrimopDenote t (P : Primop t) := primopDenote (P _).
|
adamc@175
|
256 End CPS.
|
adamc@175
|
257
|
adamc@175
|
258 Import Source CPS.
|
adamc@175
|
259
|
adamc@175
|
260 Fixpoint cpsType (t : Source.type) : CPS.type :=
|
adamc@175
|
261 match t with
|
adamc@175
|
262 | Nat => Nat%cps
|
adamc@175
|
263 | t1 --> t2 => (cpsType t1 ** (cpsType t2 --->) --->)%cps
|
adamc@175
|
264 end%source.
|
adamc@175
|
265
|
adamc@175
|
266 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
|
adamc@175
|
267
|
adamc@175
|
268 Section cpsExp.
|
adamc@175
|
269 Variable var : CPS.type -> Type.
|
adamc@175
|
270
|
adamc@175
|
271 Import Source.
|
adamc@175
|
272 Open Scope cps_scope.
|
adamc@175
|
273
|
adamc@175
|
274 Fixpoint cpsExp t (e : exp (fun t => var (cpsType t)) t) {struct e}
|
adamc@175
|
275 : (var (cpsType t) -> prog var) -> prog var :=
|
adamc@175
|
276 match e in (exp _ t) return ((var (cpsType t) -> prog var) -> prog var) with
|
adamc@175
|
277 | Var _ v => fun k => k v
|
adamc@175
|
278
|
adamc@175
|
279 | Const n => fun k =>
|
adamc@175
|
280 x <- ^n;
|
adamc@175
|
281 k x
|
adamc@175
|
282 | Plus e1 e2 => fun k =>
|
adamc@175
|
283 x1 <-- e1;
|
adamc@175
|
284 x2 <-- e2;
|
adamc@175
|
285 x <- x1 +^ x2;
|
adamc@175
|
286 k x
|
adamc@175
|
287
|
adamc@175
|
288 | App _ _ e1 e2 => fun k =>
|
adamc@175
|
289 f <-- e1;
|
adamc@175
|
290 x <-- e2;
|
adamc@175
|
291 kf <- \r, k r;
|
adamc@175
|
292 p <- [x, kf];
|
adamc@175
|
293 f @@ p
|
adamc@175
|
294 | Abs _ _ e' => fun k =>
|
adamc@175
|
295 f <- CPS.Abs (var := var) (fun p =>
|
adamc@175
|
296 x <- #1 p;
|
adamc@175
|
297 kf <- #2 p;
|
adamc@175
|
298 r <-- e' x;
|
adamc@175
|
299 kf @@ r);
|
adamc@175
|
300 k f
|
adamc@175
|
301 end
|
adamc@175
|
302
|
adamc@175
|
303 where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
|
adamc@175
|
304 End cpsExp.
|
adamc@175
|
305
|
adamc@175
|
306 Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)) : cps_scope.
|
adamc@175
|
307 Notation "! <-- e1 ; e2" := (cpsExp e1 (fun _ => e2))
|
adamc@175
|
308 (right associativity, at level 76, e1 at next level) : cps_scope.
|
adamc@175
|
309
|
adamc@175
|
310 Implicit Arguments cpsExp [var t].
|
adamc@175
|
311 Definition CpsExp (E : Exp Nat) : Prog :=
|
adamc@175
|
312 fun var => cpsExp (E _) (PHalt (var := _)).
|
adamc@175
|
313
|
adamc@175
|
314 Eval compute in CpsExp zero.
|
adamc@175
|
315 Eval compute in CpsExp one.
|
adamc@175
|
316 Eval compute in CpsExp zpo.
|
adamc@175
|
317 Eval compute in CpsExp app_ident.
|
adamc@175
|
318 Eval compute in CpsExp app_ident'.
|
adamc@175
|
319
|
adamc@175
|
320 Eval compute in ProgDenote (CpsExp zero).
|
adamc@175
|
321 Eval compute in ProgDenote (CpsExp one).
|
adamc@175
|
322 Eval compute in ProgDenote (CpsExp zpo).
|
adamc@175
|
323 Eval compute in ProgDenote (CpsExp app_ident).
|
adamc@175
|
324 Eval compute in ProgDenote (CpsExp app_ident').
|
adamc@175
|
325
|
adamc@176
|
326 Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop :=
|
adamc@176
|
327 match t return (Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop) with
|
adamc@176
|
328 | Nat => fun n1 n2 => n1 = n2
|
adamc@176
|
329 | t1 --> t2 => fun f1 f2 =>
|
adamc@176
|
330 forall x1 x2, lr _ x1 x2
|
adamc@176
|
331 -> forall k, exists r,
|
adamc@176
|
332 f2 (x2, k) = k r
|
adamc@176
|
333 /\ lr _ (f1 x1) r
|
adamc@176
|
334 end%source.
|
adamc@176
|
335
|
adamc@176
|
336 Lemma cpsExp_correct : forall G t (e1 : exp _ t) (e2 : exp _ t),
|
adamc@176
|
337 exp_equiv G e1 e2
|
adamc@176
|
338 -> (forall t v1 v2, In (existT _ t (v1, v2)) G -> lr t v1 v2)
|
adamc@176
|
339 -> forall k, exists r,
|
adamc@176
|
340 progDenote (cpsExp e2 k) = progDenote (k r)
|
adamc@176
|
341 /\ lr t (expDenote e1) r.
|
adamc@176
|
342 induction 1; crush; fold typeDenote in *;
|
adamc@176
|
343 repeat (match goal with
|
adamc@176
|
344 | [ H : forall k, exists r, progDenote (cpsExp ?E k) = _ /\ _
|
adamc@176
|
345 |- context[cpsExp ?E ?K] ] =>
|
adamc@176
|
346 generalize (H K); clear H
|
adamc@176
|
347 | [ |- exists r, progDenote (_ ?R) = progDenote (_ r) /\ _ ] =>
|
adamc@176
|
348 exists R
|
adamc@176
|
349 | [ t1 : Source.type |- _ ] =>
|
adamc@176
|
350 match goal with
|
adamc@176
|
351 | [ Hlr : lr t1 ?X1 ?X2, IH : forall v1 v2, _ |- _ ] =>
|
adamc@176
|
352 generalize (IH X1 X2); clear IH; intro IH;
|
adamc@176
|
353 match type of IH with
|
adamc@176
|
354 | ?P -> _ => assert P
|
adamc@176
|
355 end
|
adamc@176
|
356 end
|
adamc@176
|
357 end; crush); eauto.
|
adamc@176
|
358 Qed.
|
adamc@176
|
359
|
adamc@176
|
360 Lemma vars_easy : forall (t : Source.type) (v1 : Source.typeDenote t)
|
adamc@176
|
361 (v2 : typeDenote (cpsType t)),
|
adamc@176
|
362 In
|
adamc@176
|
363 (existT
|
adamc@176
|
364 (fun t0 : Source.type =>
|
adamc@176
|
365 (Source.typeDenote t0 * typeDenote (cpsType t0))%type) t
|
adamc@176
|
366 (v1, v2)) nil -> lr t v1 v2.
|
adamc@176
|
367 crush.
|
adamc@176
|
368 Qed.
|
adamc@176
|
369
|
adamc@176
|
370 Theorem CpsExp_correct : forall (E : Exp Nat),
|
adamc@176
|
371 ProgDenote (CpsExp E) = ExpDenote E.
|
adamc@176
|
372 unfold ProgDenote, CpsExp, ExpDenote; intros;
|
adamc@176
|
373 generalize (cpsExp_correct (e1 := E _) (e2 := E _)
|
adamc@176
|
374 (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush.
|
adamc@176
|
375 Qed.
|
adamc@176
|
376
|
adamc@175
|
377 End STLC.
|
adamc@177
|
378
|
adamc@177
|
379
|
adamc@177
|
380 (** * A Pattern Compiler *)
|
adamc@177
|
381
|
adamc@177
|
382 Module PatMatch.
|
adamc@177
|
383 Module Source.
|
adamc@177
|
384 Inductive type : Type :=
|
adamc@177
|
385 | Unit : type
|
adamc@177
|
386 | Arrow : type -> type -> type
|
adamc@177
|
387 | Prod : type -> type -> type
|
adamc@177
|
388 | Sum : type -> type -> type.
|
adamc@177
|
389
|
adamc@177
|
390 Infix "-->" := Arrow (right associativity, at level 61).
|
adamc@177
|
391 Infix "++" := Sum (right associativity, at level 60).
|
adamc@177
|
392 Infix "**" := Prod (right associativity, at level 59).
|
adamc@177
|
393
|
adamc@177
|
394 Inductive pat : type -> list type -> Type :=
|
adamc@177
|
395 | PVar : forall t,
|
adamc@177
|
396 pat t (t :: nil)
|
adamc@177
|
397 | PPair : forall t1 t2 ts1 ts2,
|
adamc@177
|
398 pat t1 ts1
|
adamc@177
|
399 -> pat t2 ts2
|
adamc@177
|
400 -> pat (t1 ** t2) (ts1 ++ ts2)
|
adamc@177
|
401 | PInl : forall t1 t2 ts,
|
adamc@177
|
402 pat t1 ts
|
adamc@177
|
403 -> pat (t1 ++ t2) ts
|
adamc@177
|
404 | PInr : forall t1 t2 ts,
|
adamc@177
|
405 pat t2 ts
|
adamc@177
|
406 -> pat (t1 ++ t2) ts.
|
adamc@177
|
407
|
adamc@177
|
408 Implicit Arguments PVar [t].
|
adamc@177
|
409 Implicit Arguments PInl [t1 t2 ts].
|
adamc@177
|
410 Implicit Arguments PInr [t1 t2 ts].
|
adamc@177
|
411
|
adamc@177
|
412 Notation "##" := PVar (at level 70) : pat_scope.
|
adamc@177
|
413 Notation "[ p1 , p2 ]" := (PPair p1 p2) (at level 72) : pat_scope.
|
adamc@177
|
414 Notation "'Inl' p" := (PInl p) (at level 71) : pat_scope.
|
adamc@177
|
415 Notation "'Inr' p" := (PInr p) (at level 71) : pat_scope.
|
adamc@177
|
416
|
adamc@177
|
417 Bind Scope pat_scope with pat.
|
adamc@177
|
418 Delimit Scope pat_scope with pat.
|
adamc@177
|
419
|
adamc@177
|
420 Section vars.
|
adamc@177
|
421 Variable var : type -> Type.
|
adamc@177
|
422
|
adamc@177
|
423 Inductive exp : type -> Type :=
|
adamc@177
|
424 | Var : forall t,
|
adamc@177
|
425 var t
|
adamc@177
|
426 -> exp t
|
adamc@177
|
427
|
adamc@177
|
428 | EUnit : exp Unit
|
adamc@177
|
429
|
adamc@177
|
430 | App : forall t1 t2,
|
adamc@177
|
431 exp (t1 --> t2)
|
adamc@177
|
432 -> exp t1
|
adamc@177
|
433 -> exp t2
|
adamc@177
|
434 | Abs : forall t1 t2,
|
adamc@177
|
435 (var t1 -> exp t2)
|
adamc@177
|
436 -> exp (t1 --> t2)
|
adamc@177
|
437
|
adamc@177
|
438 | Pair : forall t1 t2,
|
adamc@177
|
439 exp t1
|
adamc@177
|
440 -> exp t2
|
adamc@177
|
441 -> exp (t1 ** t2)
|
adamc@177
|
442
|
adamc@177
|
443 | EInl : forall t1 t2,
|
adamc@177
|
444 exp t1
|
adamc@177
|
445 -> exp (t1 ++ t2)
|
adamc@177
|
446 | EInr : forall t1 t2,
|
adamc@177
|
447 exp t2
|
adamc@177
|
448 -> exp (t1 ++ t2)
|
adamc@177
|
449
|
adamc@177
|
450 | Case : forall t1 t2 (tss : list (list type)),
|
adamc@177
|
451 exp t1
|
adamc@177
|
452 -> (forall ts, member ts tss -> pat t1 ts)
|
adamc@177
|
453 -> (forall ts, member ts tss -> hlist var ts -> exp t2)
|
adamc@177
|
454 -> exp t2
|
adamc@177
|
455 -> exp t2.
|
adamc@177
|
456 End vars.
|
adamc@177
|
457
|
adamc@177
|
458 Definition Exp t := forall var, exp var t.
|
adamc@177
|
459
|
adamc@177
|
460 Implicit Arguments Var [var t].
|
adamc@177
|
461 Implicit Arguments EUnit [var].
|
adamc@177
|
462 Implicit Arguments App [var t1 t2].
|
adamc@177
|
463 Implicit Arguments Abs [var t1 t2].
|
adamc@177
|
464 Implicit Arguments Pair [var t1 t2].
|
adamc@177
|
465 Implicit Arguments EInl [var t1 t2].
|
adamc@177
|
466 Implicit Arguments EInr [var t1 t2].
|
adamc@177
|
467 Implicit Arguments Case [var t1 t2].
|
adamc@177
|
468
|
adamc@177
|
469 Notation "# v" := (Var v) (at level 70) : source_scope.
|
adamc@177
|
470
|
adamc@177
|
471 Notation "()" := EUnit : source_scope.
|
adamc@177
|
472
|
adamc@177
|
473 Infix "@" := App (left associativity, at level 77) : source_scope.
|
adamc@177
|
474 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
|
adamc@177
|
475
|
adamc@177
|
476 Notation "[ x , y ]" := (Pair x y) (at level 72) : source_scope.
|
adamc@177
|
477
|
adamc@177
|
478 Notation "'Inl' e" := (EInl e) (at level 71) : source_scope.
|
adamc@177
|
479 Notation "'Inr' e" := (EInr e) (at level 71) : source_scope.
|
adamc@177
|
480
|
adamc@177
|
481 Bind Scope source_scope with exp.
|
adamc@177
|
482
|
adamc@177
|
483 Open Local Scope source_scope.
|
adamc@177
|
484
|
adamc@177
|
485 Fixpoint typeDenote (t : type) : Set :=
|
adamc@177
|
486 match t with
|
adamc@177
|
487 | Unit => unit
|
adamc@177
|
488 | t1 --> t2 => typeDenote t1 -> typeDenote t2
|
adamc@177
|
489 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
|
adamc@177
|
490 | t1 ++ t2 => (typeDenote t1 + typeDenote t2)%type
|
adamc@177
|
491 end.
|
adamc@177
|
492
|
adamc@177
|
493 Fixpoint patDenote t ts (p : pat t ts) {struct p} : typeDenote t -> option (hlist typeDenote ts) :=
|
adamc@177
|
494 match p in (pat t ts) return (typeDenote t -> option (hlist typeDenote ts)) with
|
adamc@177
|
495 | PVar _ => fun v => Some (v, tt)
|
adamc@177
|
496 | PPair _ _ _ _ p1 p2 => fun v =>
|
adamc@177
|
497 match patDenote p1 (fst v), patDenote p2 (snd v) with
|
adamc@177
|
498 | Some tup1, Some tup2 => Some (happ tup1 tup2)
|
adamc@177
|
499 | _, _ => None
|
adamc@177
|
500 end
|
adamc@177
|
501 | PInl _ _ _ p' => fun v =>
|
adamc@177
|
502 match v with
|
adamc@177
|
503 | inl v' => patDenote p' v'
|
adamc@177
|
504 | _ => None
|
adamc@177
|
505 end
|
adamc@177
|
506 | PInr _ _ _ p' => fun v =>
|
adamc@177
|
507 match v with
|
adamc@177
|
508 | inr v' => patDenote p' v'
|
adamc@177
|
509 | _ => None
|
adamc@177
|
510 end
|
adamc@177
|
511 end.
|
adamc@177
|
512
|
adamc@177
|
513 Section matchesDenote.
|
adamc@177
|
514 Variables t2 : type.
|
adamc@177
|
515 Variable default : typeDenote t2.
|
adamc@177
|
516
|
adamc@177
|
517 Fixpoint matchesDenote (tss : list (list type))
|
adamc@177
|
518 : (forall ts, member ts tss -> option (hlist typeDenote ts))
|
adamc@177
|
519 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
|
adamc@177
|
520 -> typeDenote t2 :=
|
adamc@177
|
521 match tss return (forall ts, member ts tss -> _)
|
adamc@177
|
522 -> (forall ts, member ts tss -> _)
|
adamc@177
|
523 -> _ with
|
adamc@177
|
524 | nil => fun _ _ =>
|
adamc@177
|
525 default
|
adamc@177
|
526 | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss') -> option (hlist typeDenote ts'))
|
adamc@177
|
527 (bodies : forall ts', member ts' (ts :: tss') -> hlist typeDenote ts' -> typeDenote t2) =>
|
adamc@177
|
528 match envs _ (hfirst (refl_equal _)) with
|
adamc@177
|
529 | None => matchesDenote tss'
|
adamc@177
|
530 (fun _ mem => envs _ (hnext mem))
|
adamc@177
|
531 (fun _ mem => bodies _ (hnext mem))
|
adamc@177
|
532 | Some env => (bodies _ (hfirst (refl_equal _))) env
|
adamc@177
|
533 end
|
adamc@177
|
534 end.
|
adamc@177
|
535 End matchesDenote.
|
adamc@177
|
536
|
adamc@177
|
537 Implicit Arguments matchesDenote [t2 tss].
|
adamc@177
|
538
|
adamc@177
|
539 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
|
adamc@177
|
540 match e in (exp _ t) return (typeDenote t) with
|
adamc@177
|
541 | Var _ v => v
|
adamc@177
|
542
|
adamc@177
|
543 | EUnit => tt
|
adamc@177
|
544
|
adamc@177
|
545 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
|
adamc@177
|
546 | Abs _ _ e' => fun x => expDenote (e' x)
|
adamc@177
|
547
|
adamc@177
|
548 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
|
adamc@177
|
549
|
adamc@177
|
550 | EInl _ _ e' => inl _ (expDenote e')
|
adamc@177
|
551 | EInr _ _ e' => inr _ (expDenote e')
|
adamc@177
|
552
|
adamc@177
|
553 | Case _ _ _ e ps es def =>
|
adamc@177
|
554 matchesDenote (expDenote def)
|
adamc@177
|
555 (fun _ mem => patDenote (ps _ mem) (expDenote e))
|
adamc@177
|
556 (fun _ mem env => expDenote (es _ mem env))
|
adamc@177
|
557 end.
|
adamc@177
|
558
|
adamc@177
|
559 Definition ExpDenote t (E : Exp t) := expDenote (E _).
|
adamc@177
|
560 End Source.
|
adamc@177
|
561
|
adamc@177
|
562 Import Source.
|
adamc@177
|
563
|
adamc@177
|
564 Section Elab.
|
adamc@177
|
565 Section vars.
|
adamc@177
|
566 Variable var : type -> Type.
|
adamc@177
|
567
|
adamc@177
|
568 Inductive exp : type -> Type :=
|
adamc@177
|
569 | Var : forall t,
|
adamc@177
|
570 var t
|
adamc@177
|
571 -> exp t
|
adamc@177
|
572
|
adamc@177
|
573 | EUnit : exp Unit
|
adamc@177
|
574
|
adamc@177
|
575 | App : forall t1 t2,
|
adamc@177
|
576 exp (t1 --> t2)
|
adamc@177
|
577 -> exp t1
|
adamc@177
|
578 -> exp t2
|
adamc@177
|
579 | Abs : forall t1 t2,
|
adamc@177
|
580 (var t1 -> exp t2)
|
adamc@177
|
581 -> exp (t1 --> t2)
|
adamc@177
|
582
|
adamc@177
|
583 | Pair : forall t1 t2,
|
adamc@177
|
584 exp t1
|
adamc@177
|
585 -> exp t2
|
adamc@177
|
586 -> exp (t1 ** t2)
|
adamc@177
|
587 | Fst : forall t1 t2,
|
adamc@177
|
588 exp (t1 ** t2)
|
adamc@177
|
589 -> exp t1
|
adamc@177
|
590 | Snd : forall t1 t2,
|
adamc@177
|
591 exp (t1 ** t2)
|
adamc@177
|
592 -> exp t2
|
adamc@177
|
593
|
adamc@177
|
594 | EInl : forall t1 t2,
|
adamc@177
|
595 exp t1
|
adamc@177
|
596 -> exp (t1 ++ t2)
|
adamc@177
|
597 | EInr : forall t1 t2,
|
adamc@177
|
598 exp t2
|
adamc@177
|
599 -> exp (t1 ++ t2)
|
adamc@177
|
600 | Case : forall t1 t2 t,
|
adamc@177
|
601 exp (t1 ++ t2)
|
adamc@177
|
602 -> (var t1 -> exp t)
|
adamc@177
|
603 -> (var t2 -> exp t)
|
adamc@177
|
604 -> exp t.
|
adamc@177
|
605 End vars.
|
adamc@177
|
606
|
adamc@177
|
607 Definition Exp t := forall var, exp var t.
|
adamc@177
|
608
|
adamc@177
|
609 Implicit Arguments Var [var t].
|
adamc@177
|
610 Implicit Arguments EUnit [var].
|
adamc@177
|
611 Implicit Arguments App [var t1 t2].
|
adamc@177
|
612 Implicit Arguments Abs [var t1 t2].
|
adamc@177
|
613 Implicit Arguments Pair [var t1 t2].
|
adamc@177
|
614 Implicit Arguments Fst [var t1 t2].
|
adamc@177
|
615 Implicit Arguments Snd [var t1 t2].
|
adamc@177
|
616 Implicit Arguments EInl [var t1 t2].
|
adamc@177
|
617 Implicit Arguments EInr [var t1 t2].
|
adamc@177
|
618 Implicit Arguments Case [var t1 t2 t].
|
adamc@177
|
619
|
adamc@177
|
620
|
adamc@177
|
621 Notation "# v" := (Var v) (at level 70) : elab_scope.
|
adamc@177
|
622
|
adamc@177
|
623 Notation "()" := EUnit : elab_scope.
|
adamc@177
|
624
|
adamc@177
|
625 Infix "@" := App (left associativity, at level 77) : elab_scope.
|
adamc@177
|
626 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : elab_scope.
|
adamc@177
|
627 Notation "\ ? , e" := (Abs (fun _ => e)) (at level 78) : elab_scope.
|
adamc@177
|
628
|
adamc@177
|
629 Notation "[ x , y ]" := (Pair x y) (at level 72) : elab_scope.
|
adamc@177
|
630 Notation "#1 e" := (Fst e) (at level 72) : elab_scope.
|
adamc@177
|
631 Notation "#2 e" := (Snd e) (at level 72) : elab_scope.
|
adamc@177
|
632
|
adamc@177
|
633 Notation "'Inl' e" := (EInl e) (at level 71) : elab_scope.
|
adamc@177
|
634 Notation "'Inr' e" := (EInr e) (at level 71) : elab_scope.
|
adamc@177
|
635
|
adamc@177
|
636 Bind Scope elab_scope with exp.
|
adamc@177
|
637 Delimit Scope elab_scope with elab.
|
adamc@177
|
638
|
adamc@177
|
639 Open Scope elab_scope.
|
adamc@177
|
640
|
adamc@177
|
641 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
|
adamc@177
|
642 match e in (exp _ t) return (typeDenote t) with
|
adamc@177
|
643 | Var _ v => v
|
adamc@177
|
644
|
adamc@177
|
645 | EUnit => tt
|
adamc@177
|
646
|
adamc@177
|
647 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
|
adamc@177
|
648 | Abs _ _ e' => fun x => expDenote (e' x)
|
adamc@177
|
649
|
adamc@177
|
650 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
|
adamc@177
|
651 | Fst _ _ e' => fst (expDenote e')
|
adamc@177
|
652 | Snd _ _ e' => snd (expDenote e')
|
adamc@177
|
653
|
adamc@177
|
654 | EInl _ _ e' => inl _ (expDenote e')
|
adamc@177
|
655 | EInr _ _ e' => inr _ (expDenote e')
|
adamc@177
|
656 | Case _ _ _ e' e1 e2 =>
|
adamc@177
|
657 match expDenote e' with
|
adamc@177
|
658 | inl v => expDenote (e1 v)
|
adamc@177
|
659 | inr v => expDenote (e2 v)
|
adamc@177
|
660 end
|
adamc@177
|
661 end.
|
adamc@177
|
662
|
adamc@177
|
663 Definition ExpDenote t (E : Exp t) := expDenote (E _).
|
adamc@177
|
664 End Elab.
|
adamc@177
|
665
|
adamc@177
|
666 End PatMatch.
|