Changeset 2103 for src/Clight


Ignore:
Timestamp:
Jun 21, 2012, 5:21:02 PM (8 years ago)
Author:
campbell
Message:

Make transform_*program take a more general transformation to make
properties easier to state.

Location:
src/Clight
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r2074 r2103  
    20102010
    20112011definition simplify_program : clight_program → clight_program ≝
    2012 λp. transform_program … p simplify_fundef.
     2012λp. transform_program … p (λ_.simplify_fundef).
    20132013
    20142014(* Simulation on statement continuations. Stolen from labelSimulation and adapted to our setting. *)
  • src/Clight/label.ma

    r1888 r2103  
    189189
    190190definition clight_label : clight_program → clight_program ≝
    191  λp. transform_program … p label_fundef.
     191 λp. transform_program … p (λ_.label_fundef).
  • src/Clight/labelSimulation.ma

    r2050 r2103  
    1818(* FIXME with a more general result *)
    1919axiom transform_program_related : ∀F,V,init,t,p.
    20   related_globals F t (globalenv (λ_.F) V init p) (globalenv (λ_.F) V init (transform_program … p t)).
     20  related_globals F t (globalenv (λ_.F) V init p) (globalenv (λ_.F) V init (transform_program … p (λ_.t))).
    2121(*
    2222#F #V #init #t * #vars #fns #main
     
    11141114% [2: %
    11151115[ whd in ⊢ (??%?);
    1116   change with (transform_program ??? (mk_program …) label_fundef) in match (mk_program ??? (transf_program ????) ?);
     1116  change with (transform_program ??? (mk_program …) (λ_.label_fundef)) in match (mk_program ??? (transf_program ????) ?);
    11171117  <transform_program_init_mem >Em in ⊢ (??%?);
    11181118  whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?);
Note: See TracChangeset for help on using the changeset viewer.