Mercurial > cpdt > repo

annotate src/Extensional.v @ 179:8f3fc56b90d4

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