Changeset 1171 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Sep 2, 2011, 2:51:20 PM (9 years ago)
Author:
mulligan
Message:

changes made on claudio's request: changed order of nesting in the joint-ertl statements to make the semantics easier to write. big changes required...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1170 r1171  
    167167  λl.
    168168  if eq_nat (stacksize globals int_fun) 0 then
    169     〈joint_st_goto ? globals l, graph
     169    〈joint_st_goto … 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_from_acc globals RegisterSPH) l) in
    173     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub 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_to_acc globals RegisterSPH) l) in
    176     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
    177     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
    178     let 〈l, graph, lunive〉 ≝ 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 int_fun))) l) in
    180       〈joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l, graph, luniv〉.
     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〉.
    181181
    182182definition delframe ≝
    183   λint_fun.
    184   λglobals.
     183  λglobals.
     184  λint_fun.
    185185  λgraph: graph (ltl_statement globals).
    186186  λl.
    187   if eq_nat (stacksize int_fun) 0 then
    188     〈joint_st_goto ? globals l, graph
     187  if eq_nat (stacksize globals int_fun) 0 then
     188    〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun
    189189  else
    190     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
    191     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    192     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    193     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
    194     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    195       〈joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? (stacksize int_fun))) l, graph〉.
     190    let luniv ≝ ertl_if_luniverse globals int_fun in
     191    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
     192    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     193    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
     194    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
     195    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
     198check joint_st_sequential.
    196199
    197200definition translate_statement ≝
    198   λint_fun.
    199   λglobals: list ident.
    200   λgraph: graph (ltl_statement globals).
    201   λstmt: ertl_statement.
     201  λglobals: list ident.
     202  λint_fun.
     203  λgraph: ltl_statement_graph globals.
     204  λstmt: ertl_statement globals.
    202205  match stmt with
    203   [ ertl_st_skip l ⇒ 〈joint_st_goto ? globals l, graph〉
    204   | ertl_st_comment s l ⇒ 〈joint_st_sequential ? globals (joint_instr_comment globals s) l, graph〉
     206  [ ertl_st_lift_pre pre ⇒
     207    match pre with
     208    [ joint_st_sequential seq l ⇒
     209      match seq with
     210      [ joint_instr_comment c ⇒ 〈joint_st_sequential ? globals (joint_instr_comment globals s) l, graph〉
     211      | _ ⇒ ?
     212      ]
     213    | joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉
     214    | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉
     215    ]
     216  | ertl_st_new_frame l ⇒ newframe globals int_fun graph l
     217  | ertl_st_del_frame l ⇒ delframe globals int_fun graph l
     218  | ertl_st_frame_size r l ⇒
     219    let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
     220      〈joint_st_sequential … globals (joint_instr_int ltl_params … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
     221  ].
     222 
     223  match stmt with
     224  | ertl_st_comment s l ⇒
    205225  | ertl_st_cost cost_lbl l ⇒ 〈joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l, graph〉
    206226  | ertl_st_get_hdw destr sourcehwr l ⇒ move int_fun globals graph (lookup destr) (decision_colour sourcehwr) l
     
    209229    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
    210230      〈joint_st_sequential ? globals (joint_instr_to_acc globals r2) l, graph〉
    211   | ertl_st_new_frame l ⇒ newframe int_fun globals graph l
    212   | ertl_st_del_frame l ⇒ delframe int_fun globals graph l
     231  | ertl_st_new_frame l ⇒
     232  | ertl_st_del_frame l ⇒
    213233  | ertl_st_frame_size r l ⇒
    214     let 〈hdw, l〉 ≝ write int_fun globals graph r l in
    215     let 〈l, graph〉 ≝ l in
    216       〈joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? (stacksize int_fun))) l, graph〉
    217234  | ertl_st_pop r l ⇒
    218235    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
     
    335352    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    336353      〈joint_st_goto ? globals l, graph〉
    337   | ertl_st_return ⇒ 〈joint_st_return ? globals, graph〉
    338354  ].
    339355  cases daemon (* XXX: todo -- proofs regarding gvars *)
Note: See TracChangeset for help on using the changeset viewer.