Changeset 1292 for src/RTLabs

Timestamp:

Oct 5, 2011, 11:15:00 AM (9 years ago)

Author:

mulligan

Message:

more added to rtlabs translation

File:

• src/RTLabs/RTLAbstoRTL.ma (modified) (7 diffs)

src/RTLabs/RTLAbstoRTL.ma

@@ -945 +945 @@
 
 definition translate_load ≝
+  λglobals: list ident.
   λaddr.
   λaddr_prf: 2 ≤ |addr|.
@@ -950 +951 @@
   λstart_lbl: label.
   λdest_lbl: label.
-  λdef: rtl_internal_function.
-  match fresh_regs_strong def (|addr|) with
+  λdef: rtl_internal_function globals.
+  match fresh_regs_strong rtl_params0 globals def (|addr|) with
   [ dp def_save_addr save_addr_prf ⇒
     let def ≝ \fst def_save_addr in
     let save_addr ≝ \snd def_save_addr in
-    match fresh_regs_strong def (|addr|) with
+    match fresh_regs_strong rtl_params0 globals def (|addr|) with
     [ dp def_tmp_addr tmp_addr_prf ⇒
       let def ≝ \fst def_tmp_addr in
       let tmp_addr ≝ \snd def_tmp_addr in
-      let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in
-      let 〈def, tmpr〉 ≝ fresh_reg def in
-      let insts_save_addr ≝ translate_move save_addr addr in
+      let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in
+      let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
+      let insts_save_addr ≝ translate_move globals save_addr addr in
       let f ≝ λtranslates_off. λr.
         let 〈translates, off〉 ≝ translates_off in
         let translates ≝ translates @ [
-          adds_graph [
-            INT tmpr off start_lbl
+          adds_graph rtl_params1 globals [
+            sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
           ];
-          translate_op2 Oaddp tmp_addr ? save_addr [tmpr] ? ?;
-          adds_graph [
-            LOAD r tmp_addr1 tmp_addr2 dest_lbl
+          translate_op2 globals Oaddp tmp_addr ? save_addr [tmpr] ? ?;
+          adds_graph rtl_params1 globals [
+            sequential rtl_params_ globals (LOAD rtl_params_ globals r tmp_addr1 tmp_addr2)
           ]
         ]
         in
-        let 〈carry, result〉 ≝ half_add ? off int_size in
+        let 〈carry, result〉 ≝ half_add … off int_size in
           〈translates, result〉
       in
-      let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], (zero ?)〉 destrs in
-        add_translates (insts_save_addr :: translates) start_lbl dest_lbl def
+      let 〈translates, ignore〉 ≝ foldl … f 〈[ ], (zero ?)〉 destrs in
+        add_translates rtl_params1 globals (insts_save_addr :: translates) start_lbl dest_lbl def
     ]
   ].
@@ -991 +992 @@
 
 definition translate_store ≝
+  λglobals: list ident.
   λaddr.
   λaddr_prf: 2 ≤ |addr|.
@@ -996 +998 @@
   λstart_lbl: label.
   λdest_lbl: label.
-  λdef: rtl_internal_function.
-  match fresh_regs_strong def (|addr|) with
+  λdef: rtl_internal_function globals.
+  match fresh_regs_strong rtl_params0 globals def (|addr|) with
   [ dp def_tmp_addr tmp_addr_prf ⇒
     let def ≝ \fst def_tmp_addr in
     let tmp_addr ≝ \snd def_tmp_addr in
-    let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in
-    let 〈def, tmpr〉 ≝ fresh_reg def in
+    let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in
+    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     let f ≝ λtranslate_off. λsrcr.
       let 〈translates, off〉 ≝ translate_off in
       let translates ≝ translates @ [
-        adds_graph [
-          rtl_st_int tmpr off start_lbl
+        adds_graph rtl_params1 globals [
+          sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
         ];
-        translate_op2 Oaddp tmp_addr ? addr [tmpr] ? ?;
-        adds_graph [
-          rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl
+        translate_op2 globals Oaddp tmp_addr ? addr [tmpr] ? ?;
+        adds_graph rtl_params1 globals [
+          sequential rtl_params_ globals (STORE rtl_params_ globals tmp_addr1 tmp_addr2 srcr)
         ]
       ]
       in
-        let 〈carry, result〉 ≝ half_add ? off int_size in
+        let 〈carry, result〉 ≝ half_add … off int_size in
           〈translates, result〉
     in
-    let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], zero ?〉 srcrs in
-      add_translates translates start_lbl dest_lbl def
+    let 〈translates, ignore〉 ≝ foldl … f 〈[ ], zero ?〉 srcrs in
+      add_translates rtl_params1 globals translates start_lbl dest_lbl def
   ].
   [1: normalize //
@@ -1029 +1031 @@
   ]
 qed.
-*)
 
 definition translate_stmt ≝
-  λglobals.
+  λglobals: list ident.
   λlenv: local_env.
   λlbl: label.
   λstmt.
-  λdef: joint_internal_function … (rtl_params globals).
+  λdef: rtl_internal_function globals.
   match stmt with
   [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def
-  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
+  | St_cost cost_lbl lbl' ⇒ add_graph lbl (sequential rtl_params_ globals (COST_LABEL … cost_lbl lbl')) def
   | St_const destr cst lbl' ⇒
     translate_cst cst (find_local_env destr lenv) lbl lbl' def
   | St_op1 op1 destr srcr lbl' ⇒
-    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) ? lbl lbl' def
+    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
   | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
-    translate_op2 op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
+    translate_op2 op2 (find_local_env destr lenv) … (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
   | St_load ignore addr destr lbl' ⇒
-    translate_load (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
+    translate_load (find_local_env addr lenv) … (find_local_env destr lenv) lbl lbl' def
   | St_store ignore addr srcr lbl' ⇒
-    translate_store (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
+    translate_store (find_local_env addr lenv) … (find_local_env srcr lenv) lbl lbl' def
   | St_call_id f args retr lbl' ⇒
     match retr with
     [ Some retr ⇒
-      add_graph lbl (rtl_st_call_id f (rtl_args args lenv) (find_local_env retr lenv) lbl') def
-    | None ⇒ add_graph lbl (rtl_st_call_id f (rtl_args args lenv) [ ] lbl') def
+      add_graph rtl_params1 globals lbl (sequential … (CALL_ID … f (rtl_args args lenv) (find_local_env retr lenv) lbl')) def
+    | None ⇒ add_graph rtl_params1 globals lbl (sequential … (CALL_ID … f (rtl_args args lenv) [ ] lbl')) def
     ]
   | St_call_ptr f args retr lbl' ⇒
@@ -1060 +1061 @@
     [ None ⇒
       let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
-        add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) [ ] lbl') def
+        add_graph lbl rtl_params1 globals (sequential … (extension … (rtl_st_ext_call_ptr … f1 f2 (rtl_args args lenv) [ ] lbl'))) def
     | Some retr ⇒
       let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
-        add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv) lbl') def
+        add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv) lbl'))) def
     ]
   | St_tailcall_id f args ⇒
-    add_graph lbl (rtl_st_tailcall_id f (rtl_args args lenv)) def
+    add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params_ globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) lbl) def
   | St_tailcall_ptr f args ⇒
     let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
-      add_graph lbl (rtl_st_tailcall_ptr f1 f2 (rtl_args args lenv)) def
+      add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params1 globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) lbl) def
   | St_cond r lbl_true lbl_false ⇒
-    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
+    translate_cond globals (find_local_env r lenv) lbl lbl_true lbl_false def
   | St_jumptable r l ⇒ ? (* assert false: not implemented yet *)
-  | St_return ⇒ add_graph lbl rtl_st_return def
+  | St_return ⇒ add_graph rtl_params1 globals lbl (RETURN …) def
   ].
   [10: cases not_implemented (* jtable case *)
@@ -1089 +1090 @@
   let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
     (f_params def @ f_locals def) (f_result def) in
-  let params ≝ map_list_local_env lenv (map ? ? \fst (f_params def)) in
-  let locals ≝ map_list_local_env lenv (map ? ? \fst (f_locals def)) in
+  let params ≝ map_list_local_env lenv (map … \fst (f_params def)) in
+  let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in
   let result ≝
     match (f_result def) with