Changeset 1079


Ignore:
Timestamp:
Jul 19, 2011, 4:30:04 PM (8 years ago)
Author:
mulligan
Message:

finished rtl to ertl pass modulo conversion of tailcall simplification code

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r1077 r1079  
    11include "RTL/RTL.ma".
     2include "RTL/RTLTailcall.ma".
    23include "utilities/RegisterSet.ma".
    34include "common/Identifiers.ma".
     
    528529qed.   
    529530
     531(* hack with empty graphs used here *)
    530532definition translate_funct_internal ≝
    531533  λdef.
     
    535537  let entry' ≝ rtl_if_entry def in
    536538  let exit' ≝ rtl_if_exit def in
     539  let graph' ≝ add ? ? (empty_map ? ?) entry' (ertl_st_skip entry') in
     540  let graph' ≝ add ? ? graph' exit' (ertl_st_skip exit') in
    537541  let def' ≝
    538542    mk_ertl_internal_function
    539543      (rtl_if_luniverse def) (rtl_if_runiverse def)
    540544      nb_params new_locals ((rtl_if_stacksize def) + added_stacksize)
    541       (empty_map ? ?) ? ? in
     545      graph' ? ? in
    542546  let def' ≝ foldi ? ? ? translate_stmt (rtl_if_graph def) def' in
    543547  let def' ≝ add_pro_and_epilogue (rtl_if_params def) (rtl_if_result def) def' in
    544548    def'.
    545   [1: cases entry'
    546       #LBL #LBL_PRF
    547       %
    548       [1: @LBL
    549       |2: @LBL_PRF
     549  [1: %
     550      [1: @entry'
     551      |2: normalize nodelta
     552          @graph_add_lookup
     553          @graph_add
     554      ]
     555  |2: %
     556      [1: @exit'
     557      |2: normalize nodelta
     558          @graph_add
     559      ]
     560  ]
     561qed.
    550562   
    551563definition translate_funct ≝
     
    567579      nuniv (ertl_if_runiverse def) (ertl_if_params def)
    568580      (ertl_if_locals def) (ertl_if_stacksize def) graph
    569       entry (ertl_if_exit def).
    570    
    571 let generate stmt def =
    572   let entry = Label.Gen.fresh def.ERTL.f_luniverse in
    573   let def =
    574     { def with ERTL.f_graph = Label.Map.add entry stmt def.ERTL.f_graph } in
    575   { def with ERTL.f_entry = entry }
    576 
     581      ? ?.
     582  [1: %
     583    [1: @entry
     584    |2: normalize nodelta;
     585        @graph_add
     586    ]
     587  |2: generalize in match (ertl_if_exit def)
     588      #HYP
     589      cases HYP
     590      #LBL #LBL_PRF
     591      %
     592      [1: @LBL
     593      |2: normalize nodelta;
     594          @graph_add_lookup
     595          @LBL_PRF
     596      ]
     597  ]
     598qed.
     599   
     600let rec find_and_remove_first_cost_label_internal
     601  (def: ertl_internal_function) (lbl: label) (num_nodes: nat)
     602    on num_nodes ≝
     603  match num_nodes with
     604  [ O ⇒ 〈None ?, def〉
     605  | S num_nodes' ⇒
     606    match lookup ? ? (ertl_if_graph def) lbl with
     607    [ None ⇒ 〈None ?, def〉
     608    | Some stmt ⇒
     609      match stmt with
     610      [ ertl_st_cost cost_lbl next_lbl ⇒
     611          〈Some ? cost_lbl, add_graph lbl (ertl_st_skip next_lbl) def〉
     612      | ertl_st_cond _ _ _ ⇒ 〈None ?, def〉
     613      | ertl_st_return ⇒ 〈None ?, def〉
     614      | ertl_st_skip lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     615      | ertl_st_comment _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     616      | ertl_st_get_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     617      | ertl_st_set_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     618      | ertl_st_hdw_to_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     619      | ertl_st_pop _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     620      | ertl_st_push _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     621      | ertl_st_addr_h _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     622      | ertl_st_addr_l _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     623      | ertl_st_int _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     624      | ertl_st_move _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     625      | ertl_st_opaccs_a _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     626      | ertl_st_opaccs_b _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     627      | ertl_st_op1 _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     628      | ertl_st_op2 _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     629      | ertl_st_clear_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     630      | ertl_st_set_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     631      | ertl_st_load _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     632      | ertl_st_store _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     633      | ertl_st_call_id _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     634      | ertl_st_new_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     635      | ertl_st_del_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     636      | ertl_st_frame_size _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     637      ]
     638    ]
     639  ].
     640   
     641definition find_and_remove_first_cost_label ≝
     642  λdef. 
     643    find_and_remove_first_cost_label_internal def (ertl_if_entry def) (graph_num_nodes ? (ertl_if_graph def)).
     644
     645definition move_first_cost_label_up_internal ≝
     646  λdef.
     647  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label def in
     648  match cost_label with
     649  [ None ⇒ def
     650  | Some cost_label ⇒ generate (ertl_st_cost cost_label (ertl_if_entry def)) def
     651  ].
     652
     653definition move_first_cost_label_up ≝
     654  λA: Type[0].
     655  λid_def: A × ?.
     656  let 〈id, def〉 ≝ id_def in
     657  let def' ≝
     658    match def with
     659    [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal int_fun)
     660    | External ext ⇒ def
     661    ]
     662  in
     663    〈id, def'〉.
     664
     665definition translate ≝
     666  λp.
     667  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
     668  let f ≝ λfunct. move_first_cost_label_up ? (translate_funct funct) in
     669  let vars ≝ map ? ? f (rtl_pr_functs p) in
     670    mk_ertl_program (rtl_pr_vars p) vars (rtl_pr_main p).
     671
     672let translate p =
     673  (* We simplify tail calls as regular calls for now. *)
     674  let p = RTLtailcall.simplify p in
     675  (* The tranformation on each RTL function: create an ERTL function and move
     676     its first cost label at the very beginning. *)
     677  let f funct = move_first_cost_label_up (translate_funct funct) in
     678  { ERTL.vars   = p.RTL.vars ;
     679    ERTL.functs = List.map f p.RTL.functs ;
     680    ERTL.main   = p.RTL.main }
    577681
    578682definition save_return_internal ≝
Note: See TracChangeset for help on using the changeset viewer.