Ignore:
Timestamp:
Jan 8, 2013, 5:46:04 PM (7 years ago)
Author:
campbell
Message:

Lots of little changes for cl_tailcall and classifier change.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/abstract.ma

    r2511 r2571  
    201201 *)
    202202
    203 definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge. RTLabs_classify s = cl_call) → RTLabs_ext_state ge → Prop ≝
     203definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? 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. RTLabs_classify s = cl_call → ? with
     207    match s return λs. Some ? (RTLabs_classify s) = Some ? 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. RTLabs_classify s = cl_call) → ident ≝
     228definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → ident ≝
    229229λge,s.
    230230  match s with
    231231  [ mk_Sig s p ⇒
    232     match s return λs':RTLabs_ext_state ge. RTLabs_classify s' = cl_call → ident with
     232    match s return λs':RTLabs_ext_state ge. Some ? (RTLabs_classify s') = Some ? cl_call → ident with
    233233    [ mk_RTLabs_ext_state s' stk mtc0 ⇒
    234       match s' return λs'. Ras_Fn_Match ? s' ? → RTLabs_classify s' = cl_call → ident with
     234      match s' return λs'. Ras_Fn_Match ? s' ? → Some ? (RTLabs_classify s') = Some ? 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
     
    251251] qed.
    252252
     253lemma RTLabs_notail : ∀s.
     254  RTLabs_classify s = cl_tailcall →
     255  False.
     256* [ #f #fs #m whd in ⊢ (??%? → ?); cases (next_instruction f) ]
     257normalize
     258#a try #b try #c try #d try #e try #g try #h try #i try #j destruct
     259qed.
     260
     261(* Roughly corresponding to as_classifier *)
     262lemma RTLabs_notail' : ∀s.
     263  Some ? (RTLabs_classify s) = Some ? cl_tailcall →
     264  False.
     265#s #E @(RTLabs_notail … s)
     266generalize in match (RTLabs_classify s) in E ⊢ %;
     267#c #E' destruct %
     268qed.
    253269
    254270definition RTLabs_status : genv → abstract_status ≝
     
    259275    RTLabs_deqset
    260276    (RTLabs_ext_state_to_pc ge)
    261     RTLabs_classify
     277    (λs. Some ? (RTLabs_classify s))
    262278    (RTLabs_pc_to_cost_label ge)
    263279    (RTLabs_after_return ge)
    264280    (λs. RTLabs_is_final s ≠ None ?)
    265     (RTLabs_call_ident ge).
    266 
    267 
     281    (RTLabs_call_ident ge)
     282    (λs. ⊥).
     283(* No tailcalls here for now. *)
     284cases s @RTLabs_notail'
     285qed.
    268286
    269287(* Allow us to move between the different notions of when a state is cost
Note: See TracChangeset for help on using the changeset viewer.