Changeset 2286 for src/compiler.ma


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2253 r2286  
    2222include "LIN/LINToASM.ma".
    2323
     24(* these are already defined in utilities/fixpoint.ma and ERTL/Interference.ma
    2425axiom the_fixpoint : fixpoint.
    2526axiom build : ∀valuation. coloured_graph valuation.
    26 
     27*)
    2728definition back_end : RTLabs_program → pseudo_assembly_program ≝
    2829λp.
     
    5859axiom RTLabs_abstract_status : genv → abstract_status.
    5960
    60 include "joint/semantics.ma".
    61 axiom joint_abstract_status :
    62   ∀globals.∀p:params globals.genv globals p → abstract_status.
     61include "joint/Traces.ma".
    6362
    64 include "common/StructuredTraces.ma".
    6563include "ASM/Fetch.ma". (* For load_code_memory only *)
    6664
    67 definition in_clight_program : costlabel → Prop ≝ λ_.True.
     65axiom in_clight_program : costlabel → Prop.
    6866
    6967definition lift_cost_map_back_to_front :
Note: See TracChangeset for help on using the changeset viewer.