Changeset 1281 for src/RTLabs/RTLAbstoRTL.ma
 Timestamp:
 Sep 28, 2011, 11:08:37 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1280 r1281 6 6 include "joint/TranslateUtils.ma". 7 7 8 (*9 8 let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝ 10 9 match n with 11 [ O ⇒ [ ] 12  S n' ⇒ register_fresh runiverse :: (register_freshes runiverse n') 13 ]. 14 *) 10 [ O ⇒ 〈[],runiverse〉 11  S n' ⇒ 12 let 〈r,runiverse〉 ≝ fresh … runiverse in 13 let 〈res,runiverse〉 ≝ register_freshes runiverse n' in 14 〈r::res,runiverse〉 ]. 15 15 16 16 definition choose_rest ≝ … … 87 87 λr: register.λbvt. lookup … (word_of_identifier … r) bvt []. 88 88 89 (*90 89 definition initialize_local_env_internal ≝ 91 λruniverse. 92 λlenv. 90 λlenv_runiverse. 93 91 λr_sig. 92 let 〈lenv,runiverse〉 ≝ lenv_runiverse in 94 93 let 〈r, sig〉 ≝ r_sig in 95 94 let size ≝ size_of_sig_type sig in 96 let rs≝ register_freshes runiverse size in97 add_local_env r rs lenv.95 let 〈rs,runiverse〉 ≝ register_freshes runiverse size in 96 〈add_local_env r rs lenv,runiverse〉. 98 97 99 98 definition initialize_local_env ≝ … … 107 106 ] 108 107 in 109 foldl ? ? (initialize_local_env_internal runiverse) (Stub …) registers. 110 *) 108 foldl ? ? initialize_local_env_internal 〈Stub …,runiverse〉 registers. 111 109 112 110 definition map_list_local_env_internal ≝ … … 219 217 ] start_lbl dest_lbl def. 220 218 219 (* 221 220 definition translate_cast_signed ≝ 222 221 λglobals. … … 1007 1006 ] 1008 1007 qed. 1008 *) 1009 1009 1010 1010 definition translate_stmt ≝ 1011 λlenv. 1011 λglobals. 1012 λlenv: local_env. 1012 1013 λlbl: label. 1013 1014 λstmt. 1014 λdef: rtl_internal_function.1015 λdef: joint_internal_function … (rtl_params globals). 1015 1016 match stmt with 1016 [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def 1017 [ St_skip lbl' ⇒ add_graph … lbl (joint_st_goto … lbl') def 1018  _ ⇒ ? ]. 1019 (* 1017 1020  St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def 1018 1021  St_const destr cst lbl' ⇒ … … 1054 1057 *: cases daemon (* TODO: proofs regarding lengths of lists, examine! *) 1055 1058 ] 1059 *) cases daemon 1056 1060 qed. 1057 1061 … … 1061 1065 skip instructions at these nodes. *) 1062 1066 definition translate_internal ≝ 1063 λ def.1067 λglobals,def. 1064 1068 let runiverse ≝ f_reggen def in 1065 let lenv≝ initialize_local_env runiverse1069 let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse 1066 1070 (f_params def @ f_locals def) (f_result def) in 1067 1071 let params ≝ map_list_local_env lenv (map ? ? \fst (f_params def)) in … … 1083 1087 let entry' ≝ f_entry def in 1084 1088 let exit' ≝ f_exit def in 1085 let graph' ≝ add ? ? (empty_map ? ?) entry' (rtl_st_skipentry') in1086 let graph' ≝ add ? ? graph' exit' (rtl_st_skipexit') in1089 let graph' ≝ add … (empty_map ? ?) entry' (joint_st_goto … entry') in 1090 let graph' ≝ add … graph' exit' (joint_st_goto … exit') in 1087 1091 let res ≝ 1088 mk_rtl_internal_function luniverse' runiverse' result' params' 1089 locals' stack_size' graph' ? ? in 1090 foldi ? ? ? (translate_stmt lenv) (f_graph def) res. 1091 [1: % 1092 [1: @entry' 1093 2: normalize nodelta; 1094 @graph_add_lookup 1095 @graph_add 1096 ] 1097 2: % 1098 [1: @exit' 1099 2: normalize nodelta; 1100 @graph_add 1101 ] 1102 ] 1092 mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params' 1093 locals' stack_size' graph' ? ? in 1094 foldi … (translate_stmt … lenv) (f_graph def) res. 1095 [ % [@entry'  @graph_add_lookup @graph_add] 1096  % [@exit'  @graph_add]] 1103 1097 qed. 1104 1098 … … 1106 1100 because of CompCert heritage *) 1107 1101 definition rtlabs_to_rtl : RTLabs_program → rtl_program ≝ 1108 λp. transform_program … p (transf_fundef … translate_internal).1102 λp. transform_program ??? p (transf_fundef … (translate_internal (prog_var_names …))).
Note: See TracChangeset
for help on using the changeset viewer.