Changeset 1515 for src/Clight/label.ma


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (8 years ago)
Author:
campbell
Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r1224 r1515  
    172172].
    173173
    174 definition label_function : function → res function ≝
     174definition label_function : function → function ≝
    175175λf.
    176176  let costgen ≝ new_universe CostTag in
    177177  let 〈body,costgen〉 ≝ label_statement (fn_body f) costgen in
    178178  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.
    181180
    182 definition label_fundef : clight_fundef → res clight_fundef ≝
     181definition label_fundef : clight_fundef → clight_fundef ≝
    183182λf. match f with
    184 [ CL_Internal f ⇒ do f ← label_function f; OK ? (CL_Internal f)
    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
    186185].
    187186
    188 definition clight_label : clight_program → res clight_program ≝
    189  λp. transform_partial_program … p label_fundef.
     187definition clight_label : clight_program → clight_program ≝
     188 λp. transform_program … p label_fundef.
Note: See TracChangeset for help on using the changeset viewer.