Changeset 1172


Ignore:
Timestamp:
Sep 2, 2011, 3:00:31 PM (8 years ago)
Author:
mulligan
Message:

ertltoltl.ma half complete

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1171 r1172  
    7070    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    7171    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    72       〈joint_st_sequential ? ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
     72      〈joint_st_sequential ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
    7373
    7474definition set_stack:
     
    8383  let off ≝ adjust_off globals int_fun off in
    8484  let luniv ≝ ertl_if_luniverse globals int_fun in
    85   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? ? globals (joint_instr_store ltl_params … globals it it it) l) in
     85  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_store ltl_params … globals it it it) l) in
    8686  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
    8787  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
     
    9090  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    9191  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    92     〈joint_st_sequential ? ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
     92    〈joint_st_sequential ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
    9393
    9494definition write:
     
    143143      else
    144144        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
    145           〈joint_st_sequential ? ? globals (joint_instr_move … ltl_params globals (to_acc src_hwr)) l, graph, luniv〉
     145          〈joint_st_sequential globals (joint_instr_move … ltl_params globals (to_acc src_hwr)) l, graph, luniv〉
    146146    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr src_off l
    147147    ]
     
    162162
    163163definition newframe ≝
    164   λglobals.
    165   λint_fun.
     164  λglobals: list ident.
     165  λint_fun: ertl_internal_function globals.
    166166  λgraph: ltl_statement_graph globals.
    167   λl.
     167  λl: label.
    168168  if eq_nat (stacksize globals int_fun) 0 then
    169     〈joint_st_goto globals l, graph, (ertl_if_luniverse globals int_fun)〉
     169    〈joint_st_goto label unit ltl_params globals l, graph, (ertl_if_luniverse globals int_fun)〉
    170170  else
    171171    let luniv ≝ ertl_if_luniverse globals int_fun in
    172     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? ? globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    173     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
    174     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
    175     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
    176     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    177     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
    178     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_clear_carry … globals) l) in
    179     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
    180       〈joint_st_sequential … globals (joint_instr_move ltl_params … globals (to_acc RegisterSPL)) l, graph, luniv〉.
     172    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
     173    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
     174    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
     175    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
     176    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
     177    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
     178    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_clear_carry … globals) l) in
     179    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
     180      〈joint_st_sequential label unit ltl_params globals (joint_instr_move ltl_params globals (to_acc RegisterSPL)) l, graph, luniv〉.
    181181
    182182definition delframe ≝
     
    194194    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    195195    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    196       〈joint_st_sequential … globals (joint_instr_int ltl_params … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉.
    197 
    198 check joint_st_sequential.
     196      〈joint_st_sequential label unit ltl_params globals (joint_instr_int ltl_params … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉.
    199197
    200198definition translate_statement ≝
Note: See TracChangeset for help on using the changeset viewer.