source: src/RTL/RTL.ma @ 1278

Last change on this file since 1278 was 1278, checked in by sacerdot, 9 years ago

oppargs requires two more arguments. RTLtoERTL to be fixed since it was
bugged anyway

File size: 2.3 KB
Line 
1include "joint/Joint.ma".
2
3(*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
4  are not sequential. Thus there is a dummy label at the moment in the code.
5  To be fixed once we understand exactly what to do with tail calls. *)
6inductive rtl_statement_extension: Type[0] ≝
7  | rtl_st_ext_address: register → register → rtl_statement_extension
8  | rtl_st_ext_call_ptr: register → register → list register → list register → rtl_statement_extension
9  | rtl_st_ext_tailcall_id: ident → list register → rtl_statement_extension
10  | rtl_st_ext_tailcall_ptr: register → register → list register → rtl_statement_extension.
11
12definition rtl_params_: params_ ≝
13 mk_params_
14  (mk_params__ register register register register
15    (register × register) register (list register) (list register)
16      rtl_statement_extension (list register) (list register) (list register)) label.
17
18definition rtl_statement ≝ joint_statement rtl_params_.
19
20definition rtl_params: ∀globals. params globals ≝ graph_params rtl_params_.
21
22definition rtl_internal_function ≝
23  λglobals.
24    joint_internal_function globals (rtl_params globals).
25
26definition rtl_program ≝ joint_program rtl_params.
27
28(************ Same without tail calls ****************)
29
30(*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
31  are not sequential. Thus there is a dummy label at the moment in the code.
32  To be fixed once we understand exactly what to do with tail calls. *)
33inductive rtlntc_statement_extension: Type[0] ≝
34  | rtlntc_st_ext_address: register → register → rtlntc_statement_extension
35  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
36
37definition rtlntc_params_: params_ ≝
38 mk_params_
39  (mk_params__ register register register register
40    (register × register) register (list register) (list register)
41      rtlntc_statement_extension (list register) (list register) (list register)) label.
42
43definition rtlntc_statement ≝ joint_statement rtlntc_params_.
44
45definition rtlntc_params: ∀globals. params globals ≝ graph_params rtlntc_params_.
46
47definition rtlntc_internal_function ≝
48  λglobals.
49    joint_internal_function globals (rtlntc_params globals).
50
51definition rtlntc_program ≝ joint_program rtlntc_params.
Note: See TracBrowser for help on using the repository browser.