Ignore:
Timestamp:
Nov 28, 2012, 12:52:12 PM (7 years ago)
Author:
campbell
Message:

Separate out the RTLabs abstract status record from the proofs about
structured traces. Tidy up "next instruction" references from
the semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r2475 r2499  
    4949definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m.
    5050
     51definition next_instruction : frame → statement ≝
     52λf. lookup_present ?? (f_graph (func f)) (next f) (next_ok f).
     53
    5154definition init_locals : list (register × typ) → register_env val ≝
    5255foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??).
     
    8992match st return λ_. IO ??? with
    9093[ State f fs m ⇒
    91   let s ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
     94  let s ≝ next_instruction f in
    9295  match s return λs. labels_present ? s → IO ??? with
    9396  [ St_skip l ⇒ λH. return 〈E0, build_state f fs m l ?〉
     
    271274  whd in ⊢ (??%? → ?);
    272275  generalize in ⊢ (??(?%)? → ?);
    273   cases (lookup_present LabelTag statement (f_graph func) next next_ok)
     276  cases (next_instruction ?)
    274277  [ #l #LP whd in ⊢ (??%? → ?); #E destruct % %
    275278  | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % %
     
    314317[ * #func #locals #next #nok #sp #dst #fs #m #tr #fd #args #dst' #fs' #m'
    315318  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
    316   cases (lookup_present … nok)
     319  cases (next_instruction ?)
    317320  (* Function call cases. *)
    318321  [ 8,9: #x #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd' #Efd @bind_ok #vs #Evs #E normalize in E; destruct
Note: See TracChangeset for help on using the changeset viewer.