Mercurial > cpdt > repo

comparison src/Interps.v @ 174:cd39a64d41ee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Templatize Interps
author Adam Chlipala <adamc@hcoop.net>
date Sun, 09 Nov 2008 15:23:33 -0500
parents 7fd470d8a788
children cbf2f74a5130
comparison
equal deleted inserted replaced
173:7fd470d8a788 174:cd39a64d41ee
74 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _. 74 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
75 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => 75 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
76 \f, \x, #f @ #x. 76 \f, \x, #f @ #x.
77 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _. 77 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
78 78
79 (* EX: Define an interpreter for [Exp]s. *)
80
81 (* begin thide *)
79 Fixpoint typeDenote (t : type) : Set := 82 Fixpoint typeDenote (t : type) : Set :=
80 match t with 83 match t with
81 | Nat => nat 84 | Nat => nat
82 | t1 --> t2 => typeDenote t1 -> typeDenote t2 85 | t1 --> t2 => typeDenote t1 -> typeDenote t2
83 end. 86 end.
92 | App _ _ e1 e2 => (expDenote e1) (expDenote e2) 95 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
93 | Abs _ _ e' => fun x => expDenote (e' x) 96 | Abs _ _ e' => fun x => expDenote (e' x)
94 end. 97 end.
95 98
96 Definition ExpDenote t (e : Exp t) := expDenote (e _). 99 Definition ExpDenote t (e : Exp t) := expDenote (e _).
100 (* end thide *)
97 101
98 Eval compute in ExpDenote zero. 102 Eval compute in ExpDenote zero.
99 Eval compute in ExpDenote one. 103 Eval compute in ExpDenote one.
100 Eval compute in ExpDenote zpo. 104 Eval compute in ExpDenote zpo.
101 Eval compute in ExpDenote ident. 105 Eval compute in ExpDenote ident.
102 Eval compute in ExpDenote app_ident. 106 Eval compute in ExpDenote app_ident.
103 Eval compute in ExpDenote app. 107 Eval compute in ExpDenote app.
104 Eval compute in ExpDenote app_ident'. 108 Eval compute in ExpDenote app_ident'.
105 109
110 (* EX: Define a constant-folding function for [Exp]s. *)
111
112 (* begin thide *)
106 Section cfold. 113 Section cfold.
107 Variable var : type -> Type. 114 Variable var : type -> Type.
108 115
109 Fixpoint cfold t (e : exp var t) {struct e} : exp var t := 116 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
110 match e in exp _ t return exp _ t with 117 match e in exp _ t return exp _ t with
123 | Abs _ _ e' => Abs (fun x => cfold (e' x)) 130 | Abs _ _ e' => Abs (fun x => cfold (e' x))
124 end. 131 end.
125 End cfold. 132 End cfold.
126 133
127 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _). 134 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
128 135 (* end thide *)
136
137 (* EX: Prove the correctness of constant-folding. *)
138
139 (* begin thide *)
129 Lemma cfold_correct : forall t (e : exp _ t), 140 Lemma cfold_correct : forall t (e : exp _ t),
130 expDenote (cfold e) = expDenote e. 141 expDenote (cfold e) = expDenote e.
131 induction e; crush; try (ext_eq; crush); 142 induction e; crush; try (ext_eq; crush);
132 repeat (match goal with 143 repeat (match goal with
133 | [ |- context[cfold ?E] ] => dep_destruct (cfold E) 144 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
136 147
137 Theorem Cfold_correct : forall t (E : Exp t), 148 Theorem Cfold_correct : forall t (E : Exp t),
138 ExpDenote (Cfold E) = ExpDenote E. 149 ExpDenote (Cfold E) = ExpDenote E.
139 unfold ExpDenote, Cfold; intros; apply cfold_correct. 150 unfold ExpDenote, Cfold; intros; apply cfold_correct.
140 Qed. 151 Qed.
152 (* end thide *)
141 End STLC. 153 End STLC.
142 154
143 155
144 (** * Adding Products and Sums *) 156 (** * Adding Products and Sums *)
145 157
146 Module PSLC. 158 Module PSLC.
159 (* EX: Extend the development with products and sums. *)
160
161 (* begin thide *)
147 Inductive type : Type := 162 Inductive type : Type :=
148 | Nat : type 163 | Nat : type
149 | Arrow : type -> type -> type 164 | Arrow : type -> type -> type
150 | Prod : type -> type -> type 165 | Prod : type -> type -> type
151 | Sum : type -> type -> type. 166 | Sum : type -> type -> type.
167 (* end thide *)
152 168
153 Infix "-->" := Arrow (right associativity, at level 62). 169 Infix "-->" := Arrow (right associativity, at level 62).
154 Infix "**" := Prod (right associativity, at level 61). 170 Infix "**" := Prod (right associativity, at level 61).
155 Infix "++" := Sum (right associativity, at level 60). 171 Infix "++" := Sum (right associativity, at level 60).
156 172
173 (* begin thide *)
157 Section vars. 174 Section vars.
158 Variable var : type -> Type. 175 Variable var : type -> Type.
159 176
160 Inductive exp : type -> Type := 177 Inductive exp : type -> Type :=
161 | Var : forall t, 178 | Var : forall t,
196 -> (var t2 -> exp t) 213 -> (var t2 -> exp t)
197 -> exp t. 214 -> exp t.
198 End vars. 215 End vars.
199 216
200 Definition Exp t := forall var, exp var t. 217 Definition Exp t := forall var, exp var t.
218 (* end thide *)
201 219
202 Implicit Arguments Var [var t]. 220 Implicit Arguments Var [var t].
203 Implicit Arguments Const [var]. 221 Implicit Arguments Const [var].
204 Implicit Arguments Abs [var t1 t2]. 222 Implicit Arguments Abs [var t1 t2].
205 Implicit Arguments Inl [var t1 t2]. 223 Implicit Arguments Inl [var t1 t2].
231 Definition ns1 : Exp (Nat ++ Nat) := fun _ => Inl (^3). 249 Definition ns1 : Exp (Nat ++ Nat) := fun _ => Inl (^3).
232 Definition ns2 : Exp (Nat ++ Nat) := fun _ => Inr (^5). 250 Definition ns2 : Exp (Nat ++ Nat) := fun _ => Inr (^5).
233 Definition natOut_ns1 : Exp Nat := fun _ => natOut _ @ ns1 _. 251 Definition natOut_ns1 : Exp Nat := fun _ => natOut _ @ ns1 _.
234 Definition natOut_ns2 : Exp Nat := fun _ => natOut _ @ ns2 _. 252 Definition natOut_ns2 : Exp Nat := fun _ => natOut _ @ ns2 _.
235 253
254 (* begin thide *)
236 Fixpoint typeDenote (t : type) : Set := 255 Fixpoint typeDenote (t : type) : Set :=
237 match t with 256 match t with
238 | Nat => nat 257 | Nat => nat
239 | t1 --> t2 => typeDenote t1 -> typeDenote t2 258 | t1 --> t2 => typeDenote t1 -> typeDenote t2
240 | t1 ** t2 => typeDenote t1 * typeDenote t2 259 | t1 ** t2 => typeDenote t1 * typeDenote t2
263 | inr v => expDenote (e2 v) 282 | inr v => expDenote (e2 v)
264 end 283 end
265 end. 284 end.
266 285
267 Definition ExpDenote t (e : Exp t) := expDenote (e _). 286 Definition ExpDenote t (e : Exp t) := expDenote (e _).
287 (* end thide *)
268 288
269 Eval compute in ExpDenote swap. 289 Eval compute in ExpDenote swap.
270 Eval compute in ExpDenote zo. 290 Eval compute in ExpDenote zo.
271 Eval compute in ExpDenote swap_zo. 291 Eval compute in ExpDenote swap_zo.
272 292
274 Eval compute in ExpDenote ns1. 294 Eval compute in ExpDenote ns1.
275 Eval compute in ExpDenote ns2. 295 Eval compute in ExpDenote ns2.
276 Eval compute in ExpDenote natOut_ns1. 296 Eval compute in ExpDenote natOut_ns1.
277 Eval compute in ExpDenote natOut_ns2. 297 Eval compute in ExpDenote natOut_ns2.
278 298
299 (* begin thide *)
279 Section cfold. 300 Section cfold.
280 Variable var : type -> Type. 301 Variable var : type -> Type.
281 302
282 Definition pairOutType t := 303 Definition pairOutType t :=
283 match t with 304 match t with
367 388
368 Theorem Cfold_correct : forall t (E : Exp t), 389 Theorem Cfold_correct : forall t (E : Exp t),
369 ExpDenote (Cfold E) = ExpDenote E. 390 ExpDenote (Cfold E) = ExpDenote E.
370 unfold ExpDenote, Cfold; intros; apply cfold_correct. 391 unfold ExpDenote, Cfold; intros; apply cfold_correct.
371 Qed. 392 Qed.
393 (* end thide *)
372 End PSLC. 394 End PSLC.
373 395
374 396
375 (** * Type Variables *) 397 (** * Type Variables *)
376 398
377 Module SysF. 399 Module SysF.
400 (* EX: Follow a similar progression for System F. *)
401
402 (* begin thide *)
378 Section vars. 403 Section vars.
379 Variable tvar : Type. 404 Variable tvar : Type.
380 405
381 Inductive type : Type := 406 Inductive type : Type :=
382 | Nat : type 407 | Nat : type
430 -> exp (All tf). 455 -> exp (All tf).
431 End vars. 456 End vars.
432 457
433 Definition Typ := forall tvar, type tvar. 458 Definition Typ := forall tvar, type tvar.
434 Definition Exp (T : Typ) := forall tvar (var : type tvar -> Type), exp var (T _). 459 Definition Exp (T : Typ) := forall tvar (var : type tvar -> Type), exp var (T _).
460 (* end thide *)
435 461
436 Implicit Arguments Nat [tvar]. 462 Implicit Arguments Nat [tvar].
437 463
438 Notation "## v" := (TVar v) (at level 40). 464 Notation "## v" := (TVar v) (at level 40).
439 Infix "-->" := Arrow (right associativity, at level 60). 465 Infix "-->" := Arrow (right associativity, at level 60).
475 Definition ident5 : Exp (fun _ => \\\T, ##T --> ##T). 501 Definition ident5 : Exp (fun _ => \\\T, ##T --> ##T).
476 do 2 intro; refine (ident_ident _ @@ _ @ ident_ident _ @@ _ @ ident _); 502 do 2 intro; refine (ident_ident _ @@ _ @ ident_ident _ @@ _ @ ident _);
477 repeat constructor. 503 repeat constructor.
478 Defined. 504 Defined.
479 505
506 (* begin thide *)
480 Fixpoint typeDenote (t : type Set) : Set := 507 Fixpoint typeDenote (t : type Set) : Set :=
481 match t with 508 match t with
482 | Nat => nat 509 | Nat => nat
483 | t1 --> t2 => typeDenote t1 -> typeDenote t2 510 | t1 --> t2 => typeDenote t1 -> typeDenote t2
484 | ##v => v 511 | ##v => v
506 end 533 end
507 | TAbs _ e' => fun T => expDenote (e' T) 534 | TAbs _ e' => fun T => expDenote (e' T)
508 end. 535 end.
509 536
510 Definition ExpDenote T (E : Exp T) := expDenote (E _ _). 537 Definition ExpDenote T (E : Exp T) := expDenote (E _ _).
538 (* end thide *)
511 539
512 Eval compute in ExpDenote zero. 540 Eval compute in ExpDenote zero.
513 Eval compute in ExpDenote ident. 541 Eval compute in ExpDenote ident.
514 Eval compute in ExpDenote ident_zero. 542 Eval compute in ExpDenote ident_zero.
515 Eval compute in ExpDenote ident_ident. 543 Eval compute in ExpDenote ident_ident.
516 Eval compute in ExpDenote ident5. 544 Eval compute in ExpDenote ident5.
517 545
546 (* begin thide *)
518 Section cfold. 547 Section cfold.
519 Variable tvar : Type. 548 Variable tvar : Type.
520 Variable var : type tvar -> Type. 549 Variable var : type tvar -> Type.
521 550
522 Fixpoint cfold t (e : exp var t) {struct e} : exp var t := 551 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
552 581
553 Theorem Cfold_correct : forall t (E : Exp t), 582 Theorem Cfold_correct : forall t (E : Exp t),
554 ExpDenote (Cfold E) = ExpDenote E. 583 ExpDenote (Cfold E) = ExpDenote E.
555 unfold ExpDenote, Cfold; intros; apply cfold_correct. 584 unfold ExpDenote, Cfold; intros; apply cfold_correct.
556 Qed. 585 Qed.
586 (* end thide *)
557 End SysF. 587 End SysF.