Changeset 1260 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Sep 23, 2011, 3:04:20 PM (8 years ago)
Author:
mulligan
Message:

commit for csc

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1256 r1260  
    9292
    9393definition get_stack:
    94  ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label →
    95   ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag) ≝
     94 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝
    9695  λglobals: list ident.
    9796  λint_fun.
     
    10099  λoff.
    101100  λl.
     101  λoriginal_label.
    102102    let off ≝ adjust_off globals int_fun off in
    103103    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     
    105105    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
    106106    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
    107     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     107    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
    108108    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    109109    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    110     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    111       〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l, graph, luniv〉.
     110    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
     111      〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
    112112
    113113definition set_stack:
    114114  ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
    115     → Register → label → ((ltl_statement globals) × (ltl_statement_graph globals) × (universe LabelTag))
     115    → Register → label → ?
    116116  λglobals: list ident.
    117117  λint_fun.
     
    120120  λr.
    121121  λl.
     122  λoriginal_label.
    122123  let off ≝ adjust_off globals int_fun off in
    123124  let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     
    125126  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
    126127  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
    127   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     128  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
    128129  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    129130  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    130   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    131     〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l, graph, luniv〉.
     131  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
     132    〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
     133
    132134
    133135definition write ≝
    134136  λglobals: list ident.
    135   λint_fun.
     137  λint_fun: ertl_internal_function globals.
    136138  λvaluation.
    137139  λcoloured_graph.
     
    139141  λr.
    140142  λl.
     143  λoriginal_label: label.
    141144  match colouring valuation coloured_graph (inl … r) with
    142145  [ decision_spill off ⇒
    143     let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST l in
    144     let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in
     146    let luniv ≝ joint_if_luniverse … int_fun in
     147    let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST l original_label in
    145148      〈RegisterSST, l, graph, luniv〉
    146149  | decision_colour hwr ⇒
     
    151154definition read ≝
    152155  λglobals: list ident.
    153   λint_fun.
     156  λint_fun: ertl_internal_function globals.
    154157  λvaluation.
    155158  λcoloured_graph.
     
    157160  λr.
    158161  λstmt.
     162  λoriginal_label: label.
    159163  match colouring valuation coloured_graph (inl … r) with
    160   [ decision_colour hwr ⇒ generate globals (joint_if_luniverse globals (ertl_params globals) int_fun) graph (stmt hwr)
     164  [ decision_colour hwr ⇒
     165    let luniv ≝ joint_if_luniverse … int_fun in
     166      〈add_graph globals original_label (stmt hwr) graph, luniv〉
    161167  | decision_spill off ⇒
    162168    let temphwr ≝ RegisterSST in
    163     let 〈l, graph, luniv〉 ≝ generate globals (joint_if_luniverse globals (ertl_params globals) int_fun) graph (stmt temphwr) in
    164     let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l in
    165       generate globals luniv graph stmt
     169    let luniv ≝ joint_if_luniverse … int_fun in
     170    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (stmt temphwr) in
     171      get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l original_label
    166172  ].
    167173
     
    173179  λsrc: decision.
    174180  λl: label.
     181  λoriginal_label.
    175182  match dest with
    176183  [ decision_colour dest_hwr ⇒
     
    179186      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    180187      if eq_Register dest_hwr src_hwr then
    181         〈joint_st_goto … globals l, graph, luniv〉
     188        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
    182189      else
    183190        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
    184           〈joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc src_hwr)) l, graph, luniv〉
    185     | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l
     191          〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc src_hwr)) l) graph, luniv〉
     192    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label
    186193    ]
    187194  | decision_spill dest_off ⇒
    188195    match src with
    189     [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l
     196    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l original_label
    190197    | decision_spill src_off ⇒
    191198      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    192199      if eq_nat dest_off src_off then
    193         〈joint_st_goto … globals l, graph, luniv〉
     200        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
    194201      else
    195202        let temp_hwr ≝ RegisterSST in
    196         let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l in
    197         let 〈l, graph, luniv〉 ≝ generate globals luniv graph stmt in
    198           get_stack globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l
     203        let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l original_label in
     204          get_stack globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l original_label
    199205    ]
    200206  ].
     
    205211  λgraph: ltl_statement_graph globals.
    206212  λl: label.
     213  λoriginal_label: label.
    207214  if eq_nat (stacksize globals int_fun) 0 then
    208     〈joint_st_goto … globals l, graph, (joint_if_luniverse globals (ertl_params globals) int_fun)〉
     215    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     216      〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
    209217  else
    210218    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    211219    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    212     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
     220    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPH) l) in
    213221    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
    214222    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
    215223    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    216     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
     224    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPL) l) in
    217225    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_clear_carry … globals) l) in
    218226    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
    219       〈joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc RegisterSPL)) l, graph, luniv〉.
     227      〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc RegisterSPL)) l) graph, luniv〉.
    220228
    221229definition delframe ≝
     
    224232  λgraph: graph (ltl_statement globals).
    225233  λl.
     234  λoriginal_label: label.
    226235  if eq_nat (stacksize globals int_fun) 0 then
    227     〈joint_st_goto (ltl_params globals) globals l, graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
     236    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     237      〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
    228238  else
    229239    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    230240    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    231     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     241    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
    232242    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    233243    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    234     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    235       〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉.
     244    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
     245      〈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〉.
    236246
    237247definition translate_statement ≝
     
    242252  λgraph: ltl_statement_graph globals.
    243253  λstmt: ertl_statement globals.
     254  λoriginal_label: label.
    244255  match stmt with
    245256  [ joint_st_sequential seq l ⇒
     
    247258    match seq with
    248259    [ joint_instr_comment c ⇒
    249       〈joint_st_sequential (ltl_params globals) globals (joint_instr_comment … globals c) l, graph, luniv〉
     260      〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_comment … globals c) l) graph, luniv〉
    250261    | joint_instr_cost_label cost_lbl ⇒
    251       〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉
     262      〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l) graph, luniv〉
    252263    | joint_instr_pop r ⇒
    253264      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    254265      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    255         〈joint_st_sequential (ltl_params globals) globals (joint_instr_pop … globals it) l, graph, luniv〉
     266        〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_pop … globals it) l) graph, luniv〉
    256267    | joint_instr_push r ⇒
    257268      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in
    258269      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    259       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    260         〈joint_st_goto … globals l, graph, luniv〉
     270      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     271      let int_fun' ≝ set_luniverse globals ? int_fun luniv in
     272      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l frees) in
     273        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
     274    | _ ⇒ ?
     275    ]
     276  | _ ⇒ ?
     277  ].
    261278    | joint_instr_cond srcr lbl_true ⇒
    262279      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in
    263280      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    264281      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    265         〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉
    266     | joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉
     282        〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
     283    | joint_instr_call_id f ignore ⇒ 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l) graph, luniv〉
    267284    | joint_instr_store addr1 addr2 srcr ⇒
    268285      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
     
    278295      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in
    279296      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    280         〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉
     297        〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
    281298    | joint_instr_load destr addr1 addr2 ⇒
    282299      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
     
    291308      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    292309      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    293         〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉
    294     | joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉
    295     | joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉
    296     | joint_instr_op2 op2 destr srcr
     310        〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
     311    | joint_instr_clear_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_clear_carry … globals) l) graph, luniv〉
     312    | joint_instr_set_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_set_carry … globals) l) graph, luniv〉
     313    | joint_instr_op2 op2 destr srcr1 srcr2
    297314      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
    298315      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    299       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in
    300       let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    301       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     316      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it it RegisterB) l) in
     317      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     318      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    302319      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
    303320      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     321      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     322        〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
     323    | joint_instr_op1 op1 destr srcr  ⇒
     324      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
     325      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     326      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it it) l) in
     327      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    304328      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    305         〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉
    306     | joint_instr_op1 op1 acc_a ⇒
    307       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a l in
    308       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    309       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in
    310       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    311       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    312         〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉
     329        〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
    313330    | joint_instr_int r i ⇒
    314331      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    315         〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw i) l, graph, luniv〉
     332        〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw i) l) graph, luniv〉
    316333    | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
    317334      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a_reg l in
     
    334351      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    335352      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    336         〈joint_st_goto … globals l, graph, luniv〉
     353        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
    337354    | joint_instr_move pair_regs ⇒
    338355      let regl ≝ \fst pair_regs in
     
    341358      [ pseudo p1  ⇒
    342359        match regr with
    343         [ pseudo p2  ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l
    344         | hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l
     360        [ pseudo p2  ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l original_label
     361        | hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l original_label
    345362        ]
    346363      | hardware h1 ⇒
    347364        match regr with
    348         [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l
     365        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
    349366        | hardware h2 ⇒
    350367          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in
    351             〈joint_st_sequential (ltl_params globals) globals (joint_instr_move (ltl_params globals) globals (to_acc h2)) l, graph, luniv〉
     368            〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move (ltl_params globals) globals (to_acc h2)) l) graph, luniv〉
    352369        ]
    353370      ]
     371      | _ ⇒ ?
     372    ]
     373  | _ ⇒ ?
     374  ].
     375   
    354376    | joint_instr_address lbl prf dpl dph ⇒
    355377      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l in
     
    364386    | joint_instr_extension ext ⇒
    365387      match ext with
    366       [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l
    367       | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l
    368       | ertl_st_ext_frame_size r l
     388      [ ertl_st_ext_new_frame ⇒ newframe globals int_fun graph l
     389      | ertl_st_ext_del_frame ⇒ delframe globals int_fun graph l
     390      | ertl_st_ext_frame_size r
    369391        let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    370392          〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
     
    375397  ].
    376398
    377 axiom Sm_leq_n_m_leq_n:
     399lemma Sm_leq_n_m_leq_n:
    378400  ∀m, n: nat.
    379401    S m ≤ n → m ≤ n.
     402  #m #n /2/
     403qed.
    380404
    381405let rec mapi_aux
    382406  (a: Type[0]) (b: Type[0]) (f: BitVector 16 → a → b) (n: nat)
    383407    on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n ≝
    384   match n return λn. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n with
     408  match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n with
    385409  [ O ⇒ λinvariant. λtrie: BitVectorTrie a 0. λaccu: BitVector 16.
    386     match trie return λx. λtrie: BitVectorTrie a x. ∀prf: x = 0. BitVectorTrie b x with
     410    match trie return λx: nat. λtrie: BitVectorTrie a x. ∀prf: x = 0. BitVectorTrie b x with
    387411    [ Leaf l ⇒ λprf. Leaf … (f accu l)
    388412    | Stub s ⇒ λprf. Stub … s
     
    390414    ] (refl … 0)
    391415  | S n' ⇒ λinvariant. λtrie: BitVectorTrie a (S n'). λaccu: BitVector (16 - (S n')).
    392     match trie return λx. λtrie: BitVectorTrie a x. ∀prf: x = S n'. BitVectorTrie b x with
     416    match trie return λx: nat. λtrie: BitVectorTrie a x. ∀prf: x = S n'. BitVectorTrie b x with
    393417    [ Leaf l ⇒ λabsrd. ⊥
    394418    | Stub s ⇒ λprf. Stub … s
    395419    | Node n'' l r ⇒ λprf.
    396420      Node ? n'' ? ?
    397 (*      (mapi_aux a b f n' ? (l⌈n'' ↦ n'⌉) ((false ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))
    398                  (mapi_aux a b f n' ? (r⌈n'' ↦ n'⌉) ((true ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))*)
    399     ] (refl ? (S n'))
     421    ] (refl nat (S n'))
    400422  ].
    401423  [ 1,2: destruct(absrd)
     
    420442  ]
    421443qed.
     444
     445definition mapi ≝
     446  λa, b: Type[0].
     447  λf: label → a → b.
     448  λtrie: BitVectorTrie a 16.
     449    let f' ≝ λbv: BitVector 16. λa.
     450      f (an_identifier LabelTag bv) a
     451    in
     452      mapi_aux a b f' 16 ? trie [[]].
     453  //
     454qed.
    422455 
    423 check mapi_aux.
    424 
    425456definition translate_internal ≝
    426457  λglobals.
    427458  λint_fun.
    428   let uses ≝ examine_internal globals int_fun in
    429   let
     459  let graph ≝ ((empty_map …) : ltl_statement_graph globals) in
     460  let valuation ≝ analyse globals int_fun in
     461  let coloured_graph ≝ build valuation in
     462  let liveafter ≝ analyse globals int_fun in
     463  let blah ≝ mapi … (λlabel. λstmt_graph_luniv.
     464    let stmt ≝
     465      match eliminable globals (liveafter label) stmt with
     466      [ Some successor ⇒ 〈joint_st_goto … successor, graph, joint_if_luniverse … int_fun〉
     467      | None           ⇒ translate_statement globals int_fun valuation coloured_graph graph stmt
     468      ]
     469    in
     470      ?) (joint_if_code … int_fun)
     471  in ?.
     472 
     473 
     474 
     475      let stmt =
     476        match Liveness.eliminable (G.liveafter label) stmt with
     477        | Some successor ->
     478            LTL.St_skip successor
     479        | None ->
     480            I.translate_statement stmt
     481      in
     482      graph := Label.Map.add label stmt !graph
     483    ) int_fun.ERTL.f_graph
    430484
    431485definition translate_funct ≝
Note: See TracChangeset for help on using the changeset viewer.