Changeset 1257


Ignore:
Timestamp:
Sep 22, 2011, 6:04:27 PM (8 years ago)
Author:
sacerdot
Message:

More progress in porting to joint datatype.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r1254 r1257  
    3636        adds_graph globals stmt_list tmp_lbl dest_lbl def]].
    3737
    38 (*
     38(*CSC: bad programming habit: the code below puts everywhere a fake
     39  label and then adds_graph fixes them *)
     40(*CSC: the code is artificially fixed to work on ertl_statements, but
     41  it works on every graph_params *)
    3942let rec add_translates
    40   (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
    41   (def: ertl_internal_function)
     43  (globals: list ident) (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
     44  (def: ertl_internal_function globals)
    4245    on translate_list ≝
    4346  match translate_list with
    44   [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def
     47  [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def
    4548  | cons trans translate_list ⇒
    4649    match translate_list with
    4750    [ nil ⇒ trans start_lbl dest_lbl def
    4851    | _ ⇒
    49       let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
     52      let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
    5053      let def ≝ trans start_lbl tmp_lbl def in
    51         add_translates translate_list tmp_lbl dest_lbl def
    52     ]
    53   ].
    54 *)
     54        add_translates globals translate_list tmp_lbl dest_lbl def]].
    5555
    5656definition fresh_reg:
     
    129129    joint_st_sequential … (joint_instr_extension … (ertl_st_ext_frame_size addr1)) start_lbl;
    130130    joint_st_sequential … (joint_instr_int … tmpr int_offset) start_lbl;
    131     joint_st_sequential … (joint_instr_op2 … Sub addr1 addr1 tmpr) start_lbl(*;
    132     joint_st_sequential … (joint_instr_get_hdw … tmpr RegisterSPL) start_lbl;
     131    joint_st_sequential … (joint_instr_op2 … Sub addr1 addr1 tmpr) start_lbl;
     132    joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;
    133133    joint_st_sequential … (joint_instr_op2 … Add addr1 addr1 tmpr) start_lbl;
    134134    joint_st_sequential … (joint_instr_int … addr2 (bitvector_of_nat 8 0)) start_lbl;
    135     joint_st_sequential … (joint_instr_get_hdw … tmpr RegisterSPH) start_lbl;
     135    joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl;
    136136    joint_st_sequential … (joint_instr_op2 … Addc addr2 addr2 tmpr) start_lbl;
    137     joint_st_sequential … (joint_instr_load … destr addr1 addr2) start_lbl*)
     137    joint_st_sequential … (joint_instr_load … destr addr1 addr2) start_lbl
    138138  ] start_lbl dest_lbl def.
    139139 
    140140definition get_params_stack ≝
    141   λparams.
     141  λglobals,params.
    142142  match params with
    143   [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl ]
    144   | _ ⇒
    145     let f ≝ λi. λr. get_param_stack i r in
    146       mapi ? ? f params
    147   ].
     143  [ nil ⇒ [ λstart_lbl. adds_graph … [joint_st_goto … start_lbl] start_lbl ]
     144  | _ ⇒ mapi ? ? (get_param_stack globals) params ].
    148145
    149146definition get_params ≝
    150   λparams.
    151   let n ≝ min (length ? params) (length ? RegisterParams) in
    152   let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
    153   let hdw_params ≝ get_params_hdw hdw_params in
    154     hdw_params @ (get_params_stack stack_params).
     147  λglobals,params.
     148  let n ≝ min (length … params) (length … RegisterParams) in
     149  let 〈hdw_params, stack_params〉 ≝ list_split n params in
     150  let hdw_params ≝ get_params_hdw globals hdw_params in
     151    hdw_params @ (get_params_stack stack_params).
    155152 
    156153definition add_prologue ≝
     154  λglobals.
    157155  λparams: list register.
    158156  λsral.
     
    160158  λsregs.
    161159  λdef.
    162   let start_lbl ≝ ertl_if_entry def in
    163   let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
    164   match lookup ? ? (ertl_if_graph def) start_lbl
    165     return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ertl_internal_function with
    166   [ None ⇒ λnone_absrd. ?
     160  let start_lbl ≝ joint_if_entry globals (ertl_params globals) def in
     161  let 〈tmp_lbl, nuniv〉 ≝ fresh_label ? def in
     162  match lookup ? ? (joint_if_code ? (ertl_params globals) def) start_lbl
     163    return λx. x ≠ None ? → ertl_internal_function globals with
     164  [ None ⇒ λnone_absrd.
    167165  | Some last_stmt ⇒ λsome_prf.
    168166    let def ≝
    169       add_translates
    170          ((adds_graph [
    171                      ertl_st_new_frame start_lbl
     167      add_translates …
     168         ((adds_graph [
     169                     joint_st_sequential … (joint_instr_extension ertl_params_ globals ertl_st_ext_new_frame) start_lbl
    172170                   ]) ::
    173          (adds_graph [
    174                       ertl_st_pop sral start_lbl;
    175                       ertl_st_pop srah start_lbl
     171         (adds_graph [
     172                      joint_st_sequential … (joint_instr_pop … sral) start_lbl;
     173                      joint_st_sequential … (joint_instr_pop … srah) start_lbl
    176174                   ]) ::
    177          (save_hdws sregs) @
    178          (get_params params))
     175         (save_hdws sregs) @
     176         (get_params params))
    179177        start_lbl tmp_lbl def
    180178    in
    181       add_graph tmp_lbl last_stmt def
     179      add_graph tmp_lbl last_stmt def
    182180  ] ?.
    183   cases not_implemented (* dep. types here *)
     181[ cases start_lbl #x #H @H
     182| cases (none_absrd) /2/ ]
    184183qed.
    185184
Note: See TracChangeset for help on using the changeset viewer.