Changeset 1262 for src/RTL/RTLtoERTL.ma

Timestamp:

Sep 23, 2011, 4:40:54 PM (9 years ago)

Author:

sacerdot

Message:

RTLtoERTL ported to the joint syntax for ERTL. Now it is time to port RTL
to the joint syntax too.

File:

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

src/RTL/RTLtoERTL.ma

@@ -369 +369 @@
     ) start_lbl dest_lbl def.
 
-definition translate_stmt ≝
+axiom translate_stmt :
+ ∀globals: list ident. label → rtl_statement → ertl_internal_function globals → ertl_internal_function globals.
+(*
+ ≝
   λglobals.
   λlbl.
@@ -408 +411 @@
   ].
   cases not_implemented
-qed.    
+qed.*)  
 
 (* hack with empty graphs used here *)
 definition translate_funct_internal ≝
-  λdef.
+  λglobals,def.
   let nb_params ≝ |rtl_if_params def| in
   let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in
@@ -418 +421 @@
   let entry' ≝ rtl_if_entry def in
   let exit' ≝ rtl_if_exit def in
-  let graph' ≝ add ? ? (empty_map ? ?) entry' (ertl_st_skip entry') in
-  let graph' ≝ add ? ? graph' exit' (ertl_st_skip exit') in
+  let graph' ≝ add ? ? (empty_map ? ?) entry' (joint_st_goto … entry') in
+  let graph' ≝ add ? ? graph' exit' (joint_st_goto … exit') in
   let def' ≝
-    mk_ertl_internal_function
-      (rtl_if_luniverse def) (rtl_if_runiverse def)
-      nb_params new_locals ((rtl_if_stacksize def) + added_stacksize)
+    mk_joint_internal_function globals (ertl_params globals)
+      (rtl_if_luniverse def) (rtl_if_runiverse … def) it
+      nb_params new_locals ((rtl_if_stacksize … def) + added_stacksize)
       graph' ? ? in
-  let def' ≝ foldi ? ? ? translate_stmt (rtl_if_graph def) def' in
-  let def' ≝ add_pro_and_epilogue (rtl_if_params def) (rtl_if_result def) def' in
+  let def' ≝ foldi ? ? ? (translate_stmt globals) (rtl_if_graph def) def' in
+  let def' ≝ add_pro_and_epilogue … (rtl_if_params def) (rtl_if_result def) def' in
     def'.
-  [1: %
-      [1: @entry'
-      |2: normalize nodelta
-          @graph_add_lookup
-          @graph_add
-      ]
-  |2: %
-      [1: @exit'
-      |2: normalize nodelta
-          @graph_add
-      ]
-  ]
-qed.
-    
-definition translate_funct ≝
-  λid_def: ident × ?.
-  let 〈id, def〉 ≝ id_def in
-  let def' ≝
-    match def with
-    [ Internal def ⇒ Internal ? (translate_funct_internal def)
-    | External def ⇒ External ? def
-    ] in
-  〈id, def'〉.
+whd in match ertl_params (* CSC: Matita's bug here; not enough/too much reduction
+                                 makes the next application fail. Why? *)    
+%
+ [ @entry' | @graph_add_lookup @graph_add
+ | @exit'  | @graph_add ]
+qed.
 
 definition generate ≝
+  λglobals.
   λstmt.
   λdef.
-  let 〈entry, nuniv〉 ≝ fresh_label def in
-  let graph ≝ add ? ? (ertl_if_graph def) entry stmt in
-    mk_ertl_internal_function
-      nuniv (ertl_if_runiverse def) (ertl_if_params def)
-      (ertl_if_locals def) (ertl_if_stacksize def) graph
-      ? ?.
-  [1: %
-    [1: @entry
-    |2: normalize nodelta;
-        @graph_add
-    ]
-  |2: generalize in match (ertl_if_exit def)
-      #HYP
-      cases HYP
-      #LBL #LBL_PRF
-      %
-      [1: @LBL
-      |2: normalize nodelta;
-          @graph_add_lookup
-          @LBL_PRF
-      ]
-  ]
-qed.
-    
-let rec find_and_remove_first_cost_label_internal
-  (def: ertl_internal_function) (lbl: label) (num_nodes: nat)
+  let 〈entry, nuniv〉 ≝ fresh_label … def in
+  let graph ≝ add ? ? (joint_if_code … def) entry stmt in
+    mk_joint_internal_function ? (ertl_params globals)
+      nuniv (joint_if_runiverse … def) it (joint_if_params … def)
+      (joint_if_locals … def) (joint_if_stacksize … def) graph
+      ? ?.      
+  [ % [ @entry | @graph_add ]
+  | cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF ]
+qed.
+
+let rec find_and_remove_first_cost_label_internal (globals: list ident)
+  (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat)
     on num_nodes ≝
   match num_nodes with
   [ O ⇒ 〈None ?, def〉
   | S num_nodes' ⇒
-    match lookup ? ? (ertl_if_graph def) lbl with
+    match lookup … (joint_if_code … def) lbl with
     [ None ⇒ 〈None ?, def〉
-    | Some stmt ⇒
+    | Some stmt ⇒ 
       match stmt with
-      [ ertl_st_cost cost_lbl next_lbl ⇒
-          〈Some ? cost_lbl, add_graph lbl (ertl_st_skip next_lbl) def〉
-      | ertl_st_cond _ _ _ ⇒ 〈None ?, def〉
-      | ertl_st_return ⇒ 〈None ?, def〉
-      | ertl_st_skip lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_comment _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_get_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_set_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_hdw_to_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_pop _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 
-      | ertl_st_push _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_addr _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_int _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_move _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_opaccs _ _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_op1 _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_op2 _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_clear_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_set_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_load _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_store _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_call_id _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_new_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_del_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_frame_size _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      ]
-    ]
-  ].
+      [ joint_st_sequential inst lbl ⇒
+         match inst with
+          [ joint_instr_cost_label cost_lbl ⇒
+             〈Some … cost_lbl, add_graph ertl_params_ globals lbl (joint_st_goto … lbl) def〉
+          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
+      | joint_st_return ⇒ 〈None …, def〉
+      | joint_st_goto lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
+      ]]].
     
 definition find_and_remove_first_cost_label ≝
-  λdef.  
-    find_and_remove_first_cost_label_internal def (ertl_if_entry def) (graph_num_nodes ? (ertl_if_graph def)).
+  λglobals,def.  
+    find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)).
 
 definition move_first_cost_label_up_internal ≝
-  λdef.
-  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label def in
+  λglobals,def.
+  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in
   match cost_label with
   [ None ⇒ def
-  | Some cost_label ⇒ generate (ertl_st_cost cost_label (ertl_if_entry def)) def
-  ].
-
+  | Some cost_label ⇒ generate … (joint_st_sequential ertl_params_ globals (joint_instr_cost_label … cost_label) (joint_if_entry … def)) def
+  ].
+
+definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
+
+(*
 definition move_first_cost_label_up ≝
+  λglobals.
   λA: Type[0].
   λid_def: A × ?.
@@ -536 +493 @@
   let def' ≝
     match def with
-    [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal int_fun)
-    | External ext ⇒ def
+    [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal … (translate_funct_internal globals int_fun))
+    | External ext ⇒ External … ext
     ]
   in
@@ -545 +502 @@
   λp.
   let p ≝ tailcall_simplify p in (* tailcall simplification here *)
-  let f ≝ λfunct. move_first_cost_label_up ? (translate_funct funct) in
+  let f ≝ λfunct. move_first_cost_label_up ? funct in
   let vars ≝ map ? ? f (rtl_pr_functs p) in
     mk_ertl_program (rtl_pr_vars p) vars (rtl_pr_main p).
+*)
+
+definition translate : rtl_program → ertl_program ≝
+ λp.
+  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
+    transform_program ??? p (transf_fundef ?? translate_funct).