 Timestamp:
 Nov 21, 2013, 8:20:02 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Language.ma
r3396 r3397 18 18 include "../src/utilities/option.ma". 19 19 include "basics/jmeq.ma". 20 21 discriminator option. 20 22 21 23 record instr_params : Type[1] ≝ … … 95 97 }. 96 98 97 record env_item(p : env_params) (p' : instr_params) : Type[0] ≝99 record signature (p : env_params) (p' : instr_params) : Type[0] ≝ 98 100 { f_name : FunctionName 99 101 ; f_pars : form_params_type p 102 ; f_ret : return_type p' 103 }. 104 105 record env_item (p : env_params) (p' : instr_params) : Type[0] ≝ 106 { f_sig :> signature p p' 100 107 ; f_lab : CallCostLabel 101 108 ; f_body : Instructions p' 102 ; f_ret : return_type p'103 109 }. 104 110 … … 126 132 ; eval_cond_cond : cond_instr p → state p → option (bool × (store_type p)) 127 133 ; eval_loop_cond : loop_instr p → state p → option (bool × (store_type p)) 128 ; eval_call : env_itemp p → act_params_type p → state p → option (store_type p)134 ; eval_call : signature p p → act_params_type p → state p → option (store_type p) 129 135 ; eval_after_return : return_type p → store_type p → option (store_type p) 130 136 ; init_store : store_type p … … 516 522 [ None ⇒ 〈False,nil ?〉 517 523  Some w ⇒ 518 match \fst ywith524 match \fst z with 519 525 [ ret_act opt_x ⇒ 520 526 match ret_costed_abs keep opt_x with … … 522 528 get_element … m lbl = lbl :: (\fst w),(nil ?)〉 523 529  None ⇒ 524 〈\fst z= ret_act (None ?) ∧ \fst x ∧ \snd w = \snd y,\fst w〉530 〈\fst y = ret_act (None ?) ∧ \fst x ∧ \snd w = \snd y,\fst w〉 525 531 ] 526 532  cost_act opt_x ⇒ … … 624 630 (λi,x.let 〈t_env,n,m,keep〉 ≝ x in 625 631 let info ≝ call_post_trans … (f_body … i) n (nil ?) in 626 〈(mk_env_item … (f_name … i) (f_pars … i) (f_lab … i) 627 (t_code … info) (f_ret … i)) :: t_env, 632 〈(mk_env_item ?? 633 (mk_signature ??(f_name ?? i) (f_pars … i) (f_ret … i)) 634 (f_lab … i) (f_body … i)) :: t_env, 628 635 fresh … info, 〈a_call (f_lab … i),(a_call (f_lab … i)) :: (gen_labels ? info)〉 :: 629 636 ((lab_map … info) @ m),(lab_to_keep … info) @ keep〉) 630 637 (〈nil ?,max_all,nil ?,nil ?〉) (env … prog)) in 631 638 〈mk_Program ?? t_env (t_code … (call_post_trans … (main … prog) n (nil ?))),m,keep〉 . 632 633 discriminator option.634 639 635 640 definition map_labels_on_trace : … … 642 647 #m #l1 elim l1 // #hd #tl #IH #l2 >associative_append <IH // 643 648 qed. 649 650 include "../src/common/Errors.ma". 644 651 645 652 lemma correctness : ∀p,p',prog. … … 664 671 normalize nodelta inversion (foldr2 ???????) [ #_ *] * #H1 #l2 #EQHl2 665 672 >m_return_bind normalize nodelta 666 667 673 inversion (call_post_clean ?????) [ #_ **** ] 668 674 * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta 669 cases lab1 in Hio11 Hl1 EQcont11 H; normalize nodelta 670 671 [ whd in match is_silent_cost_act_b; normalize nodelta 675 cases l1' (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta 676 [1,4: [ #x #y ] (*#_ #_ #_ #H*) **** 677  #x cases (ret_costed_abs ??) normalize nodelta [#c] *****[*] #EQ @⊥ >EQ in Hl1; 678 normalize * /2/ ] * 679 [ (*#Hio11 #_ #EQcont11 #H*) normalize nodelta ***** #EQ destruct(EQ) 680 #HH1 #EQ destruct(EQ) >EQcode11 inversion(code … s1') 681 [ 682  #x 683  #seq #lbl #i #_ 684  #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ 685  #cond #ltrue #i1 #lfalse #i2 #_ #_ 686  #f #act_p #ret_post #i #_ 687  #l_in #io #l_out #i #_ 688 ] 689 [*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct(EQ)] 690 cases(call_post_clean ?????) normalize nodelta 691 [1,3,5,7,9: #EQ destruct(EQ)] cases daemon (* da fare assurdi!!!*) ] 692 #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 693 cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l1 …) 694 [2: whd whd in match check_continuations; normalize nodelta >EQHl2 695 normalize nodelta % // % // % // @EQcode_c_st12 ] 696 #l3 * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{l3} %{st3'} 697 %{(t_ind … (cost_act (None ?)) … t')} 698 [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉) 699 [3: assumption 4: assumption *:] /3 by nmk/ ] 700 % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} 701 whd in match (get_costlabels_of_trace ????); 702 whd in match (get_costlabels_of_trace ????); >EQcosts % 703  #lbl #Hiost11 #_ #EQcontst11 #H normalize nodelta ****** #EQ destruct(EQ) 704 #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 inversion(code … s1') 705 [ 706  #x 707  #seq #lbl #i #_ 708  #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ 709  #cond #ltrue #i1 #lfalse #i2 #_ #_ 710  #f #act_p #ret_post #i #_ 711  #l_in #io #l_out #i #_ 712 ] 713 [*: #_ whd in ⊢ (??%% → ?); #EQ cases daemon (* da fare assurdi !!!*) ] 714 #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio 715 cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l3 …) 716 [2: whd whd in match check_continuations; normalize nodelta >EQHl2 717 normalize nodelta % // % // % // @EQcode_c_st12 ] 718 #l3' * #st3' * #t' ** #Hst3st3' #EQcost #EQlen %{l3'} %{st3'} 719 %{(t_ind … (cost_act (Some ? lbl)) … t')} 720 [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉) 721 [3: assumption 4: assumption *:] /3 by nmk/ ] 722 % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} 723 whd in match (get_costlabels_of_trace ????); 724 whd in match (get_costlabels_of_trace ????) in ⊢ (???%); 725 whd in match map_labels_on_trace; normalize nodelta 726 whd in match (foldr ?????); 727 change with (map_labels_on_trace ??) in match (foldr ?????); >EQget_el 728 whd in match (append ???); whd in match (append ???) in ⊢ (???%); @eq_f 729 whd in match (append ???) in ⊢ (??(???%)(??%?)); @EQcost 730 ] 731  #seq #i #store * [ #lbl] #EQcode11 #EQstore #EQ destruct(EQ) #EQcont 732 #EQ destruct(EQ) #Hio_st11 #Hio_st12 #EQ destruct(EQ) #EQ1 #EQ2 destruct(EQ1 EQ2) 733 #EQ destruct(EQ) #tl #IH #st3 #l1 whd in ⊢ (% → ?); 734 inversion(check_continuations ?????) [1,3: #_ *] * #H1 #l2 735 [ >EQcont in ⊢ (% → ?);  >EQcont in ⊢ (% → ?); ] #EQcheck normalize nodelta 736 *** #HH1 [ >EQcode11 in ⊢ (% → ?);  >EQcode11 in ⊢ (% → ?); ] 737 inversion(code … st3) 738 [1,2,4,5,6,7,8,9,11,12,13,14: (*assurdi da fare *) cases daemon ] 739 #seq1 #opt_l #i1 #_ #EQcode_st3 change with (m_bind ?????) in ⊢ (??%? → ?); 740 cases daemon 741 8: #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem 742 #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 743 destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #IH #st1' #l1 whd in ⊢ (% → ?); 744 inversion(check_continuations ??????) [1,3: #_ *] * #H1 #l2 #EQcheck 745 normalize nodelta *** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1') 746 [1,2,3,4,5,7: (*assurdi da fare*) cases daemon] #f' #act_p' #opt_l' #i' #_ 747 #EQcode_st1' #EQclean #EQstore #EQio 748 cut(∃env_it',n.lookup p p (env … trans_prog) f = return env_it' ∧ 749 t_code … (call_post_trans … (f_body … env_it) n (nil ?)) = f_body … env_it') 750 [1,3: cases daemon (*TODO*) ] * #env_it' * #fresh' * #EQenv_it' #EQtrans 751 cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) l2 …) 752 [2: whd >EQcont12 change with (m_bind ??? (check_continuations ??????) ?) in match (check_continuations ??????); 753 >EQcheck >m_return_bind change with (m_bind ?????) in EQclean : (??%?); 754 inversion(call_post_clean ?????) in EQclean; [ #_ whd in ⊢ (??%% → ?); #EQ destruct] 755 * #l3 #i'' #EQi'' >m_return_bind cases opt_l' in EQcode_st1'; [ #lbl'] #EQcode_st1' 756 normalize nodelta 757 [2: inversion(memb ???) normalize nodelta #Hlbl_keep 758 [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct] 759 #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta 760 [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_ 761 lapply(H1 H) H H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta 762 [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' l3) 763 #H1 #_ lapply(H1 H) H H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ 764 #EQ destruct(EQ) whd in match ret_costed_abs; normalize nodelta >Hlbl_keep 765 normalize nodelta % // % // % [ % // % // % //] >EQcode12 <EQtrans 766 cases daemon (*TODO*) 767  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct(EQ) 768 whd in match ret_costed_abs; normalize nodelta 769 * [ #_ #l3' 770 cases(bind_inversion ????? H) in ⊢ ?; 771 772 773 >EQcost normalize 774 775 %{l1} 776 xxxxxxxx 777 whd in match is_silent_cost_act_b; normalize nodelta 672 778 cases lab1 in H Hio11; normalize nodelta 673 779 [1,2,4: [1,2: #x [ #y]] #H #Hio11 #EQ destruct]
Note: See TracChangeset
for help on using the changeset viewer.