Changeset 1061
 Timestamp:
 Jul 8, 2011, 5:49:22 PM (9 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r1060 r1061 148 148 destruct(cons_prf) 149 149 assumption 150 ] 151 qed. 152 153 let rec map3 154 (A: Type[0]) (B: Type[0]) (C: Type[0]) (D: Type[0]) (f: A → B → C → D) 155 (left: list A) (centre: list B) (right: list C) 156 (prflc: left = centre) (prfcr: centre = right) on left ≝ 157 match left return λx. x = centre → list D with 158 [ nil ⇒ λnil_prf. 159 match centre return λx. x = right → list D with 160 [ nil ⇒ λnil_nil_prf. 161 match right return λx. nil ? = x → list D with 162 [ nil ⇒ λnil_nil_nil_prf. nil D 163  cons hd tl ⇒ λcons_nil_nil_absrd. ? 164 ] nil_nil_prf 165  cons hd tl ⇒ λnil_cons_absrd. ? 166 ] prfcr 167  cons hd tl ⇒ λcons_prf. 168 match centre return λx. x = right → list D with 169 [ nil ⇒ λcons_nil_absrd. ? 170  cons hd' tl' ⇒ λcons_cons_prf. 171 match right return λx. right = x → cons ? hd' tl' = x → list D with 172 [ nil ⇒ λrefl_prf. λcons_cons_nil_absrd. ? 173  cons hd'' tl'' ⇒ λrefl_prf. λcons_cons_cons_prf. 174 (f hd hd' hd'') :: (map3 A B C D f tl tl' tl'' ? ?) 175 ] (refl ? (right)) cons_cons_prf 176 ] prfcr 177 ] prflc. 178 [ 1: normalize in cons_nil_nil_absrd; 179 destruct(cons_nil_nil_absrd) 180  2: generalize in match nil_cons_absrd; 181 <prfcr <nil_prf #HYP 182 normalize in HYP; 183 destruct(HYP) 184  3: generalize in match cons_nil_absrd; 185 <prfcr <cons_prf #HYP 186 normalize in HYP; 187 destruct(HYP) 188  4: normalize in cons_cons_nil_absrd; 189 destruct(cons_cons_nil_absrd) 190  5: normalize in cons_cons_cons_prf; 191 destruct(cons_cons_cons_prf) 192 assumption 193  6: generalize in match cons_cons_cons_prf; 194 <refl_prf <prfcr <cons_prf #HYP 195 normalize in HYP; 196 destruct(HYP) 197 @sym_eq assumption 150 198 ] 151 199 qed. 
src/RTL/RTL.ma
r1060 r1061 14 14  rtl_st_int: register → Byte → label → rtl_statement 15 15  rtl_st_move: register → register → label → rtl_statement 16  rtl_st_opaccs: inter→ register → register → register → register → label → rtl_statement17  rtl_st_op1: intermediate_op1 → register → register → label → rtl_statement18  rtl_st_op2: intermediate_op2 → register → register → register → label → rtl_statement16  rtl_st_opaccs: OpAccs → register → register → register → register → label → rtl_statement 17  rtl_st_op1: Op1 → register → register → label → rtl_statement 18  rtl_st_op2: Op2 → register → register → register → label → rtl_statement 19 19  rtl_st_clear_carry: label → rtl_statement 20 20  rtl_st_load: register → register → register → label → rtl_statement 
src/RTLabs/RTLAbstoRTL.ma
r1060 r1061 94 94 λA: Type[0]. 95 95 λleft, right: list A. 96 match left with 97 [ nil ⇒ 98 match right with 99 [ nil ⇒ None ? 100  _ ⇒ Some ? right 101 ] 102  _ ⇒ Some ? left 103 ]. 96 λprfl: 0 < left. 97 λprfr: 0 < right. 98 match left return λx. 0 < x → list A with 99 [ nil ⇒ λnil_prf. 100 match right return λx. 0 < x → list A with 101 [ nil ⇒ λnil_nil_absrd. ? 102  _ ⇒ λnil_cons_prf. right 103 ] prfr 104  _ ⇒ λcons_prf. right 105 ] prfl. 106 normalize in nil_prf; 107 cases(not_le_Sn_O 0) 108 #HYP 109 cases(HYP nil_prf) 110 qed. 104 111 105 112 definition complete_regs ≝ … … 475 482 translate_move destrs srcrs start_lbl dest_lbl def 476 483 ]. 484 485 definition translate_op ≝ 486 λop. 487 λdestrs. 488 λsrcrs1. 489 λsrcrs2. 490 λstart_lbl. 491 λdest_lbl. 492 λdef. 493 λprf: srcrs1 = srcrs2. 494 match reduce_strong ? srcrs1 srcrs2 with 495 [ dp reduced first_reduced_proof ⇒ 496 let srcrsl_common ≝ \fst (\fst reduced) in 497 let srcrsr_common ≝ \fst (\snd reduced) in 498 let srcrsl_rest ≝ \snd (\fst reduced) in 499 let srcrsr_rest ≝ \snd (\snd reduced) in 500 let srcrs_rest ≝ choose_rest ? srcrsl_rest srcrsr_rest ? ? in 501 match reduce_strong ? destrs srcrsl_common with 502 [ dp reduced second_reduced_proof ⇒ 503 let destrs_common ≝ \fst (\fst reduced) in 504 let destrs_rest ≝ \snd (\fst reduced) in 505 match reduce_strong ? destrs_rest srcrs_rest with 506 [ dp reduced third_reduced_proof ⇒ 507 let destrs_cted ≝ \fst (\fst reduced) in 508 let destrs_rest ≝ \snd (\fst reduced) in 509 let srcrs_cted ≝ \fst (\snd reduced) in 510 let 〈def, tmpr〉 ≝ fresh_reg def in 511 let insts_init ≝ [ 512 rtl_st_clear_carry start_lbl; 513 rtl_st_int tmpr (zero ?) start_lbl 514 ] in 515 let f_add ≝ λdestr. λsrcr1. λsrcr2. rtl_st_op2 op destr srcr1 srcr2 start_lbl in 516 let insts_add ≝ map3 … f_add destrs_common srcrsl_common srcrsr_common ? ? in 517 let f_add_cted ≝ λdestr. λsrcr. rtl_st_op2 op destr srcr tmpr start_lbl in 518 let insts_add_cted ≝ map2 ? ? ? f_add_cted destrs_cted srcrs_cted ? in 519 let f_rest ≝ λdestr. rtl_st_op2 op destr tmpr tmpr start_lbl in 520 let insts_rest ≝ map … f_rest destrs_rest in 521 adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def 522 ] 523 ] 524 ]. 525 [ 1: @third_reduced_proof 526  3: @first_reduced_proof 527 528 let translate_op op destrs srcrs1 srcrs2 start_lbl dest_lbl def = 529 let ((srcrs1_common, srcrs1_rest), (srcrs2_common, srcrs2_rest)) = 530 MiscPottier.reduce srcrs1 srcrs2 in 531 let srcrs_rest = choose_rest srcrs1_rest srcrs2_rest in 532 let ((destrs_common, destrs_rest), _) = 533 MiscPottier.reduce destrs srcrs1_common in 534 let ((destrs_cted, destrs_rest), (srcrs_cted, _)) = 535 MiscPottier.reduce destrs_rest srcrs_rest in 536 let (def, tmpr) = fresh_reg def in 537 let insts_init = 538 [RTL.St_clear_carry start_lbl ; 539 RTL.St_int (tmpr, 0, start_lbl)] in 540 let f_add destr srcr1 srcr2 = 541 RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in 542 let insts_add = 543 MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in 544 let f_add_cted destr srcr = 545 RTL.St_op2 (op, destr, srcr, tmpr, start_lbl) in 546 let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in 547 let f_rest destr = 548 RTL.St_op2 (op, destr, tmpr, tmpr, start_lbl) in 549 let insts_rest = List.map f_rest destrs_rest in 550 adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest) 551 start_lbl dest_lbl def 477 552 478 553 definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset
for help on using the changeset viewer.