source: src/RTL/RTL.ma @ 1270

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

Making RTL syntax an instance of Joint.

File size: 1.1 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_call_ptr: register → register → list register → list register → rtl_statement_extension
8  | rtl_st_ext_tailcall_id: ident → list register → rtl_statement_extension
9  | rtl_st_ext_tailcall_ptr: register → register → list register → rtl_statement_extension.
10
11definition rtl_params_: params_ ≝
12 mk_params_
13  (mk_params__ register register register register
14    (register × register) register (list register) (list register)
15      rtl_statement_extension unit (list register) (list register)) label.
16
17definition rtl_statement ≝ joint_statement rtl_params_.
18
19definition rtl_params: ∀globals. params globals ≝ graph_params rtl_params_.
20
21definition rtl_internal_function ≝
22  λglobals.
23    joint_internal_function globals (rtl_params globals).
24
25definition rtl_program ≝ joint_program rtl_params.
Note: See TracBrowser for help on using the repository browser.