Changeset 2490 for src/RTL/RTLToERTL.ma


Ignore:
Timestamp:
Nov 25, 2012, 1:33:09 PM (8 years ago)
Author:
tranquil
Message:

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTL.ma

    r2286 r2490  
    222222        [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
    223223      ]
    224     | CALL_ID f args ret_regs ⇒
     224    | CALL f args ret_regs ⇒
    225225      set_params ? args @@
    226       CALL_ID ERTL ? f (|args|) it :::
     226      CALL ERTL ? f (|args|) it :::
    227227      fetch_result ? ret_regs
    228     | extension_call c ⇒
    229       match c with
    230       [ rtl_call_ptr f1 f2 args dest ⇒
    231         ?
    232       ]
    233228    ]
    234229  | COND r ltrue ⇒
    235230    COND ERTL ? r ltrue
    236   ]. cases daemon (* pointer call to be ported yet *) qed.
     231  ].
    237232
    238233definition translate_fin_step :
     
    243238  [ GOTO lbl' ⇒ GOTO … lbl'
    244239  | RETURN ⇒ RETURN ?
    245   | tailcall abs ⇒ match abs in void with [ ]
     240  | TAILCALL abs _ _ ⇒ match abs in False with [ ]
    246241  ].
    247242
    248243(* hack with empty graphs used here *)
    249244definition translate_funct :
    250   ∀globals.joint_internal_function RTL_ntc globals →
    251     joint_internal_function ERTL globals ≝
     245  ∀globals.joint_closed_internal_function RTL_ntc globals →
     246    joint_closed_internal_function ERTL globals ≝
    252247  λglobals,def.
    253248  let nb_params ≝ |joint_if_params ?? def| in
     
    267262    def in
    268263  add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
     264 cases daemon (* TODO *) qed.
    269265
    270266(* removing this because of how insert_prologue is now defined
Note: See TracChangeset for help on using the changeset viewer.