Changeset 2286 for src/RTL/RTLTailcall.ma

Timestamp:

Aug 2, 2012, 3:18:11 PM (9 years ago)

Author:

tranquil

Message:

Big update!

• merge of all _paolo variants
• reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
• split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:

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

src/RTL/RTLTailcall.ma

@@ -5 +5 @@
   λexit: label.
   λlbl: label.
-  λstmt: rtl_statement globals.
-  λgraph: codeT … (rtlntc_params globals).
+  λstmt: joint_statement RTL globals.
+  λgraph: codeT RTL_ntc globals.
   match stmt with
-  [ sequential seq DUMMY ⇒
-     match seq with
-      [ extension ext ⇒
+  [ final fin ⇒
+     match fin with
+      [ tailcall ext ⇒
          match ext with
-          [ rtl_st_ext_tailcall_id f args ⇒
-              add ? ? graph lbl (sequential … (CALL_ID … f args [ ]) exit) 
-          | rtl_st_ext_tailcall_ptr f1 f2 args ⇒
-              add ? ? graph lbl (sequential … (extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit)
-          | _ ⇒ graph ]
+          [ 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 ].
@@ -23 +23 @@
   λglobals.
   λexit: label.
-  λgraph: codeT … (rtl_params globals).
+  λgraph: codeT RTL globals.
     foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
 
 axiom simplify_graph_preserves_labels:
   ∀globals.
-  ∀g: codeT … (rtl_params globals).
-  ∀l: label.
+  ∀g: codeT RTL globals.
   ∀exit: label.
-    lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph globals exit g) l ≠ None ?.
+  ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g.
     
 definition simplify_internal :
  ∀globals.
-  joint_internal_function … (rtl_params globals) →
-   joint_internal_function … (rtlntc_params globals)
+  joint_internal_function RTL globals →
+   joint_internal_function RTL_ntc globals
 ≝
   λglobals,def.
@@ -49 +48 @@
 qed.
 
-definition tailcall_simplify : rtl_program → rtlntc_program ≝
+definition tailcall_simplify : rtl_program → rtl_ntc_program ≝
  λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).