Changeset 237


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

More functions on bitvectors written.

Location:
Deliverables/D4.1/Matita
Files:
4 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    ].
  • Deliverables/D4.1/Matita/List.ma

    r236 r237  
    8383    | Cons hd tl ⇒ f hd :: map A B f tl
    8484    ].
    85    
    86 nlet rec zip_safe (A: Type[0]) (B: Type[0])
    87                   (l: List A) (m: List B) (p: length A l = length B m) ≝ True.
    8885
    8986(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • Deliverables/D4.1/Matita/Nat.ma

    r236 r237  
    3434    ].
    3535   
    36 notation "n break ≤ m"
     36notation "hvbox(n break ≤ m)"
    3737  non associative with precedence 47
    3838  for @{ 'less_than_or_equal $n $m }.
     
    4949    n ≤ m.
    5050   
    51 notation "n break ≥ m"
     51notation "hvbox(n break ≥ m)"
    5252  non associative with precedence 47
    5353  for @{ 'greater_than_or_equal $n $m }.
     
    6262    m ≤ n ∧ ¬(m = n).
    6363   
    64 notation "n break < m"
     64notation "hvbox(n break < m)"
    6565  non associative with precedence 47
    6666  for @{ 'less_than $n $m }.
     
    7272    n < m.
    7373   
    74 notation "n break > m"
     74notation "hvbox(n break > m)"
    7575  non associative with precedence 47
    7676  for @{ 'greater_than $n $m }.
     
    8787    ].
    8888   
    89 notation "n break + m"
     89notation "hvbox(n break + m)"
    9090  right associative with precedence 52
    9191  for @{ 'plus $n $m }.
     
    103103    ].
    104104   
    105 notation "n break - m"
     105notation "hvbox(n break - m)"
    106106  right associative with precedence 47
    107107  for @{ 'minus $n $m }.
     
    119119    ].
    120120   
    121 notation "n break * m"
     121notation "hvbox(n break * m)"
    122122  right associative with precedence 47
    123123  for @{ 'multiplication $n $m }.
     
    142142      ].
    143143     
    144 notation "n break ÷ m"
     144notation "hvbox(n break ÷ m)"
    145145  right associative with precedence 47
    146146  for @{ 'division $n $m }.
     
    165165      ].
    166166   
    167 notation "n break % m"
     167notation "hvbox(n break % m)"
    168168  right associative with precedence 47
    169169  for @{ 'modulus $n $m }.
    170170 
    171171interpretation "Nat modulus" 'modulus m n = (modulus m n).
     172
     173ndefinition divide_with_remainder ≝
     174  λm, n: Nat.
     175    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
     176
     177(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     178(* Exponentials, and square roots.                                            *)
     179(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     180
     181nlet rec exponential (m: Nat) (n: Nat) on n ≝
     182  match n with
     183    [ Z ⇒ S (Z)
     184    | S o ⇒ m * exponential m o
     185    ].
     186   
     187notation "hvbox(n ^ m)"
     188  left associative with precedence 52
     189  for @{ 'exponential $n $m }.
     190 
     191interpretation "Nat exponential" 'exponential n m = (exponential n m).
    172192
    173193(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • Deliverables/D4.1/Matita/Vector.ma

    r236 r237  
    166166    ].
    167167
    168 (*
    169168nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
    170169  match l return λl. Vector A (length A l) with
    171     [ Empty ⇒ cic:/matita/Cerco/Vector/Vector.con(0,1,1) A
    172     | Cons hd tl ⇒ ? (hd :: (from_list A tl))
    173     ].
    174     //.
    175 nqed.
    176 *)
     170    [ Empty ⇒ ? (cic:/matita/Cerco/Vector/Vector.con(0,1,1) A)
     171    | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
     172    ].
     173    nnormalize.
     174    //.
     175    //.
     176nqed.
    177177
    178178(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
Note: See TracChangeset for help on using the changeset viewer.