Mercurial > cpdt > repo

annotate src/Extensional.v @ 221:54e8ecb5ec88

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port Reflection
author Adam Chlipala <adamc@hcoop.net>
date Mon, 16 Nov 2009 11:09:47 -0500
parents d1464997078d
children 4b73ea13574d
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@175 93 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@175 94 match e in (exp _ t) return (typeDenote t) 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@176 110 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop :=
adamc@181 111 | EqVar : forall G t (v1 : var1 t) v2,
adamc@176 112 In (existT _ t (v1, v2)) G
adamc@176 113 -> exp_equiv G (#v1) (#v2)
adamc@176 114
adamc@181 115 | EqConst : forall G n,
adamc@176 116 exp_equiv G (^n) (^n)
adamc@181 117 | EqPlus : forall G x1 y1 x2 y2,
adamc@176 118 exp_equiv G x1 x2
adamc@176 119 -> exp_equiv G y1 y2
adamc@176 120 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
adamc@176 121
adamc@181 122 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
adamc@176 123 exp_equiv G f1 f2
adamc@176 124 -> exp_equiv G x1 x2
adamc@176 125 -> exp_equiv G (f1 @ x1) (f2 @ x2)
adamc@181 126 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
adamc@176 127 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
adamc@176 128 -> exp_equiv G (Abs f1) (Abs f2).
adamc@176 129 End exp_equiv.
adamc@176 130
adamc@176 131 Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
adamc@176 132 exp_equiv nil (E var1) (E var2).
adamc@180 133 (* end thide *)
adamc@175 134 End Source.
adamc@175 135
adamc@175 136 Module CPS.
adamc@175 137 Inductive type : Type :=
adamc@175 138 | TNat : type
adamc@175 139 | Cont : type -> type
adamc@175 140 | TUnit : type
adamc@175 141 | Prod : type -> type -> type.
adamc@175 142
adamc@175 143 Notation "'Nat'" := TNat : cps_scope.
adamc@175 144 Notation "'Unit'" := TUnit : cps_scope.
adamc@175 145 Notation "t --->" := (Cont t) (at level 61) : cps_scope.
adamc@175 146 Infix "**" := Prod (right associativity, at level 60) : cps_scope.
adamc@175 147
adamc@175 148 Bind Scope cps_scope with type.
adamc@175 149 Delimit Scope cps_scope with cps.
adamc@175 150
adamc@175 151 Section vars.
adamc@175 152 Variable var : type -> Type.
adamc@175 153
adamc@175 154 Inductive prog : Type :=
adamc@175 155 | PHalt :
adamc@175 156 var Nat
adamc@175 157 -> prog
adamc@175 158 | App : forall t,
adamc@175 159 var (t --->)
adamc@175 160 -> var t
adamc@175 161 -> prog
adamc@175 162 | Bind : forall t,
adamc@175 163 primop t
adamc@175 164 -> (var t -> prog)
adamc@175 165 -> prog
adamc@175 166
adamc@175 167 with primop : type -> Type :=
adamc@175 168 | Var : forall t,
adamc@175 169 var t
adamc@175 170 -> primop t
adamc@175 171
adamc@175 172 | Const : nat -> primop Nat
adamc@175 173 | Plus : var Nat -> var Nat -> primop Nat
adamc@175 174
adamc@175 175 | Abs : forall t,
adamc@175 176 (var t -> prog)
adamc@175 177 -> primop (t --->)
adamc@175 178
adamc@175 179 | Pair : forall t1 t2,
adamc@175 180 var t1
adamc@175 181 -> var t2
adamc@175 182 -> primop (t1 ** t2)
adamc@175 183 | Fst : forall t1 t2,
adamc@175 184 var (t1 ** t2)
adamc@175 185 -> primop t1
adamc@175 186 | Snd : forall t1 t2,
adamc@175 187 var (t1 ** t2)
adamc@175 188 -> primop t2.
adamc@175 189 End vars.
adamc@175 190
adamc@175 191 Implicit Arguments PHalt [var].
adamc@175 192 Implicit Arguments App [var t].
adamc@175 193
adamc@175 194 Implicit Arguments Var [var t].
adamc@175 195 Implicit Arguments Const [var].
adamc@175 196 Implicit Arguments Plus [var].
adamc@175 197 Implicit Arguments Abs [var t].
adamc@175 198 Implicit Arguments Pair [var t1 t2].
adamc@175 199 Implicit Arguments Fst [var t1 t2].
adamc@175 200 Implicit Arguments Snd [var t1 t2].
adamc@175 201
adamc@175 202 Notation "'Halt' x" := (PHalt x) (no associativity, at level 75) : cps_scope.
adamc@175 203 Infix "@@" := App (no associativity, at level 75) : cps_scope.
adamc@175 204 Notation "x <- p ; e" := (Bind p (fun x => e))
adamc@175 205 (right associativity, at level 76, p at next level) : cps_scope.
adamc@175 206 Notation "! <- p ; e" := (Bind p (fun _ => e))
adamc@175 207 (right associativity, at level 76, p at next level) : cps_scope.
adamc@175 208
adamc@175 209 Notation "# v" := (Var v) (at level 70) : cps_scope.
adamc@175 210
adamc@175 211 Notation "^ n" := (Const n) (at level 70) : cps_scope.
adamc@175 212 Infix "+^" := Plus (left associativity, at level 79) : cps_scope.
adamc@175 213
adamc@175 214 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : cps_scope.
adamc@175 215 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : cps_scope.
adamc@175 216
adamc@179 217 Notation "[ x1 , x2 ]" := (Pair x1 x2) : cps_scope.
adamc@175 218 Notation "#1 x" := (Fst x) (at level 72) : cps_scope.
adamc@175 219 Notation "#2 x" := (Snd x) (at level 72) : cps_scope.
adamc@175 220
adamc@175 221 Bind Scope cps_scope with prog primop.
adamc@175 222
adamc@175 223 Open Scope cps_scope.
adamc@175 224
adamc@175 225 Fixpoint typeDenote (t : type) : Set :=
adamc@175 226 match t with
adamc@175 227 | Nat => nat
adamc@175 228 | t' ---> => typeDenote t' -> nat
adamc@175 229 | Unit => unit
adamc@175 230 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
adamc@175 231 end.
adamc@175 232
adamc@175 233 Fixpoint progDenote (e : prog typeDenote) : nat :=
adamc@175 234 match e with
adamc@175 235 | PHalt n => n
adamc@175 236 | App _ f x => f x
adamc@175 237 | Bind _ p x => progDenote (x (primopDenote p))
adamc@175 238 end
adamc@175 239
adamc@175 240 with primopDenote t (p : primop typeDenote t) {struct p} : typeDenote t :=
adamc@175 241 match p in (primop _ t) return (typeDenote t) with
adamc@175 242 | Var _ v => v
adamc@175 243
adamc@175 244 | Const n => n
adamc@175 245 | Plus n1 n2 => n1 + n2
adamc@175 246
adamc@175 247 | Abs _ e => fun x => progDenote (e x)
adamc@175 248
adamc@175 249 | Pair _ _ v1 v2 => (v1, v2)
adamc@175 250 | Fst _ _ v => fst v
adamc@175 251 | Snd _ _ v => snd v
adamc@175 252 end.
adamc@175 253
adamc@175 254 Definition Prog := forall var, prog var.
adamc@175 255 Definition Primop t := forall var, primop var t.
adamc@175 256 Definition ProgDenote (E : Prog) := progDenote (E _).
adamc@175 257 Definition PrimopDenote t (P : Primop t) := primopDenote (P _).
adamc@175 258 End CPS.
adamc@175 259
adamc@175 260 Import Source CPS.
adamc@175 261
adamc@180 262 (* begin thide *)
adamc@175 263 Fixpoint cpsType (t : Source.type) : CPS.type :=
adamc@175 264 match t with
adamc@175 265 | Nat => Nat%cps
adamc@175 266 | t1 --> t2 => (cpsType t1 ** (cpsType t2 --->) --->)%cps
adamc@175 267 end%source.
adamc@175 268
adamc@175 269 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
adamc@175 270
adamc@175 271 Section cpsExp.
adamc@175 272 Variable var : CPS.type -> Type.
adamc@175 273
adamc@175 274 Import Source.
adamc@175 275 Open Scope cps_scope.
adamc@175 276
adamc@175 277 Fixpoint cpsExp t (e : exp (fun t => var (cpsType t)) t) {struct e}
adamc@175 278 : (var (cpsType t) -> prog var) -> prog var :=
adamc@175 279 match e in (exp _ t) return ((var (cpsType t) -> prog var) -> prog var) with
adamc@175 280 | Var _ v => fun k => k v
adamc@175 281
adamc@175 282 | Const n => fun k =>
adamc@175 283 x <- ^n;
adamc@175 284 k x
adamc@175 285 | Plus e1 e2 => fun k =>
adamc@175 286 x1 <-- e1;
adamc@175 287 x2 <-- e2;
adamc@175 288 x <- x1 +^ x2;
adamc@175 289 k x
adamc@175 290
adamc@175 291 | App _ _ e1 e2 => fun k =>
adamc@175 292 f <-- e1;
adamc@175 293 x <-- e2;
adamc@175 294 kf <- \r, k r;
adamc@175 295 p <- [x, kf];
adamc@175 296 f @@ p
adamc@175 297 | Abs _ _ e' => fun k =>
adamc@175 298 f <- CPS.Abs (var := var) (fun p =>
adamc@175 299 x <- #1 p;
adamc@175 300 kf <- #2 p;
adamc@175 301 r <-- e' x;
adamc@175 302 kf @@ r);
adamc@175 303 k f
adamc@175 304 end
adamc@175 305
adamc@175 306 where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@175 307 End cpsExp.
adamc@175 308
adamc@175 309 Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)) : cps_scope.
adamc@175 310 Notation "! <-- e1 ; e2" := (cpsExp e1 (fun _ => e2))
adamc@175 311 (right associativity, at level 76, e1 at next level) : cps_scope.
adamc@175 312
adamc@175 313 Implicit Arguments cpsExp [var t].
adamc@175 314 Definition CpsExp (E : Exp Nat) : Prog :=
adamc@175 315 fun var => cpsExp (E _) (PHalt (var := _)).
adamc@180 316 (* end thide *)
adamc@175 317
adamc@175 318 Eval compute in CpsExp zero.
adamc@175 319 Eval compute in CpsExp one.
adamc@175 320 Eval compute in CpsExp zpo.
adamc@175 321 Eval compute in CpsExp app_ident.
adamc@175 322 Eval compute in CpsExp app_ident'.
adamc@175 323
adamc@175 324 Eval compute in ProgDenote (CpsExp zero).
adamc@175 325 Eval compute in ProgDenote (CpsExp one).
adamc@175 326 Eval compute in ProgDenote (CpsExp zpo).
adamc@175 327 Eval compute in ProgDenote (CpsExp app_ident).
adamc@175 328 Eval compute in ProgDenote (CpsExp app_ident').
adamc@175 329
adamc@180 330 (* begin thide *)
adamc@176 331 Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop :=
adamc@176 332 match t return (Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop) with
adamc@176 333 | Nat => fun n1 n2 => n1 = n2
adamc@176 334 | t1 --> t2 => fun f1 f2 =>
adamc@176 335 forall x1 x2, lr _ x1 x2
adamc@176 336 -> forall k, exists r,
adamc@176 337 f2 (x2, k) = k r
adamc@176 338 /\ lr _ (f1 x1) r
adamc@176 339 end%source.
adamc@176 340
adamc@176 341 Lemma cpsExp_correct : forall G t (e1 : exp _ t) (e2 : exp _ t),
adamc@176 342 exp_equiv G e1 e2
adamc@176 343 -> (forall t v1 v2, In (existT _ t (v1, v2)) G -> lr t v1 v2)
adamc@176 344 -> forall k, exists r,
adamc@176 345 progDenote (cpsExp e2 k) = progDenote (k r)
adamc@176 346 /\ lr t (expDenote e1) r.
adamc@176 347 induction 1; crush; fold typeDenote in *;
adamc@176 348 repeat (match goal with
adamc@176 349 | [ H : forall k, exists r, progDenote (cpsExp ?E k) = _ /\ _
adamc@176 350 |- context[cpsExp ?E ?K] ] =>
adamc@176 351 generalize (H K); clear H
adamc@176 352 | [ |- exists r, progDenote (_ ?R) = progDenote (_ r) /\ _ ] =>
adamc@176 353 exists R
adamc@176 354 | [ t1 : Source.type |- _ ] =>
adamc@176 355 match goal with
adamc@176 356 | [ Hlr : lr t1 ?X1 ?X2, IH : forall v1 v2, _ |- _ ] =>
adamc@176 357 generalize (IH X1 X2); clear IH; intro IH;
adamc@176 358 match type of IH with
adamc@176 359 | ?P -> _ => assert P
adamc@176 360 end
adamc@176 361 end
adamc@176 362 end; crush); eauto.
adamc@176 363 Qed.
adamc@176 364
adamc@176 365 Lemma vars_easy : forall (t : Source.type) (v1 : Source.typeDenote t)
adamc@176 366 (v2 : typeDenote (cpsType t)),
adamc@176 367 In
adamc@176 368 (existT
adamc@176 369 (fun t0 : Source.type =>
adamc@176 370 (Source.typeDenote t0 * typeDenote (cpsType t0))%type) t
adamc@176 371 (v1, v2)) nil -> lr t v1 v2.
adamc@176 372 crush.
adamc@176 373 Qed.
adamc@176 374
adamc@176 375 Theorem CpsExp_correct : forall (E : Exp Nat),
adamc@176 376 ProgDenote (CpsExp E) = ExpDenote E.
adamc@176 377 unfold ProgDenote, CpsExp, ExpDenote; intros;
adamc@176 378 generalize (cpsExp_correct (e1 := E _) (e2 := E _)
adamc@176 379 (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush.
adamc@176 380 Qed.
adamc@180 381 (* end thide *)
adamc@176 382
adamc@175 383 End STLC.
adamc@177 384
adamc@177 385
adamc@177 386 (** * A Pattern Compiler *)
adamc@177 387
adamc@177 388 Module PatMatch.
adamc@177 389 Module Source.
adamc@177 390 Inductive type : Type :=
adamc@177 391 | Unit : type
adamc@177 392 | Arrow : type -> type -> type
adamc@177 393 | Prod : type -> type -> type
adamc@177 394 | Sum : type -> type -> type.
adamc@177 395
adamc@177 396 Infix "-->" := Arrow (right associativity, at level 61).
adamc@177 397 Infix "++" := Sum (right associativity, at level 60).
adamc@177 398 Infix "**" := Prod (right associativity, at level 59).
adamc@177 399
adamc@177 400 Inductive pat : type -> list type -> Type :=
adamc@177 401 | PVar : forall t,
adamc@177 402 pat t (t :: nil)
adamc@177 403 | PPair : forall t1 t2 ts1 ts2,
adamc@177 404 pat t1 ts1
adamc@177 405 -> pat t2 ts2
adamc@177 406 -> pat (t1 ** t2) (ts1 ++ ts2)
adamc@177 407 | PInl : forall t1 t2 ts,
adamc@177 408 pat t1 ts
adamc@177 409 -> pat (t1 ++ t2) ts
adamc@177 410 | PInr : forall t1 t2 ts,
adamc@177 411 pat t2 ts
adamc@177 412 -> pat (t1 ++ t2) ts.
adamc@177 413
adamc@177 414 Implicit Arguments PVar [t].
adamc@177 415 Implicit Arguments PInl [t1 t2 ts].
adamc@177 416 Implicit Arguments PInr [t1 t2 ts].
adamc@177 417
adamc@177 418 Notation "##" := PVar (at level 70) : pat_scope.
adamc@179 419 Notation "[ p1 , p2 ]" := (PPair p1 p2) : pat_scope.
adamc@177 420 Notation "'Inl' p" := (PInl p) (at level 71) : pat_scope.
adamc@177 421 Notation "'Inr' p" := (PInr p) (at level 71) : pat_scope.
adamc@177 422
adamc@177 423 Bind Scope pat_scope with pat.
adamc@177 424 Delimit Scope pat_scope with pat.
adamc@177 425
adamc@177 426 Section vars.
adamc@177 427 Variable var : type -> Type.
adamc@177 428
adamc@177 429 Inductive exp : type -> Type :=
adamc@177 430 | Var : forall t,
adamc@177 431 var t
adamc@177 432 -> exp t
adamc@177 433
adamc@177 434 | EUnit : exp Unit
adamc@177 435
adamc@177 436 | App : forall t1 t2,
adamc@177 437 exp (t1 --> t2)
adamc@177 438 -> exp t1
adamc@177 439 -> exp t2
adamc@177 440 | Abs : forall t1 t2,
adamc@177 441 (var t1 -> exp t2)
adamc@177 442 -> exp (t1 --> t2)
adamc@177 443
adamc@177 444 | Pair : forall t1 t2,
adamc@177 445 exp t1
adamc@177 446 -> exp t2
adamc@177 447 -> exp (t1 ** t2)
adamc@177 448
adamc@177 449 | EInl : forall t1 t2,
adamc@177 450 exp t1
adamc@177 451 -> exp (t1 ++ t2)
adamc@177 452 | EInr : forall t1 t2,
adamc@177 453 exp t2
adamc@177 454 -> exp (t1 ++ t2)
adamc@177 455
adamc@177 456 | Case : forall t1 t2 (tss : list (list type)),
adamc@177 457 exp t1
adamc@177 458 -> (forall ts, member ts tss -> pat t1 ts)
adamc@177 459 -> (forall ts, member ts tss -> hlist var ts -> exp t2)
adamc@177 460 -> exp t2
adamc@177 461 -> exp t2.
adamc@177 462 End vars.
adamc@177 463
adamc@177 464 Definition Exp t := forall var, exp var t.
adamc@177 465
adamc@177 466 Implicit Arguments Var [var t].
adamc@177 467 Implicit Arguments EUnit [var].
adamc@177 468 Implicit Arguments App [var t1 t2].
adamc@177 469 Implicit Arguments Abs [var t1 t2].
adamc@177 470 Implicit Arguments Pair [var t1 t2].
adamc@177 471 Implicit Arguments EInl [var t1 t2].
adamc@177 472 Implicit Arguments EInr [var t1 t2].
adamc@177 473 Implicit Arguments Case [var t1 t2].
adamc@177 474
adamc@177 475 Notation "# v" := (Var v) (at level 70) : source_scope.
adamc@177 476
adamc@177 477 Notation "()" := EUnit : source_scope.
adamc@177 478
adamc@177 479 Infix "@" := App (left associativity, at level 77) : source_scope.
adamc@177 480 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
adamc@177 481
adamc@179 482 Notation "[ x , y ]" := (Pair x y) : source_scope.
adamc@177 483
adamc@177 484 Notation "'Inl' e" := (EInl e) (at level 71) : source_scope.
adamc@177 485 Notation "'Inr' e" := (EInr e) (at level 71) : source_scope.
adamc@177 486
adamc@178 487 Delimit Scope source_scope with source.
adamc@177 488 Bind Scope source_scope with exp.
adamc@177 489
adamc@221 490 Local Open Scope source_scope.
adamc@177 491
adamc@177 492 Fixpoint typeDenote (t : type) : Set :=
adamc@177 493 match t with
adamc@177 494 | Unit => unit
adamc@177 495 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@177 496 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
adamc@177 497 | t1 ++ t2 => (typeDenote t1 + typeDenote t2)%type
adamc@177 498 end.
adamc@177 499
adamc@177 500 Fixpoint patDenote t ts (p : pat t ts) {struct p} : typeDenote t -> option (hlist typeDenote ts) :=
adamc@177 501 match p in (pat t ts) return (typeDenote t -> option (hlist typeDenote ts)) with
adamc@216 502 | PVar _ => fun v => Some (v ::: HNil)
adamc@177 503 | PPair _ _ _ _ p1 p2 => fun v =>
adamc@177 504 match patDenote p1 (fst v), patDenote p2 (snd v) with
adamc@177 505 | Some tup1, Some tup2 => Some (happ tup1 tup2)
adamc@177 506 | _, _ => None
adamc@177 507 end
adamc@177 508 | PInl _ _ _ p' => fun v =>
adamc@177 509 match v with
adamc@177 510 | inl v' => patDenote p' v'
adamc@177 511 | _ => None
adamc@177 512 end
adamc@177 513 | PInr _ _ _ p' => fun v =>
adamc@177 514 match v with
adamc@177 515 | inr v' => patDenote p' v'
adamc@177 516 | _ => None
adamc@177 517 end
adamc@177 518 end.
adamc@177 519
adamc@177 520 Section matchesDenote.
adamc@177 521 Variables t2 : type.
adamc@177 522 Variable default : typeDenote t2.
adamc@177 523
adamc@177 524 Fixpoint matchesDenote (tss : list (list type))
adamc@177 525 : (forall ts, member ts tss -> option (hlist typeDenote ts))
adamc@177 526 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
adamc@177 527 -> typeDenote t2 :=
adamc@216 528 match tss return (forall ts, member ts tss -> option (hlist typeDenote ts))
adamc@216 529 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
adamc@177 530 -> _ with
adamc@177 531 | nil => fun _ _ =>
adamc@177 532 default
adamc@177 533 | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss') -> option (hlist typeDenote ts'))
adamc@177 534 (bodies : forall ts', member ts' (ts :: tss') -> hlist typeDenote ts' -> typeDenote t2) =>
adamc@216 535 match envs _ HFirst with
adamc@216 536 | None => matchesDenote
adamc@216 537 (fun _ mem => envs _ (HNext mem))
adamc@216 538 (fun _ mem => bodies _ (HNext mem))
adamc@216 539 | Some env => (bodies _ HFirst) env
adamc@177 540 end
adamc@177 541 end.
adamc@177 542 End matchesDenote.
adamc@177 543
adamc@177 544 Implicit Arguments matchesDenote [t2 tss].
adamc@177 545
adamc@177 546 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@177 547 match e in (exp _ t) return (typeDenote t) with
adamc@177 548 | Var _ v => v
adamc@177 549
adamc@177 550 | EUnit => tt
adamc@177 551
adamc@177 552 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@177 553 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@177 554
adamc@177 555 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@177 556
adamc@177 557 | EInl _ _ e' => inl _ (expDenote e')
adamc@177 558 | EInr _ _ e' => inr _ (expDenote e')
adamc@177 559
adamc@177 560 | Case _ _ _ e ps es def =>
adamc@177 561 matchesDenote (expDenote def)
adamc@177 562 (fun _ mem => patDenote (ps _ mem) (expDenote e))
adamc@177 563 (fun _ mem env => expDenote (es _ mem env))
adamc@177 564 end.
adamc@177 565
adamc@177 566 Definition ExpDenote t (E : Exp t) := expDenote (E _).
adamc@177 567 End Source.
adamc@177 568
adamc@177 569 Import Source.
adamc@177 570
adamc@178 571 Module Elab.
adamc@177 572 Section vars.
adamc@177 573 Variable var : type -> Type.
adamc@177 574
adamc@177 575 Inductive exp : type -> Type :=
adamc@177 576 | Var : forall t,
adamc@177 577 var t
adamc@177 578 -> exp t
adamc@177 579
adamc@177 580 | EUnit : exp Unit
adamc@177 581
adamc@177 582 | App : forall t1 t2,
adamc@177 583 exp (t1 --> t2)
adamc@177 584 -> exp t1
adamc@177 585 -> exp t2
adamc@177 586 | Abs : forall t1 t2,
adamc@177 587 (var t1 -> exp t2)
adamc@177 588 -> exp (t1 --> t2)
adamc@177 589
adamc@177 590 | Pair : forall t1 t2,
adamc@177 591 exp t1
adamc@177 592 -> exp t2
adamc@177 593 -> exp (t1 ** t2)
adamc@177 594 | Fst : forall t1 t2,
adamc@177 595 exp (t1 ** t2)
adamc@177 596 -> exp t1
adamc@177 597 | Snd : forall t1 t2,
adamc@177 598 exp (t1 ** t2)
adamc@177 599 -> exp t2
adamc@177 600
adamc@177 601 | EInl : forall t1 t2,
adamc@177 602 exp t1
adamc@177 603 -> exp (t1 ++ t2)
adamc@177 604 | EInr : forall t1 t2,
adamc@177 605 exp t2
adamc@177 606 -> exp (t1 ++ t2)
adamc@177 607 | Case : forall t1 t2 t,
adamc@177 608 exp (t1 ++ t2)
adamc@177 609 -> (var t1 -> exp t)
adamc@177 610 -> (var t2 -> exp t)
adamc@177 611 -> exp t.
adamc@177 612 End vars.
adamc@177 613
adamc@177 614 Definition Exp t := forall var, exp var t.
adamc@177 615
adamc@177 616 Implicit Arguments Var [var t].
adamc@177 617 Implicit Arguments EUnit [var].
adamc@177 618 Implicit Arguments App [var t1 t2].
adamc@177 619 Implicit Arguments Abs [var t1 t2].
adamc@177 620 Implicit Arguments Pair [var t1 t2].
adamc@177 621 Implicit Arguments Fst [var t1 t2].
adamc@177 622 Implicit Arguments Snd [var t1 t2].
adamc@177 623 Implicit Arguments EInl [var t1 t2].
adamc@177 624 Implicit Arguments EInr [var t1 t2].
adamc@177 625 Implicit Arguments Case [var t1 t2 t].
adamc@177 626
adamc@177 627
adamc@177 628 Notation "# v" := (Var v) (at level 70) : elab_scope.
adamc@177 629
adamc@177 630 Notation "()" := EUnit : elab_scope.
adamc@177 631
adamc@177 632 Infix "@" := App (left associativity, at level 77) : elab_scope.
adamc@177 633 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : elab_scope.
adamc@177 634 Notation "\ ? , e" := (Abs (fun _ => e)) (at level 78) : elab_scope.
adamc@177 635
adamc@179 636 Notation "[ x , y ]" := (Pair x y) : elab_scope.
adamc@177 637 Notation "#1 e" := (Fst e) (at level 72) : elab_scope.
adamc@177 638 Notation "#2 e" := (Snd e) (at level 72) : elab_scope.
adamc@177 639
adamc@177 640 Notation "'Inl' e" := (EInl e) (at level 71) : elab_scope.
adamc@177 641 Notation "'Inr' e" := (EInr e) (at level 71) : elab_scope.
adamc@177 642
adamc@177 643 Bind Scope elab_scope with exp.
adamc@177 644 Delimit Scope elab_scope with elab.
adamc@177 645
adamc@177 646 Open Scope elab_scope.
adamc@177 647
adamc@177 648 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@177 649 match e in (exp _ t) return (typeDenote t) with
adamc@177 650 | Var _ v => v
adamc@177 651
adamc@177 652 | EUnit => tt
adamc@177 653
adamc@177 654 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@177 655 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@177 656
adamc@177 657 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@177 658 | Fst _ _ e' => fst (expDenote e')
adamc@177 659 | Snd _ _ e' => snd (expDenote e')
adamc@177 660
adamc@177 661 | EInl _ _ e' => inl _ (expDenote e')
adamc@177 662 | EInr _ _ e' => inr _ (expDenote e')
adamc@177 663 | Case _ _ _ e' e1 e2 =>
adamc@177 664 match expDenote e' with
adamc@177 665 | inl v => expDenote (e1 v)
adamc@177 666 | inr v => expDenote (e2 v)
adamc@177 667 end
adamc@177 668 end.
adamc@177 669
adamc@177 670 Definition ExpDenote t (E : Exp t) := expDenote (E _).
adamc@177 671 End Elab.
adamc@177 672
adamc@178 673 Import Elab.
adamc@178 674
adamc@178 675 Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%source
adamc@178 676 (right associativity, at level 76, e1 at next level) : source_scope.
adamc@178 677 Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%elab
adamc@178 678 (right associativity, at level 76, e1 at next level) : elab_scope.
adamc@178 679
adamc@178 680 Section choice_tree.
adamc@178 681 Open Scope source_scope.
adamc@178 682
adamc@178 683 Fixpoint choice_tree var (t : type) (result : Type) : Type :=
adamc@178 684 match t with
adamc@178 685 | t1 ** t2 =>
adamc@178 686 choice_tree var t1
adamc@178 687 (choice_tree var t2
adamc@178 688 result)
adamc@178 689 | t1 ++ t2 =>
adamc@178 690 choice_tree var t1 result
adamc@178 691 * choice_tree var t2 result
adamc@178 692 | t => exp var t -> result
adamc@178 693 end%type.
adamc@178 694
adamc@178 695 Fixpoint merge var t result {struct t}
adamc@178 696 : (result -> result -> result)
adamc@178 697 -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result :=
adamc@178 698 match t return ((result -> result -> result)
adamc@178 699 -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result) with
adamc@178 700 | _ ** _ => fun mr ct1 ct2 =>
adamc@178 701 merge _ _
adamc@178 702 (merge _ _ mr)
adamc@178 703 ct1 ct2
adamc@178 704
adamc@178 705 | _ ++ _ => fun mr ct1 ct2 =>
adamc@178 706 (merge var _ mr (fst ct1) (fst ct2),
adamc@178 707 merge var _ mr (snd ct1) (snd ct2))
adamc@178 708
adamc@178 709 | _ => fun mr ct1 ct2 e => mr (ct1 e) (ct2 e)
adamc@178 710 end.
adamc@178 711
adamc@178 712 Fixpoint everywhere var t result {struct t}
adamc@178 713 : (exp var t -> result) -> choice_tree var t result :=
adamc@178 714 match t return ((exp var t -> result) -> choice_tree var t result) with
adamc@178 715 | t1 ** t2 => fun r =>
adamc@178 716 everywhere (t := t1) (fun e1 =>
adamc@178 717 everywhere (t := t2) (fun e2 =>
adamc@178 718 r ([e1, e2])%elab))
adamc@178 719
adamc@178 720 | _ ++ _ => fun r =>
adamc@178 721 (everywhere (fun e => r (Inl e)%elab),
adamc@178 722 everywhere (fun e => r (Inr e)%elab))
adamc@178 723
adamc@178 724 | _ => fun r => r
adamc@178 725 end.
adamc@178 726 End choice_tree.
adamc@178 727
adamc@178 728 Implicit Arguments merge [var t result].
adamc@178 729
adamc@178 730 Section elaborate.
adamc@221 731 Local Open Scope elab_scope.
adamc@178 732
adamc@178 733 Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) {struct p} :
adamc@178 734 (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result :=
adamc@178 735 match p in (pat t1 ts) return ((hlist (exp var) ts -> result)
adamc@178 736 -> result -> choice_tree var t1 result) 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@178 759 Fixpoint letify var t ts {struct ts} : (hlist var ts -> exp var t)
adamc@178 760 -> hlist (exp var) ts -> exp var t :=
adamc@178 761 match ts return ((hlist var ts -> exp var t)
adamc@178 762 -> hlist (exp var) ts -> exp var t) with
adamc@216 763 | nil => fun f _ => f HNil
adamc@216 764 | _ :: _ => fun f tup => letify (fun tup' => x <- hhd tup; f (x ::: tup')) (htl tup)
adamc@178 765 end.
adamc@178 766
adamc@178 767 Implicit Arguments letify [var t ts].
adamc@178 768
adamc@178 769 Fixpoint expand var result t1 t2
adamc@178 770 (out : result -> exp var t2) {struct t1}
adamc@178 771 : forall ct : choice_tree var t1 result,
adamc@178 772 exp var t1
adamc@178 773 -> exp var t2 :=
adamc@178 774 match t1 return (forall ct : choice_tree var t1 result, exp var t1
adamc@178 775 -> exp var t2) 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@178 800 (tss : list (list type)) {struct tss}
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@178 804 match tss return (forall ts, member ts tss -> pat t1 ts)
adamc@178 805 -> (forall ts, member ts tss -> _)
adamc@178 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@178 826 Fixpoint elaborate var t (e : Source.exp var t) {struct e} : Elab.exp var t :=
adamc@178 827 match e in (Source.exp _ t) return (Elab.exp var t) 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@179 854 match t return (choice_tree typeDenote t result -> typeDenote t -> result) 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@179 878 Elab.expDenote (expand out ct disc) = Elab.expDenote (out (grab ct (Elab.expDenote disc))).
adamc@179 879 induction t1; my_crush.
adamc@179 880 Qed.
adamc@179 881
adamc@179 882 Lemma recreate_pair : forall t1 t2
adamc@179 883 (x : Elab.exp typeDenote t1)
adamc@179 884 (x0 : Elab.exp typeDenote t2)
adamc@179 885 (v : typeDenote (t1 ** t2)),
adamc@179 886 expDenote x = fst v
adamc@179 887 -> expDenote x0 = snd v
adamc@179 888 -> @eq (typeDenote t1 * typeDenote t2) (expDenote [x, x0]) v.
adamc@179 889 destruct v; crush.
adamc@179 890 Qed.
adamc@179 891
adamc@179 892 Lemma everywhere_correct : forall t1 result
adamc@179 893 (succ : Elab.exp typeDenote t1 -> result) disc,
adamc@179 894 exists disc', grab (everywhere succ) (Elab.expDenote disc) = succ disc'
adamc@179 895 /\ Elab.expDenote disc' = Elab.expDenote disc.
adamc@179 896 Hint Resolve recreate_pair.
adamc@179 897
adamc@179 898 induction t1; my_crush; eauto; fold choice_tree;
adamc@179 899 repeat (fold typeDenote in *; crush;
adamc@179 900 match goal with
adamc@179 901 | [ IH : forall result succ, _ |- context[grab (everywhere ?S) _] ] =>
adamc@179 902 generalize (IH _ S); clear IH
adamc@179 903 | [ e : exp typeDenote (?T ** _), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
adamc@179 904 generalize (IH (#1 e)); clear IH
adamc@179 905 | [ e : exp typeDenote (_ ** ?T), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
adamc@179 906 generalize (IH (#2 e)); clear IH
adamc@179 907 | [ e : typeDenote ?T, IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
adamc@179 908 generalize (IH (#e)); clear IH
adamc@179 909 end; crush); eauto.
adamc@179 910 Qed.
adamc@179 911
adamc@179 912 Lemma merge_correct : forall t result
adamc@179 913 (ct1 ct2 : choice_tree typeDenote t result)
adamc@179 914 (mr : result -> result -> result) v,
adamc@179 915 grab (merge mr ct1 ct2) v = mr (grab ct1 v) (grab ct2 v).
adamc@179 916 induction t; crush.
adamc@179 917 Qed.
adamc@179 918
adamc@179 919 Lemma everywhere_fail : forall t result
adamc@179 920 (fail : result) v,
adamc@179 921 grab (everywhere (fun _ : Elab.exp typeDenote t => fail)) v = fail.
adamc@179 922 induction t; crush.
adamc@179 923 Qed.
adamc@179 924
adamc@179 925 Lemma elaboratePat_correct : forall t1 ts (p : pat t1 ts)
adamc@179 926 result (succ : hlist (Elab.exp typeDenote) ts -> result)
adamc@179 927 (fail : result) v env,
adamc@179 928 patDenote p v = Some env
adamc@216 929 -> exists env', grab (elaboratePat p succ fail) v = succ env'
adamc@179 930 /\ env = hmap Elab.expDenote env'.
adamc@179 931 Hint Resolve hmap_happ.
adamc@179 932
adamc@179 933 induction p; crush; fold choice_tree;
adamc@179 934 repeat (match goal with
adamc@179 935 | [ |- context[grab (everywhere ?succ) ?v] ] =>
adamc@179 936 generalize (everywhere_correct succ (#v)%elab)
adamc@179 937
adamc@216 938 | [ H : forall result succ fail, _ |- context[grab (elaboratePat _ ?S ?F) ?V] ] =>
adamc@179 939 generalize (H _ S F V); clear H
adamc@179 940 | [ H1 : context[match ?E with Some _ => _ | None => _ end],
adamc@216 941 H2 : forall env, ?E = Some env -> _ |- _ ] =>
adamc@216 942 destruct E
adamc@179 943 | [ H : forall env, Some ?E = Some env -> _ |- _ ] =>
adamc@179 944 generalize (H _ (refl_equal _)); clear H
adamc@179 945 end; crush); eauto.
adamc@179 946 Qed.
adamc@179 947
adamc@179 948 Lemma elaboratePat_fails : forall t1 ts (p : pat t1 ts)
adamc@179 949 result (succ : hlist (Elab.exp typeDenote) ts -> result)
adamc@179 950 (fail : result) v,
adamc@179 951 patDenote p v = None
adamc@216 952 -> grab (elaboratePat p succ fail) v = fail.
adamc@179 953 Hint Resolve everywhere_fail.
adamc@179 954
adamc@179 955 induction p; try solve [ crush ];
adamc@179 956 simpl; fold choice_tree; intuition; simpl in *;
adamc@179 957 repeat match goal with
adamc@179 958 | [ IH : forall result succ fail v, patDenote ?P v = _ -> _
adamc@216 959 |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
adamc@179 960 generalize (IH _ S F V); clear IH; intro IH;
adamc@179 961 generalize (elaboratePat_correct P S F V); intros;
adamc@179 962 destruct (patDenote P V); try discriminate
adamc@179 963 | [ H : forall env, Some _ = Some env -> _ |- _ ] =>
adamc@179 964 destruct (H _ (refl_equal _)); clear H; intuition
adamc@179 965 | [ H : _ |- _ ] => rewrite H; intuition
adamc@204 966 | [ |- context[match ?v with inl _ => _ | inr _ => _ end] ] => destruct v; auto
adamc@179 967 end.
adamc@179 968 Qed.
adamc@179 969
adamc@179 970 Implicit Arguments letify [var t ts].
adamc@179 971
adamc@179 972 Lemma letify_correct : forall t ts (f : hlist typeDenote ts -> Elab.exp typeDenote t)
adamc@179 973 (env : hlist (Elab.exp typeDenote) ts),
adamc@179 974 Elab.expDenote (letify f env)
adamc@179 975 = Elab.expDenote (f (hmap Elab.expDenote env)).
adamc@216 976 induction ts; crush; dep_destruct env; crush.
adamc@179 977 Qed.
adamc@179 978
adamc@179 979 Theorem elaborate_correct : forall t (e : Source.exp typeDenote t),
adamc@179 980 Elab.expDenote (elaborate e) = Source.expDenote e.
adamc@179 981 Hint Rewrite expand_grab merge_correct letify_correct : cpdt.
adamc@179 982 Hint Rewrite everywhere_fail elaboratePat_fails using assumption : cpdt.
adamc@179 983
adamc@179 984 induction e; crush; try (ext_eq; crush);
adamc@179 985 match goal with
adamc@179 986 | [ tss : list (list type) |- _ ] =>
adamc@179 987 induction tss; crush;
adamc@179 988 match goal with
adamc@216 989 | [ |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
adamc@179 990 case_eq (patDenote P V); [intros env Heq;
adamc@179 991 destruct (elaboratePat_correct P S F _ Heq); crush;
adamc@179 992 match goal with
adamc@179 993 | [ H : _ |- _ ] => rewrite <- H; crush
adamc@179 994 end
adamc@179 995 | crush ]
adamc@179 996 end
adamc@179 997 end.
adamc@179 998 Qed.
adamc@179 999
adamc@179 1000 Theorem Elaborate_correct : forall t (E : Source.Exp t),
adamc@179 1001 Elab.ExpDenote (Elaborate E) = Source.ExpDenote E.
adamc@179 1002 unfold Elab.ExpDenote, Elaborate, Source.ExpDenote;
adamc@179 1003 intros; apply elaborate_correct.
adamc@179 1004 Qed.
adamc@179 1005
adamc@177 1006 End PatMatch.
adamc@181 1007
adamc@181 1008
adamc@181 1009 (** * Exercises *)
adamc@181 1010
adamc@181 1011 (** %\begin{enumerate}%#<ol>#
adamc@181 1012
adamc@181 1013 %\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 1014
adamc@181 1015 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 1016
adamc@200 1017 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 1018 #</li>#
adamc@181 1019
adamc@181 1020 #</ol>#%\end{enumerate}% *)