source: src/RTL/RTLtoERTL.ma @ 756

Last change on this file since 756 was 756, checked in by mulligan, 9 years ago

Made a start on RTL. Renaming in ERTL and below to move closer to Brian's naming convention and datatypes.

File size: 1.7 KB
Line 
1include "RTL/RTL.ma".
2
3definition change_exit_label ≝
4  λl: label.
5  λp: rtl_internal_function.
6  let rtl_if_luniverse' ≝ rtl_if_luniverse p in
7  let rtl_if_runiverse' ≝ rtl_if_runiverse p in
8  let rtl_if_sig' ≝ rtl_if_sig p in
9  let rtl_if_result' ≝ rtl_if_result p in
10  let rtl_if_params' ≝ rtl_if_params p in
11  let rtl_if_locals' ≝ rtl_if_locals p in
12  let rtl_if_stacksize' ≝ rtl_if_stacksize p in
13  let rtl_if_graph' ≝ rtl_if_graph p in
14  let rtl_if_entry' ≝ rtl_if_entry p in
15  let rtl_if_exit' ≝ l in
16    mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse'
17                             rtl_if_sig' rtl_if_result' rtl_if_params'
18                             rtl_if_locals' rtl_if_stacksize'
19                             rtl_if_graph' rtl_if_entry' rtl_if_exit'.
20
21definition change_entry_label ≝
22  λl: label.
23  λp: rtl_internal_function.
24  let rtl_if_luniverse' ≝ rtl_if_luniverse p in
25  let rtl_if_runiverse' ≝ rtl_if_runiverse p in
26  let rtl_if_sig' ≝ rtl_if_sig p in
27  let rtl_if_result' ≝ rtl_if_result p in
28  let rtl_if_params' ≝ rtl_if_params p in
29  let rtl_if_locals' ≝ rtl_if_locals p in
30  let rtl_if_stacksize' ≝ rtl_if_stacksize p in
31  let rtl_if_graph' ≝ rtl_if_graph p in
32  let rtl_if_entry' ≝ l in
33  let rtl_if_exit' ≝ rtl_if_exit p in
34    mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse'
35                             rtl_if_sig' rtl_if_result' rtl_if_params'
36                             rtl_if_locals' rtl_if_stacksize'
37                             rtl_if_graph' rtl_if_entry' rtl_if_exit'.
38                             
39definition fresh_label ≝
40  λdef.
41    fresh LabelTag (rtl_if_luniverse def).
42   
43definition change_label ≝
44  λ
Note: See TracBrowser for help on using the repository browser.