Changeset 1262


Ignore:
Timestamp:
Sep 23, 2011, 4:40:54 PM (8 years ago)
Author:
sacerdot
Message:

RTLtoERTL ported to the joint syntax for ERTL. Now it is time to port RTL
to the joint syntax too.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r1259 r1262  
    369369    ) start_lbl dest_lbl def.
    370370
    371 definition translate_stmt ≝
     371axiom translate_stmt :
     372 ∀globals: list ident. label → rtl_statement → ertl_internal_function globals → ertl_internal_function globals.
     373(*
     374 ≝
    372375  λglobals.
    373376  λlbl.
     
    408411  ].
    409412  cases not_implemented
    410 qed.   
     413qed.*) 
    411414
    412415(* hack with empty graphs used here *)
    413416definition translate_funct_internal ≝
    414   λdef.
     417  λglobals,def.
    415418  let nb_params ≝ |rtl_if_params def| in
    416419  let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in
     
    418421  let entry' ≝ rtl_if_entry def in
    419422  let exit' ≝ rtl_if_exit def in
    420   let graph' ≝ add ? ? (empty_map ? ?) entry' (ertl_st_skip entry') in
    421   let graph' ≝ add ? ? graph' exit' (ertl_st_skip exit') in
     423  let graph' ≝ add ? ? (empty_map ? ?) entry' (joint_st_goto … entry') in
     424  let graph' ≝ add ? ? graph' exit' (joint_st_goto … exit') in
    422425  let def' ≝
    423     mk_ertl_internal_function
    424       (rtl_if_luniverse def) (rtl_if_runiverse def)
    425       nb_params new_locals ((rtl_if_stacksize def) + added_stacksize)
     426    mk_joint_internal_function globals (ertl_params globals)
     427      (rtl_if_luniverse def) (rtl_if_runiverse … def) it
     428      nb_params new_locals ((rtl_if_stacksize def) + added_stacksize)
    426429      graph' ? ? in
    427   let def' ≝ foldi ? ? ? translate_stmt (rtl_if_graph def) def' in
    428   let def' ≝ add_pro_and_epilogue (rtl_if_params def) (rtl_if_result def) def' in
     430  let def' ≝ foldi ? ? ? (translate_stmt globals) (rtl_if_graph def) def' in
     431  let def' ≝ add_pro_and_epilogue (rtl_if_params def) (rtl_if_result def) def' in
    429432    def'.
    430   [1: %
    431       [1: @entry'
    432       |2: normalize nodelta
    433           @graph_add_lookup
    434           @graph_add
    435       ]
    436   |2: %
    437       [1: @exit'
    438       |2: normalize nodelta
    439           @graph_add
    440       ]
    441   ]
    442 qed.
    443    
    444 definition translate_funct ≝
    445   λid_def: ident × ?.
    446   let 〈id, def〉 ≝ id_def in
    447   let def' ≝
    448     match def with
    449     [ Internal def ⇒ Internal ? (translate_funct_internal def)
    450     | External def ⇒ External ? def
    451     ] in
    452   〈id, def'〉.
     433whd in match ertl_params (* CSC: Matita's bug here; not enough/too much reduction
     434                                 makes the next application fail. Why? *)   
     435%
     436 [ @entry' | @graph_add_lookup @graph_add
     437 | @exit'  | @graph_add ]
     438qed.
    453439
    454440definition generate ≝
     441  λglobals.
    455442  λstmt.
    456443  λdef.
    457   let 〈entry, nuniv〉 ≝ fresh_label def in
    458   let graph ≝ add ? ? (ertl_if_graph def) entry stmt in
    459     mk_ertl_internal_function
    460       nuniv (ertl_if_runiverse def) (ertl_if_params def)
    461       (ertl_if_locals def) (ertl_if_stacksize def) graph
    462       ? ?.
    463   [1: %
    464     [1: @entry
    465     |2: normalize nodelta;
    466         @graph_add
    467     ]
    468   |2: generalize in match (ertl_if_exit def)
    469       #HYP
    470       cases HYP
    471       #LBL #LBL_PRF
    472       %
    473       [1: @LBL
    474       |2: normalize nodelta;
    475           @graph_add_lookup
    476           @LBL_PRF
    477       ]
    478   ]
    479 qed.
    480    
    481 let rec find_and_remove_first_cost_label_internal
    482   (def: ertl_internal_function) (lbl: label) (num_nodes: nat)
     444  let 〈entry, nuniv〉 ≝ fresh_label … def in
     445  let graph ≝ add ? ? (joint_if_code … def) entry stmt in
     446    mk_joint_internal_function ? (ertl_params globals)
     447      nuniv (joint_if_runiverse … def) it (joint_if_params … def)
     448      (joint_if_locals … def) (joint_if_stacksize … def) graph
     449      ? ?.     
     450  [ % [ @entry | @graph_add ]
     451  | cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF ]
     452qed.
     453
     454let rec find_and_remove_first_cost_label_internal (globals: list ident)
     455  (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat)
    483456    on num_nodes ≝
    484457  match num_nodes with
    485458  [ O ⇒ 〈None ?, def〉
    486459  | S num_nodes' ⇒
    487     match lookup ? ? (ertl_if_graph def) lbl with
     460    match lookup … (joint_if_code … def) lbl with
    488461    [ None ⇒ 〈None ?, def〉
    489     | Some stmt ⇒
     462    | Some stmt ⇒ 
    490463      match stmt with
    491       [ ertl_st_cost cost_lbl next_lbl ⇒
    492           〈Some ? cost_lbl, add_graph lbl (ertl_st_skip next_lbl) def〉
    493       | ertl_st_cond _ _ _ ⇒ 〈None ?, def〉
    494       | ertl_st_return ⇒ 〈None ?, def〉
    495       | ertl_st_skip lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    496       | ertl_st_comment _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    497       | ertl_st_get_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    498       | ertl_st_set_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    499       | ertl_st_hdw_to_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    500       | ertl_st_pop _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    501       | ertl_st_push _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    502       | ertl_st_addr _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    503       | ertl_st_int _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    504       | ertl_st_move _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    505       | ertl_st_opaccs _ _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    506       | ertl_st_op1 _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    507       | ertl_st_op2 _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    508       | ertl_st_clear_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    509       | ertl_st_set_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    510       | ertl_st_load _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    511       | ertl_st_store _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    512       | ertl_st_call_id _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    513       | ertl_st_new_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    514       | ertl_st_del_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    515       | ertl_st_frame_size _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    516       ]
    517     ]
    518   ].
     464      [ joint_st_sequential inst lbl ⇒
     465         match inst with
     466          [ joint_instr_cost_label cost_lbl ⇒
     467             〈Some … cost_lbl, add_graph ertl_params_ globals lbl (joint_st_goto … lbl) def〉
     468          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
     469      | joint_st_return ⇒ 〈None …, def〉
     470      | joint_st_goto lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
     471      ]]].
    519472   
    520473definition find_and_remove_first_cost_label ≝
    521   λdef. 
    522     find_and_remove_first_cost_label_internal def (ertl_if_entry def) (graph_num_nodes ? (ertl_if_graph def)).
     474  λglobals,def. 
     475    find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)).
    523476
    524477definition move_first_cost_label_up_internal ≝
    525   λdef.
    526   let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label def in
     478  λglobals,def.
     479  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label def in
    527480  match cost_label with
    528481  [ None ⇒ def
    529   | Some cost_label ⇒ generate (ertl_st_cost cost_label (ertl_if_entry def)) def
    530   ].
    531 
     482  | Some cost_label ⇒ generate … (joint_st_sequential ertl_params_ globals (joint_instr_cost_label … cost_label) (joint_if_entry … def)) def
     483  ].
     484
     485definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
     486
     487(*
    532488definition move_first_cost_label_up ≝
     489  λglobals.
    533490  λA: Type[0].
    534491  λid_def: A × ?.
     
    536493  let def' ≝
    537494    match def with
    538     [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal int_fun)
    539     | External ext ⇒ def
     495    [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal … (translate_funct_internal globals int_fun))
     496    | External ext ⇒ External … ext
    540497    ]
    541498  in
     
    545502  λp.
    546503  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
    547   let f ≝ λfunct. move_first_cost_label_up ? (translate_funct funct) in
     504  let f ≝ λfunct. move_first_cost_label_up ? funct in
    548505  let vars ≝ map ? ? f (rtl_pr_functs p) in
    549506    mk_ertl_program (rtl_pr_vars p) vars (rtl_pr_main p).
     507*)
     508
     509definition translate : rtl_program → ertl_program ≝
     510 λp.
     511  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
     512    transform_program ??? p (transf_fundef ?? translate_funct).
Note: See TracChangeset for help on using the changeset viewer.