adamc@170
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@170
|
2 *
|
adamc@170
|
3 * This work is licensed under a
|
adamc@170
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
adamc@170
|
5 * Unported License.
|
adamc@170
|
6 * The license text is available at:
|
adamc@170
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
adamc@170
|
8 *)
|
adamc@170
|
9
|
adamc@170
|
10 (* begin hide *)
|
adamc@170
|
11 Require Import String List.
|
adamc@170
|
12
|
adamc@170
|
13 Require Import Axioms Tactics.
|
adamc@170
|
14
|
adamc@170
|
15 Set Implicit Arguments.
|
adamc@170
|
16 (* end hide *)
|
adamc@170
|
17
|
adamc@170
|
18
|
adamc@170
|
19 (** %\chapter{Type-Theoretic Interpreters}% *)
|
adamc@170
|
20
|
adamc@170
|
21 (** TODO: Prose for this chapter *)
|
adamc@170
|
22
|
adamc@170
|
23
|
adamc@170
|
24 (** * Simply-Typed Lambda Calculus *)
|
adamc@170
|
25
|
adamc@170
|
26 Module STLC.
|
adamc@170
|
27 Inductive type : Type :=
|
adamc@170
|
28 | Nat : type
|
adamc@170
|
29 | Arrow : type -> type -> type.
|
adamc@170
|
30
|
adamc@170
|
31 Infix "-->" := Arrow (right associativity, at level 60).
|
adamc@170
|
32
|
adamc@170
|
33 Section vars.
|
adamc@170
|
34 Variable var : type -> Type.
|
adamc@170
|
35
|
adamc@170
|
36 Inductive exp : type -> Type :=
|
adamc@170
|
37 | Var : forall t,
|
adamc@170
|
38 var t
|
adamc@170
|
39 -> exp t
|
adamc@170
|
40
|
adamc@170
|
41 | Const : nat -> exp Nat
|
adamc@170
|
42 | Plus : exp Nat -> exp Nat -> exp Nat
|
adamc@170
|
43
|
adamc@170
|
44 | App : forall t1 t2,
|
adamc@170
|
45 exp (t1 --> t2)
|
adamc@170
|
46 -> exp t1
|
adamc@170
|
47 -> exp t2
|
adamc@170
|
48 | Abs : forall t1 t2,
|
adamc@170
|
49 (var t1 -> exp t2)
|
adamc@170
|
50 -> exp (t1 --> t2).
|
adamc@170
|
51 End vars.
|
adamc@170
|
52
|
adamc@170
|
53 Definition Exp t := forall var, exp var t.
|
adamc@170
|
54
|
adamc@170
|
55 Implicit Arguments Var [var t].
|
adamc@170
|
56 Implicit Arguments Const [var].
|
adamc@170
|
57 Implicit Arguments Plus [var].
|
adamc@170
|
58 Implicit Arguments App [var t1 t2].
|
adamc@170
|
59 Implicit Arguments Abs [var t1 t2].
|
adamc@170
|
60
|
adamc@170
|
61 Notation "# v" := (Var v) (at level 70).
|
adamc@170
|
62
|
adamc@170
|
63 Notation "^ n" := (Const n) (at level 70).
|
adamc@171
|
64 Infix "+^" := Plus (left associativity, at level 79).
|
adamc@170
|
65
|
adamc@170
|
66 Infix "@" := App (left associativity, at level 77).
|
adamc@170
|
67 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
|
adamc@170
|
68 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
|
adamc@170
|
69
|
adamc@172
|
70 Definition zero : Exp Nat := fun _ => ^0.
|
adamc@172
|
71 Definition one : Exp Nat := fun _ => ^1.
|
adamc@172
|
72 Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
|
adamc@172
|
73 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
|
adamc@172
|
74 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
|
adamc@172
|
75 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
|
adamc@172
|
76 \f, \x, #f @ #x.
|
adamc@172
|
77 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
|
adamc@172
|
78
|
adamc@170
|
79 Fixpoint typeDenote (t : type) : Set :=
|
adamc@170
|
80 match t with
|
adamc@170
|
81 | Nat => nat
|
adamc@170
|
82 | t1 --> t2 => typeDenote t1 -> typeDenote t2
|
adamc@170
|
83 end.
|
adamc@170
|
84
|
adamc@170
|
85 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
|
adamc@170
|
86 match e in (exp _ t) return (typeDenote t) with
|
adamc@170
|
87 | Var _ v => v
|
adamc@170
|
88
|
adamc@170
|
89 | Const n => n
|
adamc@170
|
90 | Plus e1 e2 => expDenote e1 + expDenote e2
|
adamc@170
|
91
|
adamc@170
|
92 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
|
adamc@170
|
93 | Abs _ _ e' => fun x => expDenote (e' x)
|
adamc@170
|
94 end.
|
adamc@170
|
95
|
adamc@170
|
96 Definition ExpDenote t (e : Exp t) := expDenote (e _).
|
adamc@170
|
97
|
adamc@172
|
98 Eval compute in ExpDenote zero.
|
adamc@172
|
99 Eval compute in ExpDenote one.
|
adamc@172
|
100 Eval compute in ExpDenote zpo.
|
adamc@172
|
101 Eval compute in ExpDenote ident.
|
adamc@172
|
102 Eval compute in ExpDenote app_ident.
|
adamc@172
|
103 Eval compute in ExpDenote app.
|
adamc@172
|
104 Eval compute in ExpDenote app_ident'.
|
adamc@172
|
105
|
adamc@170
|
106 Section cfold.
|
adamc@170
|
107 Variable var : type -> Type.
|
adamc@170
|
108
|
adamc@170
|
109 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
|
adamc@170
|
110 match e in exp _ t return exp _ t with
|
adamc@170
|
111 | Var _ v => #v
|
adamc@170
|
112
|
adamc@170
|
113 | Const n => ^n
|
adamc@170
|
114 | Plus e1 e2 =>
|
adamc@170
|
115 let e1' := cfold e1 in
|
adamc@170
|
116 let e2' := cfold e2 in
|
adamc@170
|
117 match e1', e2' with
|
adamc@170
|
118 | Const n1, Const n2 => ^(n1 + n2)
|
adamc@171
|
119 | _, _ => e1' +^ e2'
|
adamc@170
|
120 end
|
adamc@170
|
121
|
adamc@170
|
122 | App _ _ e1 e2 => cfold e1 @ cfold e2
|
adamc@170
|
123 | Abs _ _ e' => Abs (fun x => cfold (e' x))
|
adamc@170
|
124 end.
|
adamc@170
|
125 End cfold.
|
adamc@170
|
126
|
adamc@170
|
127 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
|
adamc@170
|
128
|
adamc@170
|
129 Lemma cfold_correct : forall t (e : exp _ t),
|
adamc@170
|
130 expDenote (cfold e) = expDenote e.
|
adamc@170
|
131 induction e; crush; try (ext_eq; crush);
|
adamc@170
|
132 repeat (match goal with
|
adamc@170
|
133 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
|
adamc@170
|
134 end; crush).
|
adamc@170
|
135 Qed.
|
adamc@170
|
136
|
adamc@170
|
137 Theorem Cfold_correct : forall t (E : Exp t),
|
adamc@170
|
138 ExpDenote (Cfold E) = ExpDenote E.
|
adamc@170
|
139 unfold ExpDenote, Cfold; intros; apply cfold_correct.
|
adamc@170
|
140 Qed.
|
adamc@170
|
141 End STLC.
|
adamc@171
|
142
|
adamc@171
|
143
|
adamc@171
|
144 (** * Adding Products and Sums *)
|
adamc@171
|
145
|
adamc@171
|
146 Module PSLC.
|
adamc@171
|
147 Inductive type : Type :=
|
adamc@171
|
148 | Nat : type
|
adamc@171
|
149 | Arrow : type -> type -> type
|
adamc@171
|
150 | Prod : type -> type -> type
|
adamc@171
|
151 | Sum : type -> type -> type.
|
adamc@171
|
152
|
adamc@171
|
153 Infix "-->" := Arrow (right associativity, at level 62).
|
adamc@171
|
154 Infix "**" := Prod (right associativity, at level 61).
|
adamc@171
|
155 Infix "++" := Sum (right associativity, at level 60).
|
adamc@171
|
156
|
adamc@171
|
157 Section vars.
|
adamc@171
|
158 Variable var : type -> Type.
|
adamc@171
|
159
|
adamc@171
|
160 Inductive exp : type -> Type :=
|
adamc@171
|
161 | Var : forall t,
|
adamc@171
|
162 var t
|
adamc@171
|
163 -> exp t
|
adamc@171
|
164
|
adamc@171
|
165 | Const : nat -> exp Nat
|
adamc@171
|
166 | Plus : exp Nat -> exp Nat -> exp Nat
|
adamc@171
|
167
|
adamc@171
|
168 | App : forall t1 t2,
|
adamc@171
|
169 exp (t1 --> t2)
|
adamc@171
|
170 -> exp t1
|
adamc@171
|
171 -> exp t2
|
adamc@171
|
172 | Abs : forall t1 t2,
|
adamc@171
|
173 (var t1 -> exp t2)
|
adamc@171
|
174 -> exp (t1 --> t2)
|
adamc@171
|
175
|
adamc@171
|
176 | Pair : forall t1 t2,
|
adamc@171
|
177 exp t1
|
adamc@171
|
178 -> exp t2
|
adamc@171
|
179 -> exp (t1 ** t2)
|
adamc@171
|
180 | Fst : forall t1 t2,
|
adamc@171
|
181 exp (t1 ** t2)
|
adamc@171
|
182 -> exp t1
|
adamc@171
|
183 | Snd : forall t1 t2,
|
adamc@171
|
184 exp (t1 ** t2)
|
adamc@171
|
185 -> exp t2
|
adamc@171
|
186
|
adamc@171
|
187 | Inl : forall t1 t2,
|
adamc@171
|
188 exp t1
|
adamc@171
|
189 -> exp (t1 ++ t2)
|
adamc@171
|
190 | Inr : forall t1 t2,
|
adamc@171
|
191 exp t2
|
adamc@171
|
192 -> exp (t1 ++ t2)
|
adamc@171
|
193 | SumCase : forall t1 t2 t,
|
adamc@171
|
194 exp (t1 ++ t2)
|
adamc@171
|
195 -> (var t1 -> exp t)
|
adamc@171
|
196 -> (var t2 -> exp t)
|
adamc@171
|
197 -> exp t.
|
adamc@171
|
198 End vars.
|
adamc@171
|
199
|
adamc@171
|
200 Definition Exp t := forall var, exp var t.
|
adamc@171
|
201
|
adamc@171
|
202 Implicit Arguments Var [var t].
|
adamc@171
|
203 Implicit Arguments Const [var].
|
adamc@171
|
204 Implicit Arguments Abs [var t1 t2].
|
adamc@171
|
205 Implicit Arguments Inl [var t1 t2].
|
adamc@171
|
206 Implicit Arguments Inr [var t1 t2].
|
adamc@171
|
207
|
adamc@171
|
208 Notation "# v" := (Var v) (at level 70).
|
adamc@171
|
209
|
adamc@171
|
210 Notation "^ n" := (Const n) (at level 70).
|
adamc@172
|
211 Infix "+^" := Plus (left associativity, at level 78).
|
adamc@171
|
212
|
adamc@171
|
213 Infix "@" := App (left associativity, at level 77).
|
adamc@171
|
214 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
|
adamc@171
|
215 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
|
adamc@171
|
216
|
adamc@171
|
217 Notation "[ e1 , e2 ]" := (Pair e1 e2).
|
adamc@171
|
218 Notation "#1 e" := (Fst e) (at level 75).
|
adamc@171
|
219 Notation "#2 e" := (Snd e) (at level 75).
|
adamc@171
|
220
|
adamc@171
|
221 Notation "'case' e 'of' x => e1 | y => e2" := (SumCase e (fun x => e1) (fun y => e2))
|
adamc@171
|
222 (at level 79).
|
adamc@171
|
223
|
adamc@172
|
224 Definition swap : Exp (Nat ** Nat --> Nat ** Nat) := fun _ =>
|
adamc@172
|
225 \p, [#2 #p, #1 #p].
|
adamc@172
|
226 Definition zo : Exp (Nat ** Nat) := fun _ => [^0, ^1].
|
adamc@172
|
227 Definition swap_zo : Exp (Nat ** Nat) := fun _ => swap _ @ zo _.
|
adamc@172
|
228
|
adamc@172
|
229 Definition natOut : Exp (Nat ++ Nat --> Nat) := fun _ =>
|
adamc@172
|
230 \s, case #s of x => #x | y => #y +^ #y.
|
adamc@172
|
231 Definition ns1 : Exp (Nat ++ Nat) := fun _ => Inl (^3).
|
adamc@172
|
232 Definition ns2 : Exp (Nat ++ Nat) := fun _ => Inr (^5).
|
adamc@172
|
233 Definition natOut_ns1 : Exp Nat := fun _ => natOut _ @ ns1 _.
|
adamc@172
|
234 Definition natOut_ns2 : Exp Nat := fun _ => natOut _ @ ns2 _.
|
adamc@172
|
235
|
adamc@171
|
236 Fixpoint typeDenote (t : type) : Set :=
|
adamc@171
|
237 match t with
|
adamc@171
|
238 | Nat => nat
|
adamc@171
|
239 | t1 --> t2 => typeDenote t1 -> typeDenote t2
|
adamc@171
|
240 | t1 ** t2 => typeDenote t1 * typeDenote t2
|
adamc@171
|
241 | t1 ++ t2 => typeDenote t1 + typeDenote t2
|
adamc@171
|
242 end%type.
|
adamc@171
|
243
|
adamc@171
|
244 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
|
adamc@171
|
245 match e in (exp _ t) return (typeDenote t) with
|
adamc@171
|
246 | Var _ v => v
|
adamc@171
|
247
|
adamc@171
|
248 | Const n => n
|
adamc@171
|
249 | Plus e1 e2 => expDenote e1 + expDenote e2
|
adamc@171
|
250
|
adamc@171
|
251 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
|
adamc@171
|
252 | Abs _ _ e' => fun x => expDenote (e' x)
|
adamc@171
|
253
|
adamc@171
|
254 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
|
adamc@171
|
255 | Fst _ _ e' => fst (expDenote e')
|
adamc@171
|
256 | Snd _ _ e' => snd (expDenote e')
|
adamc@171
|
257
|
adamc@171
|
258 | Inl _ _ e' => inl _ (expDenote e')
|
adamc@171
|
259 | Inr _ _ e' => inr _ (expDenote e')
|
adamc@171
|
260 | SumCase _ _ _ e' e1 e2 =>
|
adamc@171
|
261 match expDenote e' with
|
adamc@171
|
262 | inl v => expDenote (e1 v)
|
adamc@171
|
263 | inr v => expDenote (e2 v)
|
adamc@171
|
264 end
|
adamc@171
|
265 end.
|
adamc@171
|
266
|
adamc@171
|
267 Definition ExpDenote t (e : Exp t) := expDenote (e _).
|
adamc@171
|
268
|
adamc@172
|
269 Eval compute in ExpDenote swap.
|
adamc@172
|
270 Eval compute in ExpDenote zo.
|
adamc@172
|
271 Eval compute in ExpDenote swap_zo.
|
adamc@172
|
272
|
adamc@172
|
273 Eval compute in ExpDenote natOut.
|
adamc@172
|
274 Eval compute in ExpDenote ns1.
|
adamc@172
|
275 Eval compute in ExpDenote ns2.
|
adamc@172
|
276 Eval compute in ExpDenote natOut_ns1.
|
adamc@172
|
277 Eval compute in ExpDenote natOut_ns2.
|
adamc@172
|
278
|
adamc@171
|
279 Section cfold.
|
adamc@171
|
280 Variable var : type -> Type.
|
adamc@171
|
281
|
adamc@172
|
282 Definition pairOutType t :=
|
adamc@172
|
283 match t with
|
adamc@172
|
284 | t1 ** t2 => option (exp var t1 * exp var t2)
|
adamc@172
|
285 | _ => unit
|
adamc@172
|
286 end.
|
adamc@172
|
287
|
adamc@172
|
288 Definition pairOutDefault (t : type) : pairOutType t :=
|
adamc@172
|
289 match t return pairOutType t with
|
adamc@172
|
290 | _ ** _ => None
|
adamc@172
|
291 | _ => tt
|
adamc@172
|
292 end.
|
adamc@172
|
293
|
adamc@172
|
294 Definition pairOut t1 t2 (e : exp var (t1 ** t2)) : option (exp var t1 * exp var t2) :=
|
adamc@172
|
295 match e in exp _ t return pairOutType t with
|
adamc@172
|
296 | Pair _ _ e1 e2 => Some (e1, e2)
|
adamc@172
|
297 | _ => pairOutDefault _
|
adamc@172
|
298 end.
|
adamc@172
|
299
|
adamc@171
|
300 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
|
adamc@171
|
301 match e in exp _ t return exp _ t with
|
adamc@171
|
302 | Var _ v => #v
|
adamc@171
|
303
|
adamc@171
|
304 | Const n => ^n
|
adamc@171
|
305 | Plus e1 e2 =>
|
adamc@171
|
306 let e1' := cfold e1 in
|
adamc@171
|
307 let e2' := cfold e2 in
|
adamc@171
|
308 match e1', e2' with
|
adamc@171
|
309 | Const n1, Const n2 => ^(n1 + n2)
|
adamc@171
|
310 | _, _ => e1' +^ e2'
|
adamc@171
|
311 end
|
adamc@171
|
312
|
adamc@171
|
313 | App _ _ e1 e2 => cfold e1 @ cfold e2
|
adamc@171
|
314 | Abs _ _ e' => Abs (fun x => cfold (e' x))
|
adamc@171
|
315
|
adamc@171
|
316 | Pair _ _ e1 e2 => [cfold e1, cfold e2]
|
adamc@172
|
317 | Fst t1 _ e' =>
|
adamc@172
|
318 let e'' := cfold e' in
|
adamc@172
|
319 match pairOut e'' with
|
adamc@172
|
320 | None => #1 e''
|
adamc@172
|
321 | Some (e1, _) => e1
|
adamc@172
|
322 end
|
adamc@172
|
323 | Snd _ _ e' =>
|
adamc@172
|
324 let e'' := cfold e' in
|
adamc@172
|
325 match pairOut e'' with
|
adamc@172
|
326 | None => #2 e''
|
adamc@172
|
327 | Some (_, e2) => e2
|
adamc@172
|
328 end
|
adamc@171
|
329
|
adamc@171
|
330 | Inl _ _ e' => Inl (cfold e')
|
adamc@171
|
331 | Inr _ _ e' => Inr (cfold e')
|
adamc@171
|
332 | SumCase _ _ _ e' e1 e2 =>
|
adamc@171
|
333 case cfold e' of
|
adamc@171
|
334 x => cfold (e1 x)
|
adamc@171
|
335 | y => cfold (e2 y)
|
adamc@171
|
336 end.
|
adamc@171
|
337 End cfold.
|
adamc@171
|
338
|
adamc@171
|
339 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
|
adamc@171
|
340
|
adamc@172
|
341 Section pairs.
|
adamc@172
|
342 Variables A B : Type.
|
adamc@172
|
343
|
adamc@172
|
344 Variable v1 : A.
|
adamc@172
|
345 Variable v2 : B.
|
adamc@172
|
346 Variable v : A * B.
|
adamc@172
|
347
|
adamc@172
|
348 Theorem pair_eta1 : (v1, v2) = v -> v1 = fst v.
|
adamc@172
|
349 destruct v; crush.
|
adamc@172
|
350 Qed.
|
adamc@172
|
351
|
adamc@172
|
352 Theorem pair_eta2 : (v1, v2) = v -> v2 = snd v.
|
adamc@172
|
353 destruct v; crush.
|
adamc@172
|
354 Qed.
|
adamc@172
|
355 End pairs.
|
adamc@172
|
356
|
adamc@172
|
357 Hint Resolve pair_eta1 pair_eta2.
|
adamc@172
|
358
|
adamc@171
|
359 Lemma cfold_correct : forall t (e : exp _ t),
|
adamc@171
|
360 expDenote (cfold e) = expDenote e.
|
adamc@171
|
361 induction e; crush; try (ext_eq; crush);
|
adamc@171
|
362 repeat (match goal with
|
adamc@171
|
363 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
|
adamc@171
|
364 | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E
|
adamc@172
|
365 end; crush); eauto.
|
adamc@171
|
366 Qed.
|
adamc@171
|
367
|
adamc@171
|
368 Theorem Cfold_correct : forall t (E : Exp t),
|
adamc@171
|
369 ExpDenote (Cfold E) = ExpDenote E.
|
adamc@171
|
370 unfold ExpDenote, Cfold; intros; apply cfold_correct.
|
adamc@171
|
371 Qed.
|
adamc@171
|
372 End PSLC.
|