Changeset 237 for Deliverables/D4.1/Matita/BitVector.ma

Timestamp:

Nov 12, 2010, 4:51:45 PM (10 years ago)

Author:

mulligan

Message:

More functions on bitvectors written.

File:

• Deliverables/D4.1/Matita/BitVector.ma (modified) (7 diffs)

Deliverables/D4.1/Matita/BitVector.ma

@@ -23 +23 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 
-(* @name: zero
-   @desc: Produces a bitvector containing <tt>n</tt> copies of <tt>False</tt>.
-*)
 ndefinition zero ≝
   λn: Nat.
@@ -34 +31 @@
     replicate Bool n True.
     
-ndefinition append ≝ append.
+ndefinition append ≝
+  λm, n: Nat.
+  λb: BitVector m.
+  λc: BitVector n.
+    append Bool m n b c.
+
+ndefinition pad ≝
+  λm, n: Nat.
+  λb: BitVector n.
+    let padding ≝ replicate Bool m False in
+      append Bool m n padding b.
 
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
@@ -40 +47 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
-(*
- @name: conjunction
- @desc: The logical conjunction of two bitvectors of length <tt>n</tt>.
-*)
 ndefinition conjunction ≝
   λn: Nat.
@@ -49 +52 @@
   λc: BitVector n.
     zip Bool Bool Bool n conjunction b c.
-
-(* 
- @name: inclusive_disjunction
- @desc: The logical inclusive disjunction of two bitvectors of length
-        <tt>n</tt>.
-*)    
+   
 ndefinition inclusive_disjunction ≝
   λn: Nat.
@@ -60 +58 @@
   λc: BitVector n.
     zip Bool Bool Bool n inclusive_disjunction b c.
-    
-(* 
- @name: exclusive_disjunction
- @desc: The logical exclusive disjunction of two bitvectors of length
-        <tt>n</tt>.  (XOR).
-*)       
+         
 ndefinition exclusive_disjunction ≝
   λn: Nat.
@@ -72 +65 @@
     zip Bool Bool Bool n exclusive_disjunction b c.
     
-(* 
- @name: complement
- @desc: The logical complement of a bitvector of length <tt>n</tt>.
-*)   
 ndefinition complement ≝
   λn: Nat.
@@ -85 +74 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 
-ndefinition divide_with_remainder ≝
-  λm, n: Nat.
-    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
+ndefinition list_of_bitvector ≝
+  λn: Nat.
+  λb: BitVector n.
+    list_of_vector Bool n b.
     
-(* @name: pad
-   @desc: Pads the front of a bitvector of length <tt>n</tt> with <tt>m</tt>
-          copies of <tt>False</tt>.
-*)
-ndefinition pad ≝
-  λm, n: Nat.
-  λb: BitVector n.
-    let padding ≝ replicate Bool m False in
-      append Bool m n padding b.
+ndefinition bitvector_of_list ≝
+  λl: List Bool.
+    vector_of_list Bool l.
 
 nlet rec bitvector_of_nat_aux (n: Nat) on n ≝
-  let div_rem ≝ divide_with_remainder n (S (S Z)) in
-  let div ≝ first Nat Nat div_rem in
-  let rem ≝ second Nat Nat div_rem in
+  let divrem ≝ divide_with_remainder n (S (S Z)) in
+  let div ≝ first Nat Nat divrem in
+  let rem ≝ second Nat Nat divrem in
     match div with
       [ Z ⇒
         match rem with
           [ Z ⇒ Empty Bool
-          | S r ⇒ True :: (bitvector_of_nat_aux Z)
+          | S r ⇒ ? (True :: (bitvector_of_nat_aux Z))
           ]
       | S d ⇒
         match rem with
-          [ Z ⇒ False :: (bitvector_of_nat_aux (S d))
-          | S r ⇒ True :: (bitvector_of_nat_aux (S d))
+          [ Z ⇒ ? (False :: (bitvector_of_nat_aux (S d)))
+          | S r ⇒ ? (True :: (bitvector_of_nat_aux (S d)))
           ]
       ].
+      //.
+nqed.
 
-(* @name: bitvector_of_nat
-   @desc: Constructs a bitvector whose integer value is the same as <tt>m</tt>.
-          Size of the resulting bitvector is clamped to <tt>n</tt>.
-*)
 ndefinition bitvector_of_nat ≝
   λm, n: Nat.
     let biglist ≝ reverse Bool (bitvector_of_nat_aux m) in
     let size ≝ length Bool biglist in
-    let bvector ≝ bitvector_of_list Bool biglist in
+    let bitvector ≝ bitvector_of_list biglist in
     let difference ≝ n - size in
-      pad difference size bvector.
-      
-ndefinition list_of_bitvector ≝ list_of_vector.
-ndefinition bitvector_of_list ≝ vector_of_list.
+      pad difference size bitvector.
+
+nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
+  match b with
+    [ Empty ⇒ Z
+    | Cons o hd tl ⇒
+      let hdval ≝ match hd with [ True ⇒ S Z | False ⇒ Z ] in
+        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
+    ].