Changeset 1343 for src/RTLabs/RTLabsToRTL.ma
 Timestamp:
 Oct 10, 2011, 5:27:34 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL.ma
r1331 r1343 98 98 λA. 99 99 λlst: list A. 100 λprf: 2 ≤length A lst.101 match lst return λx. 2 ≤x → A × A with100 λprf: 2 = length A lst. 101 match lst return λx. 2 = x → A × A with 102 102 [ nil ⇒ λlst_nil_prf. ? 103 103  cons hd tl ⇒ λprf. 104 match tl return λx. 1 ≤x → A × A with104 match tl return λx. 1 = x → A × A with 105 105 [ nil ⇒ λtl_nil_prf. ? 106 106  cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉 … … 108 108 ] prf. 109 109 [1: normalize in lst_nil_prf; 110 cases(not_le_Sn_O 1); 111 #HYP cases(HYP lst_nil_prf) 110 destruct(lst_nil_prf) 112 111 2: normalize in prf; 113 @ le_S_S_to_le112 @injective_S 114 113 assumption 115 114 3: normalize in tl_nil_prf; 116 cases(not_le_Sn_O 0)117 #HYP cases(HYP tl_nil_prf)]115 destruct(tl_nil_prf) 116 ] 118 117 qed. 119 118 … … 228 227  Oaddrstack offset ⇒ 229 228 let 〈r1, r2〉 ≝ make_addr … destrs ? in 230 let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (extension rtl_params_ globals (rtl_st_ext_ address r1 r2)) dest_lbl) def in229 let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (extension rtl_params_ globals (rtl_st_ext_stack_address r1 r2)) dest_lbl) def in 231 230 let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in 232 231 def … … 538 537 in 539 538 translates @ tmp_destrs2'. 540 539 541 540 axiom foldi_strong: 542 541 ∀a: Type[0]. 543 542 ∀b: Type[0]. 544 543 ∀the_list: list b. 545 ∀f: ∀n: nat. n ≤ the_list → a → b → a.544 ∀f: (∀i: nat. ∀proof: i ≤ the_list. a → b → a). 546 545 ∀seed: a. 547 546 a. … … 552 551 λsrcrs1: list register. 553 552 λsrcrs2: list register. 554 λregs_proof:  srcrs2 = destrs.553 λregs_proof: destrs = srcrs2. 555 554 λstart_lbl: label. 556 555 λdest_lbl: label. … … 571 570 in 572 571 let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in 573 let f' ≝ λi. λ proof: i ≤ srcrs2. f i ? in574 let insts_mul ≝ foldi_strong ? ?srcrs2 f' [ ] in572 let f' ≝ λi. λi_proof: i ≤ srcrs2. f i ? in 573 let insts_mul ≝ foldi_strong … srcrs2 f' [ ] in 575 574 add_translates rtl_params1 globals (insts_init @ insts_mul) start_lbl dest_lbl def 576 575 ]. 577 576 >tmp_destrs_prf 578 <regs_proof577 >regs_proof 579 578 assumption 580 579 qed. … … 856 855 λsrcrs1: list register. 857 856 λsrcrs2: list register. 858 λsrcrs1_prf: 0 < srcrs1. (* XXX: can this be relaxed? i think it can 859 but we need more dep. typ. in modu/divu 860 cases *) 861 λsrcrs2_prf: srcrs2 = destrs. 857 λsrcrs2_destrs_prf: srcrs2 = destrs. 858 λsrcrs1_destrs_prf: srcrs1 = destrs. 862 859 λstart_lbl: label. 863 860 λdest_lbl: label. … … 884 881 ] 885 882  nil ⇒ λnil_absrd. ? 886 ] srcrs1_prf883 ] ? 887 884  Omodu ⇒ 888 885 match srcrs1 return λx. 0 < x → rtl_internal_function globals with … … 893 890 ] 894 891  nil ⇒ λnil_absrd. ? 895 ] srcrs1_prf892 ] ? 896 893  Oand ⇒ 897 894 translate_op globals And destrs srcrs1 srcrs2 start_lbl dest_lbl def … … 965 962  _ ⇒ ? (* assert false, implemented in run time or float op *) 966 963 ]. 967 [ 3,7: normalize in nil_absrd; 968 cases(not_le_Sn_O 0) 969 #HYP cases(HYP nil_absrd) 970  4,8,19,20,21,22,17,18,24: 971 >srcrs2_prf 972 assumption 973  1,23: 974 assumption 975  *: cases not_implemented (* yes, really *) 964 [1: 965 @sym_eq 966 assumption 967 3,8,19,22,24,25: 968 >srcrs1_destrs_prf 969 assumption 970 4,9: 971 normalize in nil_absrd; 972 cases(not_le_Sn_O 0) 973 #HYP cases(HYP nil_absrd) 974 5,10,20,21,23,26: 975 >srcrs2_destrs_prf 976 assumption 977 *: 978 cases not_implemented (* XXX: yes, really *) 976 979 ] 977 980 qed. … … 994 997 λglobals: list ident. 995 998 λaddr. 996 λaddr_prf: 2 ≤addr.999 λaddr_prf: 2 = addr. 997 1000 λdestrs: list register. 998 1001 λstart_lbl: label. … … 1009 1012 let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in 1010 1013 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 1014 let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in 1011 1015 let insts_save_addr ≝ translate_move globals save_addr addr in 1012 1016 let f ≝ λtranslates_off. λr. … … 1016 1020 sequential rtl_params_ globals (INT rtl_params_ globals tmpr off) 1017 1021 ]; 1018 translate_op2 globals Oaddp tmp_addr ? save_addr [ tmpr] ? ?;1022 translate_op2 globals Oaddp tmp_addr ? save_addr [dummy; tmpr] ? ?; 1019 1023 adds_graph rtl_params1 globals [ 1020 1024 sequential rtl_params_ globals (LOAD rtl_params_ globals r tmp_addr1 tmp_addr2) … … 1029 1033 ] 1030 1034 ]. 1031 [1: normalize //1032 2: >save_addr_prf normalize1033 @ (transitive_le 1 2 (addr)) //1035 [1: >tmp_addr_prf >save_addr_prf % 1036 2: >save_addr_prf >tmp_addr_prf 1037 @addr_prf 1034 1038 3: >tmp_addr_prf normalize 1035 @(transitive_le 1 2 (addr))//1036  *: >tmp_addr_prf assumption1039 <addr_prf // 1040 4: >tmp_addr_prf assumption 1037 1041 ] 1038 1042 qed. … … 1041 1045 λglobals: list ident. 1042 1046 λaddr. 1043 λaddr_prf: 2 ≤addr.1047 λaddr_prf: 2 = addr. 1044 1048 λsrcrs: list register. 1045 1049 λstart_lbl: label. … … 1052 1056 let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in 1053 1057 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 1058 let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in 1054 1059 let f ≝ λtranslate_off. λsrcr. 1055 1060 let 〈translates, off〉 ≝ translate_off in … … 1058 1063 sequential rtl_params_ globals (INT rtl_params_ globals tmpr off) 1059 1064 ]; 1060 translate_op2 globals Oaddp tmp_addr … addr [ tmpr] ? ?;1065 translate_op2 globals Oaddp tmp_addr … addr [dummy; tmpr] ? ?; 1061 1066 adds_graph rtl_params1 globals [ 1062 1067 sequential rtl_params_ globals (STORE rtl_params_ globals tmp_addr1 tmp_addr2 srcr) … … 1070 1075 add_translates rtl_params1 globals translates start_lbl dest_lbl def 1071 1076 ]. 1072 [1: normalize //1077 [1: >tmp_addr_prf % 1073 1078 2: >tmp_addr_prf normalize 1074 @(transitive_le 1 2 (addr)) // 1075 3: >tmp_addr_prf normalize 1076 @(transitive_le 1 2 (addr)) // 1077 *: >tmp_addr_prf assumption 1079 <addr_prf // 1080 3: >tmp_addr_prf <addr_prf // 1081 4: >tmp_addr_prf @addr_prf 1078 1082 ] 1079 1083 qed.
Note: See TracChangeset
for help on using the changeset viewer.