Changeset 2105


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

Show some results about globalenvs and program transformations.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2103 r2105  
    33include "Clight/Cexec.ma".
    44include "Clight/CexecInd.ma".
    5 
    6 (* TODO: make something general that can live in common/Globalenvs.ma. *)
    7 record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
    8   rg_find_symbol: ∀s.
    9     find_symbol … ge s = find_symbol … ge' s;
    10   rg_find_funct: ∀v,f.
    11     find_funct … ge v = Some ? f →
    12     find_funct … ge' v = Some ? (t f);
    13   rg_find_funct_ptr: ∀b,f.
    14     find_funct_ptr … ge b = Some ? f →
    15     find_funct_ptr … ge' b = Some ? (t f)
    16 }.
    17 
    18 (* FIXME with a more general result *)
    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))).
    21 (*
    22 #F #V #init #t * #vars #fns #main
    23 whd in match (transform_program ?????);
    24 whd in match (transf_program ????);
    25 elim fns
    26 [ % [ // | * [ | #sz #i | #f | #r | #ptr ] #f #F1 whd in F1:(??%?); destruct
    27              cases (eq_offset ??) in F1; #F1 whd in F1:(??%?);
    28              whd in match (globalenv ?????) in F1;
    29              whd in match (globalenv_allocmem ????) in F1;
    30              elim
    31 %
    32 [ #s
    33 *)
    345
    356(* Useful for breaking up the labeling functions, because we don't care about
     
    8455
    8556theorem label_expr_ok : ∀ge,ge',en,m.
    86   related_globals ? label_fundef ge ge' →
     57  related_globals label_fundef ge ge' →
    8758  (∀e,v,tr.
    8859   exec_expr ge en m e = OK … 〈v,tr〉 →
     
    274245
    275246lemma label_exprs_ok : ∀ge,ge'.
    276    related_globals ? label_fundef ge ge' →
     247   related_globals label_fundef ge ge' →
    277248   ∀en,m,es,vs,tr.
    278249   exec_exprlist ge en m es = OK … 〈vs,tr〉 →
     
    397368
    398369lemma opt_find_funct : ∀ge,ge',m,vf,fd.
    399   related_globals ? label_fundef ge ge' →
     370  related_globals label_fundef ge ge' →
    400371  opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd →
    401372  opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (label_fundef fd).
     
    684655   for labeled_statements. *)
    685656lemma step_with_labels_partial : ∀ge,ge'.
    686   related_globals ? label_fundef ge ge' →
     657  related_globals label_fundef ge ge' →
    687658  ∀s1,s1',tr,s2.
    688659  state_with_labels_partial s1 s1' →
     
    10651036
    10661037theorem step_with_labels : ∀ge,ge'.
    1067   related_globals ? label_fundef ge ge' →
     1038  related_globals label_fundef ge ge' →
    10681039  ∀s1,s1',tr,s2.
    10691040  state_with_labels s1 s1' →
     
    11101081whd in match (make_initial_state ?);
    11111082letin ge' ≝ (make_global ?)
    1112 cut (related_globals ? label_fundef ge ge')
     1083cut (related_globals label_fundef ge ge')
    11131084[ // ] #RG
    11141085% [2: %
  • src/common/AST.ma

    r2103 r2105  
    378378qed.
    379379
     380lemma map_partial_All2 : ∀A,B,C,f. ∀P:A×B → A×C → Prop.
     381  (∀i,x,y. f x = OK ? y → P 〈i,x〉 〈i,y〉) →
     382  ∀l,l'.
     383  map_partial A B C f l = OK ? l' →
     384  All2 (A×B) (A×C) P l l'.
     385#A #B #C #f #P #H #l elim l
     386[ * [ // | #h #t #E normalize in E; destruct ]
     387| * #a #b #tl #IH #l' #M
     388  cases (bind_inversion ????? M) -M * #a' #c * #AC #M
     389  cases (bind_inversion ????? M) -M #tl' * #TL #M
     390  cases (bind_inversion ????? AC) -AC #c' * #C #C'
     391  normalize in C C' M; destruct %
     392  [ @H @C
     393  | @IH @TL
     394  ]
     395] qed.
     396
    380397(*
    381398Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
     
    525542qed.
    526543
     544lemma transform_partial_program2_preserves_var_names : ∀A,B,V,W,p,tf,tv,p'.
     545  transform_partial_program2 A B V W p tf tv = OK ? p' →
     546  prog_var_names … p = prog_var_names … p'.
     547#A #B #V #W * #vars #fns #main #tf #tv * #vars' #fns' #main'
     548#T cases (bind_inversion ????? T) -T #vars1 * #Evars1
     549generalize in match (map_partial_preserves_first ?????); #MPPF
     550lapply (refl ? (map_partial ??? tv vars))
     551cases (map_partial ?????) in ⊢ (???% → ?);
     552[ 2: #m #M >M in MPPF ⊢ %; #MPPF #E normalize in E; destruct ]
     553#vs #VS >VS in MPPF ⊢ %; #MPPF
     554whd in ⊢ (??%% → ?);
     555generalize in match (map_fst ???????); #MF
     556#E destruct
     557whd in ⊢ (??%%); @MF
     558qed.
     559
     560
    527561(*
    528562Lemma transform_partial_program2_function:
     
    569603Variable match_varinfo: V -> W -> Prop.
    570604
    571 Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
    572   match x1, x2 with
    573   | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
    574   end.
    575 
    576 Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
    577   match x1, x2 with
    578   | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
    579   end.
    580 
    581 Definition match_program (p1: program A V) (p2: program B W) : Prop :=
    582   list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
    583   /\ p1.(prog_main) = p2.(prog_main)
    584   /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
    585 
     605*)
     606
     607record matching : Type[1] ≝ {
     608  m_A : list ident → Type[0];  m_B : list ident → Type[0];  (* function types *)
     609  m_V : Type[0];  m_W : Type[0];  (* variable types *)
     610  match_fundef : ∀vs. m_A vs → m_B vs → Prop;
     611  match_varinfo : m_V → m_W → Prop
     612}.
     613
     614(* When defining a matching between function entries, quietly enforce equality
     615   of the list of global variables (vs and vs'). *)
     616
     617inductive match_funct_entry (M:matching) : ∀vs,vs'. ident × (m_A M vs) → ident × (m_B M vs') → Prop ≝
     618| mfe_intro : ∀vs,id,f1,f2. match_fundef M vs f1 f2 → match_funct_entry M vs vs 〈id,f1〉 〈id,f2〉.
     619
     620(* but we'll need some care to usefully invert it *)
     621
     622definition mfe_cast_fn_type : ∀M,vs,vs'. ∀E:vs'=vs. m_B M vs' → m_B M vs ≝
     623λM,vs,vs',E. ?.
     624>E #m @m
     625qed.
     626
     627let rec match_funct_entry_inv (M:matching)
     628  (P:∀vs,id,f,id',f'. Prop)
     629  (H:∀vs,id,f,id',f'. match_fundef M vs f f' → P vs id f id' f')
     630  vs id f id' f'
     631  (MFE:match_funct_entry M vs vs 〈id,f〉 〈id',f'〉) on MFE : P vs id f id' f' ≝
     632match MFE return λvs,vs',idf,idf',MFE. ∀E:vs'=vs. P vs (\fst idf) (\snd idf) (\fst idf') (mfe_cast_fn_type … E (\snd idf')) with
     633[ mfe_intro vs id f1 f2 MF ⇒ ?
     634] (refl ??).
     635#E >(K ?? E) @H @MF
     636qed.
     637
     638(* and continue as before *)
     639
     640inductive match_var_entry (M:matching) : ident × region × (m_V M) → ident × region × (m_W M) → Prop ≝
     641| mve_intro : ∀id,r,v1,v2. match_varinfo M v1 v2 → match_var_entry M 〈id,r,v1〉 〈id,r,v2〉.
     642
     643lemma matching_vars : ∀M.∀p1:program (m_A M) (m_V M).∀p2:program (m_B M) (m_W M).
     644  All2 … (match_var_entry M) (prog_vars … p1) (prog_vars … p2) →
     645  prog_var_names … p1 = prog_var_names … p2.
     646#M * #vs1 #mn1 #fn1 * #vs2 #mn2 #fn2
     647normalize generalize in match vs2;
     648elim vs1
     649[ * [ // | #h #t * ]
     650| * * #id1 #r1 #v1 #tl1 #IH * [ * ]
     651  * * #id2 #r2 #v2 #tl2 * *
     652  #id #r #v1' #v2' #_ #H
     653  whd in ⊢ (??%%); >(IH … H) %
     654] qed.
     655
     656record match_program (M:matching) (p1: program (m_A M) (m_V M)) (p2: program (m_B M) (m_W M)) : Prop ≝ {
     657  mp_vars : All2 … (match_var_entry M) (prog_vars … p1) (prog_vars … p2);
     658  mp_funct : All2 ?? … (match_funct_entry M (prog_var_names … p1) (prog_var_names … p2)) (prog_funct … p1) (prog_funct ??… p2);
     659  mp_main : prog_main … p1 = prog_main … p2
     660}.
     661
     662(*
    586663End MATCH_PROGRAM.
    587 
    588 Remark transform_partial_program2_match:
    589   forall (A B V W: Type)
    590          (transf_partial_function: A -> res B)
    591          (transf_partial_variable: V -> res W)
    592          (p: program A V) (tp: program B W),
    593   transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
    594   match_program
    595     (fun fd tfd => transf_partial_function fd = OK tfd)
    596     (fun info tinfo => transf_partial_variable info = OK tinfo)
     664*)
     665
     666(* Now show that all the transformations are instances of match_program. *)
     667
     668lemma transform_partial_program2_match:
     669  ∀A,B,V,W.
     670         ∀transf_partial_function: ∀vs. A vs -> res (B vs).
     671         ∀transf_partial_variable: V -> res W.
     672         ∀p: program A V. ∀tp: program B W.
     673  transform_partial_program2 … p transf_partial_function transf_partial_variable = OK ? tp →
     674  match_program (mk_matching A B V W
     675    (λvs,fd,tfd. transf_partial_function vs … fd = OK ? tfd)
     676    (λinfo,tinfo. transf_partial_variable info = OK ? tinfo))
    597677    p tp.
    598 Proof.
    599   intros. monadInv H. split.
    600   apply list_forall2_imply with
    601     (fun (ab: ident * A) (ac: ident * B) =>
    602        fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
    603   eapply map_partial_forall2. eauto.
    604   intros. destruct v1; destruct v2; simpl in *. auto.
    605   split. auto.
    606   apply list_forall2_imply with
    607     (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
    608        fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
    609   eapply map_partial_forall2. eauto.
    610   intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
    611 Qed.
    612 *)
     678#A #B #V #W #transf_partial_function #transf_partial_variable
     679* #vars #main #functs * #vars' #main' #functs'
     680#T cases (bind_inversion ????? T) -T #fl * #Efl
     681generalize in match (map_partial_preserves_first ?????); #MPPF
     682lapply (refl ? (map_partial ??? transf_partial_variable vars))
     683cases (map_partial ?????) in ⊢ (???% → ?);
     684[ 2: #m #M >M in MPPF ⊢ %; #MPPF #E normalize in E; destruct ]
     685#vs #VS >VS in MPPF ⊢ %; #MPPF
     686whd in ⊢ (??%% → ?);
     687generalize in match (map_fst ???????); #MF
     688#E destruct
     689%
     690[ @(map_partial_All2 … VS) * /2/
     691| whd in match (prog_var_names ???);
     692  whd in match (prog_var_names ???);
     693  <MF @(map_partial_All2 … Efl) #id #f1 #f2 /2/
     694| //
     695] qed.
     696
     697lemma transform_partial_program_match:
     698  ∀A,B,V.
     699    ∀trans_partial_function: ∀vs. A vs → res (B vs).
     700    ∀p: program A V. ∀tp: program B V.
     701  transform_partial_program … p trans_partial_function = OK ? tp →
     702  match_program (mk_matching A B V V
     703    (λvs,fd,tfd. trans_partial_function vs fd = OK ? tfd)
     704    (λv,w. v = w))
     705    p tp.
     706#A #B #V #tpf
     707* #vars #fns #main * #vars' #fns' #main'
     708#TPP cases (bind_inversion ????? TPP) -TPP #fns'' * #MAP
     709#E normalize in E; destruct
     710%
     711[ elim vars' // * * #id #r #v #tl #H % /2/
     712| @(map_partial_All2 … MAP) #i #f #f' #TPF % @TPF
     713| //
     714] qed.
     715
     716lemma transform_program_match:
     717  ∀A,B,V.
     718    ∀trans_function: ∀vs. A vs → B vs.
     719    ∀p: program A V.
     720  match_program (mk_matching A B V V
     721    (λvs,fd,tfd. trans_function vs fd = tfd)
     722    (λv,w. v = w))
     723    p (transform_program … p trans_function).
     724#A #B #V #tf
     725* #vars #fns #main
     726%
     727[ normalize elim vars // * * #id #r #v #tl #H % /2/
     728| whd in match (prog_var_names ???);
     729  whd in match (prog_vars ???);
     730  elim fns
     731  [ //
     732  | * #id #f #tl #IH % // % //
     733  ]
     734| //
     735] qed.
     736
    613737(* * * External functions *)
    614738
  • src/common/GenMem.ma

    r1993 r2105  
    121121qed.
    122122
    123 definition alloc : mem → Z → Z → ∀r:region. mem × Σb:block. block_region b = r ≝
    124   λm,lo,hi,r.
     123let rec alloc (m:mem) (lo:Z) (hi:Z) (r:region) on m : mem × Σb:block. block_region b = r ≝
    125124  let b ≝ mk_block r (nextblock … m) in
    126125  〈mk_mem
  • src/common/Globalenvs.ma

    r2010 r2105  
    202202definition globalenv_noinit: ∀F. ∀p:program F nat. genv_t (F (prog_var_names … p)) ≝
    203203λF,p.
    204   \fst (globalenv_allocmem F nat (λn.[Init_space n]) p).
     204  globalenv F nat (λn.[Init_space n]) p.
    205205
    206206(* Return the initial memory state for the given program. *)
     
    242242] qed.
    243243
     244
     245lemma vars_irrelevant_to_find_funct_ptr : ∀F,V,init,b,vars,ge,m.
     246  find_funct_ptr F (\fst (add_globals F V init 〈ge,m〉 vars)) b = find_funct_ptr F ge b.
     247#F #V #init * * // * // #blk
     248whd in ⊢ (? → ? → ? → ??%%);
     249#vars elim vars
     250[ #ge #m %
     251| * * #id #r #v #tl #IH #ge #m
     252  whd in match (add_globals ?????);
     253  whd in ⊢ (??(???(??(???(????%?))))?);
     254  cases (alloc ????) #m' #b
     255  whd in ⊢ (??(???(??(???(????%?))))?);
     256  >IH cases ge #fnmap #nextblock #symmap
     257  whd in ⊢ (??(???%)?);
     258  %
     259] qed.
     260
     261lemma matching_globals_get_same_blocks : ∀A,B,V,W,initV,initW.
     262  ∀P:(ident × region × V) → (ident × region × W) → Prop.
     263  (∀v,w. P v w → \fst v = \fst w ∧ size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
     264  ∀vars,ge,ge',m,vars'.
     265  symbols ? ge = symbols … ge' →
     266  All2 … P vars vars' →
     267  symbols … (\fst (add_globals A V initV 〈ge,m〉 vars)) = symbols … (\fst (add_globals B W initW 〈ge',m〉 vars')).
     268#A #B #V #W #initV #initW #P #varsOK
     269#vars elim vars
     270[ #ge #ge' #m * [ #E #_ @E | #h #t #_ * ]
     271| * * #id #r #v #tl #IH #ge #ge' #m * [ #_ * ]
     272  * * #id' #r' #w #tl' #E * #p #TL
     273  whd in match (add_globals A ????);
     274  change with (add_globals A ????) in match (foldl ?????);
     275  whd in match (add_globals B ????);
     276  change with (add_globals B ????) in match (foldl (genv_t B × mem) ????);
     277  cases (varsOK … p) #E1 #E2
     278  destruct >E2 cases (alloc ????) #m' #b
     279  @IH //
     280  whd in match (add_symbol ????);
     281  whd in match (add_symbol ????);
     282  >E %
     283] qed.
     284
     285lemma pre_matching_fns_get_same_blocks : ∀A,B,P.
     286  (∀f,g. P f g → \fst f = \fst g) →
     287  ∀fns,fns'.
     288  All2 … P fns fns' →
     289  let ge ≝ add_functs A (empty ?) fns in
     290  let ge' ≝ add_functs B (empty ?) fns' in
     291  nextfunction … ge = nextfunction … ge' ∧ symbols … ge = symbols … ge'.
     292#A #B #P #fnOK #fns elim fns
     293[ * [ #_ % % | #h #t * ]
     294| * #id #f #tl #IH * [ * ]
     295  * #id' #g #tl' * #p lapply (fnOK … p) #E destruct #H
     296  whd in match (add_functs ???);
     297  change with (add_functs ???) in match (foldr ?????);
     298  whd in match (add_functs B ??);
     299  change with (add_functs ???) in match (foldr (ident × B) ????);
     300  cases (IH tl' H) #E1 #E2
     301  % [ >E1 % | >E1 >E2 % ]
     302] qed.
     303
     304lemma matching_fns_get_same_blocks :  ∀A,B,P.
     305  (∀f,g. P f g → \fst f = \fst g) →
     306  ∀fns,fns'.
     307  All2 … P fns fns' →
     308  let ge ≝ add_functs A (empty ?) fns in
     309  let ge' ≝ add_functs B (empty ?) fns' in
     310  symbols … ge = symbols … ge'.
     311#A #B #P #fnOK #fns #fns' #p @(proj2 … (pre_matching_fns_get_same_blocks … p)) @fnOK
     312qed.
    244313
    245314(*
     
    318387  and operations over global environments. *)
    319388
    320   find_funct_ptr_transf:
    321     ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
    322     ∀b: block. ∀f: A.
    323     find_funct_ptr ? (globalenv ?? p) b = Some ? f →
    324     find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? (transf f);
    325   find_funct_transf:
    326     ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
    327     ∀v: val. ∀f: A.
    328     find_funct ? (globalenv ?? p) v = Some ? f →
    329     find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? (transf f);
    330   find_symbol_transf:
    331     ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
    332     ∀s: ident.
    333     find_symbol ? (globalenv ?? (transform_program … transf p)) s =
    334     find_symbol ? (globalenv ?? p) s;
    335389  init_mem_transf:
    336390    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
     
    434488(* * Commutation properties between matching between programs
    435489  and operations over global environments. *)
     490*) *)
     491
     492(* First, show that nextfunction only depends on the number of functions: *)
     493
     494let rec nat_plus_pos (n:nat) (p:Pos) : Pos ≝
     495match n with
     496[ O ⇒ p
     497| S m ⇒ succ (nat_plus_pos m p)
     498].
     499
     500lemma nextfunction_length : ∀A,l,ge.
     501  nextfunction A (add_functs … ge l) = nat_plus_pos (|l|) (nextfunction A ge).
     502#A #l elim l // #h #t #IH #ge
     503whd in ⊢ (??%%); >IH //
     504qed.
     505
     506(* Now link functions in related programs, but without dealing with the type
     507   casts yet. *)
     508
     509lemma find_funct_ptr_All2 : ∀A,B,V,W,b,p,f,initV,initW,p',P.
     510  find_funct_ptr … (globalenv A V initV p) b = Some ? f →
     511  All2 ?? (λx,y. P (\snd x) (\snd y)) (prog_funct ?? p) (prog_funct … p') →
     512  ∃f'. find_funct_ptr … (globalenv B W initW p') b = Some ? f' ∧ P f f'.
     513#A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P
     514cases b * * [ 2,3,5,6,8,9,11,12,14,15,17,18: #bp ]
     515[ 12: | *: #F whd in F:(??%?); destruct ]
     516>vars_irrelevant_to_find_funct_ptr
     517>vars_irrelevant_to_find_funct_ptr
     518letin varnames ≝ (map ??? vars)
     519cut (lookup_opt (A varnames) bp (functions ? (add_functs ? (empty ?) [ ])) = None ?)
     520//
     521cut (nextfunction (A varnames) (empty ?) = nextfunction (B (map … (λx.\fst (\fst x)) vars')) (empty ?))
     522//
     523generalize in match (empty ?);
     524generalize in match (empty ?);
     525generalize in match fns';
     526elim fns
     527[ #fns' #ge' #ge #_ #F1 #FFP @⊥ normalize in FFP; >F1 in FFP; #E destruct
     528| * #id #fn #tl #IH #fns' #ge' #ge #NF #F1 whd in ⊢ (??%? → ?);
     529  whd in match (functions ??);
     530  change with (add_functs ???) in match (foldr ?????);
     531  cases (decidable_eq_pos bp (nextfunction … (add_functs ? ge tl)))
     532  [ #E destruct  >lookup_opt_insert_hit #E destruct
     533    cases fns' [ * ]
     534    * #id' #fn' #tl' * #M #Mtl
     535    %{fn'} % // whd in ⊢ (??%?);
     536    whd in match (functions ??);
     537    change with (add_functs ???) in match (foldr ???? tl');
     538    >nextfunction_length >nextfunction_length <NF >(All2_length  … Mtl)
     539    >lookup_opt_insert_hit @refl
     540  | #NE >lookup_opt_insert_miss //
     541    #FFP cases fns' [ * ] * #id' #fn' #tl' * #M #Mtl
     542    cases (IH ?????? Mtl)
     543    [ #fn'' * #FFP' #P' %{fn''} % [ whd in ⊢ (??%?); >lookup_opt_insert_miss [2: >nextfunction_length <NF <(All2_length … Mtl) <nextfunction_length @NE ] @FFP' | @P' ]
     544    | skip
     545    | 4: @NF
     546    | skip
     547    | //
     548    | @FFP
     549    ]
     550  ]
     551] qed.
     552
     553discriminator Prod.
     554
     555(* Now prove the full version. *)
     556
     557lemma find_funct_ptr_match:
     558    ∀M:matching.∀initV,initW.
     559    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
     560    ∀MATCH:match_program … M p p'.
     561    ∀b: block. ∀f: m_A M (prog_var_names … p).
     562    find_funct_ptr … (globalenv … initV p) b = Some ? f →
     563    ∃tf : m_B M (prog_var_names … p').
     564    find_funct_ptr … (globalenv … initW p') b = Some ? tf ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉).
     565[ 2: >(matching_vars … (mp_vars … MATCH)) % ]
     566* #A #B #V #W #match_fn #match_var #initV #initW
     567#p #p' * #Mvars #Mfn #Mmain
     568#b #f #FFP
     569@(find_funct_ptr_All2 A B V W ??????? FFP)
     570lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars)
     571#E
     572@(All2_mp … Mfn)
     573* #id #f * #id' #f'
     574<E in f' ⊢ %; #f' -Mmain -b -Mfn -Mvars -initV -initW -E
     575normalize #H @(match_funct_entry_inv … H) //
     576qed.
     577
     578lemma
     579  find_funct_ptr_transf_partial2:
     580    ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W.
     581           ∀p: program A V. ∀p': program B W.
     582    transform_partial_program2 … p transf_fun transf_var = OK ? p' →
     583    ∀b: block. ∀f: A ?.
     584    find_funct_ptr ? (globalenv … iV p) b = Some ? f →
     585    ∃f'.
     586    find_funct_ptr ? (globalenv … iW p') b = Some ? f' ∧ transf_fun ? f ≃ OK ? f'.
     587#A #B #V #W #iV #iW #tf #tv #p #p' #TPP2 #b #f #FFP
     588cases (find_funct_ptr_match … (transform_partial_program2_match … TPP2) … FFP)
     589[2: @iW
     590| #f' * #FFP' generalize in ⊢ (???(??(match % with [_⇒?])) → ?); #E
     591#TF %{f'} % //
     592-FFP -TPP2 -FFP' >TF -TF >E in f' ⊢ %; #f' %
     593qed.
     594
     595lemma match_funct_entry_id : ∀M,vs,vs',f,g.
     596  match_funct_entry M vs vs' f g → \fst f = \fst g.
     597#M #vs #vs' #f #g * //
     598qed.
     599
     600lemma
     601  find_symbol_match:
     602    ∀M:matching.
     603    ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
     604    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
     605    match_program … M p p' →
     606    ∀s: ident.
     607    find_symbol ? (globalenv … initW p') s = find_symbol ? (globalenv … initV p) s.
     608* #A #B #V #W #match_fun #match_var #initV #initW #initsize
     609* #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain #s
     610whd in ⊢ (??%%);
     611@sym_eq
     612@(eq_f ??(λx. lookup SymbolTag block x s))
     613whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
     614whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
     615change with (add_globals ?????) in match (foldl ?????);
     616change with (add_globals ?????) in match (foldl ? (ident×region×V) ???);
     617@(matching_globals_get_same_blocks … Mvars)
     618[ * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ]
     619| @(matching_fns_get_same_blocks … Mfns)
     620  #f #g @match_funct_entry_id
     621] qed.
     622 
     623lemma
     624  find_symbol_transf_partial2:
     625    ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W.
     626    (∀v,w. transf_var v = OK ? w → size_init_data_list (iV v) = size_init_data_list (iW w)) →
     627           ∀p: program A V. ∀p': program B W.
     628    transform_partial_program2 … p transf_fun transf_var = OK ? p' →
     629    ∀s: ident.
     630    find_symbol ? (globalenv … iW p') s = find_symbol ? (globalenv … iV p) s.
     631#A #B #V #W #iV #iW #tf #tv #sizeOK #p #p' #TPP2 #s
     632@(find_symbol_match … (transform_partial_program2_match … TPP2))
     633#v0 #w0 * #id #r #v #w @sizeOK
     634qed.
     635
     636lemma
     637  find_funct_ptr_transf:
     638    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
     639    ∀b: block. ∀f: A ?.
     640    find_funct_ptr ? (globalenv … iV p) b = Some ? f →
     641    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = Some ? (transf … f).
     642#A #B #V #iV * #vars #fns #main #tf #b #f #FFP
     643cases (find_funct_ptr_match … (transform_program_match … tf ?) … FFP)
     644[ 2: @iV
     645| #f' * #FFP'
     646  generalize in match (matching_vars ????);
     647  whd in match (prog_var_names ???); whd in match (prog_vars ???);
     648  #E >(K ?? E) whd in ⊢ (??%% → ?); #E' >FFP' >E' %
     649] qed.
     650
     651lemma
     652  find_funct_transf:
     653    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
     654    ∀v: val. ∀f: A ?.
     655    find_funct ? (globalenv … iV p) v = Some ? f →
     656    find_funct ? (globalenv … iV (transform_program … p transf)) v = Some ? (transf ? f).
     657#A #B #V #iV #tf #p #v #f #FF
     658cases (find_funct_find_funct_ptr ???? FF)
     659#r * #b * #pc * #E destruct #FFP
     660change with (find_funct_ptr ???) in ⊢ (??%?);
     661@(find_funct_ptr_transf A B V iV p tf b f FFP) (* XXX Matita seems to require too much detail here *)
     662qed.
     663
     664lemma
     665  find_symbol_transf:
     666    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
     667    ∀s: ident.
     668    find_symbol ? (globalenv … iV (transform_program … p transf)) s =
     669    find_symbol ? (globalenv … iV p) s.
     670#A #B #V #iV #tf #p @(find_symbol_match … (transform_program_match … tf ?))
     671#v0 #w0 * //
     672qed.
     673
     674(* Package up transform_program results nicely. *)
     675
     676record related_globals (A,B:Type[0]) (t: A → B) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
     677  rg_find_symbol: ∀s.
     678    find_symbol … ge s = find_symbol … ge' s;
     679  rg_find_funct: ∀v,f.
     680    find_funct … ge v = Some ? f →
     681    find_funct … ge' v = Some ? (t f);
     682  rg_find_funct_ptr: ∀b,f.
     683    find_funct_ptr … ge b = Some ? f →
     684    find_funct_ptr … ge' b = Some ? (t f)
     685}.
     686
     687theorem transform_program_related : ∀A,B,V,init,p. ∀tf:∀vs. A vs → B vs.
     688  related_globals (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (transform_program A B V p tf)).
     689#A #B #V #iV #p #tf %
     690[ #s @sym_eq @(find_symbol_transf A B V iV tf p)
     691| @(find_funct_transf A B V iV tf p)
     692| @(find_funct_ptr_transf A B V iV p tf)
     693] qed.
     694
     695
     696(*
    436697
    437698  find_funct_ptr_match:
     
    475736           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
    476737    match_program … match_fun match_var p p' →
    477     init_mem ?? p' = init_mem ?? p*)*)
     738    init_mem ?? p' = init_mem ?? p*)
    478739
    479740(*
Note: See TracChangeset for help on using the changeset viewer.