Changeset 1245 for src/RTL/RTLtoERTL.ma
 Timestamp:
 Sep 21, 2011, 10:22:13 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1149 r1245 1 include "RTL/RTL.ma".2 1 include "RTL/RTLTailcall.ma". 3 2 include "utilities/RegisterSet.ma". 4 3 include "common/Identifiers.ma". 5 4 include "ERTL/ERTL.ma". 6 7 definition change_exit_label ≝ 8 λl: label. 9 λp: ertl_internal_function. 10 λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?. 11 let ertl_if_luniverse' ≝ ertl_if_luniverse p in 12 let ertl_if_runiverse' ≝ ertl_if_runiverse p in 13 let ertl_if_params' ≝ ertl_if_params p in 14 let ertl_if_locals' ≝ ertl_if_locals p in 15 let ertl_if_stacksize' ≝ ertl_if_stacksize p in 16 let ertl_if_graph' ≝ ertl_if_graph p in 17 let ertl_if_entry' ≝ ertl_if_entry p in 18 let ertl_if_exit' ≝ l in 19 mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse' 20 ertl_if_params' ertl_if_locals' ertl_if_stacksize' 21 ertl_if_graph' ertl_if_entry' ertl_if_exit'. 22 @prf 23 qed. 24 25 definition change_entry_label ≝ 26 λl: label. 27 λp: ertl_internal_function. 28 λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?. 29 let ertl_if_luniverse' ≝ ertl_if_luniverse p in 30 let ertl_if_runiverse' ≝ ertl_if_runiverse p in 31 let ertl_if_params' ≝ ertl_if_params p in 32 let ertl_if_locals' ≝ ertl_if_locals p in 33 let ertl_if_stacksize' ≝ ertl_if_stacksize p in 34 let ertl_if_graph' ≝ ertl_if_graph p in 35 let ertl_if_entry' ≝ l in 36 let ertl_if_exit' ≝ ertl_if_exit p in 37 mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse' 38 ertl_if_params' ertl_if_locals' ertl_if_stacksize' 39 ertl_if_graph' ertl_if_entry' ertl_if_exit'. 40 @prf 41 qed. 42 5 43 6 definition add_graph ≝ 44 7 λl: label. … … 77 40 ] 78 41 qed. 79 42 80 43 definition fresh_label ≝ 81 44 λdef. … … 351 314 in 352 315 let def ≝ add_graph tmp_lbl last_stmt def in 353 change_exit_labeltmp_lbl def ?316 set_joint_if_exit … tmp_lbl def ? 354 317 ] ?. 355 318 cases not_implemented (* dep types here, bug in matita too! *)
Note: See TracChangeset
for help on using the changeset viewer.