Mercurial > cpdt > repo

annotate src/Intensional.v @ 185:303e9d866597

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ccTerm_correct
author Adam Chlipala <adamc@hcoop.net>
date Sun, 16 Nov 2008 19:42:32 -0500
parents 699fd70c04a7
children ecd231ba5c8b
rev   line source
adamc@182 1 (* Copyright (c) 2008, Adam Chlipala
adamc@182 2 *
adamc@182 3 * This work is licensed under a
adamc@182 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@182 5 * Unported License.
adamc@182 6 * The license text is available at:
adamc@182 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@182 8 *)
adamc@182 9
adamc@182 10 (* begin hide *)
adamc@184 11 Require Import Arith Bool String List Eqdep JMeq.
adamc@182 12
adamc@182 13 Require Import Axioms Tactics DepList.
adamc@182 14
adamc@182 15 Set Implicit Arguments.
adamc@184 16
adamc@184 17 Infix "==" := JMeq (at level 70, no associativity).
adamc@182 18 (* end hide *)
adamc@182 19
adamc@182 20
adamc@184 21
adamc@184 22
adamc@182 23 (** %\chapter{Intensional Transformations}% *)
adamc@182 24
adamc@182 25 (** TODO: Prose for this chapter *)
adamc@182 26
adamc@182 27
adamc@182 28 (** * Closure Conversion *)
adamc@182 29
adamc@182 30 Module Source.
adamc@182 31 Inductive type : Type :=
adamc@182 32 | TNat : type
adamc@182 33 | Arrow : type -> type -> type.
adamc@182 34
adamc@182 35 Notation "'Nat'" := TNat : source_scope.
adamc@182 36 Infix "-->" := Arrow (right associativity, at level 60) : source_scope.
adamc@182 37
adamc@182 38 Open Scope source_scope.
adamc@182 39 Bind Scope source_scope with type.
adamc@182 40 Delimit Scope source_scope with source.
adamc@182 41
adamc@182 42 Section vars.
adamc@182 43 Variable var : type -> Type.
adamc@182 44
adamc@182 45 Inductive exp : type -> Type :=
adamc@182 46 | Var : forall t,
adamc@182 47 var t
adamc@182 48 -> exp t
adamc@182 49
adamc@182 50 | Const : nat -> exp Nat
adamc@182 51 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@182 52
adamc@182 53 | App : forall t1 t2,
adamc@182 54 exp (t1 --> t2)
adamc@182 55 -> exp t1
adamc@182 56 -> exp t2
adamc@182 57 | Abs : forall t1 t2,
adamc@182 58 (var t1 -> exp t2)
adamc@182 59 -> exp (t1 --> t2).
adamc@182 60 End vars.
adamc@182 61
adamc@182 62 Definition Exp t := forall var, exp var t.
adamc@182 63
adamc@182 64 Implicit Arguments Var [var t].
adamc@182 65 Implicit Arguments Const [var].
adamc@182 66 Implicit Arguments Plus [var].
adamc@182 67 Implicit Arguments App [var t1 t2].
adamc@182 68 Implicit Arguments Abs [var t1 t2].
adamc@182 69
adamc@182 70 Notation "# v" := (Var v) (at level 70) : source_scope.
adamc@182 71
adamc@182 72 Notation "^ n" := (Const n) (at level 70) : source_scope.
adamc@182 73 Infix "+^" := Plus (left associativity, at level 79) : source_scope.
adamc@182 74
adamc@182 75 Infix "@" := App (left associativity, at level 77) : source_scope.
adamc@182 76 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
adamc@182 77 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope.
adamc@182 78
adamc@182 79 Bind Scope source_scope with exp.
adamc@182 80
adamc@182 81 Definition zero : Exp Nat := fun _ => ^0.
adamc@182 82 Definition one : Exp Nat := fun _ => ^1.
adamc@182 83 Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
adamc@182 84 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
adamc@182 85 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
adamc@182 86 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
adamc@182 87 \f, \x, #f @ #x.
adamc@182 88 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
adamc@182 89
adamc@182 90 Fixpoint typeDenote (t : type) : Set :=
adamc@182 91 match t with
adamc@182 92 | Nat => nat
adamc@182 93 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@182 94 end.
adamc@182 95
adamc@182 96 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@182 97 match e in (exp _ t) return (typeDenote t) with
adamc@182 98 | Var _ v => v
adamc@182 99
adamc@182 100 | Const n => n
adamc@182 101 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@182 102
adamc@182 103 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@182 104 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@182 105 end.
adamc@182 106
adamc@182 107 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@182 108
adamc@182 109 Section exp_equiv.
adamc@182 110 Variables var1 var2 : type -> Type.
adamc@182 111
adamc@182 112 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop :=
adamc@182 113 | EqVar : forall G t (v1 : var1 t) v2,
adamc@182 114 In (existT _ t (v1, v2)) G
adamc@182 115 -> exp_equiv G (#v1) (#v2)
adamc@182 116
adamc@182 117 | EqConst : forall G n,
adamc@182 118 exp_equiv G (^n) (^n)
adamc@182 119 | EqPlus : forall G x1 y1 x2 y2,
adamc@182 120 exp_equiv G x1 x2
adamc@182 121 -> exp_equiv G y1 y2
adamc@182 122 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
adamc@182 123
adamc@182 124 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
adamc@182 125 exp_equiv G f1 f2
adamc@182 126 -> exp_equiv G x1 x2
adamc@182 127 -> exp_equiv G (f1 @ x1) (f2 @ x2)
adamc@182 128 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
adamc@182 129 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
adamc@182 130 -> exp_equiv G (Abs f1) (Abs f2).
adamc@182 131 End exp_equiv.
adamc@182 132
adamc@182 133 Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
adamc@182 134 exp_equiv nil (E var1) (E var2).
adamc@182 135 End Source.
adamc@182 136
adamc@183 137 Module Closed.
adamc@182 138 Inductive type : Type :=
adamc@182 139 | TNat : type
adamc@182 140 | Arrow : type -> type -> type
adamc@182 141 | Code : type -> type -> type -> type
adamc@182 142 | Prod : type -> type -> type
adamc@182 143 | TUnit : type.
adamc@182 144
adamc@182 145 Notation "'Nat'" := TNat : cc_scope.
adamc@182 146 Notation "'Unit'" := TUnit : cc_scope.
adamc@182 147 Infix "-->" := Arrow (right associativity, at level 60) : cc_scope.
adamc@182 148 Infix "**" := Prod (right associativity, at level 59) : cc_scope.
adamc@182 149 Notation "env @@ dom ---> ran" := (Code env dom ran) (no associativity, at level 62, dom at next level) : cc_scope.
adamc@182 150
adamc@182 151 Bind Scope cc_scope with type.
adamc@182 152 Delimit Scope cc_scope with cc.
adamc@182 153
adamc@182 154 Open Local Scope cc_scope.
adamc@182 155
adamc@182 156 Section vars.
adamc@182 157 Variable var : type -> Set.
adamc@182 158
adamc@182 159 Inductive exp : type -> Type :=
adamc@182 160 | Var : forall t,
adamc@182 161 var t
adamc@182 162 -> exp t
adamc@182 163
adamc@182 164 | Const : nat -> exp Nat
adamc@182 165 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@182 166
adamc@182 167 | App : forall dom ran,
adamc@182 168 exp (dom --> ran)
adamc@182 169 -> exp dom
adamc@182 170 -> exp ran
adamc@182 171
adamc@182 172 | Pack : forall env dom ran,
adamc@182 173 exp (env @@ dom ---> ran)
adamc@182 174 -> exp env
adamc@182 175 -> exp (dom --> ran)
adamc@182 176
adamc@182 177 | EUnit : exp Unit
adamc@182 178
adamc@182 179 | Pair : forall t1 t2,
adamc@182 180 exp t1
adamc@182 181 -> exp t2
adamc@182 182 -> exp (t1 ** t2)
adamc@182 183 | Fst : forall t1 t2,
adamc@182 184 exp (t1 ** t2)
adamc@182 185 -> exp t1
adamc@182 186 | Snd : forall t1 t2,
adamc@182 187 exp (t1 ** t2)
adamc@183 188 -> exp t2
adamc@183 189
adamc@183 190 | Let : forall t1 t2,
adamc@183 191 exp t1
adamc@183 192 -> (var t1 -> exp t2)
adamc@182 193 -> exp t2.
adamc@182 194
adamc@182 195 Section funcs.
adamc@182 196 Variable T : Type.
adamc@182 197
adamc@182 198 Inductive funcs : Type :=
adamc@182 199 | Main : T -> funcs
adamc@182 200 | Abs : forall env dom ran,
adamc@182 201 (var env -> var dom -> exp ran)
adamc@182 202 -> (var (env @@ dom ---> ran) -> funcs)
adamc@182 203 -> funcs.
adamc@182 204 End funcs.
adamc@182 205
adamc@182 206 Definition prog t := funcs (exp t).
adamc@182 207 End vars.
adamc@182 208
adamc@182 209 Implicit Arguments Var [var t].
adamc@182 210 Implicit Arguments Const [var].
adamc@182 211 Implicit Arguments EUnit [var].
adamc@182 212 Implicit Arguments Fst [var t1 t2].
adamc@182 213 Implicit Arguments Snd [var t1 t2].
adamc@182 214
adamc@182 215 Implicit Arguments Main [var T].
adamc@182 216 Implicit Arguments Abs [var T env dom ran].
adamc@182 217
adamc@182 218 Notation "# v" := (Var v) (at level 70) : cc_scope.
adamc@182 219
adamc@182 220 Notation "^ n" := (Const n) (at level 70) : cc_scope.
adamc@182 221 Infix "+^" := Plus (left associativity, at level 79) : cc_scope.
adamc@182 222
adamc@183 223 Infix "@" := App (left associativity, at level 77) : cc_scope.
adamc@182 224 Infix "##" := Pack (no associativity, at level 71) : cc_scope.
adamc@182 225
adamc@182 226 Notation "()" := EUnit : cc_scope.
adamc@182 227
adamc@182 228 Notation "[ x1 , x2 ]" := (Pair x1 x2) (at level 73) : cc_scope.
adamc@182 229 Notation "#1 x" := (Fst x) (at level 72) : cc_scope.
adamc@182 230 Notation "#2 x" := (Snd x) (at level 72) : cc_scope.
adamc@182 231
adamc@183 232 Notation "f <== \\ x , y , e ; fs" :=
adamc@182 233 (Abs (fun x y => e) (fun f => fs))
adamc@182 234 (right associativity, at level 80, e at next level) : cc_scope.
adamc@182 235
adamc@183 236 Notation "x <- e1 ; e2" := (Let e1 (fun x => e2))
adamc@183 237 (right associativity, at level 80, e1 at next level) : cc_scope.
adamc@183 238
adamc@182 239 Bind Scope cc_scope with exp funcs prog.
adamc@182 240
adamc@182 241 Fixpoint typeDenote (t : type) : Set :=
adamc@182 242 match t with
adamc@182 243 | Nat => nat
adamc@182 244 | Unit => unit
adamc@182 245 | dom --> ran => typeDenote dom -> typeDenote ran
adamc@182 246 | t1 ** t2 => typeDenote t1 * typeDenote t2
adamc@182 247 | env @@ dom ---> ran => typeDenote env -> typeDenote dom -> typeDenote ran
adamc@182 248 end%type.
adamc@182 249
adamc@182 250 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@182 251 match e in (exp _ t) return (typeDenote t) with
adamc@182 252 | Var _ v => v
adamc@182 253
adamc@182 254 | Const n => n
adamc@182 255 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@182 256
adamc@182 257 | App _ _ f x => (expDenote f) (expDenote x)
adamc@182 258 | Pack _ _ _ f env => (expDenote f) (expDenote env)
adamc@182 259
adamc@182 260 | EUnit => tt
adamc@182 261
adamc@182 262 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@182 263 | Fst _ _ e' => fst (expDenote e')
adamc@182 264 | Snd _ _ e' => snd (expDenote e')
adamc@183 265
adamc@183 266 | Let _ _ e1 e2 => expDenote (e2 (expDenote e1))
adamc@182 267 end.
adamc@182 268
adamc@182 269 Fixpoint funcsDenote T (fs : funcs typeDenote T) : T :=
adamc@182 270 match fs with
adamc@182 271 | Main v => v
adamc@182 272 | Abs _ _ _ e fs =>
adamc@182 273 funcsDenote (fs (fun env arg => expDenote (e env arg)))
adamc@182 274 end.
adamc@182 275
adamc@182 276 Definition progDenote t (p : prog typeDenote t) : typeDenote t :=
adamc@182 277 expDenote (funcsDenote p).
adamc@182 278
adamc@182 279 Definition Exp t := forall var, exp var t.
adamc@182 280 Definition Prog t := forall var, prog var t.
adamc@182 281
adamc@182 282 Definition ExpDenote t (E : Exp t) := expDenote (E _).
adamc@182 283 Definition ProgDenote t (P : Prog t) := progDenote (P _).
adamc@182 284 End Closed.
adamc@182 285
adamc@183 286 Import Source Closed.
adamc@183 287
adamc@183 288 Section splice.
adamc@183 289 Open Local Scope cc_scope.
adamc@183 290
adamc@183 291 Fixpoint spliceFuncs var T1 (fs : funcs var T1)
adamc@183 292 T2 (f : T1 -> funcs var T2) {struct fs} : funcs var T2 :=
adamc@183 293 match fs with
adamc@183 294 | Main v => f v
adamc@183 295 | Abs _ _ _ e fs' => Abs e (fun x => spliceFuncs (fs' x) f)
adamc@183 296 end.
adamc@183 297 End splice.
adamc@183 298
adamc@183 299 Notation "x <-- e1 ; e2" := (spliceFuncs e1 (fun x => e2))
adamc@183 300 (right associativity, at level 80, e1 at next level) : cc_scope.
adamc@183 301
adamc@183 302 Definition natvar (_ : Source.type) := nat.
adamc@183 303 Definition isfree := hlist (fun (_ : Source.type) => bool).
adamc@183 304
adamc@183 305 Ltac maybe_destruct E :=
adamc@183 306 match goal with
adamc@183 307 | [ x : _ |- _ ] =>
adamc@183 308 match E with
adamc@183 309 | x => idtac
adamc@183 310 end
adamc@183 311 | _ =>
adamc@183 312 match E with
adamc@183 313 | eq_nat_dec _ _ => idtac
adamc@183 314 end
adamc@183 315 end; destruct E.
adamc@183 316
adamc@183 317 Ltac my_crush :=
adamc@183 318 crush; repeat (match goal with
adamc@183 319 | [ x : (_ * _)%type |- _ ] => destruct x
adamc@183 320 | [ |- context[if ?B then _ else _] ] => maybe_destruct B
adamc@183 321 | [ _ : context[if ?B then _ else _] |- _ ] => maybe_destruct B
adamc@183 322 end; crush).
adamc@183 323
adamc@183 324 Section isfree.
adamc@183 325 Import Source.
adamc@183 326 Open Local Scope source_scope.
adamc@183 327
adamc@183 328 Hint Extern 3 False => omega.
adamc@183 329
adamc@183 330 Fixpoint lookup_type (envT : list Source.type) (n : nat) {struct envT}
adamc@183 331 : isfree envT -> option Source.type :=
adamc@183 332 match envT return (isfree envT -> _) with
adamc@183 333 | nil => fun _ => None
adamc@183 334 | first :: rest => fun fvs =>
adamc@183 335 if eq_nat_dec n (length rest)
adamc@183 336 then match fvs with
adamc@183 337 | (true, _) => Some first
adamc@183 338 | (false, _) => None
adamc@183 339 end
adamc@183 340 else lookup_type rest n (snd fvs)
adamc@183 341 end.
adamc@183 342
adamc@183 343 Implicit Arguments lookup_type [envT].
adamc@183 344
adamc@183 345 Notation ok := (fun (envT : list Source.type) (fvs : isfree envT)
adamc@183 346 (n : nat) (t : Source.type)
adamc@183 347 => lookup_type n fvs = Some t).
adamc@183 348
adamc@183 349 Fixpoint wfExp (envT : list Source.type) (fvs : isfree envT)
adamc@183 350 t (e : Source.exp natvar t) {struct e} : Prop :=
adamc@183 351 match e with
adamc@183 352 | Var t v => ok envT fvs v t
adamc@183 353
adamc@183 354 | Const _ => True
adamc@183 355 | Plus e1 e2 => wfExp envT fvs e1 /\ wfExp envT fvs e2
adamc@183 356
adamc@183 357 | App _ _ e1 e2 => wfExp envT fvs e1 /\ wfExp envT fvs e2
adamc@183 358 | Abs dom _ e' => wfExp (dom :: envT) (true ::: fvs) (e' (length envT))
adamc@183 359 end.
adamc@183 360
adamc@183 361 Implicit Arguments wfExp [envT t].
adamc@183 362
adamc@183 363 Theorem wfExp_weaken : forall t (e : exp natvar t) envT (fvs fvs' : isfree envT),
adamc@183 364 wfExp fvs e
adamc@183 365 -> (forall n t, ok _ fvs n t -> ok _ fvs' n t)
adamc@183 366 -> wfExp fvs' e.
adamc@183 367 Hint Extern 1 (lookup_type (envT := _ :: _) _ _ = Some _) =>
adamc@183 368 simpl in *; my_crush.
adamc@183 369
adamc@183 370 induction e; my_crush; eauto.
adamc@183 371 Defined.
adamc@183 372
adamc@183 373 Fixpoint isfree_none (envT : list Source.type) : isfree envT :=
adamc@183 374 match envT return (isfree envT) with
adamc@183 375 | nil => tt
adamc@183 376 | _ :: _ => (false, isfree_none _)
adamc@183 377 end.
adamc@183 378
adamc@183 379 Implicit Arguments isfree_none [envT].
adamc@183 380
adamc@183 381 Fixpoint isfree_one (envT : list Source.type) (n : nat) {struct envT} : isfree envT :=
adamc@183 382 match envT return (isfree envT) with
adamc@183 383 | nil => tt
adamc@183 384 | _ :: rest =>
adamc@183 385 if eq_nat_dec n (length rest)
adamc@183 386 then (true, isfree_none)
adamc@183 387 else (false, isfree_one _ n)
adamc@183 388 end.
adamc@183 389
adamc@183 390 Implicit Arguments isfree_one [envT].
adamc@183 391
adamc@183 392 Fixpoint isfree_merge (envT : list Source.type) : isfree envT -> isfree envT -> isfree envT :=
adamc@183 393 match envT return (isfree envT -> isfree envT -> isfree envT) with
adamc@183 394 | nil => fun _ _ => tt
adamc@183 395 | _ :: _ => fun fv1 fv2 => (fst fv1 || fst fv2, isfree_merge _ (snd fv1) (snd fv2))
adamc@183 396 end.
adamc@183 397
adamc@183 398 Implicit Arguments isfree_merge [envT].
adamc@183 399
adamc@183 400 Fixpoint fvsExp t (e : exp natvar t)
adamc@183 401 (envT : list Source.type) {struct e} : isfree envT :=
adamc@183 402 match e with
adamc@183 403 | Var _ n => isfree_one n
adamc@183 404
adamc@183 405 | Const _ => isfree_none
adamc@183 406 | Plus e1 e2 => isfree_merge (fvsExp e1 envT) (fvsExp e2 envT)
adamc@183 407
adamc@183 408 | App _ _ e1 e2 => isfree_merge (fvsExp e1 envT) (fvsExp e2 envT)
adamc@183 409 | Abs dom _ e' => snd (fvsExp (e' (length envT)) (dom :: envT))
adamc@183 410 end.
adamc@183 411
adamc@183 412 Lemma isfree_one_correct : forall t (v : natvar t) envT fvs,
adamc@183 413 ok envT fvs v t
adamc@183 414 -> ok envT (isfree_one (envT:=envT) v) v t.
adamc@183 415 induction envT; my_crush; eauto.
adamc@183 416 Defined.
adamc@183 417
adamc@183 418 Lemma isfree_merge_correct1 : forall t (v : natvar t) envT fvs1 fvs2,
adamc@183 419 ok envT fvs1 v t
adamc@183 420 -> ok envT (isfree_merge (envT:=envT) fvs1 fvs2) v t.
adamc@183 421 induction envT; my_crush; eauto.
adamc@183 422 Defined.
adamc@183 423
adamc@183 424 Hint Rewrite orb_true_r : cpdt.
adamc@183 425
adamc@183 426 Lemma isfree_merge_correct2 : forall t (v : natvar t) envT fvs1 fvs2,
adamc@183 427 ok envT fvs2 v t
adamc@183 428 -> ok envT (isfree_merge (envT:=envT) fvs1 fvs2) v t.
adamc@183 429 induction envT; my_crush; eauto.
adamc@183 430 Defined.
adamc@183 431
adamc@183 432 Hint Resolve isfree_one_correct isfree_merge_correct1 isfree_merge_correct2.
adamc@183 433
adamc@183 434 Lemma fvsExp_correct : forall t (e : exp natvar t)
adamc@183 435 envT (fvs : isfree envT), wfExp fvs e
adamc@183 436 -> forall (fvs' : isfree envT),
adamc@183 437 (forall v t, ok envT (fvsExp e envT) v t -> ok envT fvs' v t)
adamc@183 438 -> wfExp fvs' e.
adamc@183 439 Hint Extern 1 (_ = _) =>
adamc@183 440 match goal with
adamc@183 441 | [ H : lookup_type _ (fvsExp ?X ?Y) = _ |- _ ] =>
adamc@183 442 destruct (fvsExp X Y); my_crush
adamc@183 443 end.
adamc@183 444
adamc@183 445 induction e; my_crush; eauto.
adamc@183 446 Defined.
adamc@183 447
adamc@183 448 Lemma lookup_type_unique : forall v t1 t2 envT (fvs1 fvs2 : isfree envT),
adamc@183 449 lookup_type v fvs1 = Some t1
adamc@183 450 -> lookup_type v fvs2 = Some t2
adamc@183 451 -> t1 = t2.
adamc@183 452 induction envT; my_crush; eauto.
adamc@183 453 Defined.
adamc@183 454
adamc@183 455 Implicit Arguments lookup_type_unique [v t1 t2 envT fvs1 fvs2].
adamc@183 456
adamc@183 457 Hint Extern 2 (lookup_type _ _ = Some _) =>
adamc@183 458 match goal with
adamc@183 459 | [ H1 : lookup_type ?v _ = Some _,
adamc@183 460 H2 : lookup_type ?v _ = Some _ |- _ ] =>
adamc@183 461 (generalize (lookup_type_unique H1 H2); intro; subst)
adamc@183 462 || rewrite <- (lookup_type_unique H1 H2)
adamc@183 463 end.
adamc@183 464
adamc@183 465 Lemma lookup_none : forall v t envT,
adamc@183 466 lookup_type (envT:=envT) v (isfree_none (envT:=envT)) = Some t
adamc@183 467 -> False.
adamc@183 468 induction envT; my_crush.
adamc@183 469 Defined.
adamc@183 470
adamc@183 471 Hint Extern 2 (_ = _) => elimtype False; eapply lookup_none; eassumption.
adamc@183 472
adamc@183 473 Lemma lookup_one : forall v' v t envT,
adamc@183 474 lookup_type (envT:=envT) v' (isfree_one (envT:=envT) v) = Some t
adamc@183 475 -> v' = v.
adamc@183 476 induction envT; my_crush.
adamc@183 477 Defined.
adamc@183 478
adamc@183 479 Implicit Arguments lookup_one [v' v t envT].
adamc@183 480
adamc@183 481 Hint Extern 2 (lookup_type _ _ = Some _) =>
adamc@183 482 match goal with
adamc@183 483 | [ H : lookup_type _ _ = Some _ |- _ ] =>
adamc@183 484 generalize (lookup_one H); intro; subst
adamc@183 485 end.
adamc@183 486
adamc@183 487 Lemma lookup_merge : forall v t envT (fvs1 fvs2 : isfree envT),
adamc@183 488 lookup_type v (isfree_merge fvs1 fvs2) = Some t
adamc@183 489 -> lookup_type v fvs1 = Some t
adamc@183 490 \/ lookup_type v fvs2 = Some t.
adamc@183 491 induction envT; my_crush.
adamc@183 492 Defined.
adamc@183 493
adamc@183 494 Implicit Arguments lookup_merge [v t envT fvs1 fvs2].
adamc@183 495
adamc@183 496 Lemma lookup_bound : forall v t envT (fvs : isfree envT),
adamc@183 497 lookup_type v fvs = Some t
adamc@183 498 -> v < length envT.
adamc@183 499 Hint Resolve lt_S.
adamc@183 500 induction envT; my_crush; eauto.
adamc@183 501 Defined.
adamc@183 502
adamc@183 503 Hint Resolve lookup_bound.
adamc@183 504
adamc@183 505 Lemma lookup_bound_contra : forall t envT (fvs : isfree envT),
adamc@183 506 lookup_type (length envT) fvs = Some t
adamc@183 507 -> False.
adamc@183 508 intros; assert (length envT < length envT); eauto.
adamc@183 509 Defined.
adamc@183 510
adamc@183 511 Hint Resolve lookup_bound_contra.
adamc@183 512
adamc@183 513 Hint Extern 3 (_ = _) => elimtype False; omega.
adamc@183 514
adamc@183 515 Lemma lookup_push_drop : forall v t t' envT fvs,
adamc@183 516 v < length envT
adamc@183 517 -> lookup_type (envT := t :: envT) v (true, fvs) = Some t'
adamc@183 518 -> lookup_type (envT := envT) v fvs = Some t'.
adamc@183 519 my_crush.
adamc@183 520 Defined.
adamc@183 521
adamc@183 522 Lemma lookup_push_add : forall v t t' envT fvs,
adamc@183 523 lookup_type (envT := envT) v (snd fvs) = Some t'
adamc@183 524 -> lookup_type (envT := t :: envT) v fvs = Some t'.
adamc@183 525 my_crush; elimtype False; eauto.
adamc@183 526 Defined.
adamc@183 527
adamc@183 528 Hint Resolve lookup_bound lookup_push_drop lookup_push_add.
adamc@183 529
adamc@183 530 Theorem fvsExp_minimal : forall t (e : exp natvar t)
adamc@183 531 envT (fvs : isfree envT), wfExp fvs e
adamc@183 532 -> (forall v t, ok envT (fvsExp e envT) v t -> ok envT fvs v t).
adamc@183 533 Hint Extern 1 (_ = _) =>
adamc@183 534 match goal with
adamc@183 535 | [ H : lookup_type _ (isfree_merge _ _) = Some _ |- _ ] =>
adamc@183 536 destruct (lookup_merge H); clear H; eauto
adamc@183 537 end.
adamc@183 538
adamc@183 539 induction e; my_crush; eauto.
adamc@183 540 Defined.
adamc@183 541
adamc@183 542 Fixpoint ccType (t : Source.type) : Closed.type :=
adamc@183 543 match t with
adamc@183 544 | Nat%source => Nat
adamc@183 545 | (dom --> ran)%source => ccType dom --> ccType ran
adamc@183 546 end%cc.
adamc@183 547
adamc@183 548 Open Local Scope cc_scope.
adamc@183 549
adamc@183 550 Fixpoint envType (envT : list Source.type) : isfree envT -> Closed.type :=
adamc@183 551 match envT return (isfree envT -> _) with
adamc@183 552 | nil => fun _ => Unit
adamc@183 553 | t :: _ => fun tup =>
adamc@183 554 if fst tup
adamc@183 555 then ccType t ** envType _ (snd tup)
adamc@183 556 else envType _ (snd tup)
adamc@183 557 end.
adamc@183 558
adamc@183 559 Implicit Arguments envType [envT].
adamc@183 560
adamc@183 561 Fixpoint envOf (var : Closed.type -> Set) (envT : list Source.type) {struct envT}
adamc@183 562 : isfree envT -> Set :=
adamc@183 563 match envT return (isfree envT -> _) with
adamc@183 564 | nil => fun _ => unit
adamc@183 565 | first :: rest => fun fvs =>
adamc@183 566 match fvs with
adamc@183 567 | (true, fvs') => (var (ccType first) * envOf var rest fvs')%type
adamc@183 568 | (false, fvs') => envOf var rest fvs'
adamc@183 569 end
adamc@183 570 end.
adamc@183 571
adamc@183 572 Implicit Arguments envOf [envT].
adamc@183 573
adamc@183 574 Notation "var <| to" := (match to with
adamc@183 575 | None => unit
adamc@183 576 | Some t => var (ccType t)
adamc@183 577 end) (no associativity, at level 70).
adamc@183 578
adamc@183 579 Fixpoint lookup (var : Closed.type -> Set) (envT : list Source.type) :
adamc@183 580 forall (n : nat) (fvs : isfree envT), envOf var fvs -> var <| lookup_type n fvs :=
adamc@183 581 match envT return (forall (n : nat) (fvs : isfree envT), envOf var fvs
adamc@183 582 -> var <| lookup_type n fvs) with
adamc@183 583 | nil => fun _ _ _ => tt
adamc@183 584 | first :: rest => fun n fvs =>
adamc@183 585 match (eq_nat_dec n (length rest)) as Heq return
adamc@183 586 (envOf var (envT := first :: rest) fvs
adamc@183 587 -> var <| (if Heq
adamc@183 588 then match fvs with
adamc@183 589 | (true, _) => Some first
adamc@183 590 | (false, _) => None
adamc@183 591 end
adamc@183 592 else lookup_type n (snd fvs))) with
adamc@183 593 | left _ =>
adamc@183 594 match fvs return (envOf var (envT := first :: rest) fvs
adamc@183 595 -> var <| (match fvs with
adamc@183 596 | (true, _) => Some first
adamc@183 597 | (false, _) => None
adamc@183 598 end)) with
adamc@183 599 | (true, _) => fun env => fst env
adamc@183 600 | (false, _) => fun _ => tt
adamc@183 601 end
adamc@183 602 | right _ =>
adamc@183 603 match fvs return (envOf var (envT := first :: rest) fvs
adamc@183 604 -> var <| (lookup_type n (snd fvs))) with
adamc@183 605 | (true, fvs') => fun env => lookup var rest n fvs' (snd env)
adamc@183 606 | (false, fvs') => fun env => lookup var rest n fvs' env
adamc@183 607 end
adamc@183 608 end
adamc@183 609 end.
adamc@183 610
adamc@183 611 Theorem lok : forall var n t envT (fvs : isfree envT),
adamc@183 612 lookup_type n fvs = Some t
adamc@183 613 -> var <| lookup_type n fvs = var (ccType t).
adamc@183 614 crush.
adamc@183 615 Defined.
adamc@183 616 End isfree.
adamc@183 617
adamc@183 618 Implicit Arguments lookup_type [envT].
adamc@183 619 Implicit Arguments lookup [envT fvs].
adamc@183 620 Implicit Arguments wfExp [t envT].
adamc@183 621 Implicit Arguments envType [envT].
adamc@183 622 Implicit Arguments envOf [envT].
adamc@183 623 Implicit Arguments lok [var n t envT fvs].
adamc@183 624
adamc@183 625 Section lookup_hints.
adamc@183 626 Hint Resolve lookup_bound_contra.
adamc@183 627
adamc@183 628 (*Ltac my_chooser T k :=
adamc@183 629 match T with
adamc@183 630 | ptype =>
adamc@183 631 match goal with
adamc@183 632 | [ H : lookup _ _ = Some ?t |- _ ] => k t
adamc@183 633 end
adamc@183 634 | _ => default_chooser T k
adamc@183 635 end.
adamc@183 636
adamc@183 637 Ltac my_matching := matching equation my_chooser.*)
adamc@183 638
adamc@183 639 Hint Resolve lookup_bound_contra.
adamc@183 640
adamc@183 641 Lemma lookup_type_push : forall t' envT (fvs1 fvs2 : isfree envT) b1 b2,
adamc@183 642 (forall (n : nat) (t : Source.type),
adamc@183 643 lookup_type (envT := t' :: envT) n (b1, fvs1) = Some t ->
adamc@183 644 lookup_type (envT := t' :: envT) n (b2, fvs2) = Some t)
adamc@183 645 -> (forall (n : nat) (t : Source.type),
adamc@183 646 lookup_type n fvs1 = Some t ->
adamc@183 647 lookup_type n fvs2 = Some t).
adamc@183 648 intros until b2; intro H; intros n t;
adamc@183 649 generalize (H n t); my_crush; elimtype False; eauto.
adamc@183 650 Defined.
adamc@183 651
adamc@183 652 Lemma lookup_type_push_contra : forall t' envT (fvs1 fvs2 : isfree envT),
adamc@183 653 (forall (n : nat) (t : Source.type),
adamc@183 654 lookup_type (envT := t' :: envT) n (true, fvs1) = Some t ->
adamc@183 655 lookup_type (envT := t' :: envT) n (false, fvs2) = Some t)
adamc@183 656 -> False.
adamc@183 657 intros until fvs2; intro H; generalize (H (length envT) t'); my_crush.
adamc@183 658 Defined.
adamc@183 659 End lookup_hints.
adamc@183 660
adamc@183 661 Section packing.
adamc@183 662 Open Local Scope cc_scope.
adamc@183 663
adamc@183 664 Hint Resolve lookup_type_push lookup_type_push_contra.
adamc@183 665
adamc@183 666 Definition packExp (var : Closed.type -> Set) (envT : list Source.type)
adamc@183 667 (fvs1 fvs2 : isfree envT)
adamc@183 668 : (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t)
adamc@183 669 -> envOf var fvs2 -> exp var (envType fvs1).
adamc@183 670 refine (fix packExp (var : Closed.type -> Set) (envT : list Source.type) {struct envT}
adamc@183 671 : forall fvs1 fvs2 : isfree envT,
adamc@183 672 (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t)
adamc@183 673 -> envOf var fvs2 -> exp var (envType fvs1) :=
adamc@183 674 match envT return (forall fvs1 fvs2 : isfree envT,
adamc@183 675 (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t)
adamc@183 676 -> envOf var fvs2
adamc@183 677 -> exp var (envType fvs1)) with
adamc@183 678 | nil => fun _ _ _ _ => ()
adamc@183 679 | first :: rest => fun fvs1 =>
adamc@183 680 match fvs1 return (forall fvs2 : isfree (first :: rest),
adamc@183 681 (forall n t, lookup_type (envT := first :: rest) n fvs1 = Some t
adamc@183 682 -> lookup_type n fvs2 = Some t)
adamc@183 683 -> envOf var fvs2
adamc@183 684 -> exp var (envType (envT := first :: rest) fvs1)) with
adamc@183 685 | (false, fvs1') => fun fvs2 =>
adamc@183 686 match fvs2 return ((forall n t, lookup_type (envT := first :: rest) n (false, fvs1') = Some t
adamc@183 687 -> lookup_type (envT := first :: rest) n fvs2 = Some t)
adamc@183 688 -> envOf (envT := first :: rest) var fvs2
adamc@183 689 -> exp var (envType (envT := first :: rest) (false, fvs1'))) with
adamc@183 690 | (false, fvs2') => fun Hmin env =>
adamc@183 691 packExp var _ fvs1' fvs2' _ env
adamc@183 692 | (true, fvs2') => fun Hmin env =>
adamc@183 693 packExp var _ fvs1' fvs2' _ (snd env)
adamc@183 694 end
adamc@183 695 | (true, fvs1') => fun fvs2 =>
adamc@183 696 match fvs2 return ((forall n t, lookup_type (envT := first :: rest) n (true, fvs1') = Some t
adamc@183 697 -> lookup_type (envT := first :: rest) n fvs2 = Some t)
adamc@183 698 -> envOf (envT := first :: rest) var fvs2
adamc@183 699 -> exp var (envType (envT := first :: rest) (true, fvs1'))) with
adamc@183 700 | (false, fvs2') => fun Hmin env =>
adamc@183 701 False_rect _ _
adamc@183 702 | (true, fvs2') => fun Hmin env =>
adamc@183 703 [#(fst env), packExp var _ fvs1' fvs2' _ (snd env)]
adamc@183 704 end
adamc@183 705 end
adamc@183 706 end); eauto.
adamc@183 707 Defined.
adamc@183 708
adamc@183 709 Hint Resolve fvsExp_correct fvsExp_minimal.
adamc@183 710 Hint Resolve lookup_push_drop lookup_bound lookup_push_add.
adamc@183 711
adamc@183 712 Implicit Arguments packExp [var envT].
adamc@183 713
adamc@183 714 Fixpoint unpackExp (var : Closed.type -> Set) t (envT : list Source.type) {struct envT}
adamc@183 715 : forall fvs : isfree envT,
adamc@183 716 exp var (envType fvs)
adamc@183 717 -> (envOf var fvs -> exp var t) -> exp var t :=
adamc@183 718 match envT return (forall fvs : isfree envT,
adamc@183 719 exp var (envType fvs)
adamc@183 720 -> (envOf var fvs -> exp var t) -> exp var t) with
adamc@183 721 | nil => fun _ _ f => f tt
adamc@183 722 | first :: rest => fun fvs =>
adamc@183 723 match fvs return (exp var (envType (envT := first :: rest) fvs)
adamc@183 724 -> (envOf var (envT := first :: rest) fvs -> exp var t)
adamc@183 725 -> exp var t) with
adamc@183 726 | (false, fvs') => fun p f =>
adamc@183 727 unpackExp rest fvs' p f
adamc@183 728 | (true, fvs') => fun p f =>
adamc@183 729 x <- #1 p;
adamc@183 730 unpackExp rest fvs' (#2 p)
adamc@183 731 (fun env => f (x, env))
adamc@183 732 end
adamc@183 733 end.
adamc@183 734
adamc@183 735 Implicit Arguments unpackExp [var t envT fvs].
adamc@183 736
adamc@183 737 Theorem wfExp_lax : forall t t' envT (fvs : isfree envT) (e : Source.exp natvar t),
adamc@183 738 wfExp (envT := t' :: envT) (true, fvs) e
adamc@183 739 -> wfExp (envT := t' :: envT) (true, snd (fvsExp e (t' :: envT))) e.
adamc@183 740 Hint Extern 1 (_ = _) =>
adamc@183 741 match goal with
adamc@183 742 | [ H : lookup_type _ (fvsExp ?X ?Y) = _ |- _ ] =>
adamc@183 743 destruct (fvsExp X Y); my_crush
adamc@183 744 end.
adamc@183 745 eauto.
adamc@183 746 Defined.
adamc@183 747
adamc@183 748 Implicit Arguments wfExp_lax [t t' envT fvs e].
adamc@183 749
adamc@183 750 Lemma inclusion : forall t t' envT fvs (e : Source.exp natvar t),
adamc@183 751 wfExp (envT := t' :: envT) (true, fvs) e
adamc@183 752 -> (forall n t, lookup_type n (snd (fvsExp e (t' :: envT))) = Some t
adamc@183 753 -> lookup_type n fvs = Some t).
adamc@183 754 eauto.
adamc@183 755 Defined.
adamc@183 756
adamc@183 757 Implicit Arguments inclusion [t t' envT fvs e].
adamc@183 758
adamc@183 759 Definition env_prog var t envT (fvs : isfree envT) :=
adamc@183 760 funcs var (envOf var fvs -> Closed.exp var t).
adamc@183 761
adamc@183 762 Implicit Arguments env_prog [envT].
adamc@183 763
adamc@183 764 Axiom cheat : forall T, T.
adamc@183 765
adamc@183 766 Import Source.
adamc@183 767 Open Local Scope cc_scope.
adamc@183 768
adamc@183 769 Fixpoint ccExp var t (e : Source.exp natvar t)
adamc@183 770 (envT : list Source.type) (fvs : isfree envT)
adamc@183 771 {struct e} : wfExp fvs e -> env_prog var (ccType t) fvs :=
adamc@183 772 match e in (Source.exp _ t) return (wfExp fvs e -> env_prog var (ccType t) fvs) with
adamc@183 773 | Const n => fun _ => Main (fun _ => ^n)
adamc@183 774 | Plus e1 e2 => fun wf =>
adamc@183 775 n1 <-- ccExp var e1 _ fvs (proj1 wf);
adamc@183 776 n2 <-- ccExp var e2 _ fvs (proj2 wf);
adamc@183 777 Main (fun env => n1 env +^ n2 env)
adamc@183 778
adamc@183 779 | Var _ n => fun wf =>
adamc@183 780 Main (fun env => #(match lok wf in _ = T return T with
adamc@183 781 | refl_equal => lookup var n env
adamc@183 782 end))
adamc@183 783
adamc@183 784 | App _ _ f x => fun wf =>
adamc@183 785 f' <-- ccExp var f _ fvs (proj1 wf);
adamc@183 786 x' <-- ccExp var x _ fvs (proj2 wf);
adamc@183 787 Main (fun env => f' env @ x' env)
adamc@183 788
adamc@183 789 | Abs dom _ b => fun wf =>
adamc@183 790 b' <-- ccExp var (b (length envT)) (dom :: envT) _ (wfExp_lax wf);
adamc@183 791 f <== \\env, arg, unpackExp (#env) (fun env => b' (arg, env));
adamc@183 792 Main (fun env => #f ##
adamc@183 793 packExp
adamc@183 794 (snd (fvsExp (b (length envT)) (dom :: envT)))
adamc@183 795 fvs (inclusion wf) env)
adamc@183 796 end.
adamc@183 797 End packing.
adamc@183 798
adamc@183 799 Implicit Arguments packExp [var envT].
adamc@183 800 Implicit Arguments unpackExp [var t envT fvs].
adamc@183 801
adamc@183 802 Implicit Arguments ccExp [var t envT].
adamc@183 803
adamc@184 804 Fixpoint map_funcs var T1 T2 (f : T1 -> T2) (fs : funcs var T1) {struct fs}
adamc@184 805 : funcs var T2 :=
adamc@183 806 match fs with
adamc@184 807 | Main v => Main (f v)
adamc@184 808 | Abs _ _ _ e fs' => Abs e (fun x => map_funcs f (fs' x))
adamc@183 809 end.
adamc@183 810
adamc@184 811 Definition CcTerm' t (E : Source.Exp t) (Hwf : wfExp (envT := nil) tt (E _)) : Prog (ccType t) :=
adamc@184 812 fun _ => map_funcs (fun f => f tt) (ccExp (E _) (envT := nil) tt Hwf).
adamc@183 813
adamc@183 814
adamc@183 815 (** * Correctness *)
adamc@183 816
adamc@184 817 Section spliceFuncs_correct.
adamc@184 818 Variables T1 T2 : Type.
adamc@184 819 Variable f : T1 -> funcs typeDenote T2.
adamc@183 820
adamc@184 821 Theorem spliceFuncs_correct : forall fs,
adamc@184 822 funcsDenote (spliceFuncs fs f)
adamc@184 823 = funcsDenote (f (funcsDenote fs)).
adamc@184 824 induction fs; crush.
adamc@183 825 Qed.
adamc@183 826 End spliceFuncs_correct.
adamc@183 827
adamc@183 828
adamc@185 829 Notation "var <| to" := (match to return Set with
adamc@183 830 | None => unit
adamc@184 831 | Some t => var (ccType t)
adamc@183 832 end) (no associativity, at level 70).
adamc@183 833
adamc@183 834 Section packing_correct.
adamc@184 835 Fixpoint makeEnv (envT : list Source.type) : forall (fvs : isfree envT),
adamc@184 836 Closed.typeDenote (envType fvs)
adamc@184 837 -> envOf Closed.typeDenote fvs :=
adamc@183 838 match envT return (forall (fvs : isfree envT),
adamc@184 839 Closed.typeDenote (envType fvs)
adamc@184 840 -> envOf Closed.typeDenote fvs) with
adamc@183 841 | nil => fun _ _ => tt
adamc@183 842 | first :: rest => fun fvs =>
adamc@184 843 match fvs return (Closed.typeDenote (envType (envT := first :: rest) fvs)
adamc@184 844 -> envOf (envT := first :: rest) Closed.typeDenote fvs) with
adamc@183 845 | (false, fvs') => fun env => makeEnv rest fvs' env
adamc@183 846 | (true, fvs') => fun env => (fst env, makeEnv rest fvs' (snd env))
adamc@183 847 end
adamc@183 848 end.
adamc@183 849
adamc@184 850 Implicit Arguments makeEnv [envT fvs].
adamc@184 851
adamc@184 852 Theorem unpackExp_correct : forall t (envT : list Source.type) (fvs : isfree envT)
adamc@184 853 (e1 : Closed.exp Closed.typeDenote (envType fvs))
adamc@184 854 (e2 : envOf Closed.typeDenote fvs -> Closed.exp Closed.typeDenote t),
adamc@184 855 Closed.expDenote (unpackExp e1 e2)
adamc@184 856 = Closed.expDenote (e2 (makeEnv (Closed.expDenote e1))).
adamc@184 857 induction envT; my_crush.
adamc@183 858 Qed.
adamc@183 859
adamc@183 860 Lemma lookup_type_more : forall v2 envT (fvs : isfree envT) t b v,
adamc@183 861 (v2 = length envT -> False)
adamc@183 862 -> lookup_type v2 (envT := t :: envT) (b, fvs) = v
adamc@183 863 -> lookup_type v2 fvs = v.
adamc@184 864 my_crush.
adamc@183 865 Qed.
adamc@183 866
adamc@183 867 Lemma lookup_type_less : forall v2 t envT (fvs : isfree (t :: envT)) v,
adamc@183 868 (v2 = length envT -> False)
adamc@183 869 -> lookup_type v2 (snd fvs) = v
adamc@183 870 -> lookup_type v2 (envT := t :: envT) fvs = v.
adamc@184 871 my_crush.
adamc@183 872 Qed.
adamc@183 873
adamc@184 874 Hint Resolve lookup_bound_contra.
adamc@184 875
adamc@183 876 Lemma lookup_bound_contra_eq : forall t envT (fvs : isfree envT) v,
adamc@183 877 lookup_type v fvs = Some t
adamc@183 878 -> v = length envT
adamc@183 879 -> False.
adamc@184 880 my_crush; elimtype False; eauto.
adamc@184 881 Qed.
adamc@183 882
adamc@184 883 Lemma lookup_type_inner : forall t t' envT v t'' (fvs : isfree envT) e,
adamc@184 884 wfExp (envT := t' :: envT) (true, fvs) e
adamc@184 885 -> lookup_type v (snd (fvsExp (t := t) e (t' :: envT))) = Some t''
adamc@184 886 -> lookup_type v fvs = Some t''.
adamc@184 887 Hint Resolve lookup_bound_contra_eq fvsExp_minimal
adamc@183 888 lookup_type_more lookup_type_less.
adamc@184 889 Hint Extern 2 (Some _ = Some _) => elimtype False.
adamc@183 890
adamc@183 891 eauto 6.
adamc@183 892 Qed.
adamc@183 893
adamc@183 894 Lemma cast_irrel : forall T1 T2 x (H1 H2 : T1 = T2),
adamc@184 895 match H1 in _ = T return T with
adamc@184 896 | refl_equal => x
adamc@184 897 end
adamc@184 898 = match H2 in _ = T return T with
adamc@184 899 | refl_equal => x
adamc@184 900 end.
adamc@184 901 intros; generalize H1; crush;
adamc@184 902 repeat match goal with
adamc@184 903 | [ |- context[match ?pf with refl_equal => _ end] ] =>
adamc@184 904 rewrite (UIP_refl _ _ pf)
adamc@184 905 end;
adamc@184 906 reflexivity.
adamc@183 907 Qed.
adamc@183 908
adamc@183 909 Hint Immediate cast_irrel.
adamc@183 910
adamc@184 911 Hint Extern 3 (_ == _) =>
adamc@183 912 match goal with
adamc@183 913 | [ |- context[False_rect _ ?H] ] =>
adamc@183 914 apply False_rect; exact H
adamc@183 915 end.
adamc@183 916
adamc@184 917 Theorem packExp_correct : forall v envT (fvs1 fvs2 : isfree envT)
adamc@183 918 Hincl env,
adamc@184 919 lookup_type v fvs1 <> None
adamc@184 920 -> lookup Closed.typeDenote v env
adamc@184 921 == lookup Closed.typeDenote v
adamc@184 922 (makeEnv (Closed.expDenote
adamc@184 923 (packExp fvs1 fvs2 Hincl env))).
adamc@184 924 induction envT; my_crush.
adamc@183 925 Qed.
adamc@183 926 End packing_correct.
adamc@183 927
adamc@185 928 About packExp_correct.
adamc@185 929 Implicit Arguments packExp_correct [v envT fvs1].
adamc@185 930
adamc@185 931 Implicit Arguments lookup_type_more [v2 envT fvs t b v].
adamc@184 932
adamc@184 933 Lemma typeDenote_same : forall t,
adamc@184 934 Source.typeDenote t = Closed.typeDenote (ccType t).
adamc@184 935 induction t; crush.
adamc@184 936 Qed.
adamc@184 937
adamc@184 938 Hint Resolve typeDenote_same.
adamc@184 939
adamc@183 940 Lemma look : forall envT n (fvs : isfree envT) t,
adamc@183 941 lookup_type n fvs = Some t
adamc@184 942 -> Closed.typeDenote <| lookup_type n fvs = Source.typeDenote t.
adamc@184 943 crush.
adamc@183 944 Qed.
adamc@183 945
adamc@183 946 Implicit Arguments look [envT n fvs t].
adamc@183 947
adamc@185 948 Fixpoint lr (t : Source.type) : Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop :=
adamc@185 949 match t return Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop with
adamc@185 950 | Nat => @eq nat
adamc@185 951 | dom --> ran => fun f1 f2 =>
adamc@185 952 forall x1 x2, lr dom x1 x2
adamc@185 953 -> lr ran (f1 x1) (f2 x2)
adamc@185 954 end.
adamc@184 955
adamc@184 956 Theorem ccTerm_correct : forall t G
adamc@184 957 (e1 : Source.exp Source.typeDenote t)
adamc@184 958 (e2 : Source.exp natvar t),
adamc@184 959 exp_equiv G e1 e2
adamc@184 960 -> forall (envT : list Source.type) (fvs : isfree envT)
adamc@184 961 (env : envOf Closed.typeDenote fvs) (wf : wfExp fvs e2),
adamc@184 962 (forall t (v1 : Source.typeDenote t) (v2 : natvar t),
adamc@184 963 In (existT _ _ (v1, v2)) G
adamc@183 964 -> v2 < length envT)
adamc@184 965 -> (forall t (v1 : Source.typeDenote t) (v2 : natvar t),
adamc@184 966 In (existT _ _ (v1, v2)) G
adamc@185 967 -> forall pf,
adamc@185 968 lr t v1 (match lok pf in _ = T return T with
adamc@185 969 | refl_equal => lookup Closed.typeDenote v2 env
adamc@185 970 end))
adamc@185 971 (*-> forall pf : lookup_type v2 fvs = Some t,
adamc@185 972 lr t v1 (match pf in _ = T return Closed.typeDenote <| T with
adamc@185 973 | refl_equal => lookup Closed.typeDenote v2 env
adamc@185 974 end))*)
adamc@185 975 -> lr t (Source.expDenote e1) (Closed.expDenote (funcsDenote (ccExp e2 fvs wf) env)).
adamc@183 976
adamc@184 977 Hint Rewrite spliceFuncs_correct unpackExp_correct : cpdt.
adamc@183 978 Hint Resolve packExp_correct lookup_type_inner.
adamc@183 979
adamc@184 980 induction 1.
adamc@183 981
adamc@184 982 crush.
adamc@184 983 crush.
adamc@184 984 crush.
adamc@184 985 crush.
adamc@183 986
adamc@185 987 crush.
adamc@185 988 apply (H0 x1 (length envT) (t1 :: envT) (true, snd (fvsExp (f2 (length envT)) (t1 :: envT)))).
adamc@185 989 clear H0.
adamc@185 990 crush.
adamc@185 991 eauto.
adamc@185 992 generalize (H1 _ _ _ H4).
adamc@185 993 crush.
adamc@183 994
adamc@185 995 crush.
adamc@185 996 generalize H3; clear_all.
adamc@185 997 match goal with
adamc@185 998 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
adamc@185 999 end.
adamc@184 1000 simpl.
adamc@185 1001 destruct (eq_nat_dec (length envT) (length envT)); crush.
adamc@185 1002 rewrite (UIP_refl _ _ e0); assumption.
adamc@185 1003
adamc@185 1004 match goal with
adamc@185 1005 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
adamc@185 1006 end; simpl.
adamc@185 1007 destruct (eq_nat_dec v2 (length envT)); crush.
adamc@185 1008 generalize (H1 _ _ _ H5).
adamc@185 1009 crush.
adamc@185 1010 generalize (H2 _ _ _ H5).
adamc@185 1011 clear H2; intro H2.
adamc@185 1012 generalize (H2 (lookup_type_inner _ _ _ _ _ wf pf)).
adamc@185 1013 clear H2; intro H2.
adamc@185 1014 generalize H2; clear_all.
adamc@185 1015 repeat match goal with
adamc@185 1016 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
adamc@185 1017 end; simpl.
adamc@185 1018
adamc@185 1019 match type of pf with
adamc@185 1020 | ?X = _ => assert (X <> None)
adamc@185 1021 end.
adamc@185 1022 congruence.
adamc@185 1023 assert (forall (n : nat) (t0 : Source.type),
adamc@185 1024 lookup_type (envT:=envT) n (snd (fvsExp (f2 (length envT)) (t1 :: envT))) = Some t0 ->
adamc@185 1025 lookup_type (envT:=envT) n fvs = Some t0).
adamc@185 1026 eauto.
adamc@185 1027 generalize (packExp_correct fvs (inclusion t1 envT fvs (f2 (length envT)) wf) env H).
adamc@185 1028 simpl.
adamc@185 1029 match goal with
adamc@185 1030 | [ |- ?X == ?Y -> _ ] =>
adamc@185 1031 generalize X Y
adamc@185 1032 end.
adamc@185 1033 rewrite pf.
adamc@185 1034 rewrite (lookup_type_inner _ _ _ _ _ wf pf).
adamc@185 1035 crush.
adamc@185 1036 rewrite (UIP_refl _ _ e0).
adamc@185 1037 rewrite (UIP_refl _ _ e1) in H2.
adamc@185 1038 crush.
adamc@185 1039 rewrite <- H1.
adamc@185 1040 assumption.
adamc@183 1041 Qed.
adamc@183 1042
adamc@183 1043
adamc@183 1044 (** * Parametric version *)
adamc@183 1045
adamc@183 1046 Section wf.
adamc@183 1047 Variable result : ptype.
adamc@183 1048
adamc@183 1049 Lemma Pterm_wf' : forall G (e1 e2 : pterm natvar result),
adamc@183 1050 pterm_equiv G e1 e2
adamc@183 1051 -> forall envT (fvs : isfree envT),
adamc@183 1052 (forall t (v1 v2 : natvar t), In (vars (v1, v2)) G
adamc@183 1053 -> lookup_type v1 fvs = Some t)
adamc@183 1054 -> wfTerm fvs e1.
adamc@183 1055 Hint Extern 3 (Some _ = Some _) => contradictory; eapply lookup_bound_contra; eauto.
adamc@183 1056
adamc@183 1057 apply (pterm_equiv_mut
adamc@183 1058 (fun G (e1 e2 : pterm natvar result) =>
adamc@183 1059 forall envT (fvs : isfree envT),
adamc@183 1060 (forall t (v1 v2 : natvar t), In (vars (v1, v2)) G
adamc@183 1061 -> lookup_type v1 fvs = Some t)
adamc@183 1062 -> wfTerm (envT:=envT) fvs e1)
adamc@183 1063 (fun G t (p1 p2 : pprimop natvar result t) =>
adamc@183 1064 forall envT (fvs : isfree envT),
adamc@183 1065 (forall t (v1 v2 : natvar t), In (vars (v1, v2)) G
adamc@183 1066 -> lookup_type v1 fvs = Some t)
adamc@183 1067 -> wfPrimop (envT:=envT) fvs p1));
adamc@183 1068 simpler;
adamc@183 1069 match goal with
adamc@183 1070 | [ envT : list ptype, H : _ |- _ ] =>
adamc@183 1071 apply (H (length envT) (length envT)); simpler
adamc@183 1072 end.
adamc@183 1073 Qed.
adamc@183 1074
adamc@183 1075 Theorem Pterm_wf : forall (E : Pterm result),
adamc@183 1076 wfTerm (envT := nil) tt (E _).
adamc@183 1077 intros; eapply Pterm_wf';
adamc@183 1078 [apply Pterm_equiv
adamc@183 1079 | simpler].
adamc@183 1080 Qed.
adamc@183 1081 End wf.
adamc@183 1082
adamc@183 1083 Definition CcTerm result (E : Pterm result) : Cprog result :=
adamc@183 1084 CcTerm' E (Pterm_wf E).
adamc@183 1085
adamc@183 1086 Lemma map_funcs_correct : forall result T1 T2 (f : T1 -> T2) (fs : cfuncs ctypeDenote result T1) k,
adamc@183 1087 cfuncsDenote (map_funcs f fs) k = f (cfuncsDenote fs k).
adamc@183 1088 induction fs; equation.
adamc@183 1089 Qed.
adamc@183 1090
adamc@183 1091 Theorem CcTerm_correct : forall result (E : Pterm result) k,
adamc@183 1092 PtermDenote E k
adamc@183 1093 = CprogDenote (CcTerm E) k.
adamc@183 1094 Hint Rewrite map_funcs_correct : ltamer.
adamc@183 1095
adamc@183 1096 unfold PtermDenote, CprogDenote, CcTerm, CcTerm', cprogDenote;
adamc@183 1097 simpler;
adamc@183 1098 apply (ccTerm_correct (result := result)
adamc@183 1099 (G := nil)
adamc@183 1100 (e1 := E _)
adamc@183 1101 (e2 := E _)
adamc@183 1102 (Pterm_equiv _ _ _)
adamc@183 1103 nil
adamc@183 1104 tt
adamc@183 1105 tt);
adamc@183 1106 simpler.
adamc@183 1107 Qed.