Changeset 1171 for src/ERTL


Ignore:
Timestamp:
Sep 2, 2011, 2:51:20 PM (10 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...

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • src/ERTL/ERTL.ma

    r1168 r1171  
    1515definition ertl_params: params ≝
    1616 mk_params register register register register (move_registers × move_registers) register.
     17                 
     18inductive ertl_statement_extension: Type[0] ≝
     19  | ertl_st_ext_new_frame: label → ertl_statement_extension
     20  | ertl_st_ext_del_frame: label → ertl_statement_extension
     21  | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
    1722
    18 definition pre_ertl_statement ≝ joint_statement label ertl_params.
    19                  
    20 inductive ertl_statement (globals: list ident): Type[0] ≝
    21   | ertl_st_lift_pre: pre_ertl_statement globals → ertl_statement globals
    22   | ertl_st_new_frame: label → ertl_statement globals
    23   | ertl_st_del_frame: label → ertl_statement globals
    24   | ertl_st_frame_size: register → label → ertl_statement globals.
     23definition ertl_statement ≝ joint_statement label ertl_statement_extension ertl_params.
    2524
    2625definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).

  • 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.