Changeset 1250 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Sep 22, 2011, 12:02:35 PM (9 years ago)
Author:
sacerdot
Message:
  1. Sigma types projections moved to utilities/extralib.ma
  2. Extended statement turned into extended instructions, decreasing the amount of code in the translations
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1249 r1250  
    44include "ERTL/build.ma".
    55include "ERTL/uses.ma".
    6 include "ERTL/Interference.ma".
    76include "ASM/Arithmetic.ma".
    87
     
    365364      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
    366365        〈joint_st_sequential (ltl_params globals) globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉
     366    | joint_instr_extension ext ⇒
     367      match ext with
     368      [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l
     369      | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l
     370      | ertl_st_ext_frame_size r l ⇒
     371        let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
     372          〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
     373      ]
    367374    ]
    368375  | joint_st_return ⇒ 〈joint_st_return … globals, graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
    369376  | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
    370   | joint_st_extension ext ⇒
    371     match ext with
    372     [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l
    373     | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l
    374     | ertl_st_ext_frame_size r l ⇒
    375       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    376         〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
    377     ]
    378377  ].
    379378
Note: See TracChangeset for help on using the changeset viewer.