annotate src/Extensional.v @ 224:4b73ea13574d

Port Extensional
author Adam Chlipala <adamc@hcoop.net>
date Mon, 16 Nov 2009 12:30:38 -0500
parents 54e8ecb5ec88
children 19902d0b6622
rev   line source
adamc@216 1 (* Copyright (c) 2008-2009, Adam Chlipala
adamc@175 2 *
adamc@175 3 * This work is licensed under a
adamc@175 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@175 5 * Unported License.
adamc@175 6 * The license text is available at:
adamc@175 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@175 8 *)
adamc@175 9
adamc@175 10 (* begin hide *)
adamc@175 11 Require Import String List.
adamc@175 12
adamc@182 13 Require Import Axioms Tactics DepList.
adamc@175 14
adamc@175 15 Set Implicit Arguments.
adamc@175 16 (* end hide *)
adamc@175 17
adamc@175 18
adamc@181 19 (** %\chapter{Extensional Transformations}% *)
adamc@175 20
adamc@175 21 (** TODO: Prose for this chapter *)
adamc@175 22
adamc@175 23
adamc@175 24 (** * Simply-Typed Lambda Calculus *)
adamc@175 25
adamc@175 26 Module STLC.
adamc@175 27 Module Source.
adamc@175 28 Inductive type : Type :=
adamc@175 29 | TNat : type
adamc@175 30 | Arrow : type -> type -> type.
adamc@175 31
adamc@175 32 Notation "'Nat'" := TNat : source_scope.
adamc@175 33 Infix "-->" := Arrow (right associativity, at level 60) : source_scope.
adamc@175 34
adamc@175 35 Open Scope source_scope.
adamc@175 36 Bind Scope source_scope with type.
adamc@175 37 Delimit Scope source_scope with source.
adamc@175 38
adamc@175 39 Section vars.
adamc@175 40 Variable var : type -> Type.
adamc@175 41
adamc@175 42 Inductive exp : type -> Type :=
adamc@175 43 | Var : forall t,
adamc@175 44 var t
adamc@175 45 -> exp t
adamc@175 46
adamc@175 47 | Const : nat -> exp Nat
adamc@175 48 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@175 49
adamc@175 50 | App : forall t1 t2,
adamc@175 51 exp (t1 --> t2)
adamc@175 52 -> exp t1
adamc@175 53 -> exp t2
adamc@175 54 | Abs : forall t1 t2,
adamc@175 55 (var t1 -> exp t2)
adamc@175 56 -> exp (t1 --> t2).
adamc@175 57 End vars.
adamc@175 58
adamc@175 59 Definition Exp t := forall var, exp var t.
adamc@175 60
adamc@175 61 Implicit Arguments Var [var t].
adamc@175 62 Implicit Arguments Const [var].
adamc@175 63 Implicit Arguments Plus [var].
adamc@175 64 Implicit Arguments App [var t1 t2].
adamc@175 65 Implicit Arguments Abs [var t1 t2].
adamc@175 66
adamc@175 67 Notation "# v" := (Var v) (at level 70) : source_scope.
adamc@175 68
adamc@175 69 Notation "^ n" := (Const n) (at level 70) : source_scope.
adamc@175 70 Infix "+^" := Plus (left associativity, at level 79) : source_scope.
adamc@175 71
adamc@175 72 Infix "@" := App (left associativity, at level 77) : source_scope.
adamc@175 73 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
adamc@175 74 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope.
adamc@175 75
adamc@175 76 Bind Scope source_scope with exp.
adamc@175 77
adamc@175 78 Definition zero : Exp Nat := fun _ => ^0.
adamc@175 79 Definition one : Exp Nat := fun _ => ^1.
adamc@175 80 Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
adamc@175 81 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
adamc@175 82 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
adamc@175 83 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
adamc@175 84 \f, \x, #f @ #x.
adamc@175 85 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
adamc@175 86
adamc@175 87 Fixpoint typeDenote (t : type) : Set :=
adamc@175 88 match t with
adamc@175 89 | Nat => nat
adamc@175 90 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@175 91 end.
adamc@175 92
adamc@224 93 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@224 94 match e with
adamc@175 95 | Var _ v => v
adamc@175 96
adamc@175 97 | Const n => n
adamc@175 98 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@175 99
adamc@175 100 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@175 101 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@175 102 end.
adamc@175 103
adamc@175 104 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@176 105
adamc@180 106 (* begin thide *)
adamc@176 107 Section exp_equiv.
adamc@176 108 Variables var1 var2 : type -> Type.
adamc@176 109
adamc@224 110 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type
adamc@224 111 -> forall t, exp var1 t -> exp var2 t -> Prop :=
adamc@181 112 | EqVar : forall G t (v1 : var1 t) v2,
adamc@176 113 In (existT _ t (v1, v2)) G
adamc@176 114 -> exp_equiv G (#v1) (#v2)
adamc@176 115
adamc@181 116 | EqConst : forall G n,
adamc@176 117 exp_equiv G (^n) (^n)
adamc@181 118 | EqPlus : forall G x1 y1 x2 y2,
adamc@176 119 exp_equiv G x1 x2
adamc@176 120 -> exp_equiv G y1 y2
adamc@176 121 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
adamc@176 122
adamc@181 123 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
adamc@176 124 exp_equiv G f1 f2
adamc@176 125 -> exp_equiv G x1 x2
adamc@176 126 -> exp_equiv G (f1 @ x1) (f2 @ x2)
adamc@181 127 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
adamc@176 128 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
adamc@176 129 -> exp_equiv G (Abs f1) (Abs f2).
adamc@176 130 End exp_equiv.
adamc@176 131
adamc@176 132 Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
adamc@176 133 exp_equiv nil (E var1) (E var2).
adamc@180 134 (* end thide *)
adamc@175 135 End Source.
adamc@175 136
adamc@175 137 Module CPS.
adamc@175 138 Inductive type : Type :=
adamc@175 139 | TNat : type
adamc@175 140 | Cont : type -> type
adamc@175 141 | TUnit : type
adamc@175 142 | Prod : type -> type -> type.
adamc@175 143
adamc@175 144 Notation "'Nat'" := TNat : cps_scope.
adamc@175 145 Notation "'Unit'" := TUnit : cps_scope.
adamc@175 146 Notation "t --->" := (Cont t) (at level 61) : cps_scope.
adamc@175 147 Infix "**" := Prod (right associativity, at level 60) : cps_scope.
adamc@175 148
adamc@175 149 Bind Scope cps_scope with type.
adamc@175 150 Delimit Scope cps_scope with cps.
adamc@175 151
adamc@175 152 Section vars.
adamc@175 153 Variable var : type -> Type.
adamc@175 154
adamc@175 155 Inductive prog : Type :=
adamc@175 156 | PHalt :
adamc@175 157 var Nat
adamc@175 158 -> prog
adamc@175 159 | App : forall t,
adamc@175 160 var (t --->)
adamc@175 161 -> var t
adamc@175 162 -> prog
adamc@175 163 | Bind : forall t,
adamc@175 164 primop t
adamc@175 165 -> (var t -> prog)
adamc@175 166 -> prog
adamc@175 167
adamc@175 168 with primop : type -> Type :=
adamc@175 169 | Var : forall t,
adamc@175 170 var t
adamc@175 171 -> primop t
adamc@175 172
adamc@175 173 | Const : nat -> primop Nat
adamc@175 174 | Plus : var Nat -> var Nat -> primop Nat
adamc@175 175
adamc@175 176 | Abs : forall t,
adamc@175 177 (var t -> prog)
adamc@175 178 -> primop (t --->)
adamc@175 179
adamc@175 180 | Pair : forall t1 t2,
adamc@175 181 var t1
adamc@175 182 -> var t2
adamc@175 183 -> primop (t1 ** t2)
adamc@175 184 | Fst : forall t1 t2,
adamc@175 185 var (t1 ** t2)
adamc@175 186 -> primop t1
adamc@175 187 | Snd : forall t1 t2,
adamc@175 188 var (t1 ** t2)
adamc@175 189 -> primop t2.
adamc@175 190 End vars.
adamc@175 191
adamc@175 192 Implicit Arguments PHalt [var].
adamc@175 193 Implicit Arguments App [var t].
adamc@175 194
adamc@175 195 Implicit Arguments Var [var t].
adamc@175 196 Implicit Arguments Const [var].
adamc@175 197 Implicit Arguments Plus [var].
adamc@175 198 Implicit Arguments Abs [var t].
adamc@175 199 Implicit Arguments Pair [var t1 t2].
adamc@175 200 Implicit Arguments Fst [var t1 t2].
adamc@175 201 Implicit Arguments Snd [var t1 t2].
adamc@175 202
adamc@175 203 Notation "'Halt' x" := (PHalt x) (no associativity, at level 75) : cps_scope.
adamc@175 204 Infix "@@" := App (no associativity, at level 75) : cps_scope.
adamc@175 205 Notation "x <- p ; e" := (Bind p (fun x => e))
adamc@175 206 (right associativity, at level 76, p at next level) : cps_scope.
adamc@175 207 Notation "! <- p ; e" := (Bind p (fun _ => e))
adamc@175 208 (right associativity, at level 76, p at next level) : cps_scope.
adamc@175 209
adamc@175 210 Notation "# v" := (Var v) (at level 70) : cps_scope.
adamc@175 211
adamc@175 212 Notation "^ n" := (Const n) (at level 70) : cps_scope.
adamc@175 213 Infix "+^" := Plus (left associativity, at level 79) : cps_scope.
adamc@175 214
adamc@175 215 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : cps_scope.
adamc@175 216 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : cps_scope.
adamc@175 217
adamc@179 218 Notation "[ x1 , x2 ]" := (Pair x1 x2) : cps_scope.
adamc@175 219 Notation "#1 x" := (Fst x) (at level 72) : cps_scope.
adamc@175 220 Notation "#2 x" := (Snd x) (at level 72) : cps_scope.
adamc@175 221
adamc@175 222 Bind Scope cps_scope with prog primop.
adamc@175 223
adamc@175 224 Open Scope cps_scope.
adamc@175 225
adamc@175 226 Fixpoint typeDenote (t : type) : Set :=
adamc@175 227 match t with
adamc@175 228 | Nat => nat
adamc@175 229 | t' ---> => typeDenote t' -> nat
adamc@175 230 | Unit => unit
adamc@175 231 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
adamc@175 232 end.
adamc@175 233
adamc@175 234 Fixpoint progDenote (e : prog typeDenote) : nat :=
adamc@175 235 match e with
adamc@175 236 | PHalt n => n
adamc@175 237 | App _ f x => f x
adamc@175 238 | Bind _ p x => progDenote (x (primopDenote p))
adamc@175 239 end
adamc@175 240
adamc@224 241 with primopDenote t (p : primop typeDenote t) : typeDenote t :=
adamc@224 242 match p with
adamc@175 243 | Var _ v => v
adamc@175 244
adamc@175 245 | Const n => n
adamc@175 246 | Plus n1 n2 => n1 + n2
adamc@175 247
adamc@175 248 | Abs _ e => fun x => progDenote (e x)
adamc@175 249
adamc@175 250 | Pair _ _ v1 v2 => (v1, v2)
adamc@175 251 | Fst _ _ v => fst v
adamc@175 252 | Snd _ _ v => snd v
adamc@175 253 end.
adamc@175 254
adamc@175 255 Definition Prog := forall var, prog var.
adamc@175 256 Definition Primop t := forall var, primop var t.
adamc@175 257 Definition ProgDenote (E : Prog) := progDenote (E _).
adamc@175 258 Definition PrimopDenote t (P : Primop t) := primopDenote (P _).
adamc@175 259 End CPS.
adamc@175 260
adamc@175 261 Import Source CPS.
adamc@175 262
adamc@180 263 (* begin thide *)
adamc@175 264 Fixpoint cpsType (t : Source.type) : CPS.type :=
adamc@175 265 match t with
adamc@175 266 | Nat => Nat%cps
adamc@175 267 | t1 --> t2 => (cpsType t1 ** (cpsType t2 --->) --->)%cps
adamc@175 268 end%source.
adamc@175 269
adamc@175 270 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
adamc@175 271
adamc@175 272 Section cpsExp.
adamc@175 273 Variable var : CPS.type -> Type.
adamc@175 274
adamc@175 275 Import Source.
adamc@175 276 Open Scope cps_scope.
adamc@175 277
adamc@224 278 Fixpoint cpsExp t (e : exp (fun t => var (cpsType t)) t)
adamc@175 279 : (var (cpsType t) -> prog var) -> prog var :=
adamc@224 280 match e with
adamc@175 281 | Var _ v => fun k => k v
adamc@175 282
adamc@175 283 | Const n => fun k =>
adamc@175 284 x <- ^n;
adamc@175 285 k x
adamc@175 286 | Plus e1 e2 => fun k =>
adamc@175 287 x1 <-- e1;
adamc@175 288 x2 <-- e2;
adamc@175 289 x <- x1 +^ x2;
adamc@175 290 k x
adamc@175 291
adamc@175 292 | App _ _ e1 e2 => fun k =>
adamc@175 293 f <-- e1;
adamc@175 294 x <-- e2;
adamc@175 295 kf <- \r, k r;
adamc@175 296 p <- [x, kf];
adamc@175 297 f @@ p
adamc@175 298 | Abs _ _ e' => fun k =>
adamc@175 299 f <- CPS.Abs (var := var) (fun p =>
adamc@175 300 x <- #1 p;
adamc@175 301 kf <- #2 p;
adamc@175 302 r <-- e' x;
adamc@175 303 kf @@ r);
adamc@175 304 k f
adamc@175 305 end
adamc@175 306
adamc@175 307 where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@175 308 End cpsExp.
adamc@175 309
adamc@175 310 Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)) : cps_scope.
adamc@175 311 Notation "! <-- e1 ; e2" := (cpsExp e1 (fun _ => e2))
adamc@175 312 (right associativity, at level 76, e1 at next level) : cps_scope.
adamc@175 313
adamc@175 314 Implicit Arguments cpsExp [var t].
adamc@175 315 Definition CpsExp (E : Exp Nat) : Prog :=
adamc@175 316 fun var => cpsExp (E _) (PHalt (var := _)).
adamc@180 317 (* end thide *)
adamc@175 318
adamc@175 319 Eval compute in CpsExp zero.
adamc@175 320 Eval compute in CpsExp one.
adamc@175 321 Eval compute in CpsExp zpo.
adamc@175 322 Eval compute in CpsExp app_ident.
adamc@175 323 Eval compute in CpsExp app_ident'.
adamc@175 324
adamc@175 325 Eval compute in ProgDenote (CpsExp zero).
adamc@175 326 Eval compute in ProgDenote (CpsExp one).
adamc@175 327 Eval compute in ProgDenote (CpsExp zpo).
adamc@175 328 Eval compute in ProgDenote (CpsExp app_ident).
adamc@175 329 Eval compute in ProgDenote (CpsExp app_ident').
adamc@175 330
adamc@180 331 (* begin thide *)
adamc@176 332 Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop :=
adamc@224 333 match t with
adamc@176 334 | Nat => fun n1 n2 => n1 = n2
adamc@176 335 | t1 --> t2 => fun f1 f2 =>
adamc@176 336 forall x1 x2, lr _ x1 x2
adamc@176 337 -> forall k, exists r,
adamc@176 338 f2 (x2, k) = k r
adamc@176 339 /\ lr _ (f1 x1) r
adamc@176 340 end%source.
adamc@176 341
adamc@176 342 Lemma cpsExp_correct : forall G t (e1 : exp _ t) (e2 : exp _ t),
adamc@176 343 exp_equiv G e1 e2
adamc@176 344 -> (forall t v1 v2, In (existT _ t (v1, v2)) G -> lr t v1 v2)
adamc@176 345 -> forall k, exists r,
adamc@176 346 progDenote (cpsExp e2 k) = progDenote (k r)
adamc@176 347 /\ lr t (expDenote e1) r.
adamc@176 348 induction 1; crush; fold typeDenote in *;
adamc@176 349 repeat (match goal with
adamc@176 350 | [ H : forall k, exists r, progDenote (cpsExp ?E k) = _ /\ _
adamc@176 351 |- context[cpsExp ?E ?K] ] =>
adamc@176 352 generalize (H K); clear H
adamc@176 353 | [ |- exists r, progDenote (_ ?R) = progDenote (_ r) /\ _ ] =>
adamc@176 354 exists R
adamc@176 355 | [ t1 : Source.type |- _ ] =>
adamc@176 356 match goal with
adamc@176 357 | [ Hlr : lr t1 ?X1 ?X2, IH : forall v1 v2, _ |- _ ] =>
adamc@176 358 generalize (IH X1 X2); clear IH; intro IH;
adamc@176 359 match type of IH with
adamc@176 360 | ?P -> _ => assert P
adamc@176 361 end
adamc@176 362 end
adamc@176 363 end; crush); eauto.
adamc@176 364 Qed.
adamc@176 365
adamc@176 366 Lemma vars_easy : forall (t : Source.type) (v1 : Source.typeDenote t)
adamc@176 367 (v2 : typeDenote (cpsType t)),
adamc@176 368 In
adamc@176 369 (existT
adamc@176 370 (fun t0 : Source.type =>
adamc@176 371 (Source.typeDenote t0 * typeDenote (cpsType t0))%type) t
adamc@176 372 (v1, v2)) nil -> lr t v1 v2.
adamc@176 373 crush.
adamc@176 374 Qed.
adamc@176 375
adamc@176 376 Theorem CpsExp_correct : forall (E : Exp Nat),
adamc@176 377 ProgDenote (CpsExp E) = ExpDenote E.
adamc@176 378 unfold ProgDenote, CpsExp, ExpDenote; intros;
adamc@176 379 generalize (cpsExp_correct (e1 := E _) (e2 := E _)
adamc@176 380 (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush.
adamc@176 381 Qed.
adamc@180 382 (* end thide *)
adamc@176 383
adamc@175 384 End STLC.
adamc@177 385
adamc@177 386
adamc@177 387 (** * A Pattern Compiler *)
adamc@177 388
adamc@177 389 Module PatMatch.
adamc@177 390 Module Source.
adamc@177 391 Inductive type : Type :=
adamc@177 392 | Unit : type
adamc@177 393 | Arrow : type -> type -> type
adamc@177 394 | Prod : type -> type -> type
adamc@177 395 | Sum : type -> type -> type.
adamc@177 396
adamc@177 397 Infix "-->" := Arrow (right associativity, at level 61).
adamc@177 398 Infix "++" := Sum (right associativity, at level 60).
adamc@177 399 Infix "**" := Prod (right associativity, at level 59).
adamc@177 400
adamc@177 401 Inductive pat : type -> list type -> Type :=
adamc@177 402 | PVar : forall t,
adamc@177 403 pat t (t :: nil)
adamc@177 404 | PPair : forall t1 t2 ts1 ts2,
adamc@177 405 pat t1 ts1
adamc@177 406 -> pat t2 ts2
adamc@177 407 -> pat (t1 ** t2) (ts1 ++ ts2)
adamc@177 408 | PInl : forall t1 t2 ts,
adamc@177 409 pat t1 ts
adamc@177 410 -> pat (t1 ++ t2) ts
adamc@177 411 | PInr : forall t1 t2 ts,
adamc@177 412 pat t2 ts
adamc@177 413 -> pat (t1 ++ t2) ts.
adamc@177 414
adamc@177 415 Implicit Arguments PVar [t].
adamc@177 416 Implicit Arguments PInl [t1 t2 ts].
adamc@177 417 Implicit Arguments PInr [t1 t2 ts].
adamc@177 418
adamc@177 419 Notation "##" := PVar (at level 70) : pat_scope.
adamc@179 420 Notation "[ p1 , p2 ]" := (PPair p1 p2) : pat_scope.
adamc@177 421 Notation "'Inl' p" := (PInl p) (at level 71) : pat_scope.
adamc@177 422 Notation "'Inr' p" := (PInr p) (at level 71) : pat_scope.
adamc@177 423
adamc@177 424 Bind Scope pat_scope with pat.
adamc@177 425 Delimit Scope pat_scope with pat.
adamc@177 426
adamc@177 427 Section vars.
adamc@177 428 Variable var : type -> Type.
adamc@177 429
adamc@177 430 Inductive exp : type -> Type :=
adamc@177 431 | Var : forall t,
adamc@177 432 var t
adamc@177 433 -> exp t
adamc@177 434
adamc@177 435 | EUnit : exp Unit
adamc@177 436
adamc@177 437 | App : forall t1 t2,
adamc@177 438 exp (t1 --> t2)
adamc@177 439 -> exp t1
adamc@177 440 -> exp t2
adamc@177 441 | Abs : forall t1 t2,
adamc@177 442 (var t1 -> exp t2)
adamc@177 443 -> exp (t1 --> t2)
adamc@177 444
adamc@177 445 | Pair : forall t1 t2,
adamc@177 446 exp t1
adamc@177 447 -> exp t2
adamc@177 448 -> exp (t1 ** t2)
adamc@177 449
adamc@177 450 | EInl : forall t1 t2,
adamc@177 451 exp t1
adamc@177 452 -> exp (t1 ++ t2)
adamc@177 453 | EInr : forall t1 t2,
adamc@177 454 exp t2
adamc@177 455 -> exp (t1 ++ t2)
adamc@177 456
adamc@177 457 | Case : forall t1 t2 (tss : list (list type)),
adamc@177 458 exp t1
adamc@177 459 -> (forall ts, member ts tss -> pat t1 ts)
adamc@177 460 -> (forall ts, member ts tss -> hlist var ts -> exp t2)
adamc@177 461 -> exp t2
adamc@177 462 -> exp t2.
adamc@177 463 End vars.
adamc@177 464
adamc@177 465 Definition Exp t := forall var, exp var t.
adamc@177 466
adamc@177 467 Implicit Arguments Var [var t].
adamc@177 468 Implicit Arguments EUnit [var].
adamc@177 469 Implicit Arguments App [var t1 t2].
adamc@177 470 Implicit Arguments Abs [var t1 t2].
adamc@177 471 Implicit Arguments Pair [var t1 t2].
adamc@177 472 Implicit Arguments EInl [var t1 t2].
adamc@177 473 Implicit Arguments EInr [var t1 t2].
adamc@177 474 Implicit Arguments Case [var t1 t2].
adamc@177 475
adamc@177 476 Notation "# v" := (Var v) (at level 70) : source_scope.
adamc@177 477
adamc@177 478 Notation "()" := EUnit : source_scope.
adamc@177 479
adamc@177 480 Infix "@" := App (left associativity, at level 77) : source_scope.
adamc@177 481 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
adamc@177 482
adamc@179 483 Notation "[ x , y ]" := (Pair x y) : source_scope.
adamc@177 484
adamc@177 485 Notation "'Inl' e" := (EInl e) (at level 71) : source_scope.
adamc@177 486 Notation "'Inr' e" := (EInr e) (at level 71) : source_scope.
adamc@177 487
adamc@178 488 Delimit Scope source_scope with source.
adamc@177 489 Bind Scope source_scope with exp.
adamc@177 490
adamc@221 491 Local Open Scope source_scope.
adamc@177 492
adamc@177 493 Fixpoint typeDenote (t : type) : Set :=
adamc@177 494 match t with
adamc@177 495 | Unit => unit
adamc@177 496 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@177 497 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
adamc@177 498 | t1 ++ t2 => (typeDenote t1 + typeDenote t2)%type
adamc@177 499 end.
adamc@177 500
adamc@224 501 Fixpoint patDenote t ts (p : pat t ts)
adamc@224 502 : typeDenote t -> option (hlist typeDenote ts) :=
adamc@224 503 match p with
adamc@216 504 | PVar _ => fun v => Some (v ::: HNil)
adamc@177 505 | PPair _ _ _ _ p1 p2 => fun v =>
adamc@177 506 match patDenote p1 (fst v), patDenote p2 (snd v) with
adamc@177 507 | Some tup1, Some tup2 => Some (happ tup1 tup2)
adamc@177 508 | _, _ => None
adamc@177 509 end
adamc@177 510 | PInl _ _ _ p' => fun v =>
adamc@177 511 match v with
adamc@177 512 | inl v' => patDenote p' v'
adamc@177 513 | _ => None
adamc@177 514 end
adamc@177 515 | PInr _ _ _ p' => fun v =>
adamc@177 516 match v with
adamc@177 517 | inr v' => patDenote p' v'
adamc@177 518 | _ => None
adamc@177 519 end
adamc@177 520 end.
adamc@177 521
adamc@177 522 Section matchesDenote.
adamc@177 523 Variables t2 : type.
adamc@177 524 Variable default : typeDenote t2.
adamc@177 525
adamc@177 526 Fixpoint matchesDenote (tss : list (list type))
adamc@177 527 : (forall ts, member ts tss -> option (hlist typeDenote ts))
adamc@177 528 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
adamc@177 529 -> typeDenote t2 :=
adamc@224 530 match tss with
adamc@177 531 | nil => fun _ _ =>
adamc@177 532 default
adamc@224 533 | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss')
adamc@224 534 -> option (hlist typeDenote ts'))
adamc@224 535 (bodies : forall ts', member ts' (ts :: tss')
adamc@224 536 -> hlist typeDenote ts' -> typeDenote t2) =>
adamc@216 537 match envs _ HFirst with
adamc@216 538 | None => matchesDenote
adamc@216 539 (fun _ mem => envs _ (HNext mem))
adamc@216 540 (fun _ mem => bodies _ (HNext mem))
adamc@216 541 | Some env => (bodies _ HFirst) env
adamc@177 542 end
adamc@177 543 end.
adamc@177 544 End matchesDenote.
adamc@177 545
adamc@177 546 Implicit Arguments matchesDenote [t2 tss].
adamc@177 547
adamc@224 548 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@224 549 match e with
adamc@177 550 | Var _ v => v
adamc@177 551
adamc@177 552 | EUnit => tt
adamc@177 553
adamc@177 554 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@177 555 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@177 556
adamc@177 557 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@177 558
adamc@177 559 | EInl _ _ e' => inl _ (expDenote e')
adamc@177 560 | EInr _ _ e' => inr _ (expDenote e')
adamc@177 561
adamc@177 562 | Case _ _ _ e ps es def =>
adamc@177 563 matchesDenote (expDenote def)
adamc@177 564 (fun _ mem => patDenote (ps _ mem) (expDenote e))
adamc@177 565 (fun _ mem env => expDenote (es _ mem env))
adamc@177 566 end.
adamc@177 567
adamc@177 568 Definition ExpDenote t (E : Exp t) := expDenote (E _).
adamc@177 569 End Source.
adamc@177 570
adamc@177 571 Import Source.
adamc@177 572
adamc@178 573 Module Elab.
adamc@177 574 Section vars.
adamc@177 575 Variable var : type -> Type.
adamc@177 576
adamc@177 577 Inductive exp : type -> Type :=
adamc@177 578 | Var : forall t,
adamc@177 579 var t
adamc@177 580 -> exp t
adamc@177 581
adamc@177 582 | EUnit : exp Unit
adamc@177 583
adamc@177 584 | App : forall t1 t2,
adamc@177 585 exp (t1 --> t2)
adamc@177 586 -> exp t1
adamc@177 587 -> exp t2
adamc@177 588 | Abs : forall t1 t2,
adamc@177 589 (var t1 -> exp t2)
adamc@177 590 -> exp (t1 --> t2)
adamc@177 591
adamc@177 592 | Pair : forall t1 t2,
adamc@177 593 exp t1
adamc@177 594 -> exp t2
adamc@177 595 -> exp (t1 ** t2)
adamc@177 596 | Fst : forall t1 t2,
adamc@177 597 exp (t1 ** t2)
adamc@177 598 -> exp t1
adamc@177 599 | Snd : forall t1 t2,
adamc@177 600 exp (t1 ** t2)
adamc@177 601 -> exp t2
adamc@177 602
adamc@177 603 | EInl : forall t1 t2,
adamc@177 604 exp t1
adamc@177 605 -> exp (t1 ++ t2)
adamc@177 606 | EInr : forall t1 t2,
adamc@177 607 exp t2
adamc@177 608 -> exp (t1 ++ t2)
adamc@177 609 | Case : forall t1 t2 t,
adamc@177 610 exp (t1 ++ t2)
adamc@177 611 -> (var t1 -> exp t)
adamc@177 612 -> (var t2 -> exp t)
adamc@177 613 -> exp t.
adamc@177 614 End vars.
adamc@177 615
adamc@177 616 Definition Exp t := forall var, exp var t.
adamc@177 617
adamc@177 618 Implicit Arguments Var [var t].
adamc@177 619 Implicit Arguments EUnit [var].
adamc@177 620 Implicit Arguments App [var t1 t2].
adamc@177 621 Implicit Arguments Abs [var t1 t2].
adamc@177 622 Implicit Arguments Pair [var t1 t2].
adamc@177 623 Implicit Arguments Fst [var t1 t2].
adamc@177 624 Implicit Arguments Snd [var t1 t2].
adamc@177 625 Implicit Arguments EInl [var t1 t2].
adamc@177 626 Implicit Arguments EInr [var t1 t2].
adamc@177 627 Implicit Arguments Case [var t1 t2 t].
adamc@177 628
adamc@177 629
adamc@177 630 Notation "# v" := (Var v) (at level 70) : elab_scope.
adamc@177 631
adamc@177 632 Notation "()" := EUnit : elab_scope.
adamc@177 633
adamc@177 634 Infix "@" := App (left associativity, at level 77) : elab_scope.
adamc@177 635 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : elab_scope.
adamc@177 636 Notation "\ ? , e" := (Abs (fun _ => e)) (at level 78) : elab_scope.
adamc@177 637
adamc@179 638 Notation "[ x , y ]" := (Pair x y) : elab_scope.
adamc@177 639 Notation "#1 e" := (Fst e) (at level 72) : elab_scope.
adamc@177 640 Notation "#2 e" := (Snd e) (at level 72) : elab_scope.
adamc@177 641
adamc@177 642 Notation "'Inl' e" := (EInl e) (at level 71) : elab_scope.
adamc@177 643 Notation "'Inr' e" := (EInr e) (at level 71) : elab_scope.
adamc@177 644
adamc@177 645 Bind Scope elab_scope with exp.
adamc@177 646 Delimit Scope elab_scope with elab.
adamc@177 647
adamc@177 648 Open Scope elab_scope.
adamc@177 649
adamc@224 650 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@224 651 match e with
adamc@177 652 | Var _ v => v
adamc@177 653
adamc@177 654 | EUnit => tt
adamc@177 655
adamc@177 656 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@177 657 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@177 658
adamc@177 659 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@177 660 | Fst _ _ e' => fst (expDenote e')
adamc@177 661 | Snd _ _ e' => snd (expDenote e')
adamc@177 662
adamc@177 663 | EInl _ _ e' => inl _ (expDenote e')
adamc@177 664 | EInr _ _ e' => inr _ (expDenote e')
adamc@177 665 | Case _ _ _ e' e1 e2 =>
adamc@177 666 match expDenote e' with
adamc@177 667 | inl v => expDenote (e1 v)
adamc@177 668 | inr v => expDenote (e2 v)
adamc@177 669 end
adamc@177 670 end.
adamc@177 671
adamc@177 672 Definition ExpDenote t (E : Exp t) := expDenote (E _).
adamc@177 673 End Elab.
adamc@177 674
adamc@178 675 Import Elab.
adamc@178 676
adamc@178 677 Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%source
adamc@178 678 (right associativity, at level 76, e1 at next level) : source_scope.
adamc@178 679 Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%elab
adamc@178 680 (right associativity, at level 76, e1 at next level) : elab_scope.
adamc@178 681
adamc@178 682 Section choice_tree.
adamc@178 683 Open Scope source_scope.
adamc@178 684
adamc@178 685 Fixpoint choice_tree var (t : type) (result : Type) : Type :=
adamc@178 686 match t with
adamc@178 687 | t1 ** t2 =>
adamc@178 688 choice_tree var t1
adamc@178 689 (choice_tree var t2
adamc@178 690 result)
adamc@178 691 | t1 ++ t2 =>
adamc@178 692 choice_tree var t1 result
adamc@178 693 * choice_tree var t2 result
adamc@178 694 | t => exp var t -> result
adamc@178 695 end%type.
adamc@178 696
adamc@224 697 Fixpoint merge var t result
adamc@178 698 : (result -> result -> result)
adamc@178 699 -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result :=
adamc@224 700 match t with
adamc@178 701 | _ ** _ => fun mr ct1 ct2 =>
adamc@178 702 merge _ _
adamc@178 703 (merge _ _ mr)
adamc@178 704 ct1 ct2
adamc@178 705
adamc@178 706 | _ ++ _ => fun mr ct1 ct2 =>
adamc@178 707 (merge var _ mr (fst ct1) (fst ct2),
adamc@178 708 merge var _ mr (snd ct1) (snd ct2))
adamc@178 709
adamc@178 710 | _ => fun mr ct1 ct2 e => mr (ct1 e) (ct2 e)
adamc@178 711 end.
adamc@178 712
adamc@224 713 Fixpoint everywhere var t result
adamc@178 714 : (exp var t -> result) -> choice_tree var t result :=
adamc@224 715 match t with
adamc@178 716 | t1 ** t2 => fun r =>
adamc@178 717 everywhere (t := t1) (fun e1 =>
adamc@178 718 everywhere (t := t2) (fun e2 =>
adamc@178 719 r ([e1, e2])%elab))
adamc@178 720
adamc@178 721 | _ ++ _ => fun r =>
adamc@178 722 (everywhere (fun e => r (Inl e)%elab),
adamc@178 723 everywhere (fun e => r (Inr e)%elab))
adamc@178 724
adamc@178 725 | _ => fun r => r
adamc@178 726 end.
adamc@178 727 End choice_tree.
adamc@178 728
adamc@178 729 Implicit Arguments merge [var t result].
adamc@178 730
adamc@178 731 Section elaborate.
adamc@221 732 Local Open Scope elab_scope.
adamc@178 733
adamc@224 734 Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) :
adamc@178 735 (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result :=
adamc@224 736 match p with
adamc@178 737 | PVar _ => fun succ fail =>
adamc@216 738 everywhere (fun disc => succ (disc ::: HNil))
adamc@178 739
adamc@178 740 | PPair _ _ _ _ p1 p2 => fun succ fail =>
adamc@216 741 elaboratePat p1
adamc@178 742 (fun tup1 =>
adamc@216 743 elaboratePat p2
adamc@178 744 (fun tup2 =>
adamc@178 745 succ (happ tup1 tup2))
adamc@178 746 fail)
adamc@178 747 (everywhere (fun _ => fail))
adamc@178 748
adamc@178 749 | PInl _ _ _ p' => fun succ fail =>
adamc@216 750 (elaboratePat p' succ fail,
adamc@178 751 everywhere (fun _ => fail))
adamc@178 752 | PInr _ _ _ p' => fun succ fail =>
adamc@178 753 (everywhere (fun _ => fail),
adamc@216 754 elaboratePat p' succ fail)
adamc@178 755 end.
adamc@178 756
adamc@178 757 Implicit Arguments elaboratePat [var t1 ts result].
adamc@178 758
adamc@224 759 Fixpoint letify var t ts : (hlist var ts -> exp var t)
adamc@178 760 -> hlist (exp var) ts -> exp var t :=
adamc@224 761 match ts with
adamc@216 762 | nil => fun f _ => f HNil
adamc@216 763 | _ :: _ => fun f tup => letify (fun tup' => x <- hhd tup; f (x ::: tup')) (htl tup)
adamc@178 764 end.
adamc@178 765
adamc@178 766 Implicit Arguments letify [var t ts].
adamc@178 767
adamc@178 768 Fixpoint expand var result t1 t2
adamc@224 769 (out : result -> exp var t2)
adamc@178 770 : forall ct : choice_tree var t1 result,
adamc@178 771 exp var t1
adamc@178 772 -> exp var t2 :=
adamc@224 773 match t1 with
adamc@178 774 | (_ ** _)%source => fun ct disc =>
adamc@178 775 expand
adamc@178 776 (fun ct' => expand out ct' (#2 disc)%source)
adamc@178 777 ct
adamc@178 778 (#1 disc)
adamc@178 779
adamc@178 780 | (_ ++ _)%source => fun ct disc =>
adamc@178 781 Case disc
adamc@178 782 (fun x => expand out (fst ct) (#x))
adamc@178 783 (fun y => expand out (snd ct) (#y))
adamc@178 784
adamc@178 785 | _ => fun ct disc =>
adamc@178 786 x <- disc; out (ct (#x))
adamc@178 787 end.
adamc@178 788
adamc@178 789 Definition mergeOpt A (o1 o2 : option A) :=
adamc@178 790 match o1 with
adamc@178 791 | None => o2
adamc@178 792 | _ => o1
adamc@178 793 end.
adamc@178 794
adamc@178 795 Import Source.
adamc@178 796
adamc@178 797 Fixpoint elaborateMatches var t1 t2
adamc@224 798 (tss : list (list type))
adamc@178 799 : (forall ts, member ts tss -> pat t1 ts)
adamc@178 800 -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2)
adamc@178 801 -> choice_tree var t1 (option (Elab.exp var t2)) :=
adamc@224 802 match tss with
adamc@178 803 | nil => fun _ _ =>
adamc@178 804 everywhere (fun _ => None)
adamc@178 805 | ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts')
adamc@178 806 (es : forall ts', member ts' (ts :: tss') -> hlist var ts' -> Elab.exp var t2) =>
adamc@178 807 merge (@mergeOpt _)
adamc@216 808 (elaboratePat (ps _ HFirst)
adamc@178 809 (fun ts => Some (letify
adamc@216 810 (fun ts' => es _ HFirst ts')
adamc@178 811 ts))
adamc@178 812 None)
adamc@216 813 (elaborateMatches
adamc@216 814 (fun _ mem => ps _ (HNext mem))
adamc@216 815 (fun _ mem => es _ (HNext mem)))
adamc@178 816 end.
adamc@178 817
adamc@178 818 Implicit Arguments elaborateMatches [var t1 t2 tss].
adamc@178 819
adamc@178 820 Open Scope cps_scope.
adamc@178 821
adamc@224 822 Fixpoint elaborate var t (e : Source.exp var t) : Elab.exp var t :=
adamc@224 823 match e with
adamc@178 824 | Var _ v => #v
adamc@178 825
adamc@178 826 | EUnit => ()
adamc@178 827
adamc@178 828 | App _ _ e1 e2 => elaborate e1 @ elaborate e2
adamc@178 829 | Abs _ _ e' => \x, elaborate (e' x)
adamc@178 830
adamc@178 831 | Pair _ _ e1 e2 => [elaborate e1, elaborate e2]
adamc@178 832 | EInl _ _ e' => Inl (elaborate e')
adamc@178 833 | EInr _ _ e' => Inr (elaborate e')
adamc@178 834
adamc@178 835 | Case _ _ _ e' ps es def =>
adamc@178 836 expand
adamc@178 837 (fun eo => match eo with
adamc@178 838 | None => elaborate def
adamc@178 839 | Some e => e
adamc@178 840 end)
adamc@178 841 (elaborateMatches ps (fun _ mem env => elaborate (es _ mem env)))
adamc@178 842 (elaborate e')
adamc@178 843 end.
adamc@178 844 End elaborate.
adamc@178 845
adamc@178 846 Definition Elaborate t (E : Source.Exp t) : Elab.Exp t :=
adamc@178 847 fun _ => elaborate (E _).
adamc@178 848
adamc@179 849 Fixpoint grab t result : choice_tree typeDenote t result -> typeDenote t -> result :=
adamc@224 850 match t with
adamc@179 851 | t1 ** t2 => fun ct v =>
adamc@179 852 grab t2 _ (grab t1 _ ct (fst v)) (snd v)
adamc@179 853 | t1 ++ t2 => fun ct v =>
adamc@179 854 match v with
adamc@179 855 | inl v' => grab t1 _ (fst ct) v'
adamc@179 856 | inr v' => grab t2 _ (snd ct) v'
adamc@179 857 end
adamc@179 858 | t => fun ct v => ct (#v)%elab
adamc@179 859 end%source%type.
adamc@179 860
adamc@179 861 Implicit Arguments grab [t result].
adamc@179 862
adamc@179 863 Ltac my_crush :=
adamc@179 864 crush;
adamc@179 865 repeat (match goal with
adamc@179 866 | [ |- context[match ?E with inl _ => _ | inr _ => _ end] ] =>
adamc@179 867 destruct E
adamc@179 868 end; crush).
adamc@179 869
adamc@179 870 Lemma expand_grab : forall t2 t1 result
adamc@179 871 (out : result -> Elab.exp typeDenote t2)
adamc@179 872 (ct : choice_tree typeDenote t1 result)
adamc@179 873 (disc : Elab.exp typeDenote t1),
adamc@224 874 Elab.expDenote (expand out ct disc)
adamc@224 875 = Elab.expDenote (out (grab ct (Elab.expDenote disc))).
adamc@179 876 induction t1; my_crush.
adamc@179 877 Qed.
adamc@179 878
adamc@179 879 Lemma recreate_pair : forall t1 t2
adamc@179 880 (x : Elab.exp typeDenote t1)
adamc@179 881 (x0 : Elab.exp typeDenote t2)
adamc@179 882 (v : typeDenote (t1 ** t2)),
adamc@179 883 expDenote x = fst v
adamc@179 884 -> expDenote x0 = snd v
adamc@179 885 -> @eq (typeDenote t1 * typeDenote t2) (expDenote [x, x0]) v.
adamc@179 886 destruct v; crush.
adamc@179 887 Qed.
adamc@179 888
adamc@179 889 Lemma everywhere_correct : forall t1 result
adamc@179 890 (succ : Elab.exp typeDenote t1 -> result) disc,
adamc@179 891 exists disc', grab (everywhere succ) (Elab.expDenote disc) = succ disc'
adamc@179 892 /\ Elab.expDenote disc' = Elab.expDenote disc.
adamc@179 893 Hint Resolve recreate_pair.
adamc@179 894
adamc@179 895 induction t1; my_crush; eauto; fold choice_tree;
adamc@179 896 repeat (fold typeDenote in *; crush;
adamc@179 897 match goal with
adamc@179 898 | [ IH : forall result succ, _ |- context[grab (everywhere ?S) _] ] =>
adamc@179 899 generalize (IH _ S); clear IH
adamc@179 900 | [ e : exp typeDenote (?T ** _), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
adamc@179 901 generalize (IH (#1 e)); clear IH
adamc@179 902 | [ e : exp typeDenote (_ ** ?T), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
adamc@179 903 generalize (IH (#2 e)); clear IH
adamc@179 904 | [ e : typeDenote ?T, IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
adamc@179 905 generalize (IH (#e)); clear IH
adamc@179 906 end; crush); eauto.
adamc@179 907 Qed.
adamc@179 908
adamc@179 909 Lemma merge_correct : forall t result
adamc@179 910 (ct1 ct2 : choice_tree typeDenote t result)
adamc@179 911 (mr : result -> result -> result) v,
adamc@179 912 grab (merge mr ct1 ct2) v = mr (grab ct1 v) (grab ct2 v).
adamc@179 913 induction t; crush.
adamc@179 914 Qed.
adamc@179 915
adamc@179 916 Lemma everywhere_fail : forall t result
adamc@179 917 (fail : result) v,
adamc@179 918 grab (everywhere (fun _ : Elab.exp typeDenote t => fail)) v = fail.
adamc@179 919 induction t; crush.
adamc@179 920 Qed.
adamc@179 921
adamc@179 922 Lemma elaboratePat_correct : forall t1 ts (p : pat t1 ts)
adamc@179 923 result (succ : hlist (Elab.exp typeDenote) ts -> result)
adamc@179 924 (fail : result) v env,
adamc@179 925 patDenote p v = Some env
adamc@216 926 -> exists env', grab (elaboratePat p succ fail) v = succ env'
adamc@179 927 /\ env = hmap Elab.expDenote env'.
adamc@179 928 Hint Resolve hmap_happ.
adamc@179 929
adamc@179 930 induction p; crush; fold choice_tree;
adamc@179 931 repeat (match goal with
adamc@179 932 | [ |- context[grab (everywhere ?succ) ?v] ] =>
adamc@179 933 generalize (everywhere_correct succ (#v)%elab)
adamc@179 934
adamc@224 935 | [ H : forall result succ fail, _
adamc@224 936 |- context[grab (elaboratePat _ ?S ?F) ?V] ] =>
adamc@179 937 generalize (H _ S F V); clear H
adamc@179 938 | [ H1 : context[match ?E with Some _ => _ | None => _ end],
adamc@216 939 H2 : forall env, ?E = Some env -> _ |- _ ] =>
adamc@216 940 destruct E
adamc@179 941 | [ H : forall env, Some ?E = Some env -> _ |- _ ] =>
adamc@179 942 generalize (H _ (refl_equal _)); clear H
adamc@179 943 end; crush); eauto.
adamc@179 944 Qed.
adamc@179 945
adamc@179 946 Lemma elaboratePat_fails : forall t1 ts (p : pat t1 ts)
adamc@179 947 result (succ : hlist (Elab.exp typeDenote) ts -> result)
adamc@179 948 (fail : result) v,
adamc@179 949 patDenote p v = None
adamc@216 950 -> grab (elaboratePat p succ fail) v = fail.
adamc@179 951 Hint Resolve everywhere_fail.
adamc@179 952
adamc@179 953 induction p; try solve [ crush ];
adamc@179 954 simpl; fold choice_tree; intuition; simpl in *;
adamc@179 955 repeat match goal with
adamc@179 956 | [ IH : forall result succ fail v, patDenote ?P v = _ -> _
adamc@216 957 |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
adamc@179 958 generalize (IH _ S F V); clear IH; intro IH;
adamc@179 959 generalize (elaboratePat_correct P S F V); intros;
adamc@179 960 destruct (patDenote P V); try discriminate
adamc@179 961 | [ H : forall env, Some _ = Some env -> _ |- _ ] =>
adamc@179 962 destruct (H _ (refl_equal _)); clear H; intuition
adamc@179 963 | [ H : _ |- _ ] => rewrite H; intuition
adamc@224 964 | [ |- context[match ?v with inl _ => _ | inr _ => _ end] ] =>
adamc@224 965 destruct v; auto
adamc@179 966 end.
adamc@179 967 Qed.
adamc@179 968
adamc@179 969 Implicit Arguments letify [var t ts].
adamc@179 970
adamc@179 971 Lemma letify_correct : forall t ts (f : hlist typeDenote ts -> Elab.exp typeDenote t)
adamc@179 972 (env : hlist (Elab.exp typeDenote) ts),
adamc@179 973 Elab.expDenote (letify f env)
adamc@179 974 = Elab.expDenote (f (hmap Elab.expDenote env)).
adamc@216 975 induction ts; crush; dep_destruct env; crush.
adamc@179 976 Qed.
adamc@179 977
adamc@179 978 Theorem elaborate_correct : forall t (e : Source.exp typeDenote t),
adamc@179 979 Elab.expDenote (elaborate e) = Source.expDenote e.
adamc@179 980 Hint Rewrite expand_grab merge_correct letify_correct : cpdt.
adamc@179 981 Hint Rewrite everywhere_fail elaboratePat_fails using assumption : cpdt.
adamc@179 982
adamc@179 983 induction e; crush; try (ext_eq; crush);
adamc@179 984 match goal with
adamc@179 985 | [ tss : list (list type) |- _ ] =>
adamc@179 986 induction tss; crush;
adamc@179 987 match goal with
adamc@216 988 | [ |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
adamc@179 989 case_eq (patDenote P V); [intros env Heq;
adamc@179 990 destruct (elaboratePat_correct P S F _ Heq); crush;
adamc@179 991 match goal with
adamc@179 992 | [ H : _ |- _ ] => rewrite <- H; crush
adamc@179 993 end
adamc@179 994 | crush ]
adamc@179 995 end
adamc@179 996 end.
adamc@179 997 Qed.
adamc@179 998
adamc@179 999 Theorem Elaborate_correct : forall t (E : Source.Exp t),
adamc@179 1000 Elab.ExpDenote (Elaborate E) = Source.ExpDenote E.
adamc@179 1001 unfold Elab.ExpDenote, Elaborate, Source.ExpDenote;
adamc@179 1002 intros; apply elaborate_correct.
adamc@179 1003 Qed.
adamc@179 1004
adamc@177 1005 End PatMatch.
adamc@181 1006
adamc@181 1007
adamc@181 1008 (** * Exercises *)
adamc@181 1009
adamc@181 1010 (** %\begin{enumerate}%#<ol>#
adamc@181 1011
adamc@181 1012 %\item%#<li># When in the last chapter we implemented constant folding for simply-typed lambda calculus, it may have seemed natural to try applying beta reductions. This would have been a lot more trouble than is apparent at first, because we would have needed to convince Coq that our normalizing function always terminated.
adamc@181 1013
adamc@181 1014 It might also seem that beta reduction is a lost cause because we have no effective way of substituting in the [exp] type; we only managed to write a substitution function for the parametric [Exp] type. This is not as big of a problem as it seems. For instance, for the language we built by extending simply-typed lambda calculus with products and sums, it also appears that we need substitution for simplifying [case] expressions whose discriminees are known to be [inl] or [inr], but the function is still implementable.
adamc@181 1015
adamc@200 1016 For this exercise, extend the products and sums constant folder from the last chapter so that it simplifies [case] expressions as well, by checking if the discriminee is a known [inl] or known [inr]. Also extend the correctness theorem to apply to your new definition. You will probably want to assert an axiom relating to an expression equivalence relation like the one defined in this chapter. Any such axiom should only mention syntax; it should not mention any compilation or denotation functions. Following the format of the axiom from the last chapter is the safest bet to avoid proving a worthless theorem.
adamc@181 1017 #</li>#
adamc@181 1018
adamc@181 1019 #</ol>#%\end{enumerate}% *)