Changeset 1599 for src/Clight/Cexec.ma
- Timestamp:
- Dec 13, 2011, 1:34:37 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/Cexec.ma
r1545 r1599 145 145 146 146 definition load_value_of_type' ≝ 147 λty,m,l. match l with [ pair loc ofs ⇒ load_value_of_type ty m loc ofs ].147 λty,m,l. let 〈loc,ofs〉 ≝ l in load_value_of_type ty m loc ofs. 148 148 149 149 axiom BadlyTypedTerm : String. … … 185 185 match ty with 186 186 [ Tpointer r _ ⇒ 187 match lo with [ pair loc ofs ⇒187 let 〈loc,ofs〉 ≝ lo in 188 188 match pointer_compat_dec loc r with 189 189 [ inl pc ⇒ OK ? 〈Vptr (mk_pointer r loc pc ofs), tr〉 190 190 | inr _ ⇒ Error ? (msg TypeMismatch) 191 191 ] 192 ]193 192 | _ ⇒ Error ? (msg BadlyTypedTerm) 194 193 ] … … 294 293 [ nil ⇒ 〈en, m〉 295 294 | cons h vars ⇒ 296 match h with [ pair id ty ⇒297 match alloc m 0 (sizeof ty) Any with [ pair m1 b1 ⇒295 let 〈id,ty〉 ≝ h in 296 let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) Any in 298 297 exec_alloc_variables (add ?? en id b1) m1 vars 299 ] ]].298 ]. 300 299 301 300 axiom WrongNumberOfParameters : String. … … 306 305 match params with 307 306 [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? (msg WrongNumberOfParameters) ] 308 | cons idty params' ⇒ match idty with [ pair id ty ⇒307 | cons idty params' ⇒ let 〈id,ty〉 ≝ idty in 309 308 match vs with 310 309 [ nil ⇒ Error ? (msg WrongNumberOfParameters) … … 314 313 exec_bind_parameters e m1 params' vl 315 314 ] 316 ] ].315 ]. 317 316 318 317 let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝ … … 338 337 definition store_value_of_type' ≝ 339 338 λty,m,l,v. 340 match l with [ pair loc ofs ⇒ 341 store_value_of_type ty m loc ofs v ].339 let 〈loc,ofs〉 ≝ l in 340 store_value_of_type ty m loc ofs v. 342 341 343 342 axiom NonsenseState : String. … … 465 464 | Sgoto lbl ⇒ 466 465 match find_label lbl (fn_body f) (call_cont k) with 467 [ Some sk' ⇒ match sk' with [ pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ]466 [ Some sk' ⇒ let 〈s',k'〉 ≝ sk' in ret ? 〈E0, State f s' k' e m〉 468 467 | None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl] 469 468 ] … … 473 472 match f0 with 474 473 [ CL_Internal f ⇒ 475 match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ pair e m1 ⇒474 let 〈e,m1〉 ≝ exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) in 476 475 ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs; 477 476 ret ? 〈E0, State f (fn_body f) k e m2〉 478 ]479 477 | CL_External f argtys retty ⇒ 480 478 ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys); … … 488 486 [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉 489 487 | Some r' ⇒ 490 match r' with [ pair l ty ⇒488 let 〈l,ty〉 ≝ r' in 491 489 ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' ty m l res); 492 490 ret ? 〈E0, (State f Sskip k' e m')〉 493 ]494 491 ] 495 492 | _ ⇒ Wrong ??? (msg NonsenseState)
Note: See TracChangeset
for help on using the changeset viewer.