Changeset 1643 for src/RTLabs/RTLabsToRTL_paolo.ma
- Timestamp:
- Jan 13, 2012, 12:23:30 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabsToRTL_paolo.ma
r1640 r1643 816 816 axiom fake_label: label. 817 817 818 definition stmt_not_ return≝ λstmt.match stmt with818 definition stmt_not_final ≝ λstmt.match stmt with 819 819 [ St_return ⇒ False 820 | St_tailcall_id _ _ ⇒ False 821 | St_tailcall_ptr _ _ ⇒ False 820 822 | _ ⇒ True ]. 821 823 … … 824 826 tailcall_* instructions. *) 825 827 definition translate_inst : ∀globals.?→?→?→ 826 Prod (bind_list register unit (rtl_instruction globals))label ≝828 (bind_list register unit (rtl_instruction globals)) × label ≝ 827 829 λglobals: list ident. 828 830 λlenv: local_env. 829 831 λstmt. 830 λstmt_prf : stmt_not_ returnstmt.832 λstmt_prf : stmt_not_final stmt. 831 833 match stmt return λx.stmt = x → 832 834 (bind_list register unit (rtl_instruction globals)) × label with … … 873 875 extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ]) 874 876 ]) [ ], lbl'〉 875 | St_tailcall_id f args ⇒ λ_.876 〈[extension rtl_params globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))], fake_label〉877 | St_tailcall_ptr f args ⇒ λ_.878 let 〈f1, f2〉 ≝ find_and_addr f lenv ? in879 〈bcons … (extension rtl_params globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) [ ], fake_label〉880 877 | St_cond r lbl_true lbl_false ⇒ λ_. 881 878 〈translate_cond globals (find_local_env r lenv) lbl_true, lbl_false〉 882 879 | St_jumptable r l ⇒ λ_.? (* assert false: not implemented yet *) 883 | St_return⇒ λeq_stmt.⊥880 | _ ⇒ λeq_stmt.⊥ 884 881 ] (refl …). 885 [1 1: cases not_implemented (* jtable case *)886 |1 2: >eq_stmt in stmt_prf; normalize //882 [12: cases not_implemented (* jtable case *) 883 |10,11,13: >eq_stmt in stmt_prf; normalize // 887 884 |*: cases daemon 888 885 (* TODO: proofs regarding lengths of lists, examine! *) … … 895 892 match stmt return λx.stmt = x → rtl_internal_function globals with 896 893 [ St_return ⇒ λ_.add_graph rtl_params globals lbl (RETURN …) def 894 | St_tailcall_id f args ⇒ λ_. 895 add_graph rtl_params globals lbl 896 (extension_fin rtl_params globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) def 897 | St_tailcall_ptr f args ⇒ λ_. 898 let 〈f1, f2〉 ≝ find_and_addr f lenv ? in 899 add_graph rtl_params globals lbl 900 (extension_fin rtl_params globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) def 897 901 | _ ⇒ λstmt_eq. 898 902 let 〈translation, lbl'〉 ≝ translate_inst globals lenv stmt ? in 899 903 rtl_adds_graph globals translation lbl lbl' def 900 904 ] (refl …). 901 >stmt_eq normalize % qed. 905 [10: cases daemon (* length of address lookup *) 906 |*: >stmt_eq normalize %] qed. 902 907 903 908
Note: See TracChangeset
for help on using the changeset viewer.