Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (9 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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r727 r744  
    171171  ].
    172172 
    173 (* FIXME: switch to alias, or rename, or … *)
    174 definition int_eq : int → int → bool ≝ eq.
    175173definition ev_notbool : val → option val ≝ λv.
    176174  match v with
     
    181179  ].
    182180
    183 definition ev_zero_ext ≝ λnbits: Z. λv: val.
     181definition ev_zero_ext ≝ λnbits: nat. λv: val.
    184182  match v with
    185183  [ Vint n ⇒ Some ? (Vint (zero_ext nbits n))
     
    187185  ].
    188186
    189 definition ev_sign_ext ≝ λnbits:Z. λv:val.
     187definition ev_sign_ext ≝ λnbits:nat. λv:val.
    190188  match v with
    191189  [ Vint i ⇒ Some ? (Vint (sign_ext nbits i))
     
    203201  match v1 with
    204202  [ Vint n1 ⇒ match v2 with
    205     [ Vint n2 ⇒ Some ? (Vint (add n1 n2))
     203    [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2))
    206204    | Vptr r b2 p ofs2 ⇒ Some ? (Vptr r b2 p (shift_offset ofs2 n1))
    207205    | _ ⇒ None ? ]
     
    214212  match v1 with
    215213  [ Vint n1 ⇒ match v2 with
    216     [ Vint n2 ⇒ Some ? (Vint (sub n1 n2))
     214    [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2))
    217215    | _ ⇒ None ? ]
    218216  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     
    234232  match v1 with
    235233  [ Vint n1 ⇒ match v2 with
    236     [ Vint n2 ⇒ Some ? (Vint (divs n1 n2))
     234    [ Vint n2 ⇒ option_map ?? Vint (division_s ? n1 n2)
    237235    | _ ⇒ None ? ]
    238236  | _ ⇒ None ? ].
     
    241239  match v1 with
    242240  [ Vint n1 ⇒ match v2 with
    243     [ Vint n2 ⇒
    244        if eq n2 zero then None ? else Some ? (Vint (mods n1 n2))
     241    [ Vint n2 ⇒ option_map ?? Vint (modulus_s ? n1 n2)
    245242    | _ ⇒ None ?
    246243    ]
     
    251248  match v1 with
    252249  [ Vint n1 ⇒ match v2 with
    253     [ Vint n2 ⇒
    254         if eq n2 zero then None ? else Some ? (Vint (divu n1 n2))
     250    [ Vint n2 ⇒ option_map ?? Vint (division_u ? n1 n2)
    255251    | _ ⇒ None ?
    256252    ]
     
    261257  match v1 with
    262258  [ Vint n1 ⇒ match v2 with
    263     [ Vint n2 ⇒
    264       if eq n2 zero then None ? else Some ? (Vint (modu n1 n2))
     259    [ Vint n2 ⇒ option_map ?? Vint (modulus_u ? n1 n2)
    265260    | _ ⇒ None ?
    266261    ]
Note: See TracChangeset for help on using the changeset viewer.