Mercurial > cpdt > repo

annotate src/Extensional.v @ 180:de33d1ed7c63

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Templatize Extensional
author Adam Chlipala <adamc@hcoop.net>
date Mon, 10 Nov 2008 14:17:26 -0500
parents 8f3fc56b90d4
children ec44782bffdd
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@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@176 111 | EqEVar : 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@176 115 | EqEConst : forall G n,
adamc@176 116 exp_equiv G (^n) (^n)
adamc@176 117 | EqEPlus : 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@176 122 | EqEApp : 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@176 126 | EqEAbs : 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@177 490 Open Local 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@177 502 | PVar _ => fun v => Some (v, tt)
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@177 528 match tss return (forall ts, member ts tss -> _)
adamc@177 529 -> (forall ts, member ts tss -> _)
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@177 535 match envs _ (hfirst (refl_equal _)) with
adamc@177 536 | None => matchesDenote tss'
adamc@177 537 (fun _ mem => envs _ (hnext mem))
adamc@177 538 (fun _ mem => bodies _ (hnext mem))
adamc@177 539 | Some env => (bodies _ (hfirst (refl_equal _))) 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@178 731 Open Local 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@178 738 everywhere (fun disc => succ (disc, tt))
adamc@178 739
adamc@178 740 | PPair _ _ _ _ p1 p2 => fun succ fail =>
adamc@178 741 elaboratePat _ p1
adamc@178 742 (fun tup1 =>
adamc@178 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@178 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@178 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@178 763 | nil => fun f _ => f tt
adamc@178 764 | _ :: _ => fun f tup => letify _ (fun tup' => x <- fst tup; f (x, tup')) (snd 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@178 812 (elaboratePat (ps _ (hfirst (refl_equal _)))
adamc@178 813 (fun ts => Some (letify
adamc@178 814 (fun ts' => es _ (hfirst (refl_equal _)) ts')
adamc@178 815 ts))
adamc@178 816 None)
adamc@178 817 (elaborateMatches tss'
adamc@178 818 (fun _ mem => ps _ (hnext mem))
adamc@178 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@179 929 -> exists env', grab (elaboratePat typeDenote 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@179 938 | [ H : forall result sudc 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@179 941 H2 : forall env, ?E = Some env -> _ |- _ ] =>
adamc@179 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@179 952 -> grab (elaboratePat typeDenote 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@179 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@179 966 end.
adamc@179 967 Qed.
adamc@179 968
adamc@179 969 Implicit Arguments letify [var t ts].
adamc@179 970
adamc@179 971 Lemma letify_correct : forall t ts (f : hlist typeDenote ts -> Elab.exp typeDenote t)
adamc@179 972 (env : hlist (Elab.exp typeDenote) ts),
adamc@179 973 Elab.expDenote (letify f env)
adamc@179 974 = Elab.expDenote (f (hmap Elab.expDenote env)).
adamc@179 975 induction ts; crush.
adamc@179 976 Qed.
adamc@179 977
adamc@179 978 Theorem elaborate_correct : forall t (e : Source.exp typeDenote t),
adamc@179 979 Elab.expDenote (elaborate e) = Source.expDenote e.
adamc@179 980 Hint Rewrite expand_grab merge_correct letify_correct : cpdt.
adamc@179 981 Hint Rewrite everywhere_fail elaboratePat_fails using assumption : cpdt.
adamc@179 982
adamc@179 983 induction e; crush; try (ext_eq; crush);
adamc@179 984 match goal with
adamc@179 985 | [ tss : list (list type) |- _ ] =>
adamc@179 986 induction tss; crush;
adamc@179 987 match goal with
adamc@179 988 | [ |- context[grab (elaboratePat _ ?P ?S ?F) ?V] ] =>
adamc@179 989 case_eq (patDenote P V); [intros env Heq;
adamc@179 990 destruct (elaboratePat_correct P S F _ Heq); crush;
adamc@179 991 match goal with
adamc@179 992 | [ H : _ |- _ ] => rewrite <- H; crush
adamc@179 993 end
adamc@179 994 | crush ]
adamc@179 995 end
adamc@179 996 end.
adamc@179 997 Qed.
adamc@179 998
adamc@179 999 Theorem Elaborate_correct : forall t (E : Source.Exp t),
adamc@179 1000 Elab.ExpDenote (Elaborate E) = Source.ExpDenote E.
adamc@179 1001 unfold Elab.ExpDenote, Elaborate, Source.ExpDenote;
adamc@179 1002 intros; apply elaborate_correct.
adamc@179 1003 Qed.
adamc@179 1004
adamc@177 1005 End PatMatch.