Changeset 1163 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Sep 1, 2011, 4:23:42 PM (9 years ago)
Author:
mulligan
Message:

even more streamlining and fixes to get things type checking

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1161 r1163  
    3131  let 〈l, luniv〉 ≝ fresh_label globals luniv in
    3232  let graph ≝ add_graph globals l stmt graph in
    33     〈l, 〈graph, luniv〉〉.
     33    〈l, graph, luniv〉.
    3434
    3535definition num_locals ≝
    36   λint_fun.
    37     colour_locals + (ertl_if_stacksize int_fun).
     36  λglobals.
     37  λint_fun.
     38    colour_locals + (ertl_if_stacksize globals int_fun).
    3839
    3940definition stacksize ≝
    40   λint_fun.
    41     colour_locals + (ertl_if_stacksize int_fun).
     41  λglobals.
     42  λint_fun.
     43    colour_locals + (ertl_if_stacksize globals int_fun).
    4244
    4345definition adjust_off ≝
     46  λglobals.
    4447  λint_fun.
    4548  λoff.
    4649  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
    47   let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals int_fun)) int_off false in
     50  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in
    4851    sub.
    4952
     53check
     54
    5055definition get_stack ≝
    51   λint_fun.
    52   λglobals.
     56  λglobals.
     57  λint_fun.
    5358  λgraph: graph (ltl_statement (globals)).
    5459  λr.
    5560  λoff.
    5661  λl.
    57     let off ≝ adjust_off int_fun off in
    58     let luniv ≝ ertl_if_luniverse int_fun in
    59     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in
     62    let off ≝ adjust_off globals int_fun off in
     63    let luniv ≝ ertl_if_luniverse globals int_fun in
     64    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_hdw_to_hdw globals … 〈RegisterA, r〉) l) in
     65    ?.
     66   
    6067    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
    6168    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
Note: See TracChangeset for help on using the changeset viewer.