Changeset 2693 for src/compiler.ma


Ignore:
Timestamp:
Feb 22, 2013, 11:39:03 AM (8 years ago)
Author:
sacerdot
Message:
  1. Stuff moved to correct places.
  2. ERTLptr pass added
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2645 r2693  
    1616  return 〈init_cost,p',p〉.
    1717
    18 (*
    1918include "RTLabs/RTLabsToRTL.ma".
    2019include "RTL/RTLToERTL.ma".
    2120include "ERTL/ERTLToLTL.ma".
     21(*
    2222include "LTL/LTLToLIN.ma".
    2323include "LIN/LINToASM.ma".
     24*) include "ASM/ASM.ma". include "LIN/LIN.ma".
     25   axiom ltl_to_lin: ltl_program → lin_program.
     26   axiom lin_to_asm: lin_program → pseudo_assembly_program.
    2427
    2528(* these are already defined in utilities/fixpoint.ma and ERTL/Interference.ma
     
    3538  let p ≝ ltl_to_lin p in
    3639          lin_to_asm p.
    37 *)
    38 include "ASM/ASM.ma".
    39 axiom back_end : RTLabs_program → pseudo_assembly_program.
    4040
    4141(* JHM: minimum needed for assembler axiom to typecheck *)
Note: See TracChangeset for help on using the changeset viewer.