Ignore:
Timestamp:
Nov 15, 2010, 10:22:41 AM (9 years ago)
Author:
mulligan
Message:

Updated Vector / BitVector? files taken from my Matita library.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/BitVector.ma

    r238 r240  
    11(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    22(* BitVector.ma: Fixed length bitvectors, and common operations on them.      *)
    3 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    4 
    5 include "Vector.ma".
    6 include "List.ma".
    7 include "Nat.ma".
    8 include "Bool.ma".
     3(*               Most functions are specialised versions of those found in    *)
     4(*               Vector.ma as a courtesy, or Boolean functions lifted into    *)
     5(*               BitVector variants.                                          *)
     6(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     7
     8include "Universes/Universes.ma".
     9
     10include "Datatypes/Listlike/Vector/Vector.ma".
     11include "Datatypes/Listlike/List/List.ma".
     12
     13include "Datatypes/Nat/Nat.ma".
     14include "Datatypes/Nat/Addition.ma".
     15include "Datatypes/Nat/Division_Modulus.ma".
     16include "Datatypes/Nat/Exponential.ma".
     17
     18include "Datatypes/Bool.ma".
    919
    1020(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    2030
    2131(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     32(* Lookup.                                                                    *)
     33(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     34
     35ndefinition get_index ≝
     36  λn: Nat.
     37  λb: BitVector n.
     38  λm: Nat.
     39    get_index Bool n b m.
     40   
     41interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
     42   
     43ndefinition set_index ≝
     44  λn: Nat.
     45  λb: BitVector n.
     46  λm: Nat.
     47    set_index Bool n b m.
     48   
     49ndefinition drop ≝
     50  λn: Nat.
     51  λb: BitVector n.
     52  λm: Nat.
     53    drop Bool n b m.
     54
     55(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    2256(* Creating bitvectors from scratch.                                          *)
    2357(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    3670  λc: BitVector n.
    3771    append Bool m n b c.
     72   
     73interpretation "BitVector append" 'append b c = (append b c).
    3874
    3975ndefinition pad ≝
     
    4278    let padding ≝ replicate Bool m False in
    4379      append Bool m n padding b.
     80     
     81(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     82(* Other manipulations.                                                       *)
     83(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     84
     85ndefinition reverse ≝
     86  λn: Nat.
     87  λb: BitVector n.
     88    reverse Bool n b.
     89
     90ndefinition length ≝
     91  λn: Nat.
     92  λb: BitVector n.
     93    length Bool n b.
    4494
    4595(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    51101  λb: BitVector n.
    52102  λc: BitVector n.
    53     zip Bool Bool Bool n conjunction b c.
     103    zip_with Bool Bool Bool n conjunction b c.
     104   
     105interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c).
    54106   
    55107ndefinition inclusive_disjunction ≝
     
    57109  λb: BitVector n.
    58110  λc: BitVector n.
    59     zip Bool Bool Bool n inclusive_disjunction b c.
     111    zip_with Bool Bool Bool n inclusive_disjunction b c.
     112   
     113interpretation "BitVector inclusive disjunction"
     114  'inclusive_disjunction b c = (inclusive_disjunction ? b c).
    60115         
    61116ndefinition exclusive_disjunction ≝
     
    63118  λb: BitVector n.
    64119  λc: BitVector n.
    65     zip Bool Bool Bool n exclusive_disjunction b c.
    66    
    67 ndefinition complement ≝
     120    zip_with Bool Bool Bool n exclusive_disjunction b c.
     121   
     122interpretation "BitVector exclusive disjunction"
     123  'exclusive_disjunction b c = (exclusive_disjunction ? b c).
     124   
     125ndefinition negation ≝
    68126  λn: Nat.
    69127  λb: BitVector n.
    70128    map Bool Bool n (negation) b.
     129   
     130interpretation "BitVector negation" 'negation b c = (negation ? b c).
    71131
    72132(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    82142  λm, n: Nat.
    83143  λb: BitVector n.
    84     rotate_right Bool n m b.   
     144    rotate_right Bool n m b.
     145   
     146ndefinition shift_left ≝
     147  λm, n: Nat.
     148  λb: BitVector n.
     149  λc: Bool.
     150    shift_left Bool n m b c.
     151   
     152ndefinition shift_right ≝
     153  λm, n: Nat.
     154  λb: BitVector n.
     155  λc: Bool.
     156    shift_right Bool n m b c.
    85157   
    86158(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    129201    | Cons o hd tl ⇒
    130202      let hdval ≝ match hd with [ True ⇒ S Z | False ⇒ Z ] in
    131         ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
     203        ((exponential (S (S Z)) o) × hdval) + nat_of_bitvector o tl
    132204    ].
Note: See TracChangeset for help on using the changeset viewer.