Changeset 1282 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Sep 28, 2011, 11:50:32 PM (9 years ago)
Author:
sacerdot
Message:

Cosmetic change: names of joint statements/instructions shortened and made
uppercase.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1281 r1282  
    5858    let off ≝ adjust_off globals int_fun off in
    5959    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    60     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in
    61     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
    62     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
    63     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
    64     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    65     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    66     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
    67       〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
     60    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc r)) l) in
     61    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (LOAD … globals it it it) l) in
     62    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPH)) l) in
     63    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
     64    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
     65    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPL)) l) in
     66    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
     67      〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
    6868
    6969definition set_stack:
     
    7979  let off ≝ adjust_off globals int_fun off in
    8080  let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    81   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
    82   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
    83   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
    84   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
    85   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    86   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    87   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
    88     〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
     81  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (STORE … globals it it it) l) in
     82  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc r)) l) in
     83  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPH)) l) in
     84  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
     85  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
     86  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPL)) l) in
     87  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
     88    〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
    8989
    9090
     
    142142      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    143143      if eq_Register dest_hwr src_hwr then
    144         〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
     144        〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
    145145      else
    146         let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
    147           〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc src_hwr)) l) graph, luniv〉
     146        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc dest_hwr)) l) in
     147          〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc src_hwr)) l) graph, luniv〉
    148148    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label
    149149    ]
     
    154154      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    155155      if eq_nat dest_off src_off then
    156         〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
     156        〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
    157157      else
    158158        let temp_hwr ≝ RegisterSST in
     
    170170  if eq_nat (stacksize globals int_fun) 0 then
    171171    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    172       〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
     172      〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
    173173  else
    174174    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    175     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    176     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPH) l) in
    177     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
    178     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
    179     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    180     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPL) l) in
    181     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_clear_carry … globals) l) in
    182     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
    183       〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc RegisterSPL)) l) graph, luniv〉.
     175    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in
     176    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPH) l) in
     177    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPH (zero ?)) l) in
     178    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterSPH)) l) in
     179    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in
     180    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPL) l) in
     181    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (CLEAR_CARRY … globals) l) in
     182    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
     183      〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc RegisterSPL)) l) graph, luniv〉.
    184184
    185185definition delframe ≝
     
    191191  if eq_nat (stacksize globals int_fun) 0 then
    192192    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    193       〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
     193      〈add_graph globals original_label (GOTO (ltl_params globals) globals l) graph, luniv〉
    194194  else
    195195    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    196     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    197     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
    198     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    199     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    200     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
    201       〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l) graph, luniv〉.
     196    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in
     197    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
     198    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
     199    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in
     200    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
     201      〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l) graph, luniv〉.
    202202
    203203definition translate_statement:
     
    213213  λoriginal_label: label.
    214214  match stmt with
    215   [ joint_st_sequential seq l ⇒
     215  [ sequential seq l ⇒
    216216    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    217217    match seq with
    218     [ joint_instr_comment c ⇒
    219       〈add_graph globals original_label (joint_st_sequential … (joint_instr_comment … c) l) graph, luniv〉
    220     | joint_instr_cost_label cost_lbl ⇒
    221       〈add_graph globals original_label (joint_st_sequential … (joint_instr_cost_label … cost_lbl) l) graph, luniv〉
    222     | joint_instr_pop r ⇒
     218    [ COMMENT c ⇒
     219      〈add_graph globals original_label (sequential … (COMMENT … c) l) graph, luniv〉
     220    | COST_LABEL cost_lbl ⇒
     221      〈add_graph globals original_label (sequential … (COST_LABEL … cost_lbl) l) graph, luniv〉
     222    | POP r ⇒
    223223      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    224224      let int_fun ≝ set_luniverse globals ? int_fun luniv in
    225225      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
    226       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
    227         〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_pop … it) l) graph, luniv〉
    228     | joint_instr_push r ⇒
    229       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_push … it) l) in
    230       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    231       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    232       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    233       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    234         〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉
    235     | joint_instr_cond srcr lbl_true ⇒
    236       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_cond … it lbl_true) l) in
     226      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
     227        〈add_graph globals original_label (sequential ltl_params_ globals (POP … it) l) graph, luniv〉
     228    | PUSH r ⇒
     229      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (PUSH … globals it) l) in
     230      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     231      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     232      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     233      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     234        〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
     235    | COND srcr lbl_true ⇒
     236      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (COND … it lbl_true) l) in
    237237      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    238238      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    239239      let int_fun' ≝ set_luniverse globals ? int_fun luniv in
    240       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    241         〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉
    242     | joint_instr_call_id f ignore ignore' ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_call_id … f ignore ignore') l) graph, luniv〉
    243     | joint_instr_store addr1 addr2 srcr ⇒
    244       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_store … it it it) l) in
    245       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterST1)) l) in
    246       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPH)) l) in
    247       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterST0)) l) in
    248       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPL)) l) in
    249       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    250       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    251       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    252       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    253       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterST0)) fresh_lbl) in
    254       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    255       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    256       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    257       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    258       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterST1)) fresh_lbl) in
    259       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    260       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    261       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    262         〈add_graph globals original_label (joint_st_goto … l) graph, luniv〉
    263     | joint_instr_load destr addr1 addr2 ⇒
     240      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     241        〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
     242    | CALL_ID f ignore ignore' ⇒ 〈add_graph globals original_label (sequential … (CALL_ID … f ignore ignore') l) graph, luniv〉
     243    | STORE addr1 addr2 srcr ⇒
     244      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (STORE … it it it) l) in
     245      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST1)) l) in
     246      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in
     247      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in
     248      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) l) in
     249      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     250      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     251      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     252      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     253      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in
     254      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     255      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     256      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     257      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     258      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST1)) fresh_lbl) in
     259      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     260      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     261      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     262        〈add_graph globals original_label (GOTO … l) graph, luniv〉
     263    | LOAD destr addr1 addr2 ⇒
    264264      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    265265      let int_fun ≝ set_luniverse globals ? int_fun luniv in
    266266      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
    267       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
    268       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_load … it it it) l) in
    269       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPH)) l) in
    270       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterST0)) l) in
    271       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPL)) l) in
    272       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    273       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    274       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    275       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    276       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterST0)) fresh_lbl) in
    277       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    278       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    279       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    280       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    281         〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉
    282     | joint_instr_clear_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_clear_carry …) l) graph, luniv〉
    283     | joint_instr_set_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_set_carry …) l) graph, luniv〉
    284     | joint_instr_op2 op2 destr srcr1 srcr2 ⇒
     267      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
     268      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (LOAD … it it it) l) in
     269      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in
     270      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in
     271      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) l) in
     272      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     273      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     274      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     275      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     276      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in
     277      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     278      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     279      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     280      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     281        〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
     282    | CLEAR_CARRY ⇒ 〈add_graph globals original_label (sequential … (CLEAR_CARRY …) l) graph, luniv〉
     283    | SET_CARRY ⇒ 〈add_graph globals original_label (sequential … (SET_CARRY …) l) graph, luniv〉
     284    | OP2 op2 destr srcr1 srcr2 ⇒
    285285      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    286286      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    287287      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
    288       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
    289       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_op2 … op2 it it RegisterB) l) in
    290       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    291       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    292       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    293       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterB)) fresh_lbl) in
    294       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    295       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    296       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    297         〈add_graph globals original_label (joint_st_goto … l) graph, luniv〉
    298     | joint_instr_op1 op1 destr srcr ⇒
     288      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
     289      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP2 … op2 it it RegisterB) l) in
     290      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     291      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     292      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     293      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterB)) fresh_lbl) in
     294      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     295      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     296      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     297        〈add_graph globals original_label (GOTO … l) graph, luniv〉
     298    | OP1 op1 destr srcr ⇒
    299299      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    300300      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    301301      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
    302       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
    303       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_op1 … op1 it it) l) in
    304       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    305       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    306       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    307       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    308         〈add_graph globals original_label (joint_st_goto … l) graph, luniv〉
    309     | joint_instr_int r i ⇒
     302      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
     303      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP1 … op1 it it) l) in
     304      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     305      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     306      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     307      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     308        〈add_graph globals original_label (GOTO … l) graph, luniv〉
     309    | INT r i ⇒
    310310      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    311311      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    312312      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
    313         〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_int … hdw i) l) graph, luniv〉
    314     | joint_instr_move pair_regs ⇒
     313        〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw i) l) graph, luniv〉
     314    | MOVE pair_regs ⇒
    315315      let regl ≝ \fst pair_regs in
    316316      let regr ≝ \snd pair_regs in
     
    325325        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
    326326        | hardware h2 ⇒
    327           let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc h1)) l) in
    328             〈add_graph globals original_label (joint_st_sequential ltl_params_ … (joint_instr_move … (to_acc h2)) l) graph, luniv〉
     327          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc h1)) l) in
     328            〈add_graph globals original_label (sequential ltl_params_ … (MOVE … (to_acc h2)) l) graph, luniv〉
    329329        ]
    330330      ]
    331     | joint_instr_address lbl prf dpl dph ⇒
     331    | ADDRESS lbl prf dpl dph ⇒
    332332      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    333333      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    334334      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l fresh_lbl in
    335       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw1)) l) in
    336       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in
    337       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in
     335      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw1)) l) in
     336      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPH)) l) in
     337      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (ADDRESS … globals lbl prf it it) l) in
    338338      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    339339      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    340340      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    341341      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l fresh_lbl in
    342       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in
    343       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
    344         〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_address … lbl prf it it) l) graph, luniv〉
    345     | joint_instr_extension ext ⇒
     342      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw2)) l) in
     343      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPL)) l) in
     344        〈add_graph globals original_label (sequential ltl_params_ globals (ADDRESS … lbl prf it it) l) graph, luniv〉
     345    | extension ext ⇒
    346346      match ext with
    347347      [ ertl_st_ext_new_frame ⇒ newframe globals int_fun graph l original_label
     
    351351        let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    352352        let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
    353           〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_int … hdw (bitvector_of_nat … (stacksize … int_fun))) l) graph, luniv〉
     353          〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw (bitvector_of_nat … (stacksize … int_fun))) l) graph, luniv〉
    354354      ]
    355     | joint_instr_opaccs opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
     355    | OPACCS opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    356356      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    357357      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dacc_a_reg l fresh_lbl in
    358       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
    359       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_opaccs … opaccs it it it it) l) in
    360       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    361       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    362       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    363       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) fresh_lbl in
    364       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) fresh_lbl) in
    365       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    366       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    367       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    368       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) fresh_lbl in
    369         〈add_graph globals original_label (joint_st_goto … globals fresh_lbl) graph, luniv〉
     358      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
     359      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OPACCS … opaccs it it it it) l) in
     360      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     361      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     362      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     363      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_a_reg (λhdw. sequential … globals (MOVE … globals (to_acc hdw)) l) fresh_lbl in
     364      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterB)) fresh_lbl) in
     365      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     366      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     367      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     368      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_b_reg (λhdw. sequential … globals (MOVE … globals (to_acc hdw)) l) fresh_lbl in
     369        〈add_graph globals original_label (GOTO … globals fresh_lbl) graph, luniv〉
    370370    ]
    371   | joint_st_return ⇒ 〈add_graph globals original_label (joint_st_return ltl_params_ globals) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
    372   | joint_st_goto l ⇒ 〈add_graph globals original_label (joint_st_goto ltl_params_ globals l) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
     371  | RETURN ⇒ 〈add_graph globals original_label (RETURN ltl_params_ globals) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
     372  | GOTO l ⇒ 〈add_graph globals original_label (GOTO ltl_params_ globals l) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
    373373  ].
    374374
     
    435435    let 〈graph, luniv〉 ≝ graph_luniv in
    436436      match eliminable globals (valuation label) stmt with
    437       [ Some successor ⇒ 〈add_graph globals label (joint_st_goto … successor) graph, luniv〉
     437      [ Some successor ⇒ 〈add_graph globals label (GOTO … successor) graph, luniv〉
    438438      | None           ⇒
    439439        translate_statement globals int_fun valuation coloured_graph graph stmt label
Note: See TracChangeset for help on using the changeset viewer.