Changeset 1278 for src/RTL/RTLtoERTL.ma


Ignore:
Timestamp:
Sep 27, 2011, 9:57:12 AM (9 years ago)
Author:
sacerdot
Message:

oppargs requires two more arguments. RTLtoERTL to be fixed since it was
bugged anyway

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r1275 r1278  
    370370
    371371definition translate_stmt :
    372  ∀globals: list ident. label → rtl_statement globals → ertl_internal_function globals → ertl_internal_function globals
     372 ∀globals: list ident. label → rtlntc_statement globals → ertl_internal_function globals → ertl_internal_function globals
    373373 ≝
    374374  λglobals.
     
    381381  | joint_st_sequential seq lbl' ⇒
    382382     match seq with
    383       [ joint_instr_call_id f args ret_regs ⇒
     383      [ joint_instr_push _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
     384      | joint_instr_pop _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
     385      | joint_instr_call_id f args ret_regs ⇒
    384386         translate_call_id … f args ret_regs lbl lbl' def
    385387      | joint_instr_move rs ⇒
     
    389391      | joint_instr_extension ext ⇒
    390392         match ext with
    391           [ rtl_st_ext_call_ptr _ _ _ _ ⇒ ? (*CSC: XXXX not implemented in OCaml too *)
    392           | rtl_st_ext_address r1 r2 ⇒
     393          [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *)
     394          | rtlntc_st_ext_address r1 r2 ⇒
    393395             adds_graph … [
    394396              joint_st_sequential … (joint_instr_move … 〈pseudo r1, hardware RegisterSPL〉) lbl;
    395397              joint_st_sequential … (joint_instr_move … 〈pseudo r2, hardware RegisterSPH〉) lbl
    396              ] lbl lbl' def
    397           (*| _ ⇒ ? (* assert false: not implemented or should not happen *)*)
    398           ]
     398             ] lbl lbl' def]
    399399      (*CSC: everything is just copied to re-type it from now on;
    400400        the problem is call_id that takes different parameters, but that is pattern-matched
     
    421421      | joint_instr_comment msg ⇒
    422422        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_comment … msg) lbl') def
    423       | joint_instr_push _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
    424       | joint_instr_pop _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
    425423      ]].
    426   cases not_implemented
     424  cases not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
    427425qed.
    428426
    429427(* hack with empty graphs used here *)
    430428definition translate_funct_internal ≝
    431   λglobals.λdef:rtl_internal_function globals.
     429  λglobals.λdef:rtlntc_internal_function globals.
    432430  let nb_params ≝ |joint_if_params ?? def| in
    433431  let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in
Note: See TracChangeset for help on using the changeset viewer.