Changeset 1275 for src/RTL/RTL.ma


Ignore:
Timestamp:
Sep 26, 2011, 6:07:47 PM (8 years ago)
Author:
sacerdot
Message:

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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r1270 r1275  
    55  To be fixed once we understand exactly what to do with tail calls. *)
    66inductive rtl_statement_extension: Type[0] ≝
     7  | rtl_st_ext_address: register → register → rtl_statement_extension
    78  | rtl_st_ext_call_ptr: register → register → list register → list register → rtl_statement_extension
    89  | rtl_st_ext_tailcall_id: ident → list register → rtl_statement_extension
     
    2425
    2526definition 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 TracChangeset for help on using the changeset viewer.