Changeset 1061 for src/RTLabs
 Timestamp:
 Jul 8, 2011, 5:49:22 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.