Changeset 1986 for src/Clight/labelSimulation.ma
 Timestamp:
 May 24, 2012, 9:35:08 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/labelSimulation.ma
r1954 r1986 7 7 8 8 (* TODO: make something general that can live in common/Globalenvs.ma. *) 9 record related_globals (F:Type[0]) (t:F → F) (ge:genv_t Genv F) (ge':genv_t GenvF) : Prop ≝ {9 record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ { 10 10 rg_find_symbol: ∀s. 11 find_symbol ?? ge s = find_symbol ??ge' s;11 find_symbol … ge s = find_symbol … ge' s; 12 12 rg_find_funct: ∀v,f. 13 find_funct ??ge v = Some ? f →14 find_funct ??ge' v = Some ? (t f);13 find_funct … ge v = Some ? f → 14 find_funct … ge' v = Some ? (t f); 15 15 rg_find_funct_ptr: ∀b,f. 16 find_funct_ptr ??ge b = Some ? f →17 find_funct_ptr ??ge' b = Some ? (t f)16 find_funct_ptr … ge b = Some ? f → 17 find_funct_ptr … ge' b = Some ? (t f) 18 18 }. 19 19 20 20 (* FIXME with a more general result *) 21 21 axiom transform_program_related : ∀F,V,init,t,p. 22 related_globals F t (globalenv Genv ? V init p) (globalenv Genv ? V init (transform_program ???p t)).22 related_globals F t (globalenv (λ_.F) V init p) (globalenv (λ_.F) V init (transform_program … p t)). 23 23 (* 24 24 #F #V #init #t * #vars #fns #main … … 406 406 lemma opt_find_funct : ∀ge,ge',m,vf,fd. 407 407 related_globals ? label_fundef ge ge' → 408 opt_to_io io_out io_in … m (find_funct ??ge vf) = Value … fd →409 opt_to_io io_out io_in … m (find_funct ??ge' vf) = Value … (label_fundef fd).408 opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd → 409 opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (label_fundef fd). 410 410 #ge #ge' #m #vf #fd #RG 411 411 lapply (rg_find_funct … RG … vf fd) … … 1104 1104 (* FIXME: to globalenvs and prove *) 1105 1105 axiom transform_program_init_mem : ∀A,B,V,p,f,init. 1106 init_mem Genv ?? init p = init_mem Genv?? init (transform_program A B V p f).1106 init_mem ?? init p = init_mem ?? init (transform_program A B V p f). 1107 1107 1108 1108
Note: See TracChangeset
for help on using the changeset viewer.