Ignore:
Timestamp:
May 24, 2012, 9:35:08 AM (8 years ago)
Author:
campbell
Message:

Get rid of unused abstraction of Globalenvs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r1954 r1986  
    77
    88(* 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 Genv F) : Prop ≝ {
     9record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
    1010  rg_find_symbol: ∀s.
    11     find_symbol ?? ge s = find_symbol ?? ge' s;
     11    find_symbol … ge s = find_symbol … ge' s;
    1212  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);
    1515  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)
    1818}.
    1919
    2020(* FIXME with a more general result *)
    2121axiom 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)).
    2323(*
    2424#F #V #init #t * #vars #fns #main
     
    406406lemma opt_find_funct : ∀ge,ge',m,vf,fd.
    407407  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).
    410410#ge #ge' #m #vf #fd #RG
    411411lapply (rg_find_funct … RG … vf fd)
     
    11041104(* FIXME: to globalenvs and prove *)
    11051105axiom 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).
    11071107
    11081108
Note: See TracChangeset for help on using the changeset viewer.