Changeset 1515 for src/Clight/label.ma
- Timestamp:
- Nov 18, 2011, 1:03:14 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/label.ma
r1224 r1515 172 172 ]. 173 173 174 definition label_function : function → resfunction ≝174 definition label_function : function → function ≝ 175 175 λf. 176 176 let costgen ≝ new_universe CostTag in 177 177 let 〈body,costgen〉 ≝ label_statement (fn_body f) costgen in 178 178 let 〈body,costgen〉 ≝ add_cost_before body costgen in 179 do u ← check_universe_ok ? costgen; 180 OK ? (mk_function (fn_return f) (fn_params f) (fn_vars f) body). 179 mk_function (fn_return f) (fn_params f) (fn_vars f) body. 181 180 182 definition label_fundef : clight_fundef → resclight_fundef ≝181 definition label_fundef : clight_fundef → clight_fundef ≝ 183 182 λf. match f with 184 [ CL_Internal f ⇒ do f ← label_function f; OK ? (CL_Internalf)185 | CL_External id args ty ⇒ OK ? (CL_External id args ty)183 [ CL_Internal f ⇒ CL_Internal (label_function f) 184 | CL_External id args ty ⇒ CL_External id args ty 186 185 ]. 187 186 188 definition clight_label : clight_program → resclight_program ≝189 λp. transform_p artial_program … p label_fundef.187 definition clight_label : clight_program → clight_program ≝ 188 λp. transform_program … p label_fundef.
Note: See TracChangeset
for help on using the changeset viewer.