source: src/RTL/RTL.ma @ 1322

Last change on this file since 1322 was 1322, checked in by sacerdot, 8 years ago

address => stack_address

File size: 2.6 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_stack_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__ register register register register (register × register) register
14  (list register) (list register) rtl_statement_extension.
15definition rtl_params_: params_ ≝ graph_params_ rtl_params__.
16definition rtl_params0: params0 ≝ mk_params0 rtl_params__ (list register) (list register).
17definition rtl_params1: params1 ≝ rtl_ertl_params1 rtl_params0.
18definition rtl_params: ∀globals. params globals ≝ rtl_ertl_params rtl_params0.
19
20definition rtl_statement ≝ joint_statement rtl_params_.
21
22definition rtl_internal_function ≝
23  λglobals. joint_internal_function … (rtl_params globals).
24
25definition rtl_program ≝ joint_program rtl_params.
26
27(************ Same without tail calls ****************)
28
29(*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
30  are not sequential. Thus there is a dummy label at the moment in the code.
31  To be fixed once we understand exactly what to do with tail calls. *)
32inductive rtlntc_statement_extension: Type[0] ≝
33  | rtlntc_st_ext_address: register → register → rtlntc_statement_extension
34  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
35
36definition rtlntc_params__: params__ ≝
37 mk_params__ register register register register (register × register) register
38  (list register) (list register) rtlntc_statement_extension.
39definition rtlntc_params_: params_ ≝ graph_params_ rtlntc_params__.
40definition rtlntc_params0: params0 ≝ mk_params0 rtlntc_params__ (list register) (list register).
41definition rtlntc_params1: params1 ≝ rtl_ertl_params1 rtlntc_params0.
42definition rtlntc_params: ∀globals. params globals ≝ rtl_ertl_params rtlntc_params0.
43
44definition rtlntc_statement ≝ joint_statement rtlntc_params_.
45
46definition rtlntc_internal_function ≝
47  λglobals. joint_internal_function … (rtlntc_params globals).
48
49definition rtlntc_program ≝ joint_program rtlntc_params.
Note: See TracBrowser for help on using the repository browser.