Mercurial > cpdt > repo

annotate src/Intensional.v @ 183:02569049397b

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