Changeset 1258 for src/RTL

Timestamp:

Sep 23, 2011, 1:47:27 AM (9 years ago)

Author:

sacerdot

Message:

More progress towards porting to joint syntax.

File:

• src/RTL/RTLtoERTL.ma (modified) (5 diffs)

src/RTL/RTLtoERTL.ma

@@ -158 +158 @@
   λsregs.
   λdef.
-  let start_lbl ≝ joint_if_entry globals (ertl_params globals) def in
-  let 〈tmp_lbl, nuniv〉 ≝ fresh_label ? def in
-  match lookup ? ? (joint_if_code ? (ertl_params globals) def) start_lbl
+  let start_lbl ≝ joint_if_entry … (ertl_params globals) def in
+  let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
+  match lookup … (joint_if_code … (ertl_params globals) def) start_lbl
     return λx. x ≠ None ? → ertl_internal_function globals with
   [ None ⇒ λnone_absrd. ⊥
@@ -184 +184 @@
 
 definition save_return ≝
+  λglobals.
   λret_regs.
   λstart_lbl: label.
   λdest_lbl: label.
-  λdef: ertl_internal_function.
-  let 〈def, tmpr〉 ≝ fresh_reg def in
+  λdef: ertl_internal_function globals.
+  let 〈def, tmpr〉 ≝ fresh_reg … def in
   match reduce_strong ? ? RegisterSTS ret_regs with
   [ dp crl crl_proof ⇒
@@ -195 +196 @@
     let restl ≝ \snd (\fst crl) in
     let restr ≝ \snd (\snd crl) in
-    let init_tmpr ≝ ertl_st_int tmpr (zero ?) start_lbl in
-    let f_save ≝ λst. λr. ertl_st_set_hdw st r start_lbl in
+    let init_tmpr ≝ joint_st_sequential ertl_params_ … (joint_instr_int … tmpr (zero ?)) start_lbl in
+    let f_save ≝ λst. λr. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo r〉) start_lbl in
     let saves ≝ map2 ? ? ? f_save commonl commonr crl_proof in
-    let f_default ≝ λst. ertl_st_set_hdw st tmpr start_lbl in
+    let f_default ≝ λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo tmpr〉) start_lbl in
     let defaults ≝ map ? ? f_default restl in
-      adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
+      adds_graph … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
   ].
 
 definition assign_result ≝
-  λstart_lbl: label.
+  λglobals.λstart_lbl: label.
   match reduce_strong ? ? RegisterRets RegisterSTS with
   [ dp crl crl_proof ⇒
     let commonl ≝ \fst (\fst crl) in
     let commonr ≝ \fst (\snd crl) in
-    let f ≝ λret. λst. ertl_st_hdw_to_hdw ret st start_lbl in
+    let f ≝ λret. λst. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware ret, hardware st〉) start_lbl in
     let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
-      adds_graph insts start_lbl
+      adds_graph … insts start_lbl
   ].
 
 definition add_epilogue ≝
+  λglobals.
   λret_regs.
   λsral.
@@ -220 +222 @@
   λsregs.
   λdef.
-  let start_lbl ≝ ertl_if_exit def in
-  let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
-  match lookup ? ? (ertl_if_graph def) start_lbl
-    return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ? with
-  [ None ⇒ λnone_absd. ?
+  let start_lbl ≝ joint_if_exit … (ertl_params globals) def in
+  let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
+  match lookup … (joint_if_code … (ertl_params globals) def) start_lbl
+    return λx. x ≠ None ? → ertl_internal_function globals with
+  [ None ⇒ λnone_absrd. ⊥
   | Some last_stmt ⇒ λsome_prf.
     let def ≝
-      add_translates (
-        [save_return ret_regs] @
-        restore_hdws sregs @
-        [adds_graph [
-          ertl_st_push srah start_lbl;
-          ertl_st_push sral start_lbl
+      add_translates … (
+        [save_return globals ret_regs] @
+        restore_hdws … sregs @
+        [adds_graph … [
+          joint_st_sequential … (joint_instr_push … srah) start_lbl;
+          joint_st_sequential … (joint_instr_push … sral) start_lbl
         ]] @
-        [adds_graph [
-          ertl_st_del_frame start_lbl
+        [adds_graph … [
+          joint_st_sequential … (joint_instr_extension … ertl_st_ext_del_frame) start_lbl
         ]] @
-        [assign_result]
+        [assign_result globals]
       ) start_lbl tmp_lbl def
     in
-    let def ≝ add_graph tmp_lbl last_stmt def in
-      set_joint_if_exit … tmp_lbl def ?
+    let def' ≝ add_graph … tmp_lbl last_stmt def in
+      set_joint_if_exit … tmp_lbl def' ?
   ] ?.
-  cases not_implemented (* dep types here, bug in matita too! *)
+[ cases start_lbl #x #H @H
+| cases (none_absrd) /2/
+| cases daemon (* CSC: XXXXX *)
+]
 qed.
   
-definition allocate_regs_internal ≝
-  λr: Register.
-  λdef_sregs.
-  let 〈def, sregs〉 ≝ def_sregs in
-  let 〈def, r'〉 ≝ fresh_reg def in
-    〈def, 〈r', r〉 :: sregs〉.
-  
+
 definition allocate_regs ≝
+  λglobals.
   λrs.
   λsaved: rs_set rs.
   λdef.
+   let allocate_regs_internal ≝
+    λr: Register.
+    λdef_sregs.
+    let 〈def, sregs〉 ≝ def_sregs in
+    let 〈def, r'〉 ≝ fresh_reg globals def in
+      〈def, 〈r', r〉 :: sregs〉
+   in
     rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
    
 definition add_pro_and_epilogue ≝
+  λglobals.
   λparams.
   λret_regs.
   λdef.
-  match fresh_regs_strong def 2 with
+  match fresh_regs_strong globals def 2 with
   [ dp def_sra def_sra_proof ⇒
     let def ≝ \fst def_sra in
@@ -269 +277 @@
     let sral ≝ nth_safe ? 0 sra ? in
     let srah ≝ nth_safe ? 1 sra ? in
-    let 〈def, sregs〉 ≝ allocate_regs register_list_set RegisterCalleeSaved def in
-    let def ≝ add_prologue params sral srah sregs def in
-    let def ≝ add_epilogue ret_regs sral srah sregs def in
+    let 〈def, sregs〉 ≝ allocate_regs … register_list_set RegisterCalleeSaved def in
+    let def ≝ add_prologue … params sral srah sregs def in
+    let def ≝ add_epilogue … ret_regs sral srah sregs def in
       def
   ].
-  [1: >def_sra_proof //
-  |2: >def_sra_proof //
-  ]
+>def_sra_proof //
 qed.
 
 definition set_params_hdw ≝
-  λparams.
+  λglobals,params.
   match params with
-  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
+  [ nil ⇒ [ λstart_lbl. adds_graph … [joint_st_goto … start_lbl] start_lbl]
   | _ ⇒
     let l ≝ zip_pottier ? ? params RegisterParams in
-      restore_hdws l
+      restore_hdws globals l
   ].