- Timestamp:
- Jun 21, 2012, 5:21:02 PM (9 years ago)
- Location:
- src
- Files:
-
- 12 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/SimplifyCasts.ma
r2074 r2103 2010 2010 2011 2011 definition simplify_program : clight_program → clight_program ≝ 2012 λp. transform_program … p simplify_fundef.2012 λp. transform_program … p (λ_.simplify_fundef). 2013 2013 2014 2014 (* Simulation on statement continuations. Stolen from labelSimulation and adapted to our setting. *) -
src/Clight/label.ma
r1888 r2103 189 189 190 190 definition 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 18 18 (* FIXME with a more general result *) 19 19 axiom 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))). 21 21 (* 22 22 #F #V #init #t * #vars #fns #main … … 1114 1114 % [2: % 1115 1115 [ 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 ????) ?); 1117 1117 <transform_program_init_mem >Em in ⊢ (??%?); 1118 1118 whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?); -
src/Cminor/toRTLabs.ma
r2033 r2103 939 939 940 940 definition 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). 942 942 943 943 include "Cminor/initialisation.ma". -
src/ERTL/ERTLToLTL.ma
r1601 r2103 425 425 426 426 definition 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 90 90 91 91 definition 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 50 50 51 51 definition 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 415 415 λp. 416 416 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 1251 1251 because of CompCert heritage *) 1252 1252 definition 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)). 1254 1254 1255 1255 *) -
src/RTLabs/RTLabsToRTL_paolo.ma
r2032 r2103 951 951 because of CompCert heritage *) 952 952 definition 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 325 325 map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l. 326 326 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 331 definition transform_program : ∀A,B,V. ∀p:program A V. (∀varnames. A varnames → B varnames) → program B V ≝ 328 332 λA,B,V,p,transf. 329 333 mk_program B V 330 334 (prog_vars A V p) 331 (transf_program ?? transf(prog_funct A V p))335 (transf_program ?? (transf ?) (prog_funct A V p)) 332 336 (prog_main A V p). 333 337 (* … … 446 450 MSG "In function " :: CTX id :: MSG ": " :: nil. 447 451 *) 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) ≝452 definition transform_partial_program : ∀A,B,V. ∀p:program A V. (∀varnames. A varnames → res (B varnames)) → res (program B V) ≝ 449 453 λ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); 451 455 OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)). 452 456 … … 508 512 definition transform_partial_program2 : 509 513 ∀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)) 511 515 → (V → res W) → res (program B W) ≝ 512 516 λ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); ?. 514 518 (*CSC: interactive mode because of dependent types *) 515 519 generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p)); -
src/joint/Erasure.ma
r1515 r2103 254 254 λparams1. 255 255 λ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 …))). 257 257 258 258 definition erase_lin_program: lin_program → lin_program ≝ 259 259 λ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.