Ignore:
Timestamp:
Nov 12, 2010, 4:51:45 PM (9 years ago)
Author:
mulligan
Message:

More functions on bitvectors written.

File:
1 edited

Legend:

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

    r236 r237  
    2323(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    2424
    25 (* @name: zero
    26    @desc: Produces a bitvector containing <tt>n</tt> copies of <tt>False</tt>.
    27 *)
    2825ndefinition zero ≝
    2926  λn: Nat.
     
    3431    replicate Bool n True.
    3532   
    36 ndefinition append ≝ append.
     33ndefinition append ≝
     34  λm, n: Nat.
     35  λb: BitVector m.
     36  λc: BitVector n.
     37    append Bool m n b c.
     38
     39ndefinition pad ≝
     40  λm, n: Nat.
     41  λb: BitVector n.
     42    let padding ≝ replicate Bool m False in
     43      append Bool m n padding b.
    3744
    3845(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    4047(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    4148   
    42 (*
    43  @name: conjunction
    44  @desc: The logical conjunction of two bitvectors of length <tt>n</tt>.
    45 *)
    4649ndefinition conjunction ≝
    4750  λn: Nat.
     
    4952  λc: BitVector n.
    5053    zip Bool Bool Bool n conjunction b c.
    51 
    52 (*
    53  @name: inclusive_disjunction
    54  @desc: The logical inclusive disjunction of two bitvectors of length
    55         <tt>n</tt>.
    56 *)   
     54   
    5755ndefinition inclusive_disjunction ≝
    5856  λn: Nat.
     
    6058  λc: BitVector n.
    6159    zip Bool Bool Bool n inclusive_disjunction b c.
    62    
    63 (*
    64  @name: exclusive_disjunction
    65  @desc: The logical exclusive disjunction of two bitvectors of length
    66         <tt>n</tt>.  (XOR).
    67 *)       
     60         
    6861ndefinition exclusive_disjunction ≝
    6962  λn: Nat.
     
    7265    zip Bool Bool Bool n exclusive_disjunction b c.
    7366   
    74 (*
    75  @name: complement
    76  @desc: The logical complement of a bitvector of length <tt>n</tt>.
    77 *)   
    7867ndefinition complement ≝
    7968  λn: Nat.
     
    8574(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    8675
    87 ndefinition divide_with_remainder ≝
    88   λm, n: Nat.
    89     mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
     76ndefinition list_of_bitvector ≝
     77  λn: Nat.
     78  λb: BitVector n.
     79    list_of_vector Bool n b.
    9080   
    91 (* @name: pad
    92    @desc: Pads the front of a bitvector of length <tt>n</tt> with <tt>m</tt>
    93           copies of <tt>False</tt>.
    94 *)
    95 ndefinition pad ≝
    96   λm, n: Nat.
    97   λb: BitVector n.
    98     let padding ≝ replicate Bool m False in
    99       append Bool m n padding b.
     81ndefinition bitvector_of_list ≝
     82  λl: List Bool.
     83    vector_of_list Bool l.
    10084
    10185nlet rec bitvector_of_nat_aux (n: Nat) on n ≝
    102   let div_rem ≝ divide_with_remainder n (S (S Z)) in
    103   let div ≝ first Nat Nat div_rem in
    104   let rem ≝ second Nat Nat div_rem in
     86  let divrem ≝ divide_with_remainder n (S (S Z)) in
     87  let div ≝ first Nat Nat divrem in
     88  let rem ≝ second Nat Nat divrem in
    10589    match div with
    10690      [ Z ⇒
    10791        match rem with
    10892          [ Z ⇒ Empty Bool
    109           | S r ⇒ True :: (bitvector_of_nat_aux Z)
     93          | S r ⇒ ? (True :: (bitvector_of_nat_aux Z))
    11094          ]
    11195      | S d ⇒
    11296        match rem with
    113           [ Z ⇒ False :: (bitvector_of_nat_aux (S d))
    114           | S r ⇒ True :: (bitvector_of_nat_aux (S d))
     97          [ Z ⇒ ? (False :: (bitvector_of_nat_aux (S d)))
     98          | S r ⇒ ? (True :: (bitvector_of_nat_aux (S d)))
    11599          ]
    116100      ].
     101      //.
     102nqed.
    117103
    118 (* @name: bitvector_of_nat
    119    @desc: Constructs a bitvector whose integer value is the same as <tt>m</tt>.
    120           Size of the resulting bitvector is clamped to <tt>n</tt>.
    121 *)
    122104ndefinition bitvector_of_nat ≝
    123105  λm, n: Nat.
    124106    let biglist ≝ reverse Bool (bitvector_of_nat_aux m) in
    125107    let size ≝ length Bool biglist in
    126     let bvector ≝ bitvector_of_list Bool biglist in
     108    let bitvector ≝ bitvector_of_list biglist in
    127109    let difference ≝ n - size in
    128       pad difference size bvector.
    129      
    130 ndefinition list_of_bitvector ≝ list_of_vector.
    131 ndefinition bitvector_of_list ≝ vector_of_list.
     110      pad difference size bitvector.
     111
     112nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
     113  match b with
     114    [ Empty ⇒ Z
     115    | Cons o hd tl ⇒
     116      let hdval ≝ match hd with [ True ⇒ S Z | False ⇒ Z ] in
     117        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
     118    ].
Note: See TracChangeset for help on using the changeset viewer.