Mercurial > cpdt > repo

annotate src/Interps.v @ 172:653c03f6061e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Examples; pair optimization
author Adam Chlipala <adamc@hcoop.net>
date Sun, 09 Nov 2008 14:24:31 -0500
parents b00b6a9b6b58
children 7fd470d8a788
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@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.