Changeset 1250 for src/RTL/RTLtoERTL.ma
 Timestamp:
 Sep 22, 2011, 12:02:35 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1245 r1250 3 3 include "common/Identifiers.ma". 4 4 include "ERTL/ERTL.ma". 5 include "utilities/extralib.ma". (* CSC: Only for Sigma type projections *) 5 6 6 7 definition add_graph ≝ 7 λl: label. 8 λstmt. 9 λp. 10 let ertl_if_luniverse' ≝ ertl_if_luniverse p in 11 let ertl_if_runiverse' ≝ ertl_if_runiverse p in 12 let ertl_if_params' ≝ ertl_if_params p in 13 let ertl_if_locals' ≝ ertl_if_locals p in 14 let ertl_if_stacksize' ≝ ertl_if_stacksize p in 15 let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in 16 let ertl_if_entry' ≝ ertl_if_entry p in 17 let ertl_if_exit' ≝ ertl_if_exit p in 18 mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse' 19 ertl_if_params' ertl_if_locals' ertl_if_stacksize' 20 ertl_if_graph' ? ?. 8 λglobals.λl: label.λstmt.λp: joint_internal_function … (ertl_params globals). 9 let code ≝ add … (joint_if_code … p) l stmt in 10 mk_joint_internal_function … (ertl_params globals) 11 (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) 12 (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) 13 code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)). 21 14 normalize nodelta; 22 [1: generalize in match ertl_if_entry'; 23 #HYP 24 cases HYP 25 #LBL #LBL_PRF 26 % 27 [1: @LBL 28 2: @graph_add_lookup 29 @LBL_PRF 30 ] 31 2: generalize in match ertl_if_exit'; 32 #HYP 33 cases HYP 34 #LBL #LBL_PRF 35 % 36 [1: @LBL 37 2: @graph_add_lookup 38 @LBL_PRF 39 ] 40 ] 15 [ cases (joint_if_entry … p)  cases (joint_if_exit … p)] 16 #LBL #LBL_PRF @graph_add_lookup @LBL_PRF 41 17 qed. 42 18 43 19 definition fresh_label ≝ 44 λ def.45 fresh LabelTag ( ertl_if_luniversedef).20 λglobals.λdef: joint_internal_function … (ertl_params globals). 21 fresh LabelTag (joint_if_luniverse … def). 46 22 47 23 definition change_label ≝ 48 λl. 49 λe: ertl_statement. 24 λglobals.λe: joint_statement ertl_params_ globals.λl. 50 25 match e with 51 [ ertl_st_skip _ ⇒ ertl_st_skip l 26 [ joint_st_goto _ ⇒ joint_st_goto … l 27  joint_st_return ⇒ joint_st_return … 28  joint_st_sequential instr _ ⇒ joint_st_sequential … instr l 29  joint_st_extension ]. 52 30  ertl_st_comment s _ ⇒ ertl_st_comment s l 53 31  ertl_st_cost c _ ⇒ ertl_st_cost c l
Note: See TracChangeset
for help on using the changeset viewer.