Ignore:
Timestamp:
Mar 7, 2013, 1:29:31 PM (7 years ago)
Author:
piccolo
Message:

Partial commit not yet finished

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrOK.ma

    r2785 r2801  
    223223  inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_ cases(stmt_at_spec … EQstmt1)
    224224  #labels * #registers ** #_ #EQregisters #_ -labels >EQregisters whd
    225   cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers))) ?
    226          (get_used_registers_from_seq … (functs ERTL) stmt))
    227   [3: #a cases(¬a∈registers) // |1: #H assumption] #H @⊥
     225  check excluded_middle_list
     226  cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers)))
     227         (get_used_registers_from_seq … (functs ERTL) stmt) ?)
     228  [3: #a #_ cases(¬a∈registers) // |1: #H assumption] #H @⊥
    228229  cases(Exists_All … H (regs_are_in_univers … (pi2 ?? fn) … EQstmt))
    229230  #reg ** #H1 #H2 @H1 -H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters
     
    628629 =return st2'.
    629630#prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn * [#c_id | #c_ptr]
    630 #args #dest #nxt #EQfetch lapply EQfetch >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
     631#args #dest #nxt #EQfetch whd in match eval_state; normalize nodelta >EQfetch
     632>m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     633whd in match eval_statement_advance; whd in match eval_call; normalize nodelta
     634>(fetch_stmt_ok_sigma_state_ok … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
     635>(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) #H @('bind_inversion H) -H
     636#c_bl whd in match set_no_pc; normalize nodelta #H lapply(err_eq_from_io ????? H) -H
     637#EQc_bl cases(block_of_call_ok ??????? EQc_bl) #c_bl' * #EQc_bl' #EQ destruct(EQ)
     638#H @('bind_inversion H) -H * #f1 * [1,3: #fn1 |*: #ext_f] #H
     639lapply(err_eq_from_io ????? H) -H  #EQfn1 normalize nodelta
     640[3,4: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
     641      #H @('bind_inversion H) -H #list_val #_ #H @('bind_inversion H) -H #x
     642      #_ #H @('bind_inversion H) -H #y whd in match do_io; normalize nodelta
     643      whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #H lapply(err_eq_from_io ????? H) -H
     644#H @('bind_inversion H) -H #st1'' >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
     645>(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) whd in match kind_of_call;
     646normalize nodelta change with (ertl_save_frame ? it ?) in ⊢ (??%? → ?);
     647[2: @ID |4: @PTR] #EQst1''  #H @('bind_inversion H) -H #st1'''
     648whd in match eval_internal_call; normalize nodelta #H @('bind_inversion H) -H
     649#s_size #H lapply(opt_eq_from_res ???? H) -H
     650change with (stack_size ?) in ⊢ (??%? → ?); #EQs_size whd in ⊢ (??%? → ?);
     651whd in ⊢ (???% → ??%% → ?); #EQ #EQ1 destruct(EQ EQ1)
     652lapply EQfetch >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (% → ?);
    631653#EQfetch' lapply(fetch_statement_inv … EQfetch') * #EQfn normalize nodelta #EQstmt
    632654cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
    633655#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
    634 [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #pp_labs
    635 #_ #fresh_labs #fresh_regs #_ #_ #H cases(H … EQstmt) -H #labels * #registers
     656[2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #_
     657#_ #_ #_ #_ #_ #H cases(H … EQstmt) -H #labels * #registers
    636658** #EQlabels #EQregisters normalize nodelta >if_merge_right [2,4: %]
    637 whd in match translate_step;
    638 normalize nodelta whd in ⊢ (% → ?); * #bl * whd in ⊢ (% → ?);
     659whd in match translate_step; normalize nodelta * #bl *
    639660cases registers in EQregisters; -registers normalize nodelta
    640661[2,3: [ #x #y] #_ *|4: #r #tl] #EQregisters
    641662[ whd in ⊢ (% → ?); cases tl in EQregisters; -tl [2: #x #y #_ *] normalize nodelta
    642 #EQregisters] #EQ destruct(EQ) whd in ⊢ (% → ?); *
    643 #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 whd in ⊢ (% → ?);
     663#EQregisters | whd in ⊢ (% → ?);] #EQ destruct(EQ)
     664* #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 #m_fetch_pre whd in ⊢ (% → ?);
     665* #nxt1 * #EQcall change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
     666whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) cases(pre_l) in m_fetch_pre EQmid1;
     667[* #x * #y ** #ABS destruct(ABS)
     668|4: #lab #tl * #ABS destruct(ABS)
     669| #l1 #tl #m_fetch_pre whd in ⊢ (???% → ?); #EQ destruct(EQ)
     670| * #_ #EQ destruct(EQ) whd in ⊢ (???% → ?); #EQ destruct(EQ)
     671]
     672%
     673[1,3: @hide_prf whd in ⊢ (??%?); >EQfetch %]
     674cases(ertl_save_frame_ok prog f_lbls f_regs ?
     675  (added_registers ERTL (prog_var_names … prog) fn (f_regs (pc_block (pc … st2))))
     676  ? st1''' ?)
     677[2: @PTR
     678|3,7: [ %{(mk_state_pc ? (st_no_pc … st2)
     679                     (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)
     680                     (last_pop … st2))}
     681      |%{(st2)}
     682      ] @hide_prf whd in match sigma_pc_opt; normalize nodelta @if_elim
     683      [1,3: @eqZb_elim [2,4: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn;
     684           [1,3: #EQ destruct(EQ) |*: assumption]]
     685      #_ [>point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels)
     686         | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels)
     687         ] >m_return_bind % whd in ⊢ (??%? → ?); #ABS destruct(ABS)
     688|6: @ID
     689|4,8: [change with (pc_block (pc … st2)) in match (pc_block ?);
     690       >EQfn in ⊢ (??(???match % with [_ ⇒ ?| _ ⇒ ?])?);
     691      |>EQfn in ⊢ (??(???match % with [_ ⇒ ?| _ ⇒ ?])?);
     692      ] normalize nodelta whd in match (st_no_pc ??);
     693      whd in match sigma_stored_pc in ⊢ (??(???(???%?))?);
     694      whd in match sigma_pc_opt; normalize nodelta @if_elim
     695     [1,3: @eqZb_elim [2,4: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn;
     696           [1,3: #EQ destruct(EQ) |*: assumption]]
     697      #_ [>point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels)
     698         | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels)
     699         ] >m_return_bind normalize nodelta
     700         change with (pc_block (pc … st2)) in match (pc_block ?);
     701         >pc_of_point_of_pc assumption
     702] #st_no_pc_after_call normalize nodelta *
     703[ #H @('bind_inversion H) -H #st_no_pc_pre_call #EQst_no_pc_pre_call
     704  whd in match set_no_pc; normalize nodelta]
     705#EQst_no_pc_after_call #EQ destruct(EQ)
     706[ %{(mk_state_pc ? st_no_pc_pre_call
     707                   (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)
     708                   (last_pop … st2))}
     709| %{st2}
     710]
     711%
     712[1,3: @hide_prf whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
     713      >EQcalling' >m_return_bind [>point_of_pc_of_point ] >EQcall >m_return_bind %]
     714%
     715[1,3: %
     716  [1,3: whd in ⊢ (??%%); whd in match fetch_statement in ⊢ (??%?);
     717        normalize nodelta >EQcalling' in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
     718        >m_return_bind in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
     719       [ >point_of_pc_of_point in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);]
     720       >EQcall in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); normalize nodelta
     721       >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]));
     722       >EQfetch' in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); %
     723  |*:  whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
     724      @if_elim change with (pc_block(pc … st2)) in match (pc_block ?);
     725      [1,3: @eqZb_elim [2,4: #_ *] #EQbl #_
     726      >fetch_internal_function_no_minus_one in EQcalling'; [2,4: assumption]
     727      whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #_
     728      [ >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels)
     729      | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels)
     730      ]
     731      >m_return_bind >pc_of_point_of_pc %
     732  ]
     733|4: %{(taa_base …)}
     734| lapply(produce_trace_any_any_free (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
     735           st2 ?????
     736           (mk_state_pc ? st_no_pc_pre_call
     737                   (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)
     738                   (last_pop … st2)) EQcalling' m_fetch_pre ?)
     739  [2: #taaf inversion(taaf)
     740      [ #s #EQ #EQ1 @⊥ destruct(EQ EQ1) cases s in EQ1 EQst_no_pc_pre_call;
     741        * #fms #is #bb #regs #m #y #z #EQ #H @('bind_inversion H) -H #a1
     742        #H @('bind_inversion H) -H #is1 whd in ⊢ (??%% → ?); cases is in EQ;
     743        [2: #bv1 |3: #bv1 #bv2] #EQ whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1)
     744        whd in ⊢ (??%% → ??%% → ?); #EQ1 destruct(EQ1) normalize nodelta
     745        whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) destruct(EQ)
     746      |3: #s1 #s2 #s3 #taa #H1 #H2 #H3 #EQ #EQ1 @⊥ destruct(EQ EQ1)
     747          lapply H3 -H3 whd in ⊢ (% → ?); whd in match (as_label ??);
     748          whd in match fetch_statement; normalize nodelta
     749          whd in match (as_pc_of ??); >EQcalling' >m_return_bind
     750          whd in match point_of_pc; normalize nodelta; >point_of_offset_of_point
     751          >EQcall normalize nodelta whd in match cost_label_of_stmt;
     752          normalize nodelta * #H @H %
     753      ]
     754      #s1 #s2 #s3 #taa #H1 #H2 #EQst2 #EQs3 #_ <EQst2 in taa; <EQs3 in H1; #H1 #taa
     755       %{(taa_append_taa … taa (taa_step … H1 … (taa_base …)))}
     756                 xxxxxxxxxxxxxxxxxxxx
     757|3,7: whd in match sigma_pc_opt; normalize nodelta @if_elim
     758      [1,3: @eqZb_elim [2,4: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn;
     759           [1,3: #EQ destruct(EQ) |*: assumption]]
     760      #_ [
     761
     762
     763whd in ⊢ (% → ?);
    644764[ * #mid * #resg ** #EQ destruct(EQ) whd in ⊢ (% → ?);
    645765  * #nxt1 * #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
     
    653773whd in ⊢ (% → ?); * #nxt1 * #EQcall #EQ destruct(EQ) whd in ⊢ (% → ?);
    654774* #EQ destruct(EQ) change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    655  whd in match eval_state; normalize nodelta >EQfetch
    656 >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
    657 whd in match eval_statement_advance; whd in match eval_call; normalize nodelta
    658 >(fetch_stmt_ok_sigma_state_ok … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
    659 >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) #H @('bind_inversion H) -H
    660 #c_bl whd in match set_no_pc; normalize nodelta #H lapply(err_eq_from_io ????? H) -H
    661 #EQc_bl cases(block_of_call_ok ??????? EQc_bl) #c_bl' * #EQc_bl' #EQ destruct(EQ)
    662 #H @('bind_inversion H) -H * #f1 * [1,3: #fn1 |*: #ext_f] #EQfn1 normalize nodelta
    663 [3,4: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
    664       #H @('bind_inversion H) -H #list_val #_ #H @('bind_inversion H) -H #x
    665       #_ #H @('bind_inversion H) -H #y whd in match do_io; normalize nodelta
    666       whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #H lapply(err_eq_from_io ????? H) -H
    667 #H @('bind_inversion H) -H #st1'' >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
    668 >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) whd in match kind_of_call;
    669 normalize nodelta change with (ertl_save_frame ? it ?) in ⊢ (??%? → ?);
    670 [2: @PTR |4: @ID] #EQst1'' #H @('bind_inversion H) -H #st1'''
    671 whd in match eval_internal_call; normalize nodelta #H @('bind_inversion H) -H
    672 #s_size #H lapply(opt_eq_from_res ???? H) -H
    673 change with (stack_size ?) in ⊢ (??%? → ?); #EQs_size whd in ⊢ (??%? → ?);
    674 whd in ⊢ (???% → ?); #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ destruct(EQ) %
    675 [1,3: @hide_prf whd in ⊢ (??%?); >EQfetch %]
     775
     776
     777
     778
     779
     780
     781
     782
     783
     784
     785 
    676786[ letin pairpc ≝ (beval_pair_of_pc (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1))
    677787  letin st2_pre ≝ (mk_state_pc ?
     
    844954
    845955
     956
     957
     958
     959
     960
     961
    846962inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
    847963    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
Note: See TracChangeset for help on using the changeset viewer.