Changeset 3030 for src/Clight


Ignore:
Timestamp:
Mar 29, 2013, 12:09:07 PM (7 years ago)
Author:
campbell
Message:

Break up front-end for correctness proof.
Use let rec to prevent labelling function from unfolding.

Location:
src/Clight
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r3021 r3030  
    280280
    281281
    282 
    283 definition clight_label : clight_program → clight_program × costlabel ≝
    284 λp.
     282(* Use a let rec to prevent premature unfolding in correctness.ma. *)
     283
     284let rec clight_label (p:clight_program) : clight_program × costlabel ≝
    285285  let costgen ≝ new_universe CostTag in
    286286  let 〈init_cost, costgen〉 ≝ fresh … costgen in
    287287  〈\fst (transform_program_gen … costgen p (λ_.label_fundef)), init_cost〉.
     288
     289
     290lemma unfold_clight_label : ∀p.
     291  clight_label p =
     292  (let costgen ≝ new_universe CostTag in
     293  let 〈init_cost, costgen〉 ≝ fresh … costgen in
     294  〈\fst (transform_program_gen … costgen p (λ_.label_fundef)), init_cost〉).
     295* //
     296qed.
  • src/Clight/labelSimulation.ma

    r2722 r3030  
    12741274@(swl_steps E0 E0)
    12751275[ 2: @steps_step | skip | // | @build_exec
    1276   [ @transform_program_gen_related | // | inversion NW
     1276  [ whd in match ge2; >unfold_clight_label @transform_program_gen_related
     1277  | //
     1278  | inversion NW
    12771279    [ #tr #i #s #E1 #E2 destruct
    12781280    | #trX #sX #eX #NWX #E1X #E2X destruct //
Note: See TracChangeset for help on using the changeset viewer.