Changeset 2700 for src/compiler.ma


Ignore:
Timestamp:
Feb 22, 2013, 2:12:24 PM (7 years ago)
Author:
sacerdot
Message:
  1. exponential function dropped in favour of standard library
  2. fixpoint computation and graph colouring abstracted in the back-end, axiomatized in the compiler
  3. minor speedups in Policy.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2697 r2700  
    2626   axiom lin_to_asm: lin_program → pseudo_assembly_program.
    2727
    28 (* these are already defined in utilities/fixpoint.ma and ERTL/Interference.ma
    29 axiom the_fixpoint : fixpoint.
    30 axiom build : ∀valuation. coloured_graph valuation.
    31 *)
     28axiom compute_fixpoint : fixpoint_computer.
     29axiom colour_graph : coloured_graph_computer.
    3230
    3331definition back_end : RTLabs_program → pseudo_assembly_program ≝
     
    3634  let p ≝ rtl_to_ertl p in
    3735  let p ≝ ertl_to_ertlptr p in
    38   let p ≝ ertlptr_to_ltl p in (* TODO: abstract over colouring *)
     36  let p ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
    3937  let p ≝ ltl_to_lin p in
    4038          lin_to_asm p.
     
    4846axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map).
    4947
    50 (* include "ASM/Policy.ma".
     48(* Only sloow include "ASM/Policy.ma".
     49*)include "ASM/PolicyStep.ma". include "arithmetics/nat.ma". axiom jump_expansion': ∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
     50 option (Σsigma_policy:(Word → Word) × (Word → bool).
     51   let 〈sigma,policy〉≝ sigma_policy in
     52   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy).
    5153
    5254definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
     
    6163cases daemon
    6264qed.
    63 *)
    6465
    6566include "ASM/ASMCosts.ma".
Note: See TracChangeset for help on using the changeset viewer.