Changeset 2103 for src

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

Files:

• Clight/SimplifyCasts.ma (modified) (1 diff)
• Clight/label.ma (modified) (1 diff)
• Clight/labelSimulation.ma (modified) (2 diffs)
• Cminor/toRTLabs.ma (modified) (1 diff)
• ERTL/ERTLToLTL.ma (modified) (1 diff)
• LTL/LTLToLIN.ma (modified) (1 diff)
• RTL/RTLTailcall.ma (modified) (1 diff)
• RTL/RTLToERTL.ma (modified) (1 diff)
• RTLabs/RTLabsToRTL.ma (modified) (1 diff)
• RTLabs/RTLabsToRTL_paolo.ma (modified) (1 diff)
• common/AST.ma (modified) (3 diffs)
• joint/Erasure.ma (modified) (1 diff)

src/Clight/SimplifyCasts.ma

@@ -2010 +2010 @@
 
 definition simplify_program : clight_program → clight_program ≝
-λp. transform_program … p simplify_fundef.
+λp. transform_program … p (λ_.simplify_fundef).
 
 (* Simulation on statement continuations. Stolen from labelSimulation and adapted to our setting. *)

src/Clight/label.ma

@@ -189 +189 @@
 
 definition clight_label : clight_program → clight_program ≝
- λp. transform_program … p label_fundef.
+ λp. transform_program … p (λ_.label_fundef).

src/Clight/labelSimulation.ma

@@ -18 +18 @@
 (* FIXME with a more general result *)
 axiom transform_program_related : ∀F,V,init,t,p.
-  related_globals F t (globalenv (λ_.F) V init p) (globalenv (λ_.F) V init (transform_program … p t)).
+  related_globals F t (globalenv (λ_.F) V init p) (globalenv (λ_.F) V init (transform_program … p (λ_.t))).
 (*
 #F #V #init #t * #vars #fns #main
@@ -1114 +1114 @@
 % [2: %
 [ whd in ⊢ (??%?);
-  change with (transform_program ??? (mk_program …) label_fundef) in match (mk_program ??? (transf_program ????) ?);
+  change with (transform_program ??? (mk_program …) (λ_.label_fundef)) in match (mk_program ??? (transf_program ????) ?);
   <transform_program_init_mem >Em in ⊢ (??%?);
   whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?);

src/Cminor/toRTLabs.ma

@@ -939 +939 @@
 
 definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
-λp.transform_partial_program … p (transf_partial_fundef … c2ra_function).
+λp.transform_partial_program … p (λ_. transf_partial_fundef … c2ra_function).
 
 include "Cminor/initialisation.ma".

src/ERTL/ERTLToLTL.ma

@@ -425 +425 @@
 
 definition ertl_to_ltl: ertl_program → ltl_program ≝
-  λp.transform_program … p (transf_fundef … (translate_internal …)).
+  λp.transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).

src/LTL/LTLToLIN.ma

@@ -90 +90 @@
 
 definition ltl_to_lin : ltl_program → lin_program ≝
- λp. transform_program … p (transf_fundef … (translate_int_fun …)).
+ λp. transform_program … p (λvarnames. transf_fundef … (translate_int_fun varnames)).

src/RTL/RTLTailcall.ma

@@ -50 +50 @@
 
 definition tailcall_simplify : rtl_program → rtlntc_program ≝
- λp. transform_program … p (transf_fundef … (simplify_internal …)).
+ λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).

src/RTL/RTLToERTL.ma

@@ -415 +415 @@
  λp.
   let p ≝ tailcall_simplify p in (* tailcall simplification here *)
-    transform_program ??? p (transf_fundef ?? (translate_funct …)).
+    transform_program ??? p (λvarnames. transf_fundef ?? (translate_funct varnames)).

src/RTLabs/RTLabsToRTL.ma

@@ -1251 +1251 @@
   because of CompCert heritage *)
 definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
- λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).
+ λp. transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
 
 *)

src/RTLabs/RTLabsToRTL_paolo.ma

@@ -951 +951 @@
   because of CompCert heritage *)
 definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
- λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).
+ λp. transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).

src/common/AST.ma

@@ -325 +325 @@
   map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
 
-definition transform_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → B (prog_var_names … p)) → program B V ≝
+(* In principle we could allow the transformation to be specialised to a
+   particular set of variable names, but that makes it much harder to state
+   and prove properties. *)
+
+definition transform_program : ∀A,B,V. ∀p:program A V. (∀varnames. A varnames → B varnames) → program B V ≝
 λA,B,V,p,transf.
   mk_program B V
     (prog_vars A V p)
-    (transf_program ?? transf (prog_funct A V p))
+    (transf_program ?? (transf ?) (prog_funct A V p))
     (prog_main A V p).
 (*
@@ -446 +450 @@
   MSG "In function " :: CTX id :: MSG ": " :: nil.
 *)
-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) ≝
+definition transform_partial_program : ∀A,B,V. ∀p:program A V. (∀varnames. A varnames → res (B varnames)) →  res (program B V) ≝
 λA,B,V,p,transf_partial.
-  do fl ← map_partial … transf_partial (prog_funct … p);
+  do fl ← map_partial … (transf_partial ?) (prog_funct … p);
   OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)).
 
@@ -508 +512 @@
 definition transform_partial_program2 :
  ∀A,B,V,W. ∀p: program A V.
-  (A (prog_var_names … p) → res (B (prog_var_names ?? p)))
+  (∀varnames. A varnames → res (B varnames))
   →  (V → res W) → res (program B W) ≝
 λA,B,V,W,p, transf_partial_function, transf_partial_variable.
-  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?.
+  do fl ← map_partial … (*prefix_funct_name*) (transf_partial_function ?) (prog_funct ?? p); ?.
   (*CSC: interactive mode because of dependent types *)
   generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p));

src/joint/Erasure.ma

@@ -254 +254 @@
   λparams1.
   λprogram.
-    transform_program … program (transf_fundef … (pre_erase_joint_internal_function … (pre_erase_graph_internal_function …) (relabel_graph …))).
+    transform_program … program (transf_fundef … (λvarnames. pre_erase_joint_internal_function varnames … (pre_erase_graph_internal_function varnames …) (relabel_graph varnames …))).
 
 definition erase_lin_program: lin_program → lin_program ≝
   λprogram.
-    transform_program … program (transf_fundef … (pre_erase_joint_internal_function … (pre_erase_lin_internal_function …) (relabel_lin_internal_function …))).
+    transform_program … program (transf_fundef … (λvarnames. pre_erase_joint_internal_function varnames … (pre_erase_lin_internal_function varnames …) (relabel_lin_internal_function varnames …))).