 Timestamp:
 Apr 4, 2013, 9:58:03 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/compiler.ma
r3022 r3083 87 87 definition back_end : 88 88 observe_pass → costlabel → RTLabs_program → 89 res (pseudo_assembly_program × stack_cost_model × nat) ≝89 res (pseudo_assembly_program × costlabel × stack_cost_model × nat) ≝ 90 90 λobserve,init_cost,p. 91 91 let p ≝ rtlabs_to_rtl init_cost p in … … 105 105 let i ≝ observe lin_pass 〈p,st〉 in 106 106 ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ; 107 return 〈 p,stack_cost,max_stack〉.107 return 〈〈p,init_cost〉,stack_cost,max_stack〉. 108 108 109 109 (* The assembler *) … … 148 148 ; c_stack_cost: stack_cost_model 149 149 ; c_max_stack: nat 150 ; c_init_costlabel: costlabel 150 151 ; c_labelled_clight: clight_program 151 152 ; c_clight_cost_map: clight_cost_map … … 155 156 λobserve,p. 156 157 ! 〈init_cost,p',p〉 ← front_end observe p; 157 ! 〈p,stack_cost,max_stack〉 ← back_end observe init_cost p; 158 ! 〈p_init_costlabel,stack_cost,max_stack〉 ← back_end observe init_cost p; 159 let 〈p,init_costlabel〉 ≝ p_init_costlabel in 158 160 ! p ← assembler observe p; 159 161 let k ≝ ASM_cost_map p in 160 162 let k' ≝ 161 163 lift_cost_map_back_to_front p k in 162 return mk_compiler_output p stack_cost max_stack p' k'.164 return mk_compiler_output p stack_cost max_stack init_costlabel p' k'.
Note: See TracChangeset
for help on using the changeset viewer.