Changeset 2423


Ignore:
Timestamp:
Oct 30, 2012, 5:23:44 PM (7 years ago)
Author:
tranquil
Message:

as_classifier predicate → as_classify function
as_call predicate from StructuredTraces_jaap → as_call_ident function

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r2417 r2423  
    1414
    1515record abstract_status : Type[1] ≝
    16 {
    17     as_status :> Type[0]
     16  { as_status :> Type[0]
    1817  ; as_execute : as_status → as_status → Prop
    1918  ; as_pc : DeqSet
    2019  ; as_pc_of : as_status → as_pc
    21   ; as_classifier : as_status → status_class → Prop
     20  ; as_classify : as_status → status_class
    2221  ; as_label_of_pc : as_pc → option costlabel
    23   ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
     22  ; as_after_return : (Σs:as_status. as_classify s = cl_call) → as_status → Prop
    2423  ; as_final: as_status → Prop
    25 }.
     24  ; as_call_ident : (Σs:as_status.as_classify s = cl_call) → ident
     25  }.
     26
     27definition as_classifier ≝ λS,s,cl.as_classify S s = cl.
     28definition as_call ≝ λS,s,f.as_call_ident S s = f.
    2629
    2730definition as_label ≝ λS : abstract_status. λs : S. as_label_of_pc ? (as_pc_of ? s).
     
    3639#S #s whd in match (as_costed S s);
    3740cases (as_label S s) [ %2 % * /2/ | #c %1 % #E destruct ]
    38 qed. 
     41qed.
    3942
    4043definition as_label_safe : ∀a_s : abstract_status.
     
    517520    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
    518521      (tal_base_return ? st2mid st2' H G)
    519   | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒
     522  | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒
    520523    fl2 = doesnt_end_with_ret ∧
    521     ∃st2mid.∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
     524    ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
     525    ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
    522526    (* we must allow a tal_base_call to be similar to a call followed
    523527      by a collapsable trace (trace_any_any followed by a base_not_return;
    524528      we cannot use trace_any_any as it disallows labels in the end as soon
    525529      as it is non-empty) *)
    526     (∃G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
     530    (∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
    527531      tal2 ≃ taa @ (tal_base_call … H G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨
    528     ∃st2mid'',G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
     532    ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
    529533    ∃tl2 : trace_any_label … doesnt_end_with_ret st2mid'' st2'.
    530534      tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
    531535      tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2
    532   | tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒
    533     ∃st2mid.∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
    534     (fl2 = doesnt_end_with_ret ∧ ∃G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
     536  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒
     537    ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
     538    ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
     539    (fl2 = doesnt_end_with_ret ∧ ∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
    535540      tal2 ≃ taa @ tal_base_call … H G K tlr2 L ∧
    536541      tal_collapsable … tl1 ∧ tlr_rel … tlr1 tlr2) ∨
    537     ∃st2mid'',G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
     542    ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
    538543    ∃tl2 : trace_any_label ? fl2 st2mid'' st2'.
    539544      tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
     
    569574-fl1 -s1 -s1'
    570575[1,2,3: -tal_rel_eq_fl #tal2 * //
    571 | #tal2 * #s2_mid * #taa2 * #s2' *#H2 *
    572   [ * #EQ1 *#G2 *#K2 *#tlr2 *#L2 ** #_ #coll #_ >(tal_collapsable_eq_fl … coll) //
    573   | * #s2_mid' *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #_ #step #_
     576| #tal2 * #s2_mid * #G2 * #call * #taa2 * #s2' *#H2 *
     577  [ * #EQ1 *#K2 *#tlr2 *#L2 ** #_ #coll #_ >(tal_collapsable_eq_fl … coll) //
     578  | * #s2_mid' *#K2 *#tlr2 *#L2 *#tl2 ** #_ #step #_
    574579     @(tal_rel_eq_fl … step)
    575580  ]
     
    757762|2,3,4,5,6:
    758763  [1,2,3: * #EQ destruct(EQ)]
    759   [1,2,3,4: * #st_mid * #taa
     764  [1,2,3,4: * #st_mid [1,2:|*: * #G' * #call ] * #taa
    760765    [ *#H' *#G' *#K' #EQ
    761766    | *#H' *#G' #EQ
    762     | *#st_mid' *#H' * [|*#st2_mid''] *#G' *#K' *#tlr2 *#L'
     767    | *#st_mid' *#H' * [|*#st2_mid''] *#K' *#tlr2 *#L'
    763768      [|*#tl2 *] * #EQ #H_tlr [| #H_tl]
    764769    | *#st_fun *#H' *
    765       [*#fl_EQ destruct(fl_EQ) |* #st2_mid ] *#G' *#K' *#tlr2 *#L'
     770      [*#fl_EQ destruct(fl_EQ) |* #st2_mid ] *#K' *#tlr2 *#L'
    766771      [| *#tl2] ** #EQ #H_tl #H_tlr
    767772    ] >EQ >taa_append_tal_same_flatten
Note: See TracChangeset for help on using the changeset viewer.