Changeset 2288 for src/RTLabs/Traces.ma


Ignore:
Timestamp:
Aug 2, 2012, 5:04:36 PM (8 years ago)
Author:
campbell
Message:

Remove jumptables from RTLabs. :(

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2226 r2288  
    102102    match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
    103103    [ St_cond _ _ _ ⇒ cl_jump
    104     | St_jumptable _ _ ⇒ cl_jump
     104(*    | St_jumptable _ _ ⇒ cl_jump*)
    105105    | _ ⇒ cl_other
    106106    ]
     
    666666  ∃f,fs,m. s = State f fs m ∧
    667667  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
    668   (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
     668  (∃r,l1,l2. stmt = St_cond r l1 l2) (*∨ (∃r,ls. stmt = St_jumptable r ls)*).
    669669*
    670670[ #f #fs #m #E
     
    673673  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
    674674    try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct)
    675     [ %1 %{A} %{B} %{C} @refl
    676     | %2 %{A} %{B} @refl
    677     ]
     675    (*[ %1*) %{A} %{B} %{C} @refl
     676(*    | %2 %{A} %{B} @refl
     677    ]*)
    678678  ]
    679679| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
     
    689689#ge #s #tr #s' #EV #H #CL
    690690cases (rtlabs_jump_inv s CL)
    691 #fr * #fs * #m * #Es *
    692 [ * #r * #l1 * #l2 #Estmt
     691#fr * #fs * #m * #Es(* *
     692[*) * #r * #l1 * #l2 #Estmt
    693693  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
    694694  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
     
    701701  whd in ⊢ (% → ?);
    702702  * #H1 #H2 [ @H1 | @H2 ]
    703 | * #r * #ls #Estmt
     703(*| * #r * #ls #Estmt
    704704  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
    705705  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
     
    719719    #H1 #H2 @H2
    720720  ]
    721 ] qed.
     721]*) qed.
    722722
    723723lemma rtlabs_call_inv : ∀s.
     
    13441344| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    13451345| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] //
    1346 | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
     1346(*| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
    13471347  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #E normalize in E; destruct | #p #E normalize in E; destruct ]
    13481348  whd in ⊢ (??%? → ?);
     
    13511351  [ #e #E normalize in E; destruct
    13521352  | #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El)
    1353   ]
     1353  ]*)
    13541354| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl
    13551355] qed.
     
    14231423| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
    14241424| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
    1425 | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
     1425(*| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
    14261426  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #E normalize in E; destruct | #p #E normalize in E; destruct ]
    14271427  whd in ⊢ (??%? → ?);
     
    14301430  [ #e #E normalize in E; destruct
    14311431  | #l #El whd in ⊢ (??%? → ?); #E destruct @refl
    1432   ]
     1432  ]*)
    14331433| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl
    14341434] qed.
Note: See TracChangeset for help on using the changeset viewer.