Changeset 1249


Ignore:
Timestamp:
Sep 22, 2011, 11:41:27 AM (8 years ago)
Author:
mulligan
Message:

changes to get everything to typecheck again

Location:
src/ERTL
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1241 r1249  
    7979  λglobals.
    8080  λint_fun.
    81     colour_locals + (joint_if_stacksize ertl_params globals int_fun).
     81    colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun).
    8282
    8383definition stacksize ≝
    8484  λglobals.
    8585  λint_fun.
    86     colour_locals + (joint_if_stacksize ertl_params globals int_fun).
     86    colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun).
    8787
    8888definition adjust_off ≝
     
    104104  λl.
    105105    let off ≝ adjust_off globals int_fun off in
    106     let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
     106    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    107107    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in
    108108    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
     
    112112    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    113113    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    114       〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
     114      〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l, graph, luniv〉.
    115115
    116116definition set_stack:
     
    124124  λl.
    125125  let off ≝ adjust_off globals int_fun off in
    126   let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
    127   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store ltl_params … globals it it it) l) in
     126  let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     127  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
    128128  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
    129129  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
     
    132132  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    133133  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    134     〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
     134    〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l, graph, luniv〉.
    135135
    136136definition write ≝
     
    148148      〈RegisterSST, l, graph, luniv〉
    149149  | decision_colour hwr ⇒
    150     let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
     150    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    151151      〈hwr, l, graph, luniv〉
    152152  ].
     
    161161  λstmt.
    162162  match lookup valuation coloured_graph (inl … r) with
    163   [ decision_colour hwr ⇒ generate globals (joint_if_luniverse ertl_params globals int_fun) graph (stmt hwr)
     163  [ decision_colour hwr ⇒ generate globals (joint_if_luniverse globals (ertl_params globals) int_fun) graph (stmt hwr)
    164164  | decision_spill off ⇒
    165165    let temphwr ≝ RegisterSST in
    166     let 〈l, graph, luniv〉 ≝ generate globals (joint_if_luniverse ertl_params globals int_fun) graph (stmt temphwr) in
     166    let 〈l, graph, luniv〉 ≝ generate globals (joint_if_luniverse globals (ertl_params globals) int_fun) graph (stmt temphwr) in
    167167    let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l in
    168168      generate globals luniv graph stmt
     
    180180    match src with
    181181    [ decision_colour src_hwr ⇒
    182       let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
     182      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    183183      if eq_Register dest_hwr src_hwr then
    184184        〈joint_st_goto … globals l, graph, luniv〉
    185185      else
    186186        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
    187           〈joint_st_sequential … globals (joint_instr_move … ltl_params globals (to_acc src_hwr)) l, graph, luniv〉
     187          〈joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc src_hwr)) l, graph, luniv〉
    188188    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l
    189189    ]
     
    192192    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l
    193193    | decision_spill src_off ⇒
    194       let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
     194      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    195195      if eq_nat dest_off src_off then
    196196        〈joint_st_goto … globals l, graph, luniv〉
     
    209209  λl: label.
    210210  if eq_nat (stacksize globals int_fun) 0 then
    211     〈joint_st_goto ltl_params globals l, graph, (joint_if_luniverse ertl_params globals int_fun)〉
     211    〈joint_st_goto … globals l, graph, (joint_if_luniverse globals (ertl_params globals) int_fun)〉
    212212  else
    213     let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
    214     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    215     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
    216     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
    217     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
    218     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    219     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
    220     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_clear_carry … globals) l) in
    221     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
    222       〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc RegisterSPL)) l, graph, luniv〉.
     213    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     214    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
     215    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
     216    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
     217    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
     218    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
     219    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
     220    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_clear_carry … globals) l) in
     221    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
     222      〈joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc RegisterSPL)) l, graph, luniv〉.
    223223
    224224definition delframe ≝
     
    228228  λl.
    229229  if eq_nat (stacksize globals int_fun) 0 then
    230     〈joint_st_goto ltl_params globals l, graph, joint_if_luniverse ertl_params globals int_fun〉
     230    〈joint_st_goto (ltl_params globals) globals l, graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
    231231  else
    232     let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
    233     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    234     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
    235     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    236     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    237     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    238       〈joint_st_sequential ltl_params globals (joint_instr_int ltl_params globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉.
     232    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     233    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
     234    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     235    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_int … globals RegisterA (zero ?)) l) in
     236    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
     237    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
     238      〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉.
    239239
    240240definition translate_statement ≝
     
    247247  match stmt with
    248248  [ joint_st_sequential seq l ⇒
    249     let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
     249    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    250250    match seq with
    251251    [ joint_instr_comment c ⇒
    252       〈joint_st_sequential ltl_params globals (joint_instr_comment … globals c) l, graph, luniv〉
     252      〈joint_st_sequential (ltl_params globals) globals (joint_instr_comment … globals c) l, graph, luniv〉
    253253    | joint_instr_cost_label cost_lbl ⇒
    254254      〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉
     
    256256      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    257257      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    258         〈joint_st_sequential … globals (joint_instr_pop ltl_params globals it) l, graph, luniv〉
     258        〈joint_st_sequential (ltl_params globals) globals (joint_instr_pop … globals it) l, graph, luniv〉
    259259    | joint_instr_push r ⇒
    260260      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in
    261       let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
     261      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    262262      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
    263         〈joint_st_goto ltl_params globals l, graph, luniv〉
     263        〈joint_st_goto globals l, graph, luniv〉
    264264    | joint_instr_cond srcr lbl_true ⇒
    265265      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in
    266       let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
     266      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    267267      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
    268         〈joint_st_goto ltl_params globals l, graph, luniv〉
     268        〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉
    269269    | joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉
    270270    | joint_instr_store addr1 addr2 srcr ⇒
     
    274274      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
    275275      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    276       let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
     276      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    277277      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    278278      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
    279       let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
     279      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    280280      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
    281281      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in
    282282      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
    283         〈joint_st_goto ltl_params globals l, graph, luniv〉
     283        〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉
    284284    | joint_instr_load destr addr1 addr2 ⇒
    285285      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
     
    289289      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
    290290      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    291       let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
     291      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    292292      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    293293      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
    294       let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
     294      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    295295      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
    296         〈joint_st_goto ltl_params globals l, graph, luniv〉
     296        〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉
    297297    | joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉
    298298    | joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉
     
    301301      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    302302      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in
    303       let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
     303      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    304304      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
    305305      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
    306       let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
     306      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    307307      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
    308         〈joint_st_goto ltl_params globals l, graph, luniv〉
     308        〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉
    309309    | joint_instr_op1 op1 acc_a ⇒
    310310      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a l in
    311311      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    312312      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in
    313       let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
     313      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    314314      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
    315         〈joint_st_goto ltl_params globals l, graph, luniv〉
     315        〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉
    316316    | joint_instr_int r i ⇒
    317317      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    318         〈joint_st_sequential ltl_params globals (joint_instr_int … globals hdw i) l, graph, luniv〉
     318        〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw i) l, graph, luniv〉
    319319    | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
    320320      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a_reg l in
    321321      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    322322      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
    323       let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
     323      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    324324      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    325325      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
    326       let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
     326      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    327327      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
    328328      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in
    329       let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
     329      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    330330      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_b_reg l in
    331331      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    332332      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in
    333333      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
    334       let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
     334      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    335335      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    336336      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
    337       let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
     337      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    338338      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
    339         〈joint_st_goto ltl_params globals l, graph, luniv〉
     339        〈joint_st_goto globals l, graph, luniv〉
    340340    | joint_instr_move pair_regs ⇒
    341341      let regl ≝ \fst pair_regs in
     
    352352        | hardware h2 ⇒
    353353          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in
    354             〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc h2)) l, graph, luniv〉
     354            〈joint_st_sequential (ltl_params globals) globals (joint_instr_move (ltl_params globals) globals (to_acc h2)) l, graph, luniv〉
    355355        ]
    356356      ]
     
    360360      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in
    361361      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in
    362       let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
     362      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    363363      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l in
    364364      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in
    365365      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
    366         〈joint_st_sequential ltl_params globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉
    367     ]
    368   | joint_st_return ⇒ 〈joint_st_return … globals, graph, joint_if_luniverse ertl_params globals int_fun〉
    369   | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, joint_if_luniverse ertl_params globals int_fun〉
     366        〈joint_st_sequential (ltl_params globals) globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉
     367    ]
     368  | joint_st_return ⇒ 〈joint_st_return … globals, graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
     369  | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
    370370  | joint_st_extension ext ⇒
    371371    match ext with
     
    374374    | ertl_st_ext_frame_size r l ⇒
    375375      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    376         〈joint_st_sequential … globals (joint_instr_int ltl_params globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
     376        〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
    377377    ]
    378378  ].
  • src/ERTL/liveness.ma

    r1241 r1249  
    283283  λlabel.
    284284  λliveafter: valuation.
    285   match joint_if_lookup … int_fun label with
     285  match lookup … (joint_if_code … int_fun) label with
    286286  [ None      ⇒ ?
    287287  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
     
    296296  λlabel.
    297297  λliveafter: valuation.
    298   match joint_if_lookup … int_fun label with
     298  match lookup … (joint_if_code … int_fun) label with
    299299  [ None      ⇒ ?
    300300  | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice.
  • src/ERTL/uses.ma

    r1243 r1249  
    6060  ].
    6161
    62 axiom recover_graph: ∀globals. ertl_internal_function globals → table label (ertl_statement globals).
    63 
     62(*
    6463definition examine_internal ≝
    6564  λglobals: list ident.
     
    6867  let uses ≝ tbl_fold ?? (examine_statement globals) (joint_if_graph … int_fun) (tbl_empty …) in
    6968      lookup uses.
     69*)
Note: See TracChangeset for help on using the changeset viewer.