Changeset 2774 for src/compiler.ma
- Timestamp:
- Mar 5, 2013, 6:15:06 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/compiler.ma
r2767 r2774 32 32 axiom colour_graph : coloured_graph_computer. 33 33 34 definition back_end : RTLabs_program → res pseudo_assembly_program ≝ 34 definition back_end : 35 RTLabs_program → 36 res (pseudo_assembly_program × stack_cost_model × nat) ≝ 35 37 λp. 36 38 let p ≝ rtlabs_to_rtl p in 37 39 let p ≝ rtl_to_ertl p in 38 40 let p ≝ ertl_to_ertlptr p in 39 let p≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)41 let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *) 40 42 let p ≝ ltl_to_lin p in 41 opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p). 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〉 ]. 42 47 43 48 include "ASM/Policy.ma". … … 71 76 include "ASM/ASMCostsSplit.ma". 72 77 73 definition compile : clight_program → 74 res (labelled_object_code × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝ 78 record compiler_output : Type[0] ≝ 79 { c_labelled_object_code: labelled_object_code 80 ; c_stack_cost: stack_cost_model 81 ; c_max_stack: nat 82 ; c_labelled_clight: clight_program 83 ; c_clight_cost_map: clight_cost_map c_labelled_clight 84 }. 85 86 definition compile : clight_program → res compiler_output ≝ 75 87 λp. 76 88 ! 〈init_cost,p',p〉 ← front_end p; 77 ! p← back_end p;89 ! 〈p,stack_cost,max_stack〉 ← back_end p; 78 90 ! p ← assembler p; 79 91 let k ≝ ASM_cost_map p in 80 92 let k' ≝ 81 93 lift_cost_map_back_to_front p' (load_code_memory (oc p)) (costlabels p) k in 82 return 〈p, ❬p', k'❭〉.94 return mk_compiler_output p stack_cost max_stack p' k'.
Note: See TracChangeset
for help on using the changeset viewer.