Changeset 2319 for src/Clight/label.ma


Ignore:
Timestamp:
Sep 3, 2012, 1:16:29 PM (7 years ago)
Author:
campbell
Message:

Generate per-program cost labels rather than per-function ones, and
produce an extra cost label for the global variable initialisation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r2103 r2319  
    175175].
    176176
    177 definition label_function : function → function ≝
    178 λf.
    179   let costgen ≝ new_universe CostTag in
     177definition label_function : universe CostTag → function → function × (universe CostTag) ≝
     178λcostgen,f.
    180179  let 〈body,costgen〉 ≝ label_statement (fn_body f) costgen in
    181180  let 〈body,costgen〉 ≝ add_cost_before body costgen in
    182     mk_function (fn_return f) (fn_params f) (fn_vars f) body.
     181    〈mk_function (fn_return f) (fn_params f) (fn_vars f) body, costgen〉.
    183182
    184 definition label_fundef : clight_fundef → clight_fundef ≝
    185 λf. match f with
    186 [ CL_Internal f ⇒ CL_Internal (label_function f)
    187 | CL_External id args ty ⇒ CL_External id args ty
     183definition label_fundef : universe CostTag → clight_fundef → clight_fundef × (universe CostTag) ≝
     184λgen,f. match f with
     185[ CL_Internal f ⇒
     186    let 〈f',gen'〉 ≝ label_function gen f in
     187    〈CL_Internal f', gen'〉
     188| CL_External id args ty ⇒ 〈CL_External id args ty, gen〉
    188189].
    189190
    190 definition clight_label : clight_program → clight_program ≝
    191  λp. transform_program … p (λ_.label_fundef).
     191
     192
     193definition clight_label : clight_program → clight_program × costlabel ≝
     194λp.
     195  let costgen ≝ new_universe CostTag in
     196  let 〈init_cost, costgen〉 ≝ fresh … costgen in
     197  〈\fst (transform_program_gen … costgen p (λ_.label_fundef)), init_cost〉.
Note: See TracChangeset for help on using the changeset viewer.