Changeset 2105 for src/common/AST.ma


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

Show some results about globalenvs and program transformations.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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
Note: See TracChangeset for help on using the changeset viewer.