Changeset 2927 for src/common

Timestamp:

Mar 21, 2013, 5:17:23 PM (7 years ago)

Author:

tranquil

Message:

stupid bug in bool_of_beval

File:

• src/common/ByteValues.ma (modified) (2 diffs)

src/common/ByteValues.ma

@@ -233 +233 @@
                                                    completed *)
   | BVpc _ _ ⇒ Error … [MSG ValueNotABoolean] (* we should never test on a pc *)
-  | BVByte b ⇒ OK … (eq_bv … (zero …) b)
+  | BVByte b ⇒ OK … (¬eq_bv … (zero …) b)
   | BVnull _ ⇒  OK … false
   | _ ⇒ OK ? true
@@ -257 +257 @@
     | _ ⇒ Error ? [MSG NotAnInt32Val] ].
 
+inductive add_or_sub : Type[0] ≝
+| do_add : add_or_sub
+| do_sub : add_or_sub.
+
+definition eq_add_or_sub : add_or_sub → add_or_sub → bool ≝
+λx,y.match x with
+[ do_add ⇒ match y with [ do_add ⇒ true | _ ⇒ false ]
+| do_sub ⇒ match y with [ do_sub ⇒ true | _ ⇒ false ]
+].
+
 inductive bebit : Type[0] ≝
 | BBbit : bool → bebit
 | BBundef : bebit
 | BBptrcarry :
-  (* is add *) bool → pointer → ∀p : part.BitVector (8*S p) → bebit.
+  add_or_sub → pointer → ∀p : part.BitVector (8*S p) → bebit.
 
 definition Bit_of_val: ErrorMessage → bebit → res Bit ≝ (*CSC: move elsewhere *)