Changeset 2700 for src/compiler.ma
 Timestamp:
 Feb 22, 2013, 2:12:24 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/compiler.ma
r2697 r2700 26 26 axiom lin_to_asm: lin_program → pseudo_assembly_program. 27 27 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 *) 28 axiom compute_fixpoint : fixpoint_computer. 29 axiom colour_graph : coloured_graph_computer. 32 30 33 31 definition back_end : RTLabs_program → pseudo_assembly_program ≝ … … 36 34 let p ≝ rtl_to_ertl p in 37 35 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 *) 39 37 let p ≝ ltl_to_lin p in 40 38 lin_to_asm p. … … 48 46 axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map). 49 47 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). 51 53 52 54 definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝ … … 61 63 cases daemon 62 64 qed. 63 *)64 65 65 66 include "ASM/ASMCosts.ma".
Note: See TracChangeset
for help on using the changeset viewer.