Changeset 1599 for src/Clight/Cexec.ma

Timestamp:

Dec 13, 2011, 1:34:37 AM (8 years ago)

Author:

sacerdot

Message:

Start of merging of stuff into the standard library of Matita.

File:

• src/Clight/Cexec.ma (modified) (9 diffs)

src/Clight/Cexec.ma

@@ -145 +145 @@
 
 definition load_value_of_type' ≝
-λty,m,l. match l with [ pair loc ofs ⇒ load_value_of_type ty m loc ofs ].
+λty,m,l. let 〈loc,ofs〉 ≝ l in load_value_of_type ty m loc ofs.
 
 axiom BadlyTypedTerm : String.
@@ -185 +185 @@
       match ty with
       [ Tpointer r _ ⇒
-        match lo with [ pair loc ofs ⇒ 
+        let 〈loc,ofs〉 ≝ lo in
           match pointer_compat_dec loc r with
           [ inl pc ⇒ OK ? 〈Vptr (mk_pointer r loc pc ofs), tr〉
           | inr _ ⇒ Error ? (msg TypeMismatch)
           ]
-        ]
       | _ ⇒ Error ? (msg BadlyTypedTerm)
       ]
@@ -294 +293 @@
 [ nil ⇒ 〈en, m〉
 | cons h vars ⇒
-  match h with [ pair id ty ⇒
-    match alloc m 0 (sizeof ty) Any with [ pair m1 b1 ⇒
+  let 〈id,ty〉 ≝ h in
+  let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) Any in
       exec_alloc_variables (add ?? en id b1) m1 vars
-]]].
+].
 
 axiom WrongNumberOfParameters : String.
@@ -306 +305 @@
   match params with
   [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? (msg WrongNumberOfParameters) ]
-  | cons idty params' ⇒ match idty with [ pair id ty ⇒
+  | cons idty params' ⇒ let 〈id,ty〉 ≝ idty in
       match vs with
       [ nil ⇒ Error ? (msg WrongNumberOfParameters)
@@ -314 +313 @@
           exec_bind_parameters e m1 params' vl
       ]
-  ] ].
+  ].
 
 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' ≝
 λty,m,l,v.
-match l with [ pair loc ofs ⇒
-  store_value_of_type ty m loc ofs v ].
+let 〈loc,ofs〉 ≝ l in
+  store_value_of_type ty m loc ofs v.
 
 axiom NonsenseState : String.
@@ -465 +464 @@
   | Sgoto lbl ⇒
       match find_label lbl (fn_body f) (call_cont k) with
-      [ Some sk' ⇒ match sk' with [ pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ]
+      [ Some sk' ⇒ let 〈s',k'〉 ≝ sk' in ret ? 〈E0, State f s' k' e m〉
       | None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl]
       ]
@@ -473 +472 @@
   match f0 with
   [ CL_Internal f ⇒ 
-    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ pair e m1 ⇒
+    let 〈e,m1〉 ≝ exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) in
       ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;
       ret ? 〈E0, State f (fn_body f) k e m2〉
-    ]
   | CL_External f argtys retty ⇒ 
       ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);
@@ -488 +486 @@
     [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
     | Some r' ⇒
-      match r' with [ pair l ty ⇒
+      let 〈l,ty〉 ≝ r' in
           ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' ty m l res);
           ret ? 〈E0, (State f Sskip k' e m')〉
-      ]
     ]
   | _ ⇒ Wrong ??? (msg NonsenseState)