Changeset 1275 for src/RTL/RTLtoERTL.ma
 Timestamp:
 Sep 26, 2011, 6:07:47 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1270 r1275 369 369 ) start_lbl dest_lbl def. 370 370 371 axiom translate_stmt : 372 ∀globals: list ident. label → rtl_statement globals → ertl_internal_function globals → ertl_internal_function globals. 373 (* 371 definition translate_stmt : 372 ∀globals: list ident. label → rtl_statement globals → ertl_internal_function globals → ertl_internal_function globals 374 373 ≝ 375 374 λglobals. … … 378 377 λdef. 379 378 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 retype it from now on; 400 the problem is call_id that takes different parameters, but that is patternmatched 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 ]]. 412 426 cases not_implemented 413 qed. *)427 qed. 414 428 415 429 (* hack with empty graphs used here *) … … 429 443 graph' ? ? in 430 444 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'. 433 446 whd in match ertl_params (* CSC: Matita's bug here; not enough/too much reduction 434 447 makes the next application fail. Why? *) … … 485 498 definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)). 486 499 487 (*488 definition move_first_cost_label_up ≝489 λglobals.490 λA: Type[0].491 λid_def: A × ?.492 let 〈id, def〉 ≝ id_def in493 let def' ≝494 match def with495 [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal … (translate_funct_internal globals int_fun))496  External ext ⇒ External … ext497 ]498 in499 〈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 in505 let vars ≝ map ? ? f (rtl_pr_functs p) in506 mk_ertl_program (rtl_pr_vars p) vars (rtl_pr_main p).507 *)508 509 500 definition translate : rtl_program → ertl_program ≝ 510 501 λp. 511 502 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.