Changeset 1601 for src/RTLabs/RTLabsToRTL.ma
- Timestamp:
- Dec 13, 2011, 2:49:52 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabsToRTL.ma
r1529 r1601 176 176 λdef: rtl_internal_function globals. 177 177 match reduce_strong register register srcrs1 srcrs2 with 178 [ dpreduced first_reduced_proof ⇒178 [ mk_Sig reduced first_reduced_proof ⇒ 179 179 let srcrsl_common ≝ \fst (\fst reduced) in 180 180 let srcrsr_common ≝ \fst (\snd reduced) in … … 183 183 let srcrs_rest ≝ srcrsl_rest @ srcrsr_rest in 184 184 match reduce_strong register register destrs srcrsl_common with 185 [ dpreduced second_reduced_proof ⇒185 [ mk_Sig reduced second_reduced_proof ⇒ 186 186 let destrs_common ≝ \fst (\fst reduced) in 187 187 let destrs_rest ≝ \snd (\fst reduced) in 188 188 match reduce_strong register register destrs_rest srcrs_rest with 189 [ dpreduced third_reduced_proof ⇒189 [ mk_Sig reduced third_reduced_proof ⇒ 190 190 let destrs_cted ≝ \fst (\fst reduced) in 191 191 let destrs_rest ≝ \snd (\fst reduced) in … … 225 225 [ true ⇒ λgood_case. 226 226 match split_into_bytes size const with 227 [ dpbytes bytes_length_proof ⇒227 [ mk_Sig bytes bytes_length_proof ⇒ 228 228 let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in 229 229 adds_graph rtl_params1 globals mapped start_lbl dest_lbl def … … 269 269 λstart_lbl: label. 270 270 match reduce_strong register register destrs srcrs with 271 [ dpcrl_crr len_proof ⇒271 [ mk_Sig crl_crr len_proof ⇒ 272 272 let commonl ≝ \fst (\fst crl_crr) in 273 273 let commonr ≝ \fst (\snd crl_crr) in … … 357 357 else 358 358 match reduce_strong register register destrs srcrs with 359 [ dpcrl len_proof ⇒359 [ mk_Sig crl len_proof ⇒ 360 360 let commonl ≝ \fst (\fst crl) in 361 361 let commonr ≝ \fst (\snd crl) in … … 628 628 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 629 629 match fresh_regs_strong rtl_params0 globals def (|destrs|) with 630 [ dpdef_tmp_destrs tmp_destrs_prf ⇒630 [ mk_Sig def_tmp_destrs tmp_destrs_prf ⇒ 631 631 let def ≝ \fst def_tmp_destrs in 632 632 let tmp_destrs ≝ \snd def_tmp_destrs in … … 689 689 let save_srcrs2 ≝ translate_move globals tmp_srcrs2 srcrs2 in 690 690 match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with 691 [ dpcrl their_proof ⇒691 [ mk_Sig crl their_proof ⇒ 692 692 let commonl ≝ \fst (\fst crl) in 693 693 let commonr ≝ \fst (\snd crl) in … … 826 826 | _ ⇒ 827 827 match fresh_regs_strong globals def (|destrs|) with 828 [ dpdef_tmp_destrs tmp_destrs_proof ⇒828 [ mk_Sig def_tmp_destrs tmp_destrs_proof ⇒ 829 829 let def ≝ \fst def_tmp_destrs in 830 830 let tmp_destrs ≝ \snd def_tmp_destrs in … … 836 836 let 〈def, tmpr3〉 ≝ fresh_reg rtl_params1 globals def in 837 837 match complete_regs_strong globals def srcrs1 srcrs2 with 838 [ dpsrcrs12_added srcrs12_proof ⇒838 [ mk_Sig srcrs12_added srcrs12_proof ⇒ 839 839 let srcrs1 ≝ \fst (\fst srcrs12_added) in 840 840 let srcrs2 ≝ \snd (\fst srcrs12_added) in … … 893 893 λdef: rtl_internal_function globals. 894 894 match fresh_regs_strong globals def (|srcrs1|) with 895 [ dpdef_tmp_srcrs1 srcrs1_prf ⇒895 [ mk_Sig def_tmp_srcrs1 srcrs1_prf ⇒ 896 896 let def ≝ \fst def_tmp_srcrs1 in 897 897 let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in 898 898 match fresh_regs_strong globals def (|srcrs2|) with 899 [ dpdef_tmp_srcrs2 srcrs2_prf ⇒899 [ mk_Sig def_tmp_srcrs2 srcrs2_prf ⇒ 900 900 let def ≝ \fst def_tmp_srcrs2 in 901 901 let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in … … 1073 1073 λdef: rtl_internal_function globals. 1074 1074 match fresh_regs_strong rtl_params0 globals def (|addr|) with 1075 [ dpdef_save_addr save_addr_prf ⇒1075 [ mk_Sig def_save_addr save_addr_prf ⇒ 1076 1076 let def ≝ \fst def_save_addr in 1077 1077 let save_addr ≝ \snd def_save_addr in 1078 1078 match fresh_regs_strong rtl_params0 globals def (|addr|) with 1079 [ dpdef_tmp_addr tmp_addr_prf ⇒1079 [ mk_Sig def_tmp_addr tmp_addr_prf ⇒ 1080 1080 let def ≝ \fst def_tmp_addr in 1081 1081 let tmp_addr ≝ \snd def_tmp_addr in … … 1121 1121 λdef: rtl_internal_function globals. 1122 1122 match fresh_regs_strong rtl_params0 globals def (|addr|) with 1123 [ dpdef_tmp_addr tmp_addr_prf ⇒1123 [ mk_Sig def_tmp_addr tmp_addr_prf ⇒ 1124 1124 let def ≝ \fst def_tmp_addr in 1125 1125 let tmp_addr ≝ \snd def_tmp_addr in
Note: See TracChangeset
for help on using the changeset viewer.