Changeset 2756 for src/common


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

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

Location:
src/common
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/Measurable.ma

    r2727 r2756  
    2424definition trace_is_label_to_return : ∀C. list (cs_state … C × trace) → Prop ≝
    2525λC,x. ∃tr1,s1,x',tr2,s2. x = 〈s1,tr1〉::(x'@[〈s2,tr2〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return.
    26 
    27 (* For intensional_event; should separate out definition *)
    28 include "common/StatusSimulation.ma".
    2926
    3027definition intensional_event_of_event : event → list intensional_event ≝
  • 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''
  • src/common/StructuredTraces.ma

    r2755 r2756  
    1  include "basics/types.ma".
    21include "basics/bool.ma".
    32include "basics/jmeq.ma".
     
    54include "utilities/option.ma".
    65include "basics/lists/listb.ma".
    7 include "ASM/Util.ma".
    86include "common/IO.ma".
    97include "utilities/hide.ma".
     8include "ASM/Util.ma".
    109
    1110inductive status_class: Type[0] ≝
     
    1918  { as_status :> Type[0]
    2019  ; as_eval : as_status → IO io_out io_in as_status
     20  ; as_init : res as_status
    2121  ; as_pc : DeqSet
    2222  ; as_pc_of : as_status → as_pc
    23   ; as_classify : as_status → option status_class
     23  ; as_classify : as_status → status_class
    2424  ; as_label_of_pc : as_pc → option costlabel
    25   ; as_after_return : (Σs:as_status. as_classify s = Some ? cl_call) → as_status → Prop
     25  ; as_after_return : (Σs:as_status. as_classify s = cl_call) → as_status → Prop
    2626  ; as_result: as_status → option int
    27   ; as_call_ident : (Σs:as_status.as_classify s = Some ? cl_call) → ident
    28   ; as_tailcall_ident : (Σs:as_status.as_classify s = Some ? cl_tailcall) → ident
     27  ; as_call_ident : (Σs:as_status.as_classify s = cl_call) → ident
     28  ; as_tailcall_ident : (Σs:as_status.as_classify s = cl_tailcall) → ident
    2929  }.
    3030
    31 definition as_classifier ≝ λS,s,cl.as_classify S s = Some ? cl.
     31definition as_classifier ≝ λS,s,cl.as_classify S s = cl.
    3232definition as_call ≝ λS,s,f.as_call_ident S s = f.
    3333definition as_final ≝ λS,s.as_result S s ≠ None ?.
Note: See TracChangeset for help on using the changeset viewer.