Changeset 1423 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Oct 19, 2011, 6:05:50 PM (8 years ago)
Author:
sacerdot
Message:
  • spill no longer used
  • BUG IN Interference: generating the destruct principle takes too long
  • ERTLToLTL not compiling ATM
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1352 r1423  
    11include "ERTL/ERTL.ma".
    22include "LTL/LTL.ma".
    3 include "ERTL/spill.ma".
    43include "ASM/Arithmetic.ma".
    54
     
    3029
    3130definition num_locals ≝
    32   λglobals.
    33   λint_fun.
    34     colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun).
     31  λspilled_no.
     32  λglobals.
     33  λint_fun.
     34    spilled_no + (joint_if_stacksize globals (ertl_params globals) int_fun).
    3535
    3636definition stacksize ≝
    37   λglobals.
    38   λint_fun.
    39     colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun).
     37  λspilled_no.
     38  λglobals.
     39  λint_fun.
     40    spilled_no + (joint_if_stacksize globals (ertl_params globals) int_fun).
    4041
    4142definition adjust_off ≝
     43  λspilled_no.
    4244  λglobals.
    4345  λint_fun.
    4446  λoff.
    4547  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
    46   let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in
     48  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals spilled_no globals int_fun)) int_off false in
    4749    sub.
    4850
    4951definition get_stack:
    50  ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝
     52 nat → ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝
     53  λspilled_no.
    5154  λglobals: list ident.
    5255  λint_fun.
     
    5659  λl.
    5760  λoriginal_label.
    58     let off ≝ adjust_off globals int_fun off in
     61    let off ≝ adjust_off spilled_no globals int_fun off in
    5962    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    6063    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc r)) l) in
     
    6871
    6972definition set_stack:
    70   ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
     73  nat → ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
    7174    → Register → label → ? ≝
     75  λspilled_no.
    7276  λglobals: list ident.
    7377  λint_fun.
     
    7781  λl.
    7882  λoriginal_label.
    79   let off ≝ adjust_off globals int_fun off in
     83  let off ≝ adjust_off spilled_no globals int_fun off in
    8084  let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    8185  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (STORE … globals it it it) l) in
Note: See TracChangeset for help on using the changeset viewer.