Ignore:
Timestamp:
Mar 1, 2013, 1:05:21 PM (8 years ago)
Author:
sacerdot
Message:

WARNING: this commit breaks things, sorry, Paolo is going to fix compiler.ma
in a minute...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2755 r2756  
    8181    ∀st1,st1',st2.as_execute S1 st1 st1' →
    8282    sim_status_rel st1 st2 →
    83     match as_classify … st1 with
    84     [ None ⇒ True
    85     | Some cl ⇒
    86       match cl with
     83      match as_classify … st1 with
    8784      [ cl_call ⇒ ∀prf.
    8885        (*
     
    170167        sim_status_rel st1' st2' ∧
    171168        label_rel … st1' st2'
    172       ]
    173169    ].
    174170
     
    514510  lapply (sim_execute … H st1_R_st2)
    515511  (* without try it fails... why? *)
    516   try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); normalize nodelta
     512  try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta
    517513  [ #H lapply (H K) -H ] *
    518514  #st2' ** -st2 -st2'
     
    531527| (* tal_base_return *) whd
    532528  lapply (sim_execute … H st1_R_st2)
    533   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); *
     529  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
    534530  #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
    535531  ***** #ncost #J2 #K2
     
    540536| (* tal_base_call *) whd
    541537  lapply (sim_execute … H st1_R_st2)
    542   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?);
     538  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?);
    543539  #H elim (H G) -H
    544540  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     
    569565| (* tal_base_tailcall *) whd
    570566  lapply (sim_execute … H st1_R_st2)
    571   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?);
     567  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?);
    572568  #H elim (H G) -H
    573569  * #st2_pre_call #G2 * #EQcall * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     
    583579| (* tal_step_call *)
    584580  lapply (sim_execute … H st1_R_st2)
    585   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?);
     581  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?);
    586582  #H elim (H G) -H
    587583  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     
    632628| (* step_default *)
    633629  lapply (sim_execute … H st1_R_st2)
    634   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); *
     630  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
    635631  #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
    636632  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid)
     
    873869  [1,2: (* other/jump *)
    874870    lapply (sim_execute … ex G')
    875     try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); normalize nodelta
     871    try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta
    876872    [ #H lapply (H ncost_st1') -H ] *
    877873    #st2' *#taaf ** #ncost #G'' #H''
     
    904900  |3: (* tailcall *)
    905901    lapply (sim_execute … ex G')
    906     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); #H elim (H cl) -H
     902    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
    907903    * #st2_pre_call #cl' * #EQcall * #st2_after_call * #st2'
    908904    * #taa2 * #taa2' ** #ex' #G'' #H''
     
    926922  |4: (* ret *)
    927923    lapply (sim_execute … ex G')
    928     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); *
     924    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
    929925    #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
    930926    ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'}
     
    948944  |5: (* call *)
    949945    lapply (sim_execute … ex G')
    950     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); #H elim (H cl) -H
     946    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
    951947    * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
    952948    * #taa2 * #taa2' ** #ex' #G'' #H''
Note: See TracChangeset for help on using the changeset viewer.