Changeset 2794 for src


Ignore:
Timestamp:
Mar 7, 2013, 7:47:33 AM (7 years ago)
Author:
mckinna
Message:

Minor tweaks/tidying up

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2774 r2794  
    2626include "ERTL/ERTLToERTLptr.ma".
    2727include "ERTLptr/ERTLptrToLTL.ma".
    28 include "LTL/LTLToLIN.ma".
     28include "LTL/LTLToLIN.ma". 
    2929include "LIN/LINToASM.ma".
    3030
     
    4141  let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
    4242  let p ≝ ltl_to_lin p in
    43   let p ≝ lin_to_asm p in
    44    match p with
    45    [ None ⇒ Error … (msg AssemblyTooLarge)
    46    | Some p ⇒ OK … 〈p,stack_cost,max_stack〉 ].
     43   ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
     44   return 〈p,stack_cost,max_stack〉.
    4745
    4846include "ASM/Policy.ma".
    49 (* Equivalent to the inclusion of ASM/Policy.ma, waiting for that slow
    50    file to compile
    51   include "ASM/PolicyStep.ma".
    52   axiom jump_expansion': ∀program:preamble × (Σl:list labelled_instruction.lt (S (|l|)) 2^16 ∧ is_well_labelled_p l).
    53  option (Σsigma_policy:(Word → Word) × (Word → bool).
    54    let 〈sigma,policy〉≝ sigma_policy in
    55    sigma_policy_specification 〈\fst program,\snd program〉 sigma policy). *)
    56    
     47
    5748definition assembler : pseudo_assembly_program → res labelled_object_code ≝
    5849λp.
     
    6354
    6455include "ASM/ASMCosts.ma".
    65 
    66 (*CSC: move the next definitions, e.g. in BitVectorTrie; JHM: done! *)
    6756
    6857definition lift_cost_map_back_to_front :
Note: See TracChangeset for help on using the changeset viewer.