Changeset 2687 for src/joint


Ignore:
Timestamp:
Feb 21, 2013, 4:20:19 PM (7 years ago)
Author:
tranquil
Message:
  • polished some interfaces
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils.ma

    r2683 r2687  
    164164lapply (opt_eq_from_res ???? H) -H #EQ2
    165165whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
    166 qed.
    167 
    168 lemma symbols_match :
    169     ∀M:matching.∀initV,initW.
    170      (∀v,w. match_var_entry M v w →
    171       size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
    172     ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
    173     ∀MATCH:match_program … M p p'.
    174     symbols … (globalenv … initW p') = symbols … (globalenv … initV p).
    175 * #A #B #V #W #match_fn #match_var #initV #initW #H
    176 #p #p' * #Mvars #Mfn #Mmain
    177 whd in match globalenv in ⊢ (???%); normalize nodelta
    178 whd in match (globalenv_allocmem ????);
    179 change with (add_globals ?????) in match (foldl ?????);
    180 >(proj1 … (add_globals_match … initW … Mvars))
    181 [ % |*:]
    182 [ * #idr #v * #idr' #w #MVE %
    183   [ inversion MVE
    184     #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %
    185   | @(H … MVE)
    186   ]
    187 | @(matching_fns_get_same_blocks … Mfn)
    188   #f #g @match_funct_entry_id
    189 ]
    190 qed.
    191 
    192 lemma symbols_transf:
    193  ∀A,B,V,init.∀prog_in : program A V.
    194  ∀trans : ∀vars.A vars → B vars.
    195  let prog_out ≝ transform_program … prog_in trans in
    196  symbols … (globalenv … init prog_out) = symbols … (globalenv … init prog_in).
    197 #A #B #V #iV #p #tf whd
    198 @(symbols_match … (transform_program_match … tf ?))
    199 #v0 #w0 * //
    200166qed.
    201167
     
    220186  λM,vars.pm_P … (match_fundef M ?).
    221187
    222 axiom functions_match:
     188lemma pm_P_insert :
     189  ∀A,B,P.
     190  ∀p,a1,a2,m1,m2.P a1 a2 → pm_P A B P m1 m2 →
     191  pm_P … P (insert … p a1 m1) (insert … p a2 m2).
     192#A #B #P #p #a1 #a2 #m1 #m2 #Pa1a2 #Pm1m2
     193#p'
     194@(eqb_elim p' p) #H destruct
     195[ >lookup_opt_insert_hit >lookup_opt_insert_hit @Pa1a2
     196| >(lookup_opt_insert_miss … a1 … H) >(lookup_opt_insert_miss … a2 … H)
     197  @Pm1m2
     198]
     199qed.
     200
     201lemma pm_P_set_None :
     202  ∀A,B,P.
     203  ∀p,m1,m2.pm_P A B P m1 m2 →
     204  pm_P … P (pm_set … p (None ?) m1) (pm_set … p (None ?) m2).
     205#A #B #P #p #m1 #m2 #Pm1m2
     206#p'
     207@(eqb_elim p' p) #H destruct
     208[ >lookup_opt_pm_set_hit >lookup_opt_pm_set_hit %
     209| >(lookup_opt_pm_set_miss … H) >(lookup_opt_pm_set_miss … H)
     210  @Pm1m2
     211]
     212qed.
     213
     214record match_genv_t (M : matching)
     215  (vars : list ident)
     216  (ge1 : genv_t (m_A M vars)) (ge2 : genv_t (m_B M vars)) : Prop ≝
     217{ symbols_eq : symbols … ge1 = symbols … ge2
     218; nextfunction_eq : nextfunction … ge1 = nextfunction … ge2
     219; functions_match : pm_P … (match_fundef M ?) (functions … ge1) (functions … ge2)
     220}.
     221
     222lemma add_globals_match :
     223  ∀M : matching.∀initV,initW.
     224  ∀vars1,vars2.
     225  ∀vars.
     226(*  let vars1' ≝ map … (λx.\fst (\fst x)) vars1 in
     227  let vars2' ≝ map … (λx.\fst (\fst x)) vars2 in *)
     228  ∀env_mem1 : genv_t (m_A M vars) × mem.
     229  ∀env_mem2 : genv_t (m_B M vars) × mem.
     230  All2 (ident×region×(m_V M)) (ident×region×(m_W M))
     231      (match_var_entry M) vars1 vars2 →
     232  nextblock … (\snd env_mem1) = nextblock … (\snd env_mem2) →
     233  match_genv_t M vars
     234    (\fst env_mem1) (\fst env_mem2) →
     235  match_genv_t M vars
     236    (\fst (add_globals … initV env_mem1 vars1))
     237    (\fst (add_globals … initW env_mem2 vars2)).
     238#M #init1 #init2 #vars1
     239elim vars1 -vars1 [2: ** #id1 #r1 #v1 #tl1 #IH ]
     240* [2,4: ** #id2 #r2 #v2 #tl2 ]
     241#vars * #env1 #mem1 * #env2 #mem2 *
     242[2: #_ #H @H ]
     243#H inversion H #id' #r' #v1' #v2' #P #EQ1 #EQ2 #_ destruct -H #H
     244#EQnxtbl #G @(IH tl2 … H)
     245cases mem1 in EQnxtbl; -mem1 #mem1 #nbl1 #prf1
     246cases mem2 -mem2 #mem2 #nbl2 #prf2 #EQ destruct
     247[ % ]
     248normalize nodelta %
     249whd in match add_symbol;
     250whd in match drop_fn; normalize nodelta
     251[ >(symbols_eq … G) %
     252| @(nextfunction_eq … G)
     253| >(symbols_eq … G) cases (lookup ? block ??) normalize nodelta
     254  [2: ** [2,3: #p] normalize nodelta ]
     255  try @pm_P_set_None
     256  @(functions_match … G)
     257]
     258qed.
     259
     260lemma add_functs_match :
     261  ∀M : matching.
     262  ∀vars.
     263  ∀functs1,functs2.
     264(*  let vars1' ≝ map … (λx.\fst (\fst x)) vars1 in
     265  let vars2' ≝ map … (λx.\fst (\fst x)) vars2 in *)
     266  ∀env1 : genv_t (m_A M vars).
     267  ∀env2 : genv_t (m_B M vars).
     268  All2 …
     269    (match_funct_entry M vars vars) functs1 functs2 →
     270  match_genv_t M vars env1 env2 →
     271  match_genv_t M vars
     272    (add_functs … env1 functs1)
     273    (add_functs … env2 functs2).
     274#M #vars #functs1 elim functs1 -functs1 [2: * #id1 #f1 #tl1 #IH ]
     275* [2,4: * #id2 #f2 #tl2 ]
     276#env1 #env2 *
     277[2: #H @H ]
     278#H
     279cut (id1 = id2 ∧ match_fundef M … f1 f2)
     280[ @(match_funct_entry_inv M ??????? H) #v #i #f1 #f2 #H %{H} % ]
     281* #EQ destruct #Pf1f2 #Ptl1tl2 #G
     282lapply (IH … Ptl1tl2 G) -G #G
     283%
     284whd in
     285  match (add_functs ?? (? :: tl1));
     286whd in
     287  match (add_functs ?? (? :: tl2));
     288change with (add_functs ?? tl1) in match (foldr ???? tl1);
     289change with (add_functs ?? tl2) in match (foldr ???? tl2);
     290whd in match drop_fn; normalize nodelta
     291[ >(nextfunction_eq … G)  >(symbols_eq … G) %
     292| >(nextfunction_eq … G) %
     293| >(symbols_eq … G) cases (lookup ? block ??) normalize nodelta
     294  [2: ** [2,3: #p] normalize nodelta ]
     295  >(nextfunction_eq … G)
     296  @(pm_P_insert … Pf1f2)
     297  try @pm_P_set_None @(functions_match … G)
     298]
     299qed.
     300
     301lemma globalenv_match:
    223302    ∀M:matching.∀initV,initW.
     303     (∀v,w. match_var_entry M v w →
     304      size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
    224305    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
    225306    ∀MATCH:match_program … M p p'.
    226     match_funct_map M ?
    227       (functions ? (globalenv ?? initV p))
    228       (functions ? (globalenv ?? initW p') ⌈prog_var_names … p' ↦ prog_var_names … p⌉).
    229 @sym_eq @(matching_vars … (mp_vars … MATCH)) qed.
     307    match_genv_t M ? (globalenv … initV p)
     308      (globalenv … initW p' ⌈prog_var_names … p' ↦ prog_var_names … p⌉).
     309[2: @sym_eq @(matching_vars … (mp_vars … MATCH)) ]
     310* #A #B #V #W #Pf #Pv #iV #iW #init_eq
     311* #vars1 #functs1 #main1
     312* #vars2 #functs2 #main2
     313* #Mvars #Mfns #EQmain destruct
     314lapply (sym_eq ????)
     315whd in match prog_var_names in functs2 Mfns ⊢ %;
     316normalize nodelta in functs2 Mfns ⊢ %; #E
     317lapply Mfns lapply functs2 -functs2 lapply Mvars -Mvars lapply init_eq -init_eq
     318whd in match globalenv; whd in match globalenv_allocmem;
     319normalize nodelta
     320cases daemon
     321(* TODO I hate coercions *)
     322qed.
     323
     324lemma symbols_transf:
     325 ∀A,B,V,init.∀prog_in : program A V.
     326 ∀trans : ∀vars.A vars → B vars.
     327 let prog_out ≝ transform_program … prog_in trans in
     328 symbols … (globalenv … init prog_out) = symbols … (globalenv … init prog_in).
     329#A #B #V #iV #p #tf whd
     330lapply (transform_program_match … tf p)
     331#MATCH
     332>(symbols_eq … (globalenv_match … MATCH))
     333[2: @iV |3: #v #w * // ]
     334lapply (sym_eq ????)
     335whd in match (prog_var_names ???); whd in match (prog_vars B ??);
     336#E >(K ?? E) normalize nodelta %
     337qed.
     338
    230339
    231340lemma functions_transf:
     
    236345 option_map ?? (trans ?) (lookup_opt … p (functions … (globalenv … init prog_in))).
    237346#A #B #V #iV #p #tf #n
    238 lapply(functions_match … (transform_program_match … tf p) n) try @iV
    239 cases (lookup_opt … n ?) [2: #f] normalize nodelta
    240 generalize in ⊢ (match (???match % with [ _ ⇒ ?]) with [ _ ⇒ ? | _ ⇒ ? ] → ?);
    241 #e >(K ?? e) normalize nodelta
    242 cases (lookup_opt ???) [2,4: #f'] normalize nodelta
    243 [2,3,4: * % ]
    244 #EQ destruct %
     347lapply (transform_program_match … tf p)
     348#MATCH
     349whd in match globalenv; whd in match globalenv_allocmem;
     350normalize nodelta
     351lapply (functions_match … (globalenv_match … MATCH) n)
     352[ @iV | @iV | #v #w * // ]
     353lapply (sym_eq ????)
     354whd in match (prog_var_names ???); whd in match (prog_vars B ??);
     355#E >(K ?? E) normalize nodelta
     356cases (lookup_opt ???) [2: #x ] normalize nodelta
     357cases (lookup_opt ???) [2,4: #y ] normalize nodelta
     358[ #EQ <EQ % |*: * % ]
    245359qed.
    246360
     
    255369#bl
    256370whd in match symbol_for_block; normalize nodelta
    257 >(symbols_match … (transform_program_match … tf ?))
    258 [ % |*:]
    259 #v #w * //
     371>(symbols_transf … tf) %
    260372qed.
    261373
     
    298410include alias "utilities/binary/positive.ma".
    299411
    300 lemma pm_map_cases : ∀A.∀P : positive_map A → Prop.∀m : positive_map A.
    301 ((∀p.lookup_opt … p m = None ?) → P m) →
    302 (∀p,v.lookup_opt … p m = Some ? v → P m) →
    303 P m.
    304 #A #P #m lapply P -P elim m -m
    305 [ #P #H1 #_ @H1 #p % ]
    306 * [2: #x ] #l #r #IHl #IHr #P #H1 #H2 [ @(H2 one x) % ]
    307 @IHl [2: #p #v #EQ @(H2 (p0 p) v EQ) ]
    308 #l_empty
    309 @IHr [2: #p #v #EQ @(H2 (p1 p) v EQ) ]
    310 #r_empty
    311 @H1 * normalize //
    312 qed.
    313 
    314412lemma pm_map_add_ind : ∀A.∀P : positive_map A → Prop.
    315413(∀m.(∀p.lookup_opt A p m = None ?) → P m) →
     
    338436#A #B #impl * #Bf % #At @Bf @impl @At qed-.
    339437
     438definition b_graph_transform_program_props ≝
     439  λsrc,dst : sem_graph_params.
     440  λdata,prog_in.
     441  λinit_regs : block → list register.
     442  λf_lbls : block → label → option (list label).
     443  λf_regs : block → label → option (list register).
     444   let prog_out ≝ b_graph_transform_program src dst data prog_in in
     445   let src_genv ≝ globalenv_noinit ? prog_in in
     446   let dst_genv ≝ globalenv_noinit ? prog_out in
     447  ∀bl,def_in.
     448  find_funct_ptr … src_genv bl = return (Internal ? def_in) →
     449  ∃init_data,def_out.
     450  find_funct_ptr … dst_genv bl = return (Internal ? def_out) ∧
     451  bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
     452  b_graph_translate_props src dst ? init_data (init_regs bl)
     453    def_in def_out (f_lbls bl) (f_regs bl).
     454 
    340455lemma b_graph_transform_program_find_funct_ptr :
    341456 ∀src,dst:sem_graph_params.
     
    349464 ∃f_lbls : block → label → option (list label).
    350465 ∃f_regs : block → label → option (list register).
    351  ∀bl,def_in.
    352  find_funct_ptr … src_genv bl = return (Internal ? def_in) →
    353  ∃init_data,def_out.
    354  find_funct_ptr … dst_genv bl = return (Internal ? def_out) ∧
    355  bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
    356  b_graph_translate_props src dst ? init_data (init_regs bl)
    357     def_in def_out (f_lbls bl) (f_regs bl).
     466 b_graph_transform_program_props src dst data prog_in init_regs f_lbls f_regs.
    358467#src #dst #data #prog_in
    359 whd
     468whd in match b_graph_transform_program_props; normalize nodelta
    360469letin prog_out ≝ (b_graph_transform_program … data prog_in)
    361470letin src_genv ≝ (globalenv_noinit ? prog_in)
     
    436545  bind_new register (b_graph_translate_data src dst globals).
    437546 ∀prog_in : joint_program src.
     547 ∀init_regs : block → list register.
     548 ∀f_lbls : block → label → option (list label).
     549 ∀f_regs : block → label → option (list register).
     550 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
    438551 let prog_out ≝ b_graph_transform_program … data prog_in in
    439552 let src_genv ≝ globalenv_noinit ? prog_in in
    440553 let dst_genv ≝ globalenv_noinit ? prog_out in
    441  let code_block ≝ (Σbl.block_region bl = Code) in
    442  ∃init_regs : code_block → list register.
    443  ∃f_lbls : code_block → label → option (list label).
    444  ∃f_regs : code_block → label → option (list register).
    445554 ∀bl,id,def_in.
    446555 fetch_internal_function … src_genv bl = return 〈id, def_in〉 →
     
    451560    def_in def_out (f_lbls bl) (f_regs bl).
    452561#src #dst #data #prog_in
    453 cases (b_graph_transform_program_find_funct_ptr src dst data prog_in)
    454 #init_regs * #f_lbls * #f_regs #props
    455 %{(λb.init_regs b)}
    456 %{(λb.f_lbls b)}
    457 %{(λb.f_regs b)}
     562#init_regs #f_lbls #f_regs #props
    458563#bl #id #def_in
    459564#H @('bind_inversion H) * #id' * #def_in' -H
     
    477582  bind_new register (b_graph_translate_data src dst globals).
    478583 ∀prog_in : joint_program src.
     584 ∀init_regs : block → list register.
     585 ∀f_lbls : block → label → option (list label).
     586 ∀f_regs : block → label → option (list register).
     587 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
    479588 let prog_out ≝ b_graph_transform_program … data prog_in in
    480589 let src_genv ≝ globalenv_noinit ? prog_in in
    481590 let dst_genv ≝ globalenv_noinit ? prog_out in
    482  let code_block ≝ (Σbl.block_region bl = Code) in
    483  ∃init_regs : code_block → list register.
    484  ∃f_lbls : code_block → label → option (list label).
    485  ∃f_regs : code_block → label → option (list register).
    486591 ∀pc,id,def_in,s.
    487592 fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
     
    490595 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
    491596 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
    492  b_graph_translate_props src dst ? init_data (init_regs bl)
    493     def_in def_out (f_lbls bl) (f_regs bl) ∧
    494597 let l ≝ point_of_pc dst pc in
    495598 ∃lbls,regs.
     
    509612  ].
    510613#src #dst #data #prog_in
    511 cases (b_graph_transform_program_fetch_internal_function src dst data prog_in)
    512 #init_regs * #f_lbls * #f_regs #props
    513 %{init_regs}
    514 %{f_lbls}
    515 %{f_regs}
     614#init_regs #f_lbls #f_regs #props
    516615#pc #id #def_in #s
    517616#H @('bind_inversion H) * #id' #def_in' -H
     
    520619#H lapply (opt_eq_from_res ???? H) -H
    521620#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
    522 cases (props … EQfif)
    523 #a * #b #H %{a} %{b} %{H}
    524 cases H -H #_ #props'
    525 @(multi_fetch_ok … props' … EQstmt_at)
    526 qed.
     621cases (b_graph_transform_program_fetch_internal_function … props … EQfif)
     622#a * #b ** #H1 #H2 #H3 %{a} %{b} %
     623[ %{H1 H2} | @(multi_fetch_ok … H3 … EQstmt_at) ]
     624qed.
Note: See TracChangeset for help on using the changeset viewer.