Changeset 2497


Ignore:
Timestamp:
Nov 27, 2012, 5:59:25 PM (7 years ago)
Author:
mckinna
Message:

Simplified dependencies on ASM; knock-on from changes in ASM/*.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2494 r2497  
    3636include "ASM/Assembly.ma".
    3737
     38axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map).
     39(*
    3840include "ASM/Policy.ma".
    3941
    4042axiom Jump_expansion_failed : String.
    4143
    42 include "ASM/ASMCostsSplit.ma".
    43 
    44 axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map). (*
    4544definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
    4645λp.
     
    5352  OK ? (assembly p sigma pol).
    5453cases daemon
    55 qed.*)
     54qed.
     55*)
    5656
    57 include "RTLabs/semantics.ma".
    58 
    59 include "joint/Traces.ma".
    60 
    61 include "ASM/Fetch.ma". (* For load_code_memory only *)
     57include "ASM/ASMCostsSplit.ma".
    6258
    6359definition lift_cost_map_back_to_front :
     
    7369
    7470definition compile : clight_program →
    75   res (object_code × costlabel_map × (𝚺labelled:clight_program. ((Σl.in_clight_program labelled l) → ℕ))) ≝
     71  res (object_code × costlabel_map × (𝚺labelled:clight_program. ((Σl.in_clight_program labelled l) → ℕ))) ≝ 
    7672λp.
    7773  ! 〈init_cost,p',p〉 ← front_end p;
Note: See TracChangeset for help on using the changeset viewer.