Mercurial > cpdt > repo

annotate src/Interps.v @ 224:4b73ea13574d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port Extensional
author Adam Chlipala <adamc@hcoop.net>
date Mon, 16 Nov 2009 12:30:38 -0500
parents 2a34c4dc6a10
children 05250878e4ca
rev   line source
adamc@223 1 (* Copyright (c) 2008-2009, 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@223 88 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@223 89 match e 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@223 116 Fixpoint cfold t (e : exp var t) : exp var t :=
adamc@223 117 match e 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@223 263 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@223 264 match e 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@223 315 Definition pairOut t1 t2 (e : exp var (t1 ** t2))
adamc@223 316 : option (exp var t1 * exp var t2) :=
adamc@172 317 match e in exp _ t return pairOutType t with
adamc@172 318 | Pair _ _ e1 e2 => Some (e1, e2)
adamc@172 319 | _ => pairOutDefault _
adamc@172 320 end.
adamc@172 321
adamc@223 322 Fixpoint cfold t (e : exp var t) : exp var t :=
adamc@223 323 match e with
adamc@171 324 | Var _ v => #v
adamc@171 325
adamc@171 326 | Const n => ^n
adamc@171 327 | Plus e1 e2 =>
adamc@171 328 let e1' := cfold e1 in
adamc@171 329 let e2' := cfold e2 in
adamc@204 330 match e1', e2' return _ with
adamc@171 331 | Const n1, Const n2 => ^(n1 + n2)
adamc@171 332 | _, _ => e1' +^ e2'
adamc@171 333 end
adamc@171 334
adamc@171 335 | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@171 336 | Abs _ _ e' => Abs (fun x => cfold (e' x))
adamc@171 337
adamc@171 338 | Pair _ _ e1 e2 => [cfold e1, cfold e2]
adamc@172 339 | Fst t1 _ e' =>
adamc@172 340 let e'' := cfold e' in
adamc@172 341 match pairOut e'' with
adamc@172 342 | None => #1 e''
adamc@172 343 | Some (e1, _) => e1
adamc@172 344 end
adamc@172 345 | Snd _ _ e' =>
adamc@172 346 let e'' := cfold e' in
adamc@172 347 match pairOut e'' with
adamc@172 348 | None => #2 e''
adamc@172 349 | Some (_, e2) => e2
adamc@172 350 end
adamc@171 351
adamc@171 352 | Inl _ _ e' => Inl (cfold e')
adamc@171 353 | Inr _ _ e' => Inr (cfold e')
adamc@171 354 | SumCase _ _ _ e' e1 e2 =>
adamc@171 355 case cfold e' of
adamc@171 356 x => cfold (e1 x)
adamc@171 357 | y => cfold (e2 y)
adamc@171 358 end.
adamc@171 359 End cfold.
adamc@171 360
adamc@171 361 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@171 362
adamc@172 363 Section pairs.
adamc@172 364 Variables A B : Type.
adamc@172 365
adamc@172 366 Variable v1 : A.
adamc@172 367 Variable v2 : B.
adamc@172 368 Variable v : A * B.
adamc@172 369
adamc@172 370 Theorem pair_eta1 : (v1, v2) = v -> v1 = fst v.
adamc@172 371 destruct v; crush.
adamc@172 372 Qed.
adamc@172 373
adamc@172 374 Theorem pair_eta2 : (v1, v2) = v -> v2 = snd v.
adamc@172 375 destruct v; crush.
adamc@172 376 Qed.
adamc@172 377 End pairs.
adamc@172 378
adamc@172 379 Hint Resolve pair_eta1 pair_eta2.
adamc@172 380
adamc@171 381 Lemma cfold_correct : forall t (e : exp _ t),
adamc@171 382 expDenote (cfold e) = expDenote e.
adamc@171 383 induction e; crush; try (ext_eq; crush);
adamc@171 384 repeat (match goal with
adamc@171 385 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@171 386 | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E
adamc@172 387 end; crush); eauto.
adamc@171 388 Qed.
adamc@171 389
adamc@171 390 Theorem Cfold_correct : forall t (E : Exp t),
adamc@171 391 ExpDenote (Cfold E) = ExpDenote E.
adamc@171 392 unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@171 393 Qed.
adamc@174 394 (* end thide *)
adamc@171 395 End PSLC.