Mercurial > cpdt > repo

annotate src/Interps.v @ 214:768889c969e9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish porting MoreDep
author Adam Chlipala <adamc@hcoop.net>
date Wed, 11 Nov 2009 12:21:28 -0500
parents cbf2f74a5130
children 2a34c4dc6a10
rev   line source
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@204 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@174 79 (* EX: Define an interpreter for [Exp]s. *)
adamc@174 80
adamc@174 81 (* begin thide *)
adamc@170 82 Fixpoint typeDenote (t : type) : Set :=
adamc@170 83 match t with
adamc@170 84 | Nat => nat
adamc@170 85 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@170 86 end.
adamc@170 87
adamc@170 88 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@170 89 match e in (exp _ t) return (typeDenote t) with
adamc@170 90 | Var _ v => v
adamc@170 91
adamc@170 92 | Const n => n
adamc@170 93 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@170 94
adamc@170 95 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@170 96 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@170 97 end.
adamc@170 98
adamc@170 99 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@174 100 (* end thide *)
adamc@170 101
adamc@172 102 Eval compute in ExpDenote zero.
adamc@172 103 Eval compute in ExpDenote one.
adamc@172 104 Eval compute in ExpDenote zpo.
adamc@172 105 Eval compute in ExpDenote ident.
adamc@172 106 Eval compute in ExpDenote app_ident.
adamc@172 107 Eval compute in ExpDenote app.
adamc@172 108 Eval compute in ExpDenote app_ident'.
adamc@172 109
adamc@174 110 (* EX: Define a constant-folding function for [Exp]s. *)
adamc@174 111
adamc@174 112 (* begin thide *)
adamc@170 113 Section cfold.
adamc@170 114 Variable var : type -> Type.
adamc@170 115
adamc@170 116 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
adamc@170 117 match e in exp _ t return exp _ t with
adamc@170 118 | Var _ v => #v
adamc@170 119
adamc@170 120 | Const n => ^n
adamc@170 121 | Plus e1 e2 =>
adamc@170 122 let e1' := cfold e1 in
adamc@170 123 let e2' := cfold e2 in
adamc@204 124 match e1', e2' return _ with
adamc@170 125 | Const n1, Const n2 => ^(n1 + n2)
adamc@171 126 | _, _ => e1' +^ e2'
adamc@170 127 end
adamc@170 128
adamc@170 129 | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@170 130 | Abs _ _ e' => Abs (fun x => cfold (e' x))
adamc@170 131 end.
adamc@170 132 End cfold.
adamc@170 133
adamc@170 134 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@174 135 (* end thide *)
adamc@170 136
adamc@174 137 (* EX: Prove the correctness of constant-folding. *)
adamc@174 138
adamc@174 139 (* begin thide *)
adamc@170 140 Lemma cfold_correct : forall t (e : exp _ t),
adamc@170 141 expDenote (cfold e) = expDenote e.
adamc@170 142 induction e; crush; try (ext_eq; crush);
adamc@170 143 repeat (match goal with
adamc@170 144 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@170 145 end; crush).
adamc@170 146 Qed.
adamc@170 147
adamc@170 148 Theorem Cfold_correct : forall t (E : Exp t),
adamc@170 149 ExpDenote (Cfold E) = ExpDenote E.
adamc@170 150 unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@170 151 Qed.
adamc@174 152 (* end thide *)
adamc@170 153 End STLC.
adamc@171 154
adamc@171 155
adamc@171 156 (** * Adding Products and Sums *)
adamc@171 157
adamc@171 158 Module PSLC.
adamc@174 159 (* EX: Extend the development with products and sums. *)
adamc@174 160
adamc@174 161 (* begin thide *)
adamc@171 162 Inductive type : Type :=
adamc@171 163 | Nat : type
adamc@171 164 | Arrow : type -> type -> type
adamc@171 165 | Prod : type -> type -> type
adamc@171 166 | Sum : type -> type -> type.
adamc@174 167 (* end thide *)
adamc@171 168
adamc@171 169 Infix "-->" := Arrow (right associativity, at level 62).
adamc@171 170 Infix "**" := Prod (right associativity, at level 61).
adamc@171 171 Infix "++" := Sum (right associativity, at level 60).
adamc@171 172
adamc@174 173 (* begin thide *)
adamc@171 174 Section vars.
adamc@171 175 Variable var : type -> Type.
adamc@171 176
adamc@171 177 Inductive exp : type -> Type :=
adamc@171 178 | Var : forall t,
adamc@171 179 var t
adamc@171 180 -> exp t
adamc@171 181
adamc@171 182 | Const : nat -> exp Nat
adamc@171 183 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@171 184
adamc@171 185 | App : forall t1 t2,
adamc@171 186 exp (t1 --> t2)
adamc@171 187 -> exp t1
adamc@171 188 -> exp t2
adamc@171 189 | Abs : forall t1 t2,
adamc@171 190 (var t1 -> exp t2)
adamc@171 191 -> exp (t1 --> t2)
adamc@171 192
adamc@171 193 | Pair : forall t1 t2,
adamc@171 194 exp t1
adamc@171 195 -> exp t2
adamc@171 196 -> exp (t1 ** t2)
adamc@171 197 | Fst : forall t1 t2,
adamc@171 198 exp (t1 ** t2)
adamc@171 199 -> exp t1
adamc@171 200 | Snd : forall t1 t2,
adamc@171 201 exp (t1 ** t2)
adamc@171 202 -> exp t2
adamc@171 203
adamc@171 204 | Inl : forall t1 t2,
adamc@171 205 exp t1
adamc@171 206 -> exp (t1 ++ t2)
adamc@171 207 | Inr : forall t1 t2,
adamc@171 208 exp t2
adamc@171 209 -> exp (t1 ++ t2)
adamc@171 210 | SumCase : forall t1 t2 t,
adamc@171 211 exp (t1 ++ t2)
adamc@171 212 -> (var t1 -> exp t)
adamc@171 213 -> (var t2 -> exp t)
adamc@171 214 -> exp t.
adamc@171 215 End vars.
adamc@171 216
adamc@171 217 Definition Exp t := forall var, exp var t.
adamc@174 218 (* end thide *)
adamc@171 219
adamc@171 220 Implicit Arguments Var [var t].
adamc@171 221 Implicit Arguments Const [var].
adamc@171 222 Implicit Arguments Abs [var t1 t2].
adamc@171 223 Implicit Arguments Inl [var t1 t2].
adamc@171 224 Implicit Arguments Inr [var t1 t2].
adamc@171 225
adamc@171 226 Notation "# v" := (Var v) (at level 70).
adamc@171 227
adamc@171 228 Notation "^ n" := (Const n) (at level 70).
adamc@172 229 Infix "+^" := Plus (left associativity, at level 78).
adamc@171 230
adamc@171 231 Infix "@" := App (left associativity, at level 77).
adamc@171 232 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@171 233 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@171 234
adamc@171 235 Notation "[ e1 , e2 ]" := (Pair e1 e2).
adamc@171 236 Notation "#1 e" := (Fst e) (at level 75).
adamc@171 237 Notation "#2 e" := (Snd e) (at level 75).
adamc@171 238
adamc@171 239 Notation "'case' e 'of' x => e1 | y => e2" := (SumCase e (fun x => e1) (fun y => e2))
adamc@171 240 (at level 79).
adamc@171 241
adamc@172 242 Definition swap : Exp (Nat ** Nat --> Nat ** Nat) := fun _ =>
adamc@172 243 \p, [#2 #p, #1 #p].
adamc@172 244 Definition zo : Exp (Nat ** Nat) := fun _ => [^0, ^1].
adamc@172 245 Definition swap_zo : Exp (Nat ** Nat) := fun _ => swap _ @ zo _.
adamc@172 246
adamc@172 247 Definition natOut : Exp (Nat ++ Nat --> Nat) := fun _ =>
adamc@172 248 \s, case #s of x => #x | y => #y +^ #y.
adamc@172 249 Definition ns1 : Exp (Nat ++ Nat) := fun _ => Inl (^3).
adamc@172 250 Definition ns2 : Exp (Nat ++ Nat) := fun _ => Inr (^5).
adamc@172 251 Definition natOut_ns1 : Exp Nat := fun _ => natOut _ @ ns1 _.
adamc@172 252 Definition natOut_ns2 : Exp Nat := fun _ => natOut _ @ ns2 _.
adamc@172 253
adamc@174 254 (* begin thide *)
adamc@171 255 Fixpoint typeDenote (t : type) : Set :=
adamc@171 256 match t with
adamc@171 257 | Nat => nat
adamc@171 258 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@171 259 | t1 ** t2 => typeDenote t1 * typeDenote t2
adamc@171 260 | t1 ++ t2 => typeDenote t1 + typeDenote t2
adamc@171 261 end%type.
adamc@171 262
adamc@171 263 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@171 264 match e in (exp _ t) return (typeDenote t) with
adamc@171 265 | Var _ v => v
adamc@171 266
adamc@171 267 | Const n => n
adamc@171 268 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@171 269
adamc@171 270 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@171 271 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@171 272
adamc@171 273 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@171 274 | Fst _ _ e' => fst (expDenote e')
adamc@171 275 | Snd _ _ e' => snd (expDenote e')
adamc@171 276
adamc@171 277 | Inl _ _ e' => inl _ (expDenote e')
adamc@171 278 | Inr _ _ e' => inr _ (expDenote e')
adamc@171 279 | SumCase _ _ _ e' e1 e2 =>
adamc@171 280 match expDenote e' with
adamc@171 281 | inl v => expDenote (e1 v)
adamc@171 282 | inr v => expDenote (e2 v)
adamc@171 283 end
adamc@171 284 end.
adamc@171 285
adamc@171 286 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@174 287 (* end thide *)
adamc@171 288
adamc@172 289 Eval compute in ExpDenote swap.
adamc@172 290 Eval compute in ExpDenote zo.
adamc@172 291 Eval compute in ExpDenote swap_zo.
adamc@172 292
adamc@172 293 Eval compute in ExpDenote natOut.
adamc@172 294 Eval compute in ExpDenote ns1.
adamc@172 295 Eval compute in ExpDenote ns2.
adamc@172 296 Eval compute in ExpDenote natOut_ns1.
adamc@172 297 Eval compute in ExpDenote natOut_ns2.
adamc@172 298
adamc@174 299 (* begin thide *)
adamc@171 300 Section cfold.
adamc@171 301 Variable var : type -> Type.
adamc@171 302
adamc@172 303 Definition pairOutType t :=
adamc@204 304 match t return Type with
adamc@172 305 | t1 ** t2 => option (exp var t1 * exp var t2)
adamc@172 306 | _ => unit
adamc@172 307 end.
adamc@172 308
adamc@172 309 Definition pairOutDefault (t : type) : pairOutType t :=
adamc@172 310 match t return pairOutType t with
adamc@172 311 | _ ** _ => None
adamc@172 312 | _ => tt
adamc@172 313 end.
adamc@172 314
adamc@172 315 Definition pairOut t1 t2 (e : exp var (t1 ** t2)) : option (exp var t1 * exp var t2) :=
adamc@172 316 match e in exp _ t return pairOutType t with
adamc@172 317 | Pair _ _ e1 e2 => Some (e1, e2)
adamc@172 318 | _ => pairOutDefault _
adamc@172 319 end.
adamc@172 320
adamc@171 321 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
adamc@171 322 match e in exp _ t return exp _ t with
adamc@171 323 | Var _ v => #v
adamc@171 324
adamc@171 325 | Const n => ^n
adamc@171 326 | Plus e1 e2 =>
adamc@171 327 let e1' := cfold e1 in
adamc@171 328 let e2' := cfold e2 in
adamc@204 329 match e1', e2' return _ with
adamc@171 330 | Const n1, Const n2 => ^(n1 + n2)
adamc@171 331 | _, _ => e1' +^ e2'
adamc@171 332 end
adamc@171 333
adamc@171 334 | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@171 335 | Abs _ _ e' => Abs (fun x => cfold (e' x))
adamc@171 336
adamc@171 337 | Pair _ _ e1 e2 => [cfold e1, cfold e2]
adamc@172 338 | Fst t1 _ e' =>
adamc@172 339 let e'' := cfold e' in
adamc@172 340 match pairOut e'' with
adamc@172 341 | None => #1 e''
adamc@172 342 | Some (e1, _) => e1
adamc@172 343 end
adamc@172 344 | Snd _ _ e' =>
adamc@172 345 let e'' := cfold e' in
adamc@172 346 match pairOut e'' with
adamc@172 347 | None => #2 e''
adamc@172 348 | Some (_, e2) => e2
adamc@172 349 end
adamc@171 350
adamc@171 351 | Inl _ _ e' => Inl (cfold e')
adamc@171 352 | Inr _ _ e' => Inr (cfold e')
adamc@171 353 | SumCase _ _ _ e' e1 e2 =>
adamc@171 354 case cfold e' of
adamc@171 355 x => cfold (e1 x)
adamc@171 356 | y => cfold (e2 y)
adamc@171 357 end.
adamc@171 358 End cfold.
adamc@171 359
adamc@171 360 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@171 361
adamc@172 362 Section pairs.
adamc@172 363 Variables A B : Type.
adamc@172 364
adamc@172 365 Variable v1 : A.
adamc@172 366 Variable v2 : B.
adamc@172 367 Variable v : A * B.
adamc@172 368
adamc@172 369 Theorem pair_eta1 : (v1, v2) = v -> v1 = fst v.
adamc@172 370 destruct v; crush.
adamc@172 371 Qed.
adamc@172 372
adamc@172 373 Theorem pair_eta2 : (v1, v2) = v -> v2 = snd v.
adamc@172 374 destruct v; crush.
adamc@172 375 Qed.
adamc@172 376 End pairs.
adamc@172 377
adamc@172 378 Hint Resolve pair_eta1 pair_eta2.
adamc@172 379
adamc@171 380 Lemma cfold_correct : forall t (e : exp _ t),
adamc@171 381 expDenote (cfold e) = expDenote e.
adamc@171 382 induction e; crush; try (ext_eq; crush);
adamc@171 383 repeat (match goal with
adamc@171 384 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@171 385 | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E
adamc@172 386 end; crush); eauto.
adamc@171 387 Qed.
adamc@171 388
adamc@171 389 Theorem Cfold_correct : forall t (E : Exp t),
adamc@171 390 ExpDenote (Cfold E) = ExpDenote E.
adamc@171 391 unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@171 392 Qed.
adamc@174 393 (* end thide *)
adamc@171 394 End PSLC.