Changeset 1275 for src/RTL/RTLtoERTL.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/RTLtoERTL.ma

    r1270 r1275  
    369369    ) start_lbl dest_lbl def.
    370370
    371 axiom translate_stmt :
    372  ∀globals: list ident. label → rtl_statement globals → ertl_internal_function globals → ertl_internal_function globals.
    373 (*
     371definition translate_stmt :
     372 ∀globals: list ident. label → rtl_statement globals → ertl_internal_function globals → ertl_internal_function globals
    374373 ≝
    375374  λglobals.
     
    378377  λdef.
    379378  match stmt with
    380   [ rtl_st_skip lbl' ⇒ add_graph … lbl (ertl_st_skip lbl') def
    381   | rtl_st_cost cost_lbl lbl' ⇒ add_graph … lbl (ertl_st_cost cost_lbl lbl') def
    382   | rtl_st_addr r1 r2 x lbl' ⇒ add_graph … lbl (ertl_st_addr r1 r2 x lbl') def
    383   | rtl_st_stack_addr r1 r2 lbl' ⇒
    384     adds_graph … [
    385       ertl_st_get_hdw r1 RegisterSPL lbl;
    386       ertl_st_get_hdw r2 RegisterSPH lbl
    387     ] lbl lbl' def
    388   | rtl_st_int r i lbl' ⇒  add_graph … lbl (ertl_st_int r i lbl') def
    389   | rtl_st_move r1 r2 lbl' ⇒ add_graph … lbl (ertl_st_move r1 r2 lbl') def
    390   | rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒
    391       add_graph … lbl (ertl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl) def
    392   | rtl_st_op1 op1 destr srcr lbl' ⇒
    393     add_graph … lbl (ertl_st_op1 op1 destr srcr lbl') def
    394   | rtl_st_op2 op2 destr srcr1 srcr2 lbl' ⇒
    395     add_graph … lbl (ertl_st_op2 op2 destr srcr1 srcr2 lbl') def
    396   | rtl_st_clear_carry lbl' ⇒
    397     add_graph … lbl (ertl_st_clear_carry lbl') def
    398   | rtl_st_set_carry lbl' ⇒
    399     add_graph … lbl (ertl_st_set_carry lbl') def
    400   | rtl_st_load destr addr1 addr2 lbl' ⇒
    401     add_graph … lbl (ertl_st_load destr addr1 addr2 lbl') def
    402   | rtl_st_store addr1 addr2 srcr lbl' ⇒
    403     add_graph … lbl (ertl_st_store addr1 addr2 srcr lbl') def
    404   | rtl_st_call_id f args ret_regs lbl' ⇒
    405     translate_call_id … f args ret_regs lbl lbl' def
    406   | rtl_st_cond srcr lbl_true lbl_false ⇒
    407     add_graph … lbl (ertl_st_cond srcr lbl_true lbl_false) def
    408   | rtl_st_return ⇒
    409     add_graph … lbl ertl_st_return def
    410   | _ ⇒ ? (* assert false: not implemented or should not happen *)
    411   ].
     379  [ joint_st_goto lbl' ⇒ add_graph … lbl (joint_st_goto … lbl') def
     380  | joint_st_return ⇒ add_graph … lbl (joint_st_return …) def
     381  | joint_st_sequential seq lbl' ⇒
     382     match seq with
     383      [ joint_instr_call_id f args ret_regs ⇒
     384         translate_call_id … f args ret_regs lbl lbl' def
     385      | joint_instr_move rs ⇒
     386         let 〈r1,r2〉 ≝ rs in
     387         let rs ≝ 〈pseudo r1, pseudo r2〉 in
     388          add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_move … rs) lbl') def
     389      | joint_instr_extension ext ⇒
     390         match ext with
     391          [ rtl_st_ext_call_ptr _ _ _ _ ⇒ ? (*CSC: XXXX not implemented in OCaml too *)
     392          | rtl_st_ext_address r1 r2 ⇒
     393             adds_graph … [
     394              joint_st_sequential … (joint_instr_move … 〈pseudo r1, hardware RegisterSPL〉) lbl;
     395              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          ]
     399      (*CSC: everything is just copied to re-type it from now on;
     400        the problem is call_id that takes different parameters, but that is pattern-matched
     401        above. It could be made nicer at the cost of making all the rest of the code uglier *)
     402      | joint_instr_cost_label cost_lbl ⇒ add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_cost_label … cost_lbl) lbl') def
     403      | joint_instr_address x prf r1 r2 ⇒ add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_address … x prf r1 r2) lbl') def
     404      | joint_instr_int r i ⇒  add_graph … lbl (joint_st_sequential ertl_params_ globals (joint_instr_int … r i) lbl') def
     405      | joint_instr_opaccs op destr1 destr2 srcr1 srcr2 ⇒
     406          add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_opaccs … op destr1 destr2 srcr1 srcr2) lbl') def
     407      | joint_instr_op1 op1 destr srcr ⇒
     408        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_op1 … op1 destr srcr) lbl') def
     409      | joint_instr_op2 op2 destr srcr1 srcr2 ⇒
     410        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_op2 … op2 destr srcr1 srcr2) lbl') def
     411      | joint_instr_clear_carry ⇒
     412        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_clear_carry …) lbl') def
     413      | joint_instr_set_carry ⇒
     414        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_set_carry …) lbl') def
     415      | joint_instr_load destr addr1 addr2 ⇒
     416        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_load … destr addr1 addr2) lbl') def
     417      | joint_instr_store addr1 addr2 srcr ⇒
     418        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_store … addr1 addr2 srcr) lbl') def
     419      | joint_instr_cond srcr lbl_true ⇒
     420        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_cond … srcr lbl_true) lbl') def
     421      | joint_instr_comment msg ⇒
     422        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 *)
     425      ]].
    412426  cases not_implemented
    413 qed.*) 
     427qed.
    414428
    415429(* hack with empty graphs used here *)
     
    429443      graph' ? ? in
    430444  let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in
    431   let def' ≝ add_pro_and_epilogue … (joint_if_params … def) (joint_if_result … def) def' in
    432     def'.
     445   add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
    433446whd in match ertl_params (* CSC: Matita's bug here; not enough/too much reduction
    434447                                 makes the next application fail. Why? *)   
     
    485498definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
    486499
    487 (*
    488 definition move_first_cost_label_up ≝
    489   λglobals.
    490   λA: Type[0].
    491   λid_def: A × ?.
    492   let 〈id, def〉 ≝ id_def in
    493   let def' ≝
    494     match def with
    495     [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal … (translate_funct_internal globals int_fun))
    496     | External ext ⇒ External … ext
    497     ]
    498   in
    499     〈id, def'〉.
    500 
    501 definition translate ≝
    502   λp.
    503   let p ≝ tailcall_simplify p in (* tailcall simplification here *)
    504   let f ≝ λfunct. move_first_cost_label_up ? funct in
    505   let vars ≝ map ? ? f (rtl_pr_functs p) in
    506     mk_ertl_program (rtl_pr_vars p) vars (rtl_pr_main p).
    507 *)
    508 
    509500definition translate : rtl_program → ertl_program ≝
    510501 λp.
    511502  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
    512     transform_program ??? p (transf_fundef ?? translate_funct).
     503    transform_program ??? p (transf_fundef ?? (translate_funct …)).
Note: See TracChangeset for help on using the changeset viewer.