Changeset 1643 for src/RTLabs/RTLabsToRTL_paolo.ma

Timestamp:

Jan 13, 2012, 12:23:30 PM (8 years ago)

Author:

tranquil

Message:

• some changes in everything
• separated extensions in sequential and final, to accomodate tailcalls
• finished RTL's semantics

File:

• src/RTLabs/RTLabsToRTL_paolo.ma (modified) (4 diffs)

src/RTLabs/RTLabsToRTL_paolo.ma

@@ -816 +816 @@
 axiom fake_label: label.
 
-definition stmt_not_return ≝ λstmt.match stmt with
+definition stmt_not_final ≝ λstmt.match stmt with
   [ St_return ⇒ False
+  | St_tailcall_id _ _ ⇒ False
+  | St_tailcall_ptr _ _ ⇒ False
   | _ ⇒ True ].
 
@@ -824 +826 @@
         tailcall_* instructions. *)
 definition translate_inst : ∀globals.?→?→?→
-  Prod (bind_list register unit (rtl_instruction globals)) label ≝
+  (bind_list register unit (rtl_instruction globals)) × label ≝
   λglobals: list ident.
   λlenv: local_env.
   λstmt.
-  λstmt_prf : stmt_not_return stmt.
+  λstmt_prf : stmt_not_final stmt.
   match stmt return λx.stmt = x →
     (bind_list register unit (rtl_instruction globals)) × label with
@@ -873 +875 @@
         extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])
       ]) [ ], lbl'〉
-  | St_tailcall_id f args ⇒ λ_.
-    〈[extension rtl_params globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))], fake_label〉
-  | St_tailcall_ptr f args ⇒ λ_.
-    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
-    〈bcons … (extension rtl_params globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) [ ], fake_label〉
   | St_cond r lbl_true lbl_false ⇒ λ_.
     〈translate_cond globals (find_local_env r lenv) lbl_true, lbl_false〉
   | St_jumptable r l ⇒  λ_.? (* assert false: not implemented yet *)
-  | St_return ⇒ λeq_stmt.⊥
+  | _ ⇒ λeq_stmt.⊥
   ] (refl …).
-  [11: cases not_implemented (* jtable case *)
-  |12: >eq_stmt in stmt_prf; normalize //
+  [12: cases not_implemented (* jtable case *)
+  |10,11,13: >eq_stmt in stmt_prf; normalize //
   |*: cases daemon
   (* TODO: proofs regarding lengths of lists, examine! *)
@@ -895 +892 @@
   match stmt return λx.stmt = x → rtl_internal_function globals with
   [ St_return ⇒ λ_.add_graph rtl_params globals lbl (RETURN …) def
+  | St_tailcall_id f args ⇒ λ_.
+    add_graph rtl_params globals lbl
+      (extension_fin rtl_params globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) def
+  | St_tailcall_ptr f args ⇒ λ_.
+    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
+    add_graph rtl_params globals lbl
+      (extension_fin rtl_params globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) def
   | _ ⇒ λstmt_eq.
     let 〈translation, lbl'〉 ≝ translate_inst globals lenv stmt ? in
     rtl_adds_graph globals translation lbl lbl' def
   ] (refl …).
->stmt_eq normalize % qed.
+[10: cases daemon (* length of address lookup *)
+|*: >stmt_eq normalize %] qed.