Changeset 1168 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Sep 2, 2011, 11:36:15 AM (9 years ago)
Author:
sacerdot
Message:

Joint statements parameterized over a record.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1166 r1168  
    5151    sub.
    5252
    53 definition get_stack ≝
     53definition get_stack:
     54 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label →
     55  ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag)
     56
    5457  λglobals: list ident.
    5558  λint_fun.
     
    6063    let off ≝ adjust_off globals int_fun off in
    6164    let luniv ≝ ertl_if_luniverse globals int_fun in
    62     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ??????? globals (joint_instr_move … globals (from_acc r)) l) in
    63     ?.
    64    
    65     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
    66     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    67     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    68     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    69     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    70     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    71       〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, 〈graph, luniv〉〉.
     65    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in
     66    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
     67    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
     68    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     69    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
     70    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
     71    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〉.
    7273
    7374definition set_stack ≝
Note: See TracChangeset for help on using the changeset viewer.