source: src/RTL/RTL.ma @ 1275

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

RTL ported to joint syntax, but:

  1. bug discovered: opaccs should have taken four registers
  2. push/pop should not be present in RTL :-(

ERTLToLTL and RTLtoERTL not working ATM

File size: 2.5 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 unit (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  | rtlntc_st_ext_tailcall_id: ident → list register → rtlntc_statement_extension
37  | rtlntc_st_ext_tailcall_ptr: register → register → list register → rtlntc_statement_extension.
38
39definition rtlntc_params_: params_ ≝
40 mk_params_
41  (mk_params__ register register register register
42    (register × register) register (list register) (list register)
43      rtlntc_statement_extension unit (list register) (list register)) label.
44
45definition rtlntc_statement ≝ joint_statement rtlntc_params_.
46
47definition rtlntc_params: ∀globals. params globals ≝ graph_params rtlntc_params_.
48
49definition rtlntc_internal_function ≝
50  λglobals.
51    joint_internal_function globals (rtlntc_params globals).
52
53definition rtlntc_program ≝ joint_program rtlntc_params.
Note: See TracBrowser for help on using the repository browser.