Changeset 1258


Ignore:
Timestamp:
Sep 23, 2011, 1:47:27 AM (8 years ago)
Author:
sacerdot
Message:

More progress towards porting to joint syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r1257 r1258  
    158158  λsregs.
    159159  λdef.
    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
     160  let start_lbl ≝ joint_if_entry (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
    163163    return λx. x ≠ None ? → ertl_internal_function globals with
    164164  [ None ⇒ λnone_absrd. ⊥
     
    184184
    185185definition save_return ≝
     186  λglobals.
    186187  λret_regs.
    187188  λstart_lbl: label.
    188189  λdest_lbl: label.
    189   λdef: ertl_internal_function.
    190   let 〈def, tmpr〉 ≝ fresh_reg def in
     190  λdef: ertl_internal_function globals.
     191  let 〈def, tmpr〉 ≝ fresh_reg def in
    191192  match reduce_strong ? ? RegisterSTS ret_regs with
    192193  [ dp crl crl_proof ⇒
     
    195196    let restl ≝ \snd (\fst crl) in
    196197    let restr ≝ \snd (\snd crl) in
    197     let init_tmpr ≝ ertl_st_int tmpr (zero ?) start_lbl in
    198     let f_save ≝ λst. λr. ertl_st_set_hdw st r start_lbl in
     198    let init_tmpr ≝ joint_st_sequential ertl_params_ … (joint_instr_int … tmpr (zero ?)) start_lbl in
     199    let f_save ≝ λst. λr. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo r〉) start_lbl in
    199200    let saves ≝ map2 ? ? ? f_save commonl commonr crl_proof in
    200     let f_default ≝ λst. ertl_st_set_hdw st tmpr start_lbl in
     201    let f_default ≝ λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo tmpr〉) start_lbl in
    201202    let defaults ≝ map ? ? f_default restl in
    202       adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
     203      adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
    203204  ].
    204205
    205206definition assign_result ≝
    206   λstart_lbl: label.
     207  λglobals.λstart_lbl: label.
    207208  match reduce_strong ? ? RegisterRets RegisterSTS with
    208209  [ dp crl crl_proof ⇒
    209210    let commonl ≝ \fst (\fst crl) in
    210211    let commonr ≝ \fst (\snd crl) in
    211     let f ≝ λret. λst. ertl_st_hdw_to_hdw ret st start_lbl in
     212    let f ≝ λret. λst. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware ret, hardware st〉) start_lbl in
    212213    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
    213       adds_graph insts start_lbl
     214      adds_graph insts start_lbl
    214215  ].
    215216
    216217definition add_epilogue ≝
     218  λglobals.
    217219  λret_regs.
    218220  λsral.
     
    220222  λsregs.
    221223  λdef.
    222   let start_lbl ≝ ertl_if_exit def in
    223   let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
    224   match lookup ? ? (ertl_if_graph def) start_lbl
    225     return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ? with
    226   [ None ⇒ λnone_absd. ?
     224  let start_lbl ≝ joint_if_exit … (ertl_params globals) def in
     225  let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
     226  match lookup … (joint_if_code … (ertl_params globals) def) start_lbl
     227    return λx. x ≠ None ? → ertl_internal_function globals with
     228  [ None ⇒ λnone_absrd. ⊥
    227229  | Some last_stmt ⇒ λsome_prf.
    228230    let def ≝
    229       add_translates (
    230         [save_return ret_regs] @
    231         restore_hdws sregs @
    232         [adds_graph [
    233           ertl_st_push srah start_lbl;
    234           ertl_st_push sral start_lbl
     231      add_translates (
     232        [save_return globals ret_regs] @
     233        restore_hdws sregs @
     234        [adds_graph [
     235          joint_st_sequential … (joint_instr_push … srah) start_lbl;
     236          joint_st_sequential … (joint_instr_push … sral) start_lbl
    235237        ]] @
    236         [adds_graph [
    237           ertl_st_del_frame start_lbl
     238        [adds_graph [
     239          joint_st_sequential … (joint_instr_extension … ertl_st_ext_del_frame) start_lbl
    238240        ]] @
    239         [assign_result]
     241        [assign_result globals]
    240242      ) start_lbl tmp_lbl def
    241243    in
    242     let def ≝ add_graph tmp_lbl last_stmt def in
    243       set_joint_if_exit … tmp_lbl def ?
     244    let def' ≝ add_graph … tmp_lbl last_stmt def in
     245      set_joint_if_exit … tmp_lbl def' ?
    244246  ] ?.
    245   cases not_implemented (* dep types here, bug in matita too! *)
     247[ cases start_lbl #x #H @H
     248| cases (none_absrd) /2/
     249| cases daemon (* CSC: XXXXX *)
     250]
    246251qed.
    247252 
    248 definition allocate_regs_internal ≝
    249   λr: Register.
    250   λdef_sregs.
    251   let 〈def, sregs〉 ≝ def_sregs in
    252   let 〈def, r'〉 ≝ fresh_reg def in
    253     〈def, 〈r', r〉 :: sregs〉.
    254  
     253
    255254definition allocate_regs ≝
     255  λglobals.
    256256  λrs.
    257257  λsaved: rs_set rs.
    258258  λdef.
     259   let allocate_regs_internal ≝
     260    λr: Register.
     261    λdef_sregs.
     262    let 〈def, sregs〉 ≝ def_sregs in
     263    let 〈def, r'〉 ≝ fresh_reg globals def in
     264      〈def, 〈r', r〉 :: sregs〉
     265   in
    259266    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
    260267   
    261268definition add_pro_and_epilogue ≝
     269  λglobals.
    262270  λparams.
    263271  λret_regs.
    264272  λdef.
    265   match fresh_regs_strong def 2 with
     273  match fresh_regs_strong globals def 2 with
    266274  [ dp def_sra def_sra_proof ⇒
    267275    let def ≝ \fst def_sra in
     
    269277    let sral ≝ nth_safe ? 0 sra ? in
    270278    let srah ≝ nth_safe ? 1 sra ? in
    271     let 〈def, sregs〉 ≝ allocate_regs register_list_set RegisterCalleeSaved def in
    272     let def ≝ add_prologue params sral srah sregs def in
    273     let def ≝ add_epilogue ret_regs sral srah sregs def in
     279    let 〈def, sregs〉 ≝ allocate_regs register_list_set RegisterCalleeSaved def in
     280    let def ≝ add_prologue params sral srah sregs def in
     281    let def ≝ add_epilogue ret_regs sral srah sregs def in
    274282      def
    275283  ].
    276   [1: >def_sra_proof //
    277   |2: >def_sra_proof //
    278   ]
     284>def_sra_proof //
    279285qed.
    280286
    281287definition set_params_hdw ≝
    282   λparams.
     288  λglobals,params.
    283289  match params with
    284   [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
     290  [ nil ⇒ [ λstart_lbl. adds_graph … [joint_st_goto … start_lbl] start_lbl]
    285291  | _ ⇒
    286292    let l ≝ zip_pottier ? ? params RegisterParams in
    287       restore_hdws l
     293      restore_hdws globals l
    288294  ].
    289295
Note: See TracChangeset for help on using the changeset viewer.