Changeset 2208 for src/joint/semanticsUtils_paolo.ma

Timestamp:

Jul 18, 2012, 1:26:43 PM (9 years ago)

Author:

tranquil

Message:

• moving some code around
• changed immediates to hold beval in general, not only bytes
• fixed RTLabsToRTL after redefinitions in front end

File:

• src/joint/semanticsUtils_paolo.ma (modified) (1 diff)

src/joint/semanticsUtils_paolo.ma

@@ -14 +14 @@
 (*** Store/retrieve on hardware registers ***)
 
-definition init_hw_register_env: address → hw_register_env ≝
- λaddr.
-  let 〈dpl,dph〉 ≝ addr in
+definition init_hw_register_env: xpointer → hw_register_env ≝
+ λsp.
+  let 〈dpl,dph〉 ≝
+    match beval_pair_of_pointer sp return λx.beval_pair_of_pointer sp = x → ? with
+    [ OK p ⇒ λ_.p
+    | _ ⇒ λprf.⊥
+    ] (refl …) in
   let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
    hwreg_store RegisterDPL dpl env.
+@hide_prf
+normalize in prf; destruct(prf)
+qed.
 
 (******************************** GRAPHS **************************************)