Mercurial > cpdt > repo

annotate src/Extensional.v @ 228:0be1a42b3035

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proof-reading pass through first bit of Universes
author Adam Chlipala <adamc@hcoop.net>
date Fri, 20 Nov 2009 10:18:35 -0500
parents 19902d0b6622
children 0400fa005d5a
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@225 530 match tss return (forall ts, member ts tss -> option (hlist typeDenote ts))
adamc@225 531 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
adamc@225 532 -> _ with
adamc@177 533 | nil => fun _ _ =>
adamc@177 534 default
adamc@224 535 | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss')
adamc@224 536 -> option (hlist typeDenote ts'))
adamc@224 537 (bodies : forall ts', member ts' (ts :: tss')
adamc@224 538 -> hlist typeDenote ts' -> typeDenote t2) =>
adamc@216 539 match envs _ HFirst with
adamc@216 540 | None => matchesDenote
adamc@216 541 (fun _ mem => envs _ (HNext mem))
adamc@216 542 (fun _ mem => bodies _ (HNext mem))
adamc@216 543 | Some env => (bodies _ HFirst) env
adamc@177 544 end
adamc@177 545 end.
adamc@177 546 End matchesDenote.
adamc@177 547
adamc@177 548 Implicit Arguments matchesDenote [t2 tss].
adamc@177 549
adamc@224 550 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@224 551 match e with
adamc@177 552 | Var _ v => v
adamc@177 553
adamc@177 554 | EUnit => tt
adamc@177 555
adamc@177 556 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@177 557 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@177 558
adamc@177 559 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@177 560
adamc@177 561 | EInl _ _ e' => inl _ (expDenote e')
adamc@177 562 | EInr _ _ e' => inr _ (expDenote e')
adamc@177 563
adamc@177 564 | Case _ _ _ e ps es def =>
adamc@177 565 matchesDenote (expDenote def)
adamc@177 566 (fun _ mem => patDenote (ps _ mem) (expDenote e))
adamc@177 567 (fun _ mem env => expDenote (es _ mem env))
adamc@177 568 end.
adamc@177 569
adamc@177 570 Definition ExpDenote t (E : Exp t) := expDenote (E _).
adamc@177 571 End Source.
adamc@177 572
adamc@177 573 Import Source.
adamc@177 574
adamc@178 575 Module Elab.
adamc@177 576 Section vars.
adamc@177 577 Variable var : type -> Type.
adamc@177 578
adamc@177 579 Inductive exp : type -> Type :=
adamc@177 580 | Var : forall t,
adamc@177 581 var t
adamc@177 582 -> exp t
adamc@177 583
adamc@177 584 | EUnit : exp Unit
adamc@177 585
adamc@177 586 | App : forall t1 t2,
adamc@177 587 exp (t1 --> t2)
adamc@177 588 -> exp t1
adamc@177 589 -> exp t2
adamc@177 590 | Abs : forall t1 t2,
adamc@177 591 (var t1 -> exp t2)
adamc@177 592 -> exp (t1 --> t2)
adamc@177 593
adamc@177 594 | Pair : forall t1 t2,
adamc@177 595 exp t1
adamc@177 596 -> exp t2
adamc@177 597 -> exp (t1 ** t2)
adamc@177 598 | Fst : forall t1 t2,
adamc@177 599 exp (t1 ** t2)
adamc@177 600 -> exp t1
adamc@177 601 | Snd : forall t1 t2,
adamc@177 602 exp (t1 ** t2)
adamc@177 603 -> exp t2
adamc@177 604
adamc@177 605 | EInl : forall t1 t2,
adamc@177 606 exp t1
adamc@177 607 -> exp (t1 ++ t2)
adamc@177 608 | EInr : forall t1 t2,
adamc@177 609 exp t2
adamc@177 610 -> exp (t1 ++ t2)
adamc@177 611 | Case : forall t1 t2 t,
adamc@177 612 exp (t1 ++ t2)
adamc@177 613 -> (var t1 -> exp t)
adamc@177 614 -> (var t2 -> exp t)
adamc@177 615 -> exp t.
adamc@177 616 End vars.
adamc@177 617
adamc@177 618 Definition Exp t := forall var, exp var t.
adamc@177 619
adamc@177 620 Implicit Arguments Var [var t].
adamc@177 621 Implicit Arguments EUnit [var].
adamc@177 622 Implicit Arguments App [var t1 t2].
adamc@177 623 Implicit Arguments Abs [var t1 t2].
adamc@177 624 Implicit Arguments Pair [var t1 t2].
adamc@177 625 Implicit Arguments Fst [var t1 t2].
adamc@177 626 Implicit Arguments Snd [var t1 t2].
adamc@177 627 Implicit Arguments EInl [var t1 t2].
adamc@177 628 Implicit Arguments EInr [var t1 t2].
adamc@177 629 Implicit Arguments Case [var t1 t2 t].
adamc@177 630
adamc@177 631
adamc@177 632 Notation "# v" := (Var v) (at level 70) : elab_scope.
adamc@177 633
adamc@177 634 Notation "()" := EUnit : elab_scope.
adamc@177 635
adamc@177 636 Infix "@" := App (left associativity, at level 77) : elab_scope.
adamc@177 637 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : elab_scope.
adamc@177 638 Notation "\ ? , e" := (Abs (fun _ => e)) (at level 78) : elab_scope.
adamc@177 639
adamc@179 640 Notation "[ x , y ]" := (Pair x y) : elab_scope.
adamc@177 641 Notation "#1 e" := (Fst e) (at level 72) : elab_scope.
adamc@177 642 Notation "#2 e" := (Snd e) (at level 72) : elab_scope.
adamc@177 643
adamc@177 644 Notation "'Inl' e" := (EInl e) (at level 71) : elab_scope.
adamc@177 645 Notation "'Inr' e" := (EInr e) (at level 71) : elab_scope.
adamc@177 646
adamc@177 647 Bind Scope elab_scope with exp.
adamc@177 648 Delimit Scope elab_scope with elab.
adamc@177 649
adamc@177 650 Open Scope elab_scope.
adamc@177 651
adamc@224 652 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@224 653 match e with
adamc@177 654 | Var _ v => v
adamc@177 655
adamc@177 656 | EUnit => tt
adamc@177 657
adamc@177 658 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@177 659 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@177 660
adamc@177 661 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@177 662 | Fst _ _ e' => fst (expDenote e')
adamc@177 663 | Snd _ _ e' => snd (expDenote e')
adamc@177 664
adamc@177 665 | EInl _ _ e' => inl _ (expDenote e')
adamc@177 666 | EInr _ _ e' => inr _ (expDenote e')
adamc@177 667 | Case _ _ _ e' e1 e2 =>
adamc@177 668 match expDenote e' with
adamc@177 669 | inl v => expDenote (e1 v)
adamc@177 670 | inr v => expDenote (e2 v)
adamc@177 671 end
adamc@177 672 end.
adamc@177 673
adamc@177 674 Definition ExpDenote t (E : Exp t) := expDenote (E _).
adamc@177 675 End Elab.
adamc@177 676
adamc@178 677 Import Elab.
adamc@178 678
adamc@178 679 Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%source
adamc@178 680 (right associativity, at level 76, e1 at next level) : source_scope.
adamc@178 681 Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%elab
adamc@178 682 (right associativity, at level 76, e1 at next level) : elab_scope.
adamc@178 683
adamc@178 684 Section choice_tree.
adamc@178 685 Open Scope source_scope.
adamc@178 686
adamc@178 687 Fixpoint choice_tree var (t : type) (result : Type) : Type :=
adamc@178 688 match t with
adamc@178 689 | t1 ** t2 =>
adamc@178 690 choice_tree var t1
adamc@178 691 (choice_tree var t2
adamc@178 692 result)
adamc@178 693 | t1 ++ t2 =>
adamc@178 694 choice_tree var t1 result
adamc@178 695 * choice_tree var t2 result
adamc@178 696 | t => exp var t -> result
adamc@178 697 end%type.
adamc@178 698
adamc@224 699 Fixpoint merge var t result
adamc@178 700 : (result -> result -> result)
adamc@178 701 -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result :=
adamc@224 702 match t with
adamc@178 703 | _ ** _ => fun mr ct1 ct2 =>
adamc@178 704 merge _ _
adamc@178 705 (merge _ _ mr)
adamc@178 706 ct1 ct2
adamc@178 707
adamc@178 708 | _ ++ _ => fun mr ct1 ct2 =>
adamc@178 709 (merge var _ mr (fst ct1) (fst ct2),
adamc@178 710 merge var _ mr (snd ct1) (snd ct2))
adamc@178 711
adamc@178 712 | _ => fun mr ct1 ct2 e => mr (ct1 e) (ct2 e)
adamc@178 713 end.
adamc@178 714
adamc@224 715 Fixpoint everywhere var t result
adamc@178 716 : (exp var t -> result) -> choice_tree var t result :=
adamc@224 717 match t with
adamc@178 718 | t1 ** t2 => fun r =>
adamc@178 719 everywhere (t := t1) (fun e1 =>
adamc@178 720 everywhere (t := t2) (fun e2 =>
adamc@178 721 r ([e1, e2])%elab))
adamc@178 722
adamc@178 723 | _ ++ _ => fun r =>
adamc@178 724 (everywhere (fun e => r (Inl e)%elab),
adamc@178 725 everywhere (fun e => r (Inr e)%elab))
adamc@178 726
adamc@178 727 | _ => fun r => r
adamc@178 728 end.
adamc@178 729 End choice_tree.
adamc@178 730
adamc@178 731 Implicit Arguments merge [var t result].
adamc@178 732
adamc@178 733 Section elaborate.
adamc@221 734 Local Open Scope elab_scope.
adamc@178 735
adamc@224 736 Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) :
adamc@178 737 (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result :=
adamc@224 738 match p with
adamc@178 739 | PVar _ => fun succ fail =>
adamc@216 740 everywhere (fun disc => succ (disc ::: HNil))
adamc@178 741
adamc@178 742 | PPair _ _ _ _ p1 p2 => fun succ fail =>
adamc@216 743 elaboratePat p1
adamc@178 744 (fun tup1 =>
adamc@216 745 elaboratePat p2
adamc@178 746 (fun tup2 =>
adamc@178 747 succ (happ tup1 tup2))
adamc@178 748 fail)
adamc@178 749 (everywhere (fun _ => fail))
adamc@178 750
adamc@178 751 | PInl _ _ _ p' => fun succ fail =>
adamc@216 752 (elaboratePat p' succ fail,
adamc@178 753 everywhere (fun _ => fail))
adamc@178 754 | PInr _ _ _ p' => fun succ fail =>
adamc@178 755 (everywhere (fun _ => fail),
adamc@216 756 elaboratePat p' succ fail)
adamc@178 757 end.
adamc@178 758
adamc@178 759 Implicit Arguments elaboratePat [var t1 ts result].
adamc@178 760
adamc@224 761 Fixpoint letify var t ts : (hlist var ts -> exp var t)
adamc@178 762 -> hlist (exp var) ts -> exp var t :=
adamc@224 763 match ts with
adamc@216 764 | nil => fun f _ => f HNil
adamc@216 765 | _ :: _ => fun f tup => letify (fun tup' => x <- hhd tup; f (x ::: tup')) (htl tup)
adamc@178 766 end.
adamc@178 767
adamc@178 768 Implicit Arguments letify [var t ts].
adamc@178 769
adamc@178 770 Fixpoint expand var result t1 t2
adamc@224 771 (out : result -> exp var t2)
adamc@178 772 : forall ct : choice_tree var t1 result,
adamc@178 773 exp var t1
adamc@178 774 -> exp var t2 :=
adamc@224 775 match t1 with
adamc@178 776 | (_ ** _)%source => fun ct disc =>
adamc@178 777 expand
adamc@178 778 (fun ct' => expand out ct' (#2 disc)%source)
adamc@178 779 ct
adamc@178 780 (#1 disc)
adamc@178 781
adamc@178 782 | (_ ++ _)%source => fun ct disc =>
adamc@178 783 Case disc
adamc@178 784 (fun x => expand out (fst ct) (#x))
adamc@178 785 (fun y => expand out (snd ct) (#y))
adamc@178 786
adamc@178 787 | _ => fun ct disc =>
adamc@178 788 x <- disc; out (ct (#x))
adamc@178 789 end.
adamc@178 790
adamc@178 791 Definition mergeOpt A (o1 o2 : option A) :=
adamc@178 792 match o1 with
adamc@178 793 | None => o2
adamc@178 794 | _ => o1
adamc@178 795 end.
adamc@178 796
adamc@178 797 Import Source.
adamc@178 798
adamc@178 799 Fixpoint elaborateMatches var t1 t2
adamc@224 800 (tss : list (list type))
adamc@178 801 : (forall ts, member ts tss -> pat t1 ts)
adamc@178 802 -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2)
adamc@178 803 -> choice_tree var t1 (option (Elab.exp var t2)) :=
adamc@225 804 match tss return (forall ts, member ts tss -> pat t1 ts)
adamc@225 805 -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2)
adamc@225 806 -> _ with
adamc@178 807 | nil => fun _ _ =>
adamc@178 808 everywhere (fun _ => None)
adamc@178 809 | ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts')
adamc@178 810 (es : forall ts', member ts' (ts :: tss') -> hlist var ts' -> Elab.exp var t2) =>
adamc@178 811 merge (@mergeOpt _)
adamc@216 812 (elaboratePat (ps _ HFirst)
adamc@178 813 (fun ts => Some (letify
adamc@216 814 (fun ts' => es _ HFirst ts')
adamc@178 815 ts))
adamc@178 816 None)
adamc@216 817 (elaborateMatches
adamc@216 818 (fun _ mem => ps _ (HNext mem))
adamc@216 819 (fun _ mem => es _ (HNext mem)))
adamc@178 820 end.
adamc@178 821
adamc@178 822 Implicit Arguments elaborateMatches [var t1 t2 tss].
adamc@178 823
adamc@178 824 Open Scope cps_scope.
adamc@178 825
adamc@224 826 Fixpoint elaborate var t (e : Source.exp var t) : Elab.exp var t :=
adamc@224 827 match e with
adamc@178 828 | Var _ v => #v
adamc@178 829
adamc@178 830 | EUnit => ()
adamc@178 831
adamc@178 832 | App _ _ e1 e2 => elaborate e1 @ elaborate e2
adamc@178 833 | Abs _ _ e' => \x, elaborate (e' x)
adamc@178 834
adamc@178 835 | Pair _ _ e1 e2 => [elaborate e1, elaborate e2]
adamc@178 836 | EInl _ _ e' => Inl (elaborate e')
adamc@178 837 | EInr _ _ e' => Inr (elaborate e')
adamc@178 838
adamc@178 839 | Case _ _ _ e' ps es def =>
adamc@178 840 expand
adamc@178 841 (fun eo => match eo with
adamc@178 842 | None => elaborate def
adamc@178 843 | Some e => e
adamc@178 844 end)
adamc@178 845 (elaborateMatches ps (fun _ mem env => elaborate (es _ mem env)))
adamc@178 846 (elaborate e')
adamc@178 847 end.
adamc@178 848 End elaborate.
adamc@178 849
adamc@178 850 Definition Elaborate t (E : Source.Exp t) : Elab.Exp t :=
adamc@178 851 fun _ => elaborate (E _).
adamc@178 852
adamc@179 853 Fixpoint grab t result : choice_tree typeDenote t result -> typeDenote t -> result :=
adamc@224 854 match t with
adamc@179 855 | t1 ** t2 => fun ct v =>
adamc@179 856 grab t2 _ (grab t1 _ ct (fst v)) (snd v)
adamc@179 857 | t1 ++ t2 => fun ct v =>
adamc@179 858 match v with
adamc@179 859 | inl v' => grab t1 _ (fst ct) v'
adamc@179 860 | inr v' => grab t2 _ (snd ct) v'
adamc@179 861 end
adamc@179 862 | t => fun ct v => ct (#v)%elab
adamc@179 863 end%source%type.
adamc@179 864
adamc@179 865 Implicit Arguments grab [t result].
adamc@179 866
adamc@179 867 Ltac my_crush :=
adamc@179 868 crush;
adamc@179 869 repeat (match goal with
adamc@179 870 | [ |- context[match ?E with inl _ => _ | inr _ => _ end] ] =>
adamc@179 871 destruct E
adamc@179 872 end; crush).
adamc@179 873
adamc@179 874 Lemma expand_grab : forall t2 t1 result
adamc@179 875 (out : result -> Elab.exp typeDenote t2)
adamc@179 876 (ct : choice_tree typeDenote t1 result)
adamc@179 877 (disc : Elab.exp typeDenote t1),
adamc@224 878 Elab.expDenote (expand out ct disc)
adamc@224 879 = Elab.expDenote (out (grab ct (Elab.expDenote disc))).
adamc@179 880 induction t1; my_crush.
adamc@179 881 Qed.
adamc@179 882
adamc@179 883 Lemma recreate_pair : forall t1 t2
adamc@179 884 (x : Elab.exp typeDenote t1)
adamc@179 885 (x0 : Elab.exp typeDenote t2)
adamc@179 886 (v : typeDenote (t1 ** t2)),
adamc@179 887 expDenote x = fst v
adamc@179 888 -> expDenote x0 = snd v
adamc@179 889 -> @eq (typeDenote t1 * typeDenote t2) (expDenote [x, x0]) v.
adamc@179 890 destruct v; crush.
adamc@179 891 Qed.
adamc@179 892
adamc@179 893 Lemma everywhere_correct : forall t1 result
adamc@179 894 (succ : Elab.exp typeDenote t1 -> result) disc,
adamc@179 895 exists disc', grab (everywhere succ) (Elab.expDenote disc) = succ disc'
adamc@179 896 /\ Elab.expDenote disc' = Elab.expDenote disc.
adamc@179 897 Hint Resolve recreate_pair.
adamc@179 898
adamc@179 899 induction t1; my_crush; eauto; fold choice_tree;
adamc@179 900 repeat (fold typeDenote in *; crush;
adamc@179 901 match goal with
adamc@179 902 | [ IH : forall result succ, _ |- context[grab (everywhere ?S) _] ] =>
adamc@179 903 generalize (IH _ S); clear IH
adamc@179 904 | [ e : exp typeDenote (?T ** _), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
adamc@179 905 generalize (IH (#1 e)); clear IH
adamc@179 906 | [ e : exp typeDenote (_ ** ?T), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
adamc@179 907 generalize (IH (#2 e)); clear IH
adamc@179 908 | [ e : typeDenote ?T, IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
adamc@179 909 generalize (IH (#e)); clear IH
adamc@179 910 end; crush); eauto.
adamc@179 911 Qed.
adamc@179 912
adamc@179 913 Lemma merge_correct : forall t result
adamc@179 914 (ct1 ct2 : choice_tree typeDenote t result)
adamc@179 915 (mr : result -> result -> result) v,
adamc@179 916 grab (merge mr ct1 ct2) v = mr (grab ct1 v) (grab ct2 v).
adamc@179 917 induction t; crush.
adamc@179 918 Qed.
adamc@179 919
adamc@179 920 Lemma everywhere_fail : forall t result
adamc@179 921 (fail : result) v,
adamc@179 922 grab (everywhere (fun _ : Elab.exp typeDenote t => fail)) v = fail.
adamc@179 923 induction t; crush.
adamc@179 924 Qed.
adamc@179 925
adamc@179 926 Lemma elaboratePat_correct : forall t1 ts (p : pat t1 ts)
adamc@179 927 result (succ : hlist (Elab.exp typeDenote) ts -> result)
adamc@179 928 (fail : result) v env,
adamc@179 929 patDenote p v = Some env
adamc@216 930 -> exists env', grab (elaboratePat p succ fail) v = succ env'
adamc@179 931 /\ env = hmap Elab.expDenote env'.
adamc@179 932 Hint Resolve hmap_happ.
adamc@179 933
adamc@179 934 induction p; crush; fold choice_tree;
adamc@179 935 repeat (match goal with
adamc@179 936 | [ |- context[grab (everywhere ?succ) ?v] ] =>
adamc@179 937 generalize (everywhere_correct succ (#v)%elab)
adamc@179 938
adamc@224 939 | [ H : forall result succ fail, _
adamc@224 940 |- context[grab (elaboratePat _ ?S ?F) ?V] ] =>
adamc@179 941 generalize (H _ S F V); clear H
adamc@179 942 | [ H1 : context[match ?E with Some _ => _ | None => _ end],
adamc@216 943 H2 : forall env, ?E = Some env -> _ |- _ ] =>
adamc@216 944 destruct E
adamc@179 945 | [ H : forall env, Some ?E = Some env -> _ |- _ ] =>
adamc@179 946 generalize (H _ (refl_equal _)); clear H
adamc@179 947 end; crush); eauto.
adamc@179 948 Qed.
adamc@179 949
adamc@179 950 Lemma elaboratePat_fails : forall t1 ts (p : pat t1 ts)
adamc@179 951 result (succ : hlist (Elab.exp typeDenote) ts -> result)
adamc@179 952 (fail : result) v,
adamc@179 953 patDenote p v = None
adamc@216 954 -> grab (elaboratePat p succ fail) v = fail.
adamc@179 955 Hint Resolve everywhere_fail.
adamc@179 956
adamc@179 957 induction p; try solve [ crush ];
adamc@179 958 simpl; fold choice_tree; intuition; simpl in *;
adamc@179 959 repeat match goal with
adamc@179 960 | [ IH : forall result succ fail v, patDenote ?P v = _ -> _
adamc@216 961 |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
adamc@179 962 generalize (IH _ S F V); clear IH; intro IH;
adamc@179 963 generalize (elaboratePat_correct P S F V); intros;
adamc@179 964 destruct (patDenote P V); try discriminate
adamc@179 965 | [ H : forall env, Some _ = Some env -> _ |- _ ] =>
adamc@179 966 destruct (H _ (refl_equal _)); clear H; intuition
adamc@179 967 | [ H : _ |- _ ] => rewrite H; intuition
adamc@224 968 | [ |- context[match ?v with inl _ => _ | inr _ => _ end] ] =>
adamc@224 969 destruct v; auto
adamc@179 970 end.
adamc@179 971 Qed.
adamc@179 972
adamc@179 973 Implicit Arguments letify [var t ts].
adamc@179 974
adamc@179 975 Lemma letify_correct : forall t ts (f : hlist typeDenote ts -> Elab.exp typeDenote t)
adamc@179 976 (env : hlist (Elab.exp typeDenote) ts),
adamc@179 977 Elab.expDenote (letify f env)
adamc@179 978 = Elab.expDenote (f (hmap Elab.expDenote env)).
adamc@216 979 induction ts; crush; dep_destruct env; crush.
adamc@179 980 Qed.
adamc@179 981
adamc@179 982 Theorem elaborate_correct : forall t (e : Source.exp typeDenote t),
adamc@179 983 Elab.expDenote (elaborate e) = Source.expDenote e.
adamc@179 984 Hint Rewrite expand_grab merge_correct letify_correct : cpdt.
adamc@179 985 Hint Rewrite everywhere_fail elaboratePat_fails using assumption : cpdt.
adamc@179 986
adamc@179 987 induction e; crush; try (ext_eq; crush);
adamc@179 988 match goal with
adamc@179 989 | [ tss : list (list type) |- _ ] =>
adamc@179 990 induction tss; crush;
adamc@179 991 match goal with
adamc@216 992 | [ |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
adamc@179 993 case_eq (patDenote P V); [intros env Heq;
adamc@179 994 destruct (elaboratePat_correct P S F _ Heq); crush;
adamc@179 995 match goal with
adamc@179 996 | [ H : _ |- _ ] => rewrite <- H; crush
adamc@179 997 end
adamc@179 998 | crush ]
adamc@179 999 end
adamc@179 1000 end.
adamc@179 1001 Qed.
adamc@179 1002
adamc@179 1003 Theorem Elaborate_correct : forall t (E : Source.Exp t),
adamc@179 1004 Elab.ExpDenote (Elaborate E) = Source.ExpDenote E.
adamc@179 1005 unfold Elab.ExpDenote, Elaborate, Source.ExpDenote;
adamc@179 1006 intros; apply elaborate_correct.
adamc@179 1007 Qed.
adamc@179 1008
adamc@177 1009 End PatMatch.
adamc@181 1010
adamc@181 1011
adamc@181 1012 (** * Exercises *)
adamc@181 1013
adamc@181 1014 (** %\begin{enumerate}%#<ol>#
adamc@181 1015
adamc@181 1016 %\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 1017
adamc@181 1018 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 1019
adamc@200 1020 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 1021 #</li>#
adamc@181 1022
adamc@181 1023 #</ol>#%\end{enumerate}% *)