 Timestamp:
 Oct 4, 2011, 2:00:54 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1288 r1290 942 942 let f ≝ λsrcr. sequential rtl_params_ globals (OP2 rtl_params_ globals Or tmpr tmpr srcr) in 943 943 let def ≝ adds_graph rtl_params1 globals (init :: (map ? ? f srcrs)) start_lbl tmp_lbl def in 944 add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true lbl_false)) def.944 add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true) lbl_false) def. 945 945 946 946 definition translate_load ≝ … … 966 966 let translates ≝ translates @ [ 967 967 adds_graph [ 968 rtl_st_inttmpr off start_lbl968 INT tmpr off start_lbl 969 969 ]; 970 970 translate_op2 Oaddp tmp_addr ? save_addr [tmpr] ? ?; 971 971 adds_graph [ 972 rtl_st_loadr tmp_addr1 tmp_addr2 dest_lbl972 LOAD r tmp_addr1 tmp_addr2 dest_lbl 973 973 ] 974 974 ] … … 1039 1039 match stmt with 1040 1040 [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def 1041  _ ⇒ ? ].1042 (*1043 1041  St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def 1044 1042  St_const destr cst lbl' ⇒ … … 1080 1078 *: cases daemon (* TODO: proofs regarding lengths of lists, examine! *) 1081 1079 ] 1082 *) cases daemon1083 1080 qed. 1084 1081
Note: See TracChangeset
for help on using the changeset viewer.