Changeset 2103


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

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

Location:
src
Files:
12 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 ⊢ (??%?);
  • src/Cminor/toRTLabs.ma

    r2033 r2103  
    939939
    940940definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
    941 λp.transform_partial_program … p (transf_partial_fundef … c2ra_function).
     941λp.transform_partial_program … p (λ_. transf_partial_fundef … c2ra_function).
    942942
    943943include "Cminor/initialisation.ma".
  • src/ERTL/ERTLToLTL.ma

    r1601 r2103  
    425425
    426426definition ertl_to_ltl: ertl_program → ltl_program ≝
    427   λp.transform_program … p (transf_fundef … (translate_internal …)).
     427  λp.transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
  • src/LTL/LTLToLIN.ma

    r1515 r2103  
    9090
    9191definition ltl_to_lin : ltl_program → lin_program ≝
    92  λp. transform_program … p (transf_fundef … (translate_int_fun …)).
     92 λp. transform_program … p (λvarnames. transf_fundef … (translate_int_fun varnames)).
  • src/RTL/RTLTailcall.ma

    r1282 r2103  
    5050
    5151definition tailcall_simplify : rtl_program → rtlntc_program ≝
    52  λp. transform_program … p (transf_fundef … (simplify_internal …)).
     52 λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).
  • src/RTL/RTLToERTL.ma

    r2035 r2103  
    415415 λp.
    416416  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
    417     transform_program ??? p (transf_fundef ?? (translate_funct …)).
     417    transform_program ??? p (λvarnames. transf_fundef ?? (translate_funct varnames)).
  • src/RTLabs/RTLabsToRTL.ma

    r2032 r2103  
    12511251  because of CompCert heritage *)
    12521252definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
    1253  λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).
     1253 λp. transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
    12541254
    12551255*)
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r2032 r2103  
    951951  because of CompCert heritage *)
    952952definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
    953  λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).
     953 λp. transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
  • src/common/AST.ma

    r1920 r2103  
    325325  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
    326326
    327 definition transform_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → B (prog_var_names … p)) → program B V ≝
     327(* In principle we could allow the transformation to be specialised to a
     328   particular set of variable names, but that makes it much harder to state
     329   and prove properties. *)
     330
     331definition transform_program : ∀A,B,V. ∀p:program A V. (∀varnames. A varnames → B varnames) → program B V ≝
    328332λA,B,V,p,transf.
    329333  mk_program B V
    330334    (prog_vars A V p)
    331     (transf_program ?? transf (prog_funct A V p))
     335    (transf_program ?? (transf ?) (prog_funct A V p))
    332336    (prog_main A V p).
    333337(*
     
    446450  MSG "In function " :: CTX id :: MSG ": " :: nil.
    447451*)
    448 definition transform_partial_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → res (B (prog_var_names … p))) →  res (program B V) ≝
     452definition transform_partial_program : ∀A,B,V. ∀p:program A V. (∀varnames. A varnames → res (B varnames)) →  res (program B V) ≝
    449453λA,B,V,p,transf_partial.
    450   do fl ← map_partial … transf_partial (prog_funct … p);
     454  do fl ← map_partial … (transf_partial ?) (prog_funct … p);
    451455  OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)).
    452456
     
    508512definition transform_partial_program2 :
    509513 ∀A,B,V,W. ∀p: program A V.
    510   (A (prog_var_names … p) → res (B (prog_var_names ?? p)))
     514  (∀varnames. A varnames → res (B varnames))
    511515  →  (V → res W) → res (program B W) ≝
    512516λA,B,V,W,p, transf_partial_function, transf_partial_variable.
    513   do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?.
     517  do fl ← map_partial … (*prefix_funct_name*) (transf_partial_function ?) (prog_funct ?? p); ?.
    514518  (*CSC: interactive mode because of dependent types *)
    515519  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p));
  • src/joint/Erasure.ma

    r1515 r2103  
    254254  λparams1.
    255255  λprogram.
    256     transform_program … program (transf_fundef … (pre_erase_joint_internal_function … (pre_erase_graph_internal_function …) (relabel_graph …))).
     256    transform_program … program (transf_fundef … (λvarnames. pre_erase_joint_internal_function varnames … (pre_erase_graph_internal_function varnames …) (relabel_graph varnames …))).
    257257
    258258definition erase_lin_program: lin_program → lin_program ≝
    259259  λprogram.
    260     transform_program … program (transf_fundef … (pre_erase_joint_internal_function … (pre_erase_lin_internal_function …) (relabel_lin_internal_function …))).
     260    transform_program … program (transf_fundef … (λvarnames. pre_erase_joint_internal_function varnames … (pre_erase_lin_internal_function varnames …) (relabel_lin_internal_function varnames …))).
Note: See TracChangeset for help on using the changeset viewer.