Changeset 3014 for src/compiler.ma


Ignore:
Timestamp:
Mar 28, 2013, 4:58:26 PM (8 years ago)
Author:
tranquil
Message:

ERTL to ERTLptr pass suppressed (it introduced a bug in the later ERTLptr to LTL), and integrated in a single ERTToLTL pass like before

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2946 r3014  
    1111include "RTLabs/RTLabsToRTL.ma".
    1212include "RTL/RTLToERTL.ma".
    13 include "ERTL/ERTLToERTLptr.ma".
    14 include "ERTLptr/ERTLptrToLTL.ma".
     13include "ERTL/ERTLToLTL.ma".
    1514include "LTL/LTLToLIN.ma".
    1615include "LIN/LINToASM.ma".
     
    2726 | rtl_uniq_pass: pass
    2827 | ertl_pass: pass
    29  | ertlptr_pass: pass
    3028 | ltl_pass: pass
    3129 | lin_pass: pass
     
    4846  | rtl_uniq_pass ⇒ with_stack_model rtl_program
    4947  | ertl_pass ⇒ with_stack_model ertl_program
    50   | ertlptr_pass ⇒ with_stack_model ertlptr_program
    5148  | ltl_pass ⇒ with_stack_model ltl_program
    5249  | lin_pass ⇒ with_stack_model lin_program
     
    103100  let st ≝ lookup_stack_cost … p in 
    104101  let i ≝ observe ertl_pass 〈p,st〉 in
    105   let p ≝ ertl_to_ertlptr p in
    106   let st ≝ lookup_stack_cost … p in 
    107   let i ≝ observe ertlptr_pass 〈p,st〉 in
    108   let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in
     102  let 〈p,stack_cost,max_stack〉 ≝ ertl_to_ltl compute_fixpoint colour_graph p in
    109103  (* The two stack models are the same *)
    110104  let st ≝ lookup_stack_cost … p in
Note: See TracChangeset for help on using the changeset viewer.