Mercurial > cpdt > repo

annotate src/Interps.v @ 173:7fd470d8a788

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
System F
author Adam Chlipala <adamc@hcoop.net>
date Sun, 09 Nov 2008 15:15:41 -0500
parents 653c03f6061e
children cd39a64d41ee
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@173 13 Require Import AxiomsImpred 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.
adamc@173 373
adamc@173 374
adamc@173 375 (** * Type Variables *)
adamc@173 376
adamc@173 377 Module SysF.
adamc@173 378 Section vars.
adamc@173 379 Variable tvar : Type.
adamc@173 380
adamc@173 381 Inductive type : Type :=
adamc@173 382 | Nat : type
adamc@173 383 | Arrow : type -> type -> type
adamc@173 384 | TVar : tvar -> type
adamc@173 385 | All : (tvar -> type) -> type.
adamc@173 386
adamc@173 387 Notation "## v" := (TVar v) (at level 40).
adamc@173 388 Infix "-->" := Arrow (right associativity, at level 60).
adamc@173 389
adamc@173 390 Section Subst.
adamc@173 391 Variable t : type.
adamc@173 392
adamc@173 393 Inductive Subst : (tvar -> type) -> type -> Prop :=
adamc@173 394 | SNat : Subst (fun _ => Nat) Nat
adamc@173 395 | SArrow : forall dom ran dom' ran',
adamc@173 396 Subst dom dom'
adamc@173 397 -> Subst ran ran'
adamc@173 398 -> Subst (fun v => dom v --> ran v) (dom' --> ran')
adamc@173 399 | SVarEq : Subst TVar t
adamc@173 400 | SVarNe : forall v, Subst (fun _ => ##v) (##v)
adamc@173 401 | SAll : forall ran ran',
adamc@173 402 (forall v', Subst (fun v => ran v v') (ran' v'))
adamc@173 403 -> Subst (fun v => All (ran v)) (All ran').
adamc@173 404 End Subst.
adamc@173 405
adamc@173 406 Variable var : type -> Type.
adamc@173 407
adamc@173 408 Inductive exp : type -> Type :=
adamc@173 409 | Var : forall t,
adamc@173 410 var t
adamc@173 411 -> exp t
adamc@173 412
adamc@173 413 | Const : nat -> exp Nat
adamc@173 414 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@173 415
adamc@173 416 | App : forall t1 t2,
adamc@173 417 exp (t1 --> t2)
adamc@173 418 -> exp t1
adamc@173 419 -> exp t2
adamc@173 420 | Abs : forall t1 t2,
adamc@173 421 (var t1 -> exp t2)
adamc@173 422 -> exp (t1 --> t2)
adamc@173 423
adamc@173 424 | TApp : forall tf,
adamc@173 425 exp (All tf)
adamc@173 426 -> forall t tf', Subst t tf tf'
adamc@173 427 -> exp tf'
adamc@173 428 | TAbs : forall tf,
adamc@173 429 (forall v, exp (tf v))
adamc@173 430 -> exp (All tf).
adamc@173 431 End vars.
adamc@173 432
adamc@173 433 Definition Typ := forall tvar, type tvar.
adamc@173 434 Definition Exp (T : Typ) := forall tvar (var : type tvar -> Type), exp var (T _).
adamc@173 435
adamc@173 436 Implicit Arguments Nat [tvar].
adamc@173 437
adamc@173 438 Notation "## v" := (TVar v) (at level 40).
adamc@173 439 Infix "-->" := Arrow (right associativity, at level 60).
adamc@173 440 Notation "\\\ x , t" := (All (fun x => t)) (at level 65).
adamc@173 441
adamc@173 442 Implicit Arguments Var [tvar var t].
adamc@173 443 Implicit Arguments Const [tvar var].
adamc@173 444 Implicit Arguments Plus [tvar var].
adamc@173 445 Implicit Arguments App [tvar var t1 t2].
adamc@173 446 Implicit Arguments Abs [tvar var t1 t2].
adamc@173 447
adamc@173 448 Implicit Arguments TAbs [tvar var tf].
adamc@173 449
adamc@173 450 Notation "# v" := (Var v) (at level 70).
adamc@173 451
adamc@173 452 Notation "^ n" := (Const n) (at level 70).
adamc@173 453 Infix "+^" := Plus (left associativity, at level 79).
adamc@173 454
adamc@173 455 Infix "@" := App (left associativity, at level 77).
adamc@173 456 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@173 457 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@173 458
adamc@173 459 Notation "e @@ t" := (TApp e (t := t) _) (left associativity, at level 77).
adamc@173 460 Notation "\\ x , e" := (TAbs (fun x => e)) (at level 78).
adamc@173 461 Notation "\\ ! , e" := (TAbs (fun _ => e)) (at level 78).
adamc@173 462
adamc@173 463 Definition zero : Exp (fun _ => Nat) := fun _ _ =>
adamc@173 464 ^0.
adamc@173 465 Definition ident : Exp (fun _ => \\\T, ##T --> ##T) := fun _ _ =>
adamc@173 466 \\T, \x, #x.
adamc@173 467 Definition ident_zero : Exp (fun _ => Nat).
adamc@173 468 do 2 intro; refine (ident _ @@ _ @ zero _);
adamc@173 469 repeat constructor.
adamc@173 470 Defined.
adamc@173 471 Definition ident_ident : Exp (fun _ => \\\T, ##T --> ##T).
adamc@173 472 do 2 intro; refine (ident _ @@ _ @ ident _);
adamc@173 473 repeat constructor.
adamc@173 474 Defined.
adamc@173 475 Definition ident5 : Exp (fun _ => \\\T, ##T --> ##T).
adamc@173 476 do 2 intro; refine (ident_ident _ @@ _ @ ident_ident _ @@ _ @ ident _);
adamc@173 477 repeat constructor.
adamc@173 478 Defined.
adamc@173 479
adamc@173 480 Fixpoint typeDenote (t : type Set) : Set :=
adamc@173 481 match t with
adamc@173 482 | Nat => nat
adamc@173 483 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@173 484 | ##v => v
adamc@173 485 | All tf => forall T, typeDenote (tf T)
adamc@173 486 end.
adamc@173 487
adamc@173 488 Lemma Subst_typeDenote : forall t tf tf',
adamc@173 489 Subst t tf tf'
adamc@173 490 -> typeDenote (tf (typeDenote t)) = typeDenote tf'.
adamc@173 491 induction 1; crush; ext_eq; crush.
adamc@173 492 Defined.
adamc@173 493
adamc@173 494 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@173 495 match e in (exp _ t) return (typeDenote t) with
adamc@173 496 | Var _ v => v
adamc@173 497
adamc@173 498 | Const n => n
adamc@173 499 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@173 500
adamc@173 501 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@173 502 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@173 503
adamc@173 504 | TApp _ e' t' _ pf => match Subst_typeDenote pf in _ = T return T with
adamc@173 505 | refl_equal => (expDenote e') (typeDenote t')
adamc@173 506 end
adamc@173 507 | TAbs _ e' => fun T => expDenote (e' T)
adamc@173 508 end.
adamc@173 509
adamc@173 510 Definition ExpDenote T (E : Exp T) := expDenote (E _ _).
adamc@173 511
adamc@173 512 Eval compute in ExpDenote zero.
adamc@173 513 Eval compute in ExpDenote ident.
adamc@173 514 Eval compute in ExpDenote ident_zero.
adamc@173 515 Eval compute in ExpDenote ident_ident.
adamc@173 516 Eval compute in ExpDenote ident5.
adamc@173 517
adamc@173 518 Section cfold.
adamc@173 519 Variable tvar : Type.
adamc@173 520 Variable var : type tvar -> Type.
adamc@173 521
adamc@173 522 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
adamc@173 523 match e in exp _ t return exp _ t with
adamc@173 524 | Var _ v => #v
adamc@173 525
adamc@173 526 | Const n => ^n
adamc@173 527 | Plus e1 e2 =>
adamc@173 528 let e1' := cfold e1 in
adamc@173 529 let e2' := cfold e2 in
adamc@173 530 match e1', e2' with
adamc@173 531 | Const n1, Const n2 => ^(n1 + n2)
adamc@173 532 | _, _ => e1' +^ e2'
adamc@173 533 end
adamc@173 534
adamc@173 535 | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@173 536 | Abs _ _ e' => Abs (fun x => cfold (e' x))
adamc@173 537
adamc@173 538 | TApp _ e' _ _ pf => TApp (cfold e') pf
adamc@173 539 | TAbs _ e' => \\T, cfold (e' T)
adamc@173 540 end.
adamc@173 541 End cfold.
adamc@173 542
adamc@173 543 Definition Cfold T (E : Exp T) : Exp T := fun _ _ => cfold (E _ _).
adamc@173 544
adamc@173 545 Lemma cfold_correct : forall t (e : exp _ t),
adamc@173 546 expDenote (cfold e) = expDenote e.
adamc@173 547 induction e; crush; try (ext_eq; crush);
adamc@173 548 repeat (match goal with
adamc@173 549 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@173 550 end; crush).
adamc@173 551 Qed.
adamc@173 552
adamc@173 553 Theorem Cfold_correct : forall t (E : Exp t),
adamc@173 554 ExpDenote (Cfold E) = ExpDenote E.
adamc@173 555 unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@173 556 Qed.
adamc@173 557 End SysF.