Changeset 2499 for src/RTLabs/semantics.ma

Timestamp:

Nov 28, 2012, 12:52:12 PM (8 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:

• src/RTLabs/semantics.ma (modified) (4 diffs)

src/RTLabs/semantics.ma

@@ -49 +49 @@
 definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m.
 
+definition next_instruction : frame → statement ≝
+λf. lookup_present ?? (f_graph (func f)) (next f) (next_ok f).
+
 definition init_locals : list (register × typ) → register_env val ≝
 foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??).
@@ -89 +92 @@
 match st return λ_. IO ??? with
 [ State f fs m ⇒
-  let s ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in 
+  let s ≝ next_instruction f in 
   match s return λs. labels_present ? s → IO ??? with
   [ St_skip l ⇒ λH. return 〈E0, build_state f fs m l ?〉
@@ -271 +274 @@
   whd in ⊢ (??%? → ?);
   generalize in ⊢ (??(?%)? → ?);
-  cases (lookup_present LabelTag statement (f_graph func) next next_ok)
+  cases (next_instruction ?)
   [ #l #LP whd in ⊢ (??%? → ?); #E destruct % %
   | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % %
@@ -314 +317 @@
 [ * #func #locals #next #nok #sp #dst #fs #m #tr #fd #args #dst' #fs' #m'
   whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
-  cases (lookup_present … nok)
+  cases (next_instruction ?)
   (* Function call cases. *)
   [ 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