Changeset 2559


Ignore:
Timestamp:
Dec 18, 2012, 1:56:07 PM (7 years ago)
Author:
piccolo
Message:

lineariseProof finished

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2556 r2559  
    1 (**************************************************************************)
     1 (**************************************************************************)
    22(*       ___                                                              *)
    33(*      ||M||                                                             *)
     
    1818include "joint/semanticsUtils.ma".
    1919
    20 axiom globalenv_no_minus_one :
     20include alias "common/PositiveMap.ma".
     21
     22lemma add_functs_functions_miss : ∀F. ∀ge : genv_t F.∀ l.∀ id.
     23id < (nextfunction ? ge) →
     24lookup_opt … id (functions ? ge) = None ? →
     25lookup_opt … id (functions … (add_functs F ge l)) = None ?.
     26#F #ge #l #id whd in match add_functs; normalize nodelta
     27elim l -l [ #_ normalize //]
     28* #id1 #f1 #tl #IND #H #H1 whd in match (foldr ?????);
     29>lookup_opt_insert_miss [ inversion(lookup_opt ? ? ?) [ #_ %]
     30#f1 #H3 <(drop_fn_lfn … f1 H3) @(IND H H1)
     31| cut(nextfunction F ge ≤ nextfunction F (foldr … (add_funct F) ge tl))
     32[elim tl [normalize //]
     33#x #tl2 whd in match (foldr ?????) in ⊢ (? → %); #H %2{H} ]
     34#H2 lapply(transitive_le … H H2) @lt_to_not_eq
     35qed.
     36
     37lemma add_globals_functions_miss : ∀F,V,init. ∀gem : genv_t F × mem.∀ id,l.
     38lookup_opt … id (functions ? (\fst gem)) = None ? →
     39lookup_opt … id (functions … (\fst (add_globals F V init gem l))) = None ?.
     40#F #V #init * #ge #m #id #l lapply ge -ge lapply m -m elim l [ #ge #m #H @H]
     41** #x1 #x2 #x3 #tl whd in match add_globals;
     42normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta
     43cases(alloc m ? ? x2) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;
     44normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %]
     45#f1 #H3 <(drop_fn_lfn … f1 H3) assumption
     46qed.
     47
     48 
     49lemma globalenv_no_minus_one :
    2150 ∀F,V,i,p.
    22   find_funct_ptr … (globalenv F V i p) (mk_block Code (-1)) = None ?. 
     51  find_funct_ptr … (globalenv F V i p) (mk_block Code (-1)) = None ?.
     52#F #V #i #p
     53whd in match find_funct_ptr; normalize nodelta
     54whd in match globalenv;
     55whd in match globalenv_allocmem; normalize nodelta
     56@add_globals_functions_miss @add_functs_functions_miss normalize //
     57qed.
    2358
    2459lemma fetch_internal_function_no_minus_one :
     
    444479]
    445480qed.
     481
     482include alias "common/GenMem.ma".
    446483
    447484lemma bestorev_sigma_commute :
     
    22262263qed.
    22272264
     2265lemma entry_sigma_commute:
     2266∀ p,p',graph_prog,sigma.good_sigma p graph_prog sigma →
     2267∀bl,f1,fn1.
     2268(fetch_function ? (globalenv_noinit … graph_prog) bl =
     2269return 〈f1,Internal ? fn1〉) →
     2270∃prf.
     2271sigma_pc p p' graph_prog sigma
     2272   (pc_of_point (make_sem_graph_params p p') bl (joint_if_entry ?? fn1)) prf =
     2273      pc_of_point (make_sem_lin_params p p') bl 0.
     2274#p #p' #graph_prog #sigma #good #bl #f1 #fn1 #fn1_spec
     2275cases (good fn1) * #entry_in #_ #_
     2276       % [ @hide_prf % | whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc ]
     2277       whd in match sigma_pc_opt; normalize nodelta
     2278       >eqZb_false whd in match (pc_block ?);
     2279       [2,4: % #EQbl
     2280        >(fetch_function_no_minus_one … graph_prog … EQbl) in fn1_spec;
     2281        whd in ⊢ (???%→?); #ABS destruct(ABS) ]
     2282       normalize nodelta whd in match fetch_internal_function;
     2283       normalize nodelta >fn1_spec >m_return_bind >point_of_pc_of_point
     2284       >entry_in whd in ⊢ (??%%→?); #EQ destruct(EQ) %
     2285qed.
     2286
    22282287lemma eval_call_ok :
    22292288 ∀p,p',graph_prog.
     
    23092368     cases (allocate_locals_commute … gss … (joint_if_locals … fn) … st_no_pc_wf')
    23102369     #st_no_pc_wf'' #lin_allocate_locals_spec
    2311      cut
    2312       (∃prf.sigma_pc p p' graph_prog sigma (pc_of_point (make_sem_graph_params p p') bl (joint_if_entry ?? fn)) prf =
    2313       pc_of_point (make_sem_lin_params p p') bl 0)
    2314      [ cases (good fn) * #entry_in #_ #_
    2315        % [ @hide_prf % | whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc ]
    2316        whd in match sigma_pc_opt; normalize nodelta
    2317        >eqZb_false whd in match (pc_block ?);
    2318        [2,4: % #EQbl
    2319         >(fetch_function_no_minus_one … graph_prog … EQbl) in int_f_spec;
    2320         whd in ⊢ (???%→?); #ABS destruct(ABS) ]
    2321        normalize nodelta whd in match fetch_internal_function;
    2322        normalize nodelta >int_f_spec >m_return_bind >point_of_pc_of_point
    2323        >entry_in whd in ⊢ (??%%→?); #EQ destruct(EQ) %
    2324      ] * #entry_prf #entry_spec
     2370     cases(entry_sigma_commute p p' graph_prog sigma good … int_f_spec)
     2371     #entry_prf #entry_spec
    23252372      % [ @hide_prf %{st_no_pc_wf''} %{entry_prf} @(proj1 … (proj1 … prf)) ]
    23262373      % [ whd in match joint_call_ident; normalize nodelta
     
    25782625qed.
    25792626
    2580 (* TODO *)
    2581 axiom eval_tailcall_ok :
     2627 
     2628lemma eval_tailcall_ok :
    25822629∀p,p',graph_prog.
    25832630let lin_prog ≝ linearise p graph_prog in
     
    26002647  eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes))
    26012648    st2_pre_call = return st2_after_call.
    2602 
    2603 
     2649#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn #fl #called #args
     2650#prf #fetch_spec
     2651cases(fetch_statement_sigma_commute … good (proj2 … (proj1 … prf)) … fetch_spec) *
     2652normalize nodelta #lin_fetch_spec
     2653whd in match eval_state; normalize nodelta >fetch_spec
     2654>m_return_bind whd in match eval_statement_no_pc; normalize nodelta
     2655>m_return_bind whd in match eval_statement_advance; whd in match eval_tailcall;
     2656normalize nodelta @('bind_inversion) #bl #bl_spec
     2657lapply (err_eq_from_io ????? bl_spec) -bl_spec
     2658whd in match set_no_pc; normalize nodelta #bl_spec
     2659cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ?
     2660            bl_spec) * #lin_bl_spec @('bind_inversion)
     2661* #f1 #fn1 cases fn1 normalize nodelta -fn1
     2662[2: #ext_f #_ whd in match eval_external_call; normalize nodelta @('bind_inversion)
     2663    #st @('bind_inversion) #list_val #_ @('bind_inversion) #le #_
     2664    whd in ⊢ (??%% → ?); #ABS destruct(ABS)]
     2665#fn1 #fn1_spec lapply(err_eq_from_io ????? fn1_spec) -fn1_spec #fn1_spec
     2666generalize in match (fetch_function_transf … graph_prog …
     2667      (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in)))
     2668      … fn1_spec : fetch_function … (globalenv_noinit … (linearise … graph_prog)) bl = ?) in ⊢ ?;
     2669      #lin_fn1_spec
     2670whd in match eval_internal_call; normalize nodelta
     2671#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
     2672#st1 #H @('bind_inversion H) -H #dim_s #dim_s_spec
     2673#H @('bind_inversion H) -H #st2 #st2_spec whd in ⊢ (??%% → ??%% → ?);
     2674#EQ1 #EQ2 destruct %
     2675[ @hide_prf | % [@hide_prf]]
     2676[1,2: whd in match joint_classify; normalize nodelta [>fetch_spec | >lin_fetch_spec]
     2677      >m_return_bind normalize nodelta whd in match joint_classify_final;
     2678      normalize nodelta [>bl_spec|>lin_bl_spec] >m_return_bind
     2679      [>fn1_spec|>lin_fn1_spec] %
     2680| cases (setup_call_commute … gss … (proj2 … prf) … st2_spec) #wf_st2 #lin_st2_spec
     2681  cases (allocate_locals_commute … gss … (joint_if_locals … fn1) ? wf_st2)
     2682  #wf_all_st2 #all_st2_spec
     2683  cases(entry_sigma_commute p p' graph_prog sigma good … fn1_spec) #wf_pc
     2684  #pc_spec
     2685  %
     2686  [ @hide_prf %
     2687    [ % [@(proj1 … (proj1 … prf)) | @(wf_pc)]
     2688    | @(wf_all_st2)
     2689    ]
     2690  | %
     2691    [ whd in match joint_tailcall_ident; normalize nodelta
     2692      >lin_fetch_spec in ⊢ (??match % with [ _ ⇒ ? | _ ⇒ ?]?);
     2693      >fetch_spec in ⊢ (???match % with [ _ ⇒ ? | _ ⇒ ?]);
     2694      normalize nodelta >lin_bl_spec >bl_spec >m_return_bind >m_return_bind
     2695      whd in match fetch_internal_function; normalize nodelta
     2696      >fn1_spec >lin_fn1_spec %
     2697    | >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
     2698      normalize nodelta >m_return_bind in ⊢ (??%?);
     2699      >lin_bl_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
     2700      >lin_fn1_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
     2701      normalize nodelta >dim_s_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
     2702      >lin_st2_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
     2703      >all_st2_spec in ⊢ (??%?); whd in ⊢ (??%%); @eq_f @eq_f2 [2: %]
     2704      >pc_spec %
     2705    ]
     2706  ]
     2707]
     2708qed.
     2709   
     2710   
     2711   
    26042712inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
    26052713    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
Note: See TracChangeset for help on using the changeset viewer.