Changeset 1713 for src/RTLabs/semantics.ma
 Timestamp:
 Feb 21, 2012, 11:58:12 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/semantics.ma
r1681 r1713 44 44 ∀ stk : list frame. 45 45 ∀ m : mem. 46 state. 47 48 definition mem_of_state : state → mem ≝ 49 λs. match s with [ State _ _ m ⇒ m  Callstate _ _ _ _ m ⇒ m  Returnstate _ _ _ m ⇒ m ]. 46 state 47  Finalstate : 48 ∀ r : int. 49 state 50 . 50 51 51 52 definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m. … … 183 184  Returnstate v dst fs m ⇒ 184 185 match fs with 185 [ nil ⇒ Error ? (msg FinalState) (* Already in final state *) 186 [ nil ⇒ 187 match v with 188 [ Some v' ⇒ 189 match v' with 190 [ Vint sz r ⇒ match sz return λsz. bvint sz → monad Res ? with 191 [ I32 ⇒ λr. return 〈E0, Finalstate r〉 192  _ ⇒ λ_. Error ? (msg ReturnMismatch) 193 ] r 194  _ ⇒ Error ? (msg ReturnMismatch) 195 ] 196  _ ⇒ Error ? (msg ReturnMismatch) 197 ] 186 198  cons f fs' ⇒ 187 199 ! locals ← match dst with … … 192 204 return 〈E0, State (mk_frame (func f) locals (next f) ? (sp f) (retdst f)) fs' m〉 193 205 ] 206  Finalstate r ⇒ Error ? (msg FinalState) (* Already in final state *) 194 207 ]. try @(next_ok f) try @lookup_lookup_present try @H 195 208 [ cases b [ @(proj1 ?? H)  @(proj2 ?? H) ] … … 200 213 definition RTLabs_is_final : state → option int ≝ 201 214 λs. match s with 202 [ State _ _ _ ⇒ None ? 203  Callstate _ _ _ _ _ ⇒ None ? 204  Returnstate v _ fs _ ⇒ 205 match fs with [ nil ⇒ 206 match v with [ Some v' ⇒ 207 match v' with 208 [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?) 209  _ ⇒ None ? ] 210  None ⇒ None ? ] 211  cons _ _ ⇒ None ? ] 215 [ Finalstate r ⇒ Some ? r 216  _ ⇒ None ? 212 217 ]. 213 218 … … 251 256  to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m') 252 257  from_ret : ∀ge,f,fs,rtv,dst,f',m. frame_rel f f' → state_rel ge (Returnstate rtv dst (f::fs) m) (State f' fs m) 258  finish : ∀ge,r,dst,m. state_rel ge (Returnstate (Some ? (Vint I32 r)) dst [ ] m) (Finalstate r) 253 259 . 254 260 … … 315 321 [ @bind_value #loc #Eloc #E whd in E:(??%?); destruct 316 322 %5 cases f #func #locals #next #next_ok #sp #retdst % 317  #E destruct323  cases v [ normalize #E destruct  * [ 2: * #r normalize #E destruct //  *: normalize #a try #b destruct ] ] 318 324 ] 319 ] qed. 320 325  #r #tr #s' normalize #E destruct 326 ] qed. 327
Note: See TracChangeset
for help on using the changeset viewer.