Changeset 2177 for src


Ignore:
Timestamp:
Jul 12, 2012, 2:56:50 PM (9 years ago)
Author:
campbell
Message:

Tidy up multiplication.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Arithmetic.ma

    r2154 r2177  
    364364  ].
    365365
     366definition short_multiplication : ∀n:nat. BitVector n → BitVector n → BitVector n ≝
     367λn,x,y. (\snd (vsplit ??? (multiplication ? x y))).
     368
    366369(* Division:  001...000 divided by 000...010
    367370     Shift the divisor as far left as possible,

  • src/Clight/Csem.ma

    r2176 r2177  
    197197      [ Vint sz1 n1 ⇒ match v2 with
    198198          [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    199                           (λn1. Some ? (Vint sz2 (\snd (vsplit ??? (multiplication ? n1 n2))))) (None ?)
     199                          (λn1. Some ? (Vint sz2 (short_multiplication ? n1 n2))) (None ?)
    200200        | _ ⇒ None ? ]
    201201      | _ ⇒ None ? ]

  • src/common/FrontEndOps.ma

    r2176 r2177  
    244244  [ Vint sz1 n1 ⇒ match v2 with
    245245    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    246                     (λn1. Some ? (Vint ? (\snd (vsplit … (multiplication ? n1 n2)))))
     246                    (λn1. Some ? (Vint ? (short_multiplication ? n1 n2)))
    247247                    (None ?)
    248248    | _ ⇒ None ? ]
Note: See TracChangeset for help on using the changeset viewer.