Changeset 1515 for src/Clight/label.ma

Timestamp:

Nov 18, 2011, 1:03:14 PM (9 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:

• src/Clight/label.ma (modified) (1 diff)

src/Clight/label.ma

@@ -172 +172 @@
 ].
 
-definition label_function : function → res function ≝
+definition label_function : function → function ≝
 λf.
   let costgen ≝ new_universe CostTag in
   let 〈body,costgen〉 ≝ label_statement (fn_body f) costgen in
   let 〈body,costgen〉 ≝ add_cost_before body costgen in
-  do u ← check_universe_ok ? costgen;
-  OK ? (mk_function (fn_return f) (fn_params f) (fn_vars f) body).
+    mk_function (fn_return f) (fn_params f) (fn_vars f) body.
 
-definition label_fundef : clight_fundef → res clight_fundef ≝
+definition label_fundef : clight_fundef → clight_fundef ≝
 λf. match f with
-[ CL_Internal f ⇒ do f ← label_function f; OK ? (CL_Internal f)
-| CL_External id args ty ⇒ OK ? (CL_External id args ty)
+[ CL_Internal f ⇒ CL_Internal (label_function f)
+| CL_External id args ty ⇒ CL_External id args ty
 ].
 
-definition clight_label : clight_program → res clight_program ≝
- λp. transform_partial_program … p label_fundef.
+definition clight_label : clight_program → clight_program ≝
+ λp. transform_program … p label_fundef.