Changeset 744 for src/ASM


Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (10 years ago)
Author:
campbell
Message:

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r724 r744  
    149149  λb, c: BitVector n.
    150150    addition_n n b (two_complement_negation n c).
    151    
    152 definition multiplication ≝
    153   λn: nat.
    154   λb, c: BitVector n.
    155     let b_nat ≝ nat_of_bitvector ? b in
    156     let c_nat ≝ nat_of_bitvector ? c in
    157     let result ≝ b_nat * c_nat in
    158       bitvector_of_nat (n + n) result.
    159      
    160 definition division_u ≝
    161   λn: nat.
    162   λb, c: BitVector n.
    163     let b_nat ≝ nat_of_bitvector ? b in
    164     let c_nat ≝ nat_of_bitvector ? c in
    165     match c_nat with
    166     [ O ⇒ None ?
    167     | _ ⇒
    168       let result ≝ b_nat ÷ c_nat in
    169         Some ? (bitvector_of_nat n result)
     151
     152let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝
     153match b with
     154[ VEmpty ⇒ acc
     155| VCons m' hd tl ⇒
     156    let acc' ≝ if hd then addition_n ? c acc else acc in
     157    mult_aux m' n tl (shift_right_1 ?? c false) acc'
     158].
     159
     160definition multiplication : ∀n:nat. BitVector n → BitVector n → BitVector (n + n) ≝
     161  λn: nat.
     162  match n return λn.BitVector n → BitVector n → BitVector (n + n) with
     163  [ O ⇒ λ_.λ_.[[ ]]
     164  | S m ⇒
     165    λb, c : BitVector (S m).
     166    let c' ≝ pad (S m) (S m) c in
     167      mult_aux ?? b (shift_left ?? m c' false) (zero ?)
     168  ].
     169
     170(* Division:  001...000 divided by 000...010
     171     Shift the divisor as far left as possible,
     172                                  100...000
     173      then try subtracting it at each
     174      bit position, shifting left as we go.
     175              001...000 - 100...000 X ⇒ 0
     176              001...000 - 010...000 X ⇒ 0
     177              001...000 - 001...000 Y ⇒ 1 (use subtracted value as new quotient)
     178              ...
     179      Then pad out the remaining bits at the front
     180         00..001...
     181*)
     182inductive fbs_diff : nat → Type[0] ≝
     183| fbs_diff' : ∀n,m. fbs_diff (S (n+m)).
     184
     185let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝
     186match b return λn.λ_. option (fbs_diff n) with
     187[ VEmpty ⇒ None ?
     188| VCons m h t ⇒
     189    if h then Some ? (fbs_diff' O m)
     190    else match first_bit_set m t with
     191         [ None ⇒ None ?
     192         | Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ]
     193         ]
     194].
     195
     196let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝
     197match m with
     198[ O ⇒ 〈[[ ]], q〉
     199| S m' ⇒
     200    let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in
     201    let bit ≝ head' … flags in
     202    let q'' ≝ if bit then q' else q in
     203    let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in
     204    〈bit:::tl, md〉
     205].
     206
     207definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝
     208  λn: nat.
     209  λb, c: BitVector (S n).
     210
     211    match first_bit_set ? c with
     212    [ None ⇒ None ?
     213    | Some fbs' ⇒
     214        match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒
     215          let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in
     216          Some ? 〈switch_bv_plus ??? (pad ?? d), m〉
     217        ]
    170218    ].
     219
     220definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
     221λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\fst p) ].
    171222     
    172223definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
     
    177228        let b_sign_bit ≝ get_index_v ? ? b O ? in
    178229        let c_sign_bit ≝ get_index_v ? ? c O ? in
    179         let b_as_nat ≝ nat_of_bitvector ? b in
    180         let c_as_nat ≝ nat_of_bitvector ? c in
    181         match c_as_nat with
    182         [ O ⇒ None ?
    183         | S o ⇒
    184           match b_sign_bit with
     230        match b_sign_bit with
     231        [ true ⇒
     232          let neg_b ≝ two_complement_negation ? b in
     233          match c_sign_bit with
    185234          [ true ⇒
    186             let temp_b ≝ b_as_nat - (2^p) in
    187             match c_sign_bit with
    188             [ true ⇒
    189               let temp_c ≝ c_as_nat - (2^p) in
    190                 Some ? (bitvector_of_nat ? (temp_b ÷ temp_c))
    191             | false ⇒
    192               let result ≝ (temp_b ÷ c_as_nat) + (2^p) in
    193                 Some ? (bitvector_of_nat ? result)
    194             ]
     235              (* I was worrying slightly about -2^(n-1), whose negation can't
     236                 be represented in an n bit signed number.  However, it's
     237                 negation comes out as 2^(n-1) as an n bit *unsigned* number,
     238                 so it's fine. *)
     239              division_u ? neg_b (two_complement_negation ? c)
    195240          | false ⇒
    196             match c_sign_bit with
    197             [ true ⇒
    198               let temp_c ≝ c_as_nat - (2^p) in
    199               let result ≝ (b_as_nat ÷ temp_c) + (2^p) in
    200                 Some ? (bitvector_of_nat ? result)
    201             | false ⇒ Some ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat))
    202             ]
     241              match division_u ? neg_b c with
     242              [ None ⇒ None ?
     243              | Some r ⇒ Some ? (two_complement_negation ? r)
     244              ]
     245          ]
     246        | false ⇒
     247          match c_sign_bit with
     248          [ true ⇒
     249              match division_u ? b (two_complement_negation ? c) with
     250              [ None ⇒ None ?
     251              | Some r ⇒ Some ? (two_complement_negation ? r)
     252              ]
     253          | false ⇒ division_u ? b c
    203254          ]
    204255        ]
    205     ].
     256   ].
    206257    //
    207258qed.
    208259
    209 definition modulus_u ≝
    210   λn.
    211   λb, c: BitVector n.
    212     let b_nat ≝ nat_of_bitvector ? b in
    213     let c_nat ≝ nat_of_bitvector ? c in
    214     match c_nat with
    215     [ O ⇒ None ?
    216     | _ ⇒
    217       let result ≝ modulus b_nat c_nat in
    218       Some ? (bitvector_of_nat n result)
    219     ].
     260definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
     261λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\snd p) ].
    220262           
    221263definition modulus_s ≝
  • src/ASM/BitVector.ma

    r726 r744  
    4040definition pad ≝
    4141  λm, n: nat.
    42   λb: BitVector n.
    43     let padding ≝ replicate bool m false in
    44       append bool m n padding b.
     42  λb: BitVector n. pad_vector ? false m n b.
    4543     
    4644(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • src/ASM/Vector.ma

    r726 r744  
    1212include "arithmetics/nat.ma".
    1313
     14include "utilities/extranat.ma".
    1415include "utilities/oldlib/eq.ma".
    1516
     
    152153qed.
    153154
    154 let rec split (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
     155definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝
     156λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with
     157[ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ].
     158
     159definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝
     160λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with
     161[ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
     162
     163let rec split' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
    155164 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
    156165  [ O ⇒ λv. 〈[[ ]], v〉
    157   | S m' ⇒ λv.
    158     match v return λl. λ_: Vector A l. l = S (plus m' n) → (Vector A (S m')) × (Vector A n) with
    159       [ VEmpty ⇒ λK. ⊥
    160       | VCons o he tl ⇒ λK.
    161         match split A m' n (tl⌈Vector A o ↦ Vector A (m' + n)⌉) with
    162         [ pair v1 v2 ⇒ 〈he:::v1, v2〉
    163         ]
    164       ] (?: (S (m' + n)) = S (m' + n))].
    165       //
    166       [ destruct
    167       | lapply (injective_S … K)
    168         //
    169       ]
    170 qed.
     166  | S m' ⇒ λv. let 〈l,r〉 ≝ split' A m' n (tail ?? v) in 〈head' ?? v:::l, r〉
     167  ].
     168(* Prevent undesirable unfolding. *)
     169let rec split (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝
     170 split' A m n v.
     171
    171172
    172173definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
     
    329330(* At some points matita will attempt to reduce reverse with a known vector,
    330331   which reduces the equality proof for the cast.  Normalising this proof needs
    331    to be fast enough to keep matita usable. *)
    332 let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝
    333 match n return λn'.∀m.S(n'+m) = n'+S m with
    334 [ O ⇒ λm.refl ??
    335 | S n' ⇒ λm. ?
    336 ]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed.
     332   to be fast enough to keep matita usable, so use plus_n_Sm_fast. *)
    337333
    338334let rec revapp (A: Type[0]) (n: nat) (m:nat)
     
    347343  (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
    348344< plus_n_O @refl qed.
     345
     346let rec pad_vector (A:Type[0]) (a:A) (n,m:nat) (v:Vector A m) on n : Vector A (n+m) ≝
     347match n return λn.Vector A (n+m) with
     348[ O ⇒ v
     349| S n' ⇒ a:::(pad_vector A a n' m v)
     350].
    349351
    350352(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    404406qed.
    405407
     408
     409(* XXX this is horrible - but useful to ensure that we can normalise in the proof assistant. *)
     410definition switch_bv_plus : ∀A:Type[0]. ∀n,m. Vector A (n+m) → Vector A (m+n) ≝
     411λA,n,m. match commutative_plus_faster n m with [ refl ⇒ λi.i ].
     412
    406413definition shift_right_1 ≝
    407414  λA: Type[0].
     
    409416  λv: Vector A (S n).
    410417  λa: A.
    411     reverse … (shift_left_1 … (reverse … v) a).
    412    
    413 definition shift_left ≝
     418    let 〈v',dropped〉 ≝ split ? n 1 (switch_bv_plus ? 1 n v) in a:::v'.
     419(*    reverse … (shift_left_1 … (reverse … v) a).*)
     420
     421definition shift_left : ∀A:Type[0]. ∀n,m:nat. Vector A n → A → Vector A n ≝
    414422  λA: Type[0].
    415423  λn, m: nat.
    416   λv: Vector A (S n).
    417   λa: A.
    418     iterate … (λx. shift_left_1 … x a) v m.
     424    match nat_compare n m return λx,y.λ_. Vector A x → A → Vector A x with
     425    [ nat_lt _ _ ⇒ λv,a. replicate … a
     426    | nat_eq _   ⇒ λv,a. replicate … a
     427    | nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ split … v in switch_bv_plus … (v' @@ (replicate … a))
     428    ].
     429
     430(*    iterate … (λx. shift_left_1 … x a) v m.*)
    419431   
    420432definition shift_right ≝
     
    428440(* Decidable equality.                                                        *)
    429441(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    430 
    431 definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝
    432 λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with
    433 [ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ].
    434 
    435 definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝
    436 λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with
    437 [ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
    438442
    439443let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
Note: See TracChangeset for help on using the changeset viewer.