Changeset 1161 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Aug 31, 2011, 6:24:03 PM (9 years ago)
Author:
mulligan
Message:

changes from today: merged ertl, ltl and lin into one datatype to simplify semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1160 r1161  
    5757    let off ≝ adjust_off int_fun off in
    5858    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) in
    60     let 〈l, graph〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
    61     let 〈l, graph〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    62     let 〈l, graph〉 ≝ generate globals (ertl_if_luniverse int_fun) graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    63     let 〈l, graph〉 ≝ generate globals (ertl_if_luniverse int_fun) graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    64     let 〈l, graph〉 ≝ generate globals (ertl_if_luniverse int_fun) graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    65     let 〈l, graph〉 ≝ generate globals 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〉.
     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〉〉.
    6767
    6868definition set_stack ≝
     
    7474  λl.
    7575  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〉〉.
    8485
    8586definition write ≝
     
    9192  match lookup r with
    9293  [ 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〉〉〉
    96100  ].
    97101
Note: See TracChangeset for help on using the changeset viewer.