Changeset 2490 for src/RTL/RTLTailcall.ma

Timestamp:

Nov 25, 2012, 1:33:09 PM (7 years ago)

Author:

tranquil

Message:

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

File:

• src/RTL/RTLTailcall.ma (modified) (3 diffs)

src/RTL/RTLTailcall.ma

@@ -4 +4 @@
   λglobals.
   λexit: label.
-  λlbl: label.
   λstmt: joint_statement RTL globals.
-  λgraph: codeT RTL_ntc globals.
   match stmt with
   [ final fin ⇒
      match fin with
-      [ tailcall ext ⇒
-         match ext with
-          [ rtl_tailcall_id f args ⇒
-              add … graph lbl (sequential … (CALL_ID RTL_ntc ? f args [ ]) exit)
-          | rtl_tailcall_ptr f1 f2 args ⇒
-              add … graph lbl (sequential RTL_ntc ? (rtl_call_ptr f1 f2 args [ ] : ext_call RTL_ntc) exit)
-          ]
-      | _ ⇒ graph ]
-  | _ ⇒ graph ].
+      [ TAILCALL _ f args ⇒ sequential … (CALL RTL_ntc ? f args [ ]) exit
+      | RETURN ⇒ RETURN RTL_ntc
+      | GOTO l ⇒ GOTO RTL_ntc l
+      ]
+  | sequential s next ⇒
+    sequential RTL_ntc ?
+    (match s return λ_.joint_step RTL_ntc globals with
+    [ step_seq s ⇒
+      match s return λ_.joint_seq RTL_ntc globals with
+      [ COMMENT s ⇒ COMMENT … s
+      | COST_LABEL l ⇒ COST_LABEL … l
+      | MOVE m ⇒ MOVE … m
+      | POP a ⇒ POP … a
+      | PUSH a ⇒ PUSH … a
+      | ADDRESS i prf dpl dph ⇒ ADDRESS … i prf dpl dph
+      | OPACCS op a b arg1 arg2 ⇒ OPACCS … op a b arg1 arg2
+      | OP1 op a arg ⇒ OP1 … op a arg
+      | OP2 op a arg1 arg2 ⇒ OP2 … op a arg1 arg2
+      | CLEAR_CARRY ⇒ CLEAR_CARRY ??
+      | SET_CARRY ⇒ SET_CARRY ??
+      | LOAD a dpl dph ⇒ LOAD … a dpl dph
+      | STORE dpl dph a ⇒ STORE … dpl dph a
+      | CALL f args dest ⇒ CALL … f args dest
+      | extension_seq s ⇒ extension_seq … s
+      ]
+    | COND a ltrue ⇒ COND … a ltrue
+    ]) next
+  ].
+
+definition id_map_map : ∀tag,A,B.(A → B) → identifier_map tag A → identifier_map tag B ≝
+λtag,A,B,f,m.
+match m with
+[ an_id_map m ⇒ an_id_map … (map … f m)
+].
 
 definition simplify_graph ≝
@@ -24 +47 @@
   λexit: label.
   λgraph: codeT RTL globals.
-    foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
+  id_map_map … (simplify_stmt globals exit) graph.
 
 axiom simplify_graph_preserves_labels:
@@ -34 +57 @@
 definition simplify_internal :
  ∀globals.
-  joint_internal_function RTL globals →
-   joint_internal_function RTL_ntc globals
+  joint_closed_internal_function RTL globals →
+   joint_closed_internal_function RTL_ntc globals
 ≝
   λglobals,def.
     let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in
-      mk_joint_internal_function …
+    «mk_joint_internal_function …
        (joint_if_luniverse … def) (joint_if_runiverse … def)
        (joint_if_result … def) (joint_if_params … def) (joint_if_locals … def)
        (joint_if_stacksize … def) graph
-       (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)).
- [ cases (joint_if_entry … def) | cases (joint_if_exit … def) ]
+       (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)), ?».
+ [3: cases daemon (* TODO *)
+ | cases (joint_if_exit … def) | cases (joint_if_entry … def) ]
  #l #IH @simplify_graph_preserves_labels @IH
 qed.