Ignore:
Timestamp:
Mar 1, 2013, 7:13:49 PM (7 years ago)
Author:
tranquil
Message:

many things are still broken, but there is a partial backtrack on Structured traces's execute

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_abstract.ma

    r2724 r2757  
    201201 *)
    202202
    203 definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → RTLabs_ext_state ge → Prop ≝
     203definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge.RTLabs_classify s = cl_call) → RTLabs_ext_state ge → Prop ≝
    204204λge,s,s'.
    205205  match s with
    206206  [ mk_Sig s p ⇒
    207     match s return λs. Some ? (RTLabs_classify s) = Some ? cl_call → ? with
     207    match s return λs. RTLabs_classify s = cl_call → ? with
    208208    [ Callstate _ fd args dst stk m ⇒
    209209      λ_. match s' with
     
    219219   ] p
    220220 ].
    221 [ whd in H:(??(??%)?);
     221[ whd in H:(??%?);
    222222  cases (next_instruction f) in H;
    223223  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
     
    226226] qed.
    227227
    228 definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → ident ≝
     228definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge.RTLabs_classify s = cl_call) → ident ≝
    229229λge,s.
    230230  match s with
    231231  [ mk_Sig s p ⇒
    232     match s return λs':RTLabs_ext_state ge. Some ? (RTLabs_classify s') = Some ? cl_call → ident with
     232    match s return λs':RTLabs_ext_state ge. RTLabs_classify s' = cl_call → ident with
    233233    [ mk_RTLabs_ext_state s' stk mtc0 ⇒
    234       match s' return λs'. Ras_Fn_Match ? s' ? → Some ? (RTLabs_classify s') = Some ? cl_call → ident with
     234      match s' return λs'. Ras_Fn_Match ? s' ? → RTLabs_classify s' = cl_call → ident with
    235235      [ Callstate _ fd _ _ _ _ ⇒
    236236        match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with
     
    243243    ] p
    244244  ].
    245 [ whd in H:(??(??%)?);
     245[ whd in H:(??%?);
    246246  cases (next_instruction f) in H;
    247247  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
     
    261261(* Roughly corresponding to as_classifier *)
    262262lemma RTLabs_notail' : ∀s.
    263   Some ? (RTLabs_classify s) = Some ? cl_tailcall →
     263  RTLabs_classify s = cl_tailcall →
    264264  False.
    265265#s #E @(RTLabs_notail … s)
     
    275275    RTLabs_deqset
    276276    (RTLabs_ext_state_to_pc ge)
    277     (λs. Some ? (RTLabs_classify s))
     277    (RTLabs_classify)
    278278    (RTLabs_pc_to_cost_label ge)
    279279    (RTLabs_after_return ge)
    280     (λs. RTLabs_is_final s ≠ None ?)
     280    (RTLabs_is_final)
    281281    (RTLabs_call_ident ge)
    282282    (λs. ⊥).
Note: See TracChangeset for help on using the changeset viewer.