Changeset 2105 for src/common/AST.ma
 Timestamp:
 Jun 21, 2012, 5:21:04 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/AST.ma
r2103 r2105 378 378 qed. 379 379 380 lemma map_partial_All2 : ∀A,B,C,f. ∀P:A×B → A×C → Prop. 381 (∀i,x,y. f x = OK ? y → P 〈i,x〉 〈i,y〉) → 382 ∀l,l'. 383 map_partial A B C f l = OK ? l' → 384 All2 (A×B) (A×C) P l l'. 385 #A #B #C #f #P #H #l elim l 386 [ * [ //  #h #t #E normalize in E; destruct ] 387  * #a #b #tl #IH #l' #M 388 cases (bind_inversion ????? M) M * #a' #c * #AC #M 389 cases (bind_inversion ????? M) M #tl' * #TL #M 390 cases (bind_inversion ????? AC) AC #c' * #C #C' 391 normalize in C C' M; destruct % 392 [ @H @C 393  @IH @TL 394 ] 395 ] qed. 396 380 397 (* 381 398 Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) := … … 525 542 qed. 526 543 544 lemma transform_partial_program2_preserves_var_names : ∀A,B,V,W,p,tf,tv,p'. 545 transform_partial_program2 A B V W p tf tv = OK ? p' → 546 prog_var_names … p = prog_var_names … p'. 547 #A #B #V #W * #vars #fns #main #tf #tv * #vars' #fns' #main' 548 #T cases (bind_inversion ????? T) T #vars1 * #Evars1 549 generalize in match (map_partial_preserves_first ?????); #MPPF 550 lapply (refl ? (map_partial ??? tv vars)) 551 cases (map_partial ?????) in ⊢ (???% → ?); 552 [ 2: #m #M >M in MPPF ⊢ %; #MPPF #E normalize in E; destruct ] 553 #vs #VS >VS in MPPF ⊢ %; #MPPF 554 whd in ⊢ (??%% → ?); 555 generalize in match (map_fst ???????); #MF 556 #E destruct 557 whd in ⊢ (??%%); @MF 558 qed. 559 560 527 561 (* 528 562 Lemma transform_partial_program2_function: … … 569 603 Variable match_varinfo: V > W > Prop. 570 604 571 Definition match_funct_entry (x1: ident * A) (x2: ident * B) := 572 match x1, x2 with 573  (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2 574 end. 575 576 Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) := 577 match x1, x2 with 578  (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2 579 end. 580 581 Definition match_program (p1: program A V) (p2: program B W) : Prop := 582 list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct) 583 /\ p1.(prog_main) = p2.(prog_main) 584 /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars). 585 605 *) 606 607 record matching : Type[1] ≝ { 608 m_A : list ident → Type[0]; m_B : list ident → Type[0]; (* function types *) 609 m_V : Type[0]; m_W : Type[0]; (* variable types *) 610 match_fundef : ∀vs. m_A vs → m_B vs → Prop; 611 match_varinfo : m_V → m_W → Prop 612 }. 613 614 (* When defining a matching between function entries, quietly enforce equality 615 of the list of global variables (vs and vs'). *) 616 617 inductive match_funct_entry (M:matching) : ∀vs,vs'. ident × (m_A M vs) → ident × (m_B M vs') → Prop ≝ 618  mfe_intro : ∀vs,id,f1,f2. match_fundef M vs f1 f2 → match_funct_entry M vs vs 〈id,f1〉 〈id,f2〉. 619 620 (* but we'll need some care to usefully invert it *) 621 622 definition mfe_cast_fn_type : ∀M,vs,vs'. ∀E:vs'=vs. m_B M vs' → m_B M vs ≝ 623 λM,vs,vs',E. ?. 624 >E #m @m 625 qed. 626 627 let rec match_funct_entry_inv (M:matching) 628 (P:∀vs,id,f,id',f'. Prop) 629 (H:∀vs,id,f,id',f'. match_fundef M vs f f' → P vs id f id' f') 630 vs id f id' f' 631 (MFE:match_funct_entry M vs vs 〈id,f〉 〈id',f'〉) on MFE : P vs id f id' f' ≝ 632 match MFE return λvs,vs',idf,idf',MFE. ∀E:vs'=vs. P vs (\fst idf) (\snd idf) (\fst idf') (mfe_cast_fn_type … E (\snd idf')) with 633 [ mfe_intro vs id f1 f2 MF ⇒ ? 634 ] (refl ??). 635 #E >(K ?? E) @H @MF 636 qed. 637 638 (* and continue as before *) 639 640 inductive match_var_entry (M:matching) : ident × region × (m_V M) → ident × region × (m_W M) → Prop ≝ 641  mve_intro : ∀id,r,v1,v2. match_varinfo M v1 v2 → match_var_entry M 〈id,r,v1〉 〈id,r,v2〉. 642 643 lemma matching_vars : ∀M.∀p1:program (m_A M) (m_V M).∀p2:program (m_B M) (m_W M). 644 All2 … (match_var_entry M) (prog_vars … p1) (prog_vars … p2) → 645 prog_var_names … p1 = prog_var_names … p2. 646 #M * #vs1 #mn1 #fn1 * #vs2 #mn2 #fn2 647 normalize generalize in match vs2; 648 elim vs1 649 [ * [ //  #h #t * ] 650  * * #id1 #r1 #v1 #tl1 #IH * [ * ] 651 * * #id2 #r2 #v2 #tl2 * * 652 #id #r #v1' #v2' #_ #H 653 whd in ⊢ (??%%); >(IH … H) % 654 ] qed. 655 656 record match_program (M:matching) (p1: program (m_A M) (m_V M)) (p2: program (m_B M) (m_W M)) : Prop ≝ { 657 mp_vars : All2 … (match_var_entry M) (prog_vars … p1) (prog_vars … p2); 658 mp_funct : All2 ?? … (match_funct_entry M (prog_var_names … p1) (prog_var_names … p2)) (prog_funct … p1) (prog_funct ??… p2); 659 mp_main : prog_main … p1 = prog_main … p2 660 }. 661 662 (* 586 663 End MATCH_PROGRAM. 587 588 Remark transform_partial_program2_match: 589 forall (A B V W: Type) 590 (transf_partial_function: A > res B) 591 (transf_partial_variable: V > res W) 592 (p: program A V) (tp: program B W), 593 transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp > 594 match_program 595 (fun fd tfd => transf_partial_function fd = OK tfd) 596 (fun info tinfo => transf_partial_variable info = OK tinfo) 664 *) 665 666 (* Now show that all the transformations are instances of match_program. *) 667 668 lemma transform_partial_program2_match: 669 ∀A,B,V,W. 670 ∀transf_partial_function: ∀vs. A vs > res (B vs). 671 ∀transf_partial_variable: V > res W. 672 ∀p: program A V. ∀tp: program B W. 673 transform_partial_program2 … p transf_partial_function transf_partial_variable = OK ? tp → 674 match_program (mk_matching A B V W 675 (λvs,fd,tfd. transf_partial_function vs … fd = OK ? tfd) 676 (λinfo,tinfo. transf_partial_variable info = OK ? tinfo)) 597 677 p tp. 598 Proof. 599 intros. monadInv H. split. 600 apply list_forall2_imply with 601 (fun (ab: ident * A) (ac: ident * B) => 602 fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)). 603 eapply map_partial_forall2. eauto. 604 intros. destruct v1; destruct v2; simpl in *. auto. 605 split. auto. 606 apply list_forall2_imply with 607 (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) => 608 fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)). 609 eapply map_partial_forall2. eauto. 610 intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence. 611 Qed. 612 *) 678 #A #B #V #W #transf_partial_function #transf_partial_variable 679 * #vars #main #functs * #vars' #main' #functs' 680 #T cases (bind_inversion ????? T) T #fl * #Efl 681 generalize in match (map_partial_preserves_first ?????); #MPPF 682 lapply (refl ? (map_partial ??? transf_partial_variable vars)) 683 cases (map_partial ?????) in ⊢ (???% → ?); 684 [ 2: #m #M >M in MPPF ⊢ %; #MPPF #E normalize in E; destruct ] 685 #vs #VS >VS in MPPF ⊢ %; #MPPF 686 whd in ⊢ (??%% → ?); 687 generalize in match (map_fst ???????); #MF 688 #E destruct 689 % 690 [ @(map_partial_All2 … VS) * /2/ 691  whd in match (prog_var_names ???); 692 whd in match (prog_var_names ???); 693 <MF @(map_partial_All2 … Efl) #id #f1 #f2 /2/ 694  // 695 ] qed. 696 697 lemma transform_partial_program_match: 698 ∀A,B,V. 699 ∀trans_partial_function: ∀vs. A vs → res (B vs). 700 ∀p: program A V. ∀tp: program B V. 701 transform_partial_program … p trans_partial_function = OK ? tp → 702 match_program (mk_matching A B V V 703 (λvs,fd,tfd. trans_partial_function vs fd = OK ? tfd) 704 (λv,w. v = w)) 705 p tp. 706 #A #B #V #tpf 707 * #vars #fns #main * #vars' #fns' #main' 708 #TPP cases (bind_inversion ????? TPP) TPP #fns'' * #MAP 709 #E normalize in E; destruct 710 % 711 [ elim vars' // * * #id #r #v #tl #H % /2/ 712  @(map_partial_All2 … MAP) #i #f #f' #TPF % @TPF 713  // 714 ] qed. 715 716 lemma transform_program_match: 717 ∀A,B,V. 718 ∀trans_function: ∀vs. A vs → B vs. 719 ∀p: program A V. 720 match_program (mk_matching A B V V 721 (λvs,fd,tfd. trans_function vs fd = tfd) 722 (λv,w. v = w)) 723 p (transform_program … p trans_function). 724 #A #B #V #tf 725 * #vars #fns #main 726 % 727 [ normalize elim vars // * * #id #r #v #tl #H % /2/ 728  whd in match (prog_var_names ???); 729 whd in match (prog_vars ???); 730 elim fns 731 [ // 732  * #id #f #tl #IH % // % // 733 ] 734  // 735 ] qed. 736 613 737 (* * * External functions *) 614 738
Note: See TracChangeset
for help on using the changeset viewer.