Changeset 1161 for src/ERTL/ERTLToLTL.ma
 Timestamp:
 Aug 31, 2011, 6:24:03 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1160 r1161 57 57 let off ≝ adjust_off int_fun off in 58 58 let luniv ≝ ertl_if_luniverse int_fun in 59 let 〈l, 〈graph, luniv〉〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in60 let 〈l, graph 〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_load globals) l) in61 let 〈l, graph 〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in62 let 〈l, graph 〉 ≝ generate globals (ertl_if_luniverse int_fun)graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in63 let 〈l, graph 〉 ≝ generate globals (ertl_if_luniverse int_fun)graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in64 let 〈l, graph 〉 ≝ generate globals (ertl_if_luniverse int_fun)graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in65 let 〈l, graph 〉 ≝ generate globalsgraph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in66 〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, graph〉.59 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in 60 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_load globals) l) in 61 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in 62 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in 63 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in 64 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in 65 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in 66 〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, 〈graph, luniv〉〉. 67 67 68 68 definition set_stack ≝ … … 74 74 λl. 75 75 let off ≝ adjust_off int_fun off in 76 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_store globals) l) in 77 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in 78 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in 79 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in 80 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in 81 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in 82 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in 83 〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, graph〉. 76 let luniv ≝ ertl_if_luniverse int_fun in 77 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_store globals) l) in 78 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in 79 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in 80 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in 81 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in 82 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in 83 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in 84 〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, 〈graph, luniv〉〉. 84 85 85 86 definition write ≝ … … 91 92 match lookup r with 92 93 [ decision_spill off ⇒ 93 let 〈stmt, graph〉 ≝ set_stack int_fun globals graph off RegisterSST l in 94 〈RegisterSST, generate globals graph stmt〉 95  decision_colour hwr ⇒ 〈hwr, 〈l, graph〉〉 94 let 〈stmt, graph, luniv〉 ≝ set_stack int_fun globals graph off RegisterSST l in 95 let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in 96 〈RegisterSST, 〈l, 〈graph, luniv〉〉〉 97  decision_colour hwr ⇒ 98 let luniv ≝ ertl_if_luniverse int_fun in 99 〈hwr, 〈l, 〈graph, luniv〉〉〉 96 100 ]. 97 101
Note: See TracChangeset
for help on using the changeset viewer.