Changeset 1071 for src/RTLabs
 Timestamp:
 Jul 15, 2011, 2:40:40 PM (9 years ago)
 Location:
 src/RTLabs
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1068 r1071 2 2 include "RTL/RTL.ma". 3 3 include "common/AssocList.ma". 4 include "common/FrontEndOps.ma". 4 5 include "common/Graphs.ma". 5 include "common/FrontEndOps.ma". 6 7 axiom graph_add_lookup: 8 ∀g: graph rtl_statement. 9 ∀l: label. 10 ∀s: rtl_statement. 11 ∀to_insert: label. 12 lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?. 6 13 7 14 definition add_graph ≝ … … 20 27 mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse' 21 28 rtl_if_params' rtl_if_params' rtl_if_locals' 22 rtl_if_stacksize' rtl_if_graph' rtl_if_entry' 23 rtl_if_exit'. 29 rtl_if_stacksize' rtl_if_graph' ? ?. 30 [1: cases(rtl_if_entry') 31 #LABEL #HYP 32 % 33 [1: @LABEL 34 2: cases(HYP) 35 #STMT 36 #FRST_PRF 37 % 38 [1: @STMT 39 2: <FRST_PRF @(graph_add_lookup (rtl_if_graph p) LABEL stmt) 40 ] 41 ] 42 24 43 25 44 definition fresh_label: rtl_internal_function → rtl_internal_function × label ≝ … … 316 335 λsrcrs: list register. 317 336 λstart_lbl: label. 318 match reduce_strong register destrs srcrs with337 match reduce_strong register register destrs srcrs with 319 338 [ dp crl_crr len_proof ⇒ 320 339 let commonl ≝ \fst (\fst crl_crr) in … … 399 418 translate_move destrs srcrs 400 419 else 401 match reduce_strong ?destrs srcrs with420 match reduce_strong register register destrs srcrs with 402 421 [ dp crl len_proof ⇒ 403 422 let commonl ≝ \fst (\fst crl) in … … 510 529 λdest_lbl. 511 530 λdef. 512 match reduce_strong ?srcrs1 srcrs2 with531 match reduce_strong register register srcrs1 srcrs2 with 513 532 [ dp reduced first_reduced_proof ⇒ 514 533 let srcrsl_common ≝ \fst (\fst reduced) in … … 517 536 let srcrsr_rest ≝ \snd (\snd reduced) in 518 537 let srcrs_rest ≝ choose_rest ? srcrsl_rest srcrsr_rest ? ? in 519 match reduce_strong ?destrs srcrsl_common with538 match reduce_strong register register destrs srcrsl_common with 520 539 [ dp reduced second_reduced_proof ⇒ 521 540 let destrs_common ≝ \fst (\fst reduced) in 522 541 let destrs_rest ≝ \snd (\fst reduced) in 523 match reduce_strong ?destrs_rest srcrs_rest with542 match reduce_strong register register destrs_rest srcrs_rest with 524 543 [ dp reduced third_reduced_proof ⇒ 525 544 let destrs_cted ≝ \fst (\fst reduced) in … … 704 723 let 〈def, tmp_srcrs2〉 ≝ fresh_regs def (srcrs2) in 705 724 let save_srcrs2 ≝ translate_move tmp_srcrs2 srcrs2 in 706 match reduce_strong ?tmp_srcrs1 tmp_srcrs2 with725 match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with 707 726 [ dp crl their_proof ⇒ 708 727 let commonl ≝ \fst (\fst crl) in 
src/RTLabs/syntax.ma
r1070 r1071 35 35 ; f_stacksize : nat 36 36 ; f_graph : graph statement 37 ; f_entry : Σl:label. ∃s. lookup ?? f_graph l = Some ? s38 ; f_exit : Σl:label. ∃s. lookup ?? f_graph l = Some ? s37 ; f_entry : Σl:label. lookup ?? f_graph l ≠ None ? 38 ; f_exit : Σl:label. lookup ?? f_graph l ≠ None ? 39 39 }. 40 40
Note: See TracChangeset
for help on using the changeset viewer.