Ignore:
Timestamp:
Sep 26, 2011, 6:07:47 PM (9 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/RTLTailcall.ma

    r1270 r1275  
    66  λlbl: label.
    77  λstmt: rtl_statement globals.
    8   λgraph: codeT … (rtl_params globals).
     8  λgraph: codeT … (rtlntc_params globals).
    99  match stmt with
    1010  [ joint_st_sequential seq DUMMY ⇒
     
    1515              add ? ? graph lbl (joint_st_sequential … (joint_instr_call_id … f args [ ]) exit)
    1616          | rtl_st_ext_tailcall_ptr f1 f2 args ⇒
    17               add ? ? graph lbl (joint_st_sequential … (joint_instr_extension … (rtl_st_ext_call_ptr f1 f2 args [ ])) exit)
     17              add ? ? graph lbl (joint_st_sequential … (joint_instr_extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit)
    1818          | _ ⇒ graph ]
    1919      | _ ⇒ graph ]
     
    2424  λexit: label.
    2525  λgraph: codeT … (rtl_params globals).
    26     foldi ? ? ? (simplify_stmt globals exit) graph graph.
     26    foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
    2727
    2828axiom simplify_graph_preserves_labels:
     
    3636 ∀globals.
    3737  joint_internal_function … (rtl_params globals) →
    38    joint_internal_function … (rtl_params globals)
     38   joint_internal_function … (rtlntc_params globals)
    3939
    4040  λglobals,def.
     
    4949qed.
    5050
    51 definition tailcall_simplify : rtl_program → rtl_program ≝
     51definition tailcall_simplify : rtl_program → rtlntc_program ≝
    5252 λp. transform_program … p (transf_fundef … (simplify_internal …)).
Note: See TracChangeset for help on using the changeset viewer.