Ignore:
Timestamp:
Apr 26, 2011, 4:51:44 PM (9 years ago)
Author:
campbell
Message:

Separate out the different forms of addition and subtraction in the frontend ops.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r744 r774  
    6767  | Ocmpf: comparison -> binary_operation  (**r float comparison *)
    6868  | Oaddp: binary_operation                (**r add an integer to a pointer *)
    69   | Osubp: binary_operation                (**r subtract two pointers *)
     69  | Osubpi: binary_operation               (**r subtract int from a pointers *)
     70  | Osubpp: binary_operation               (**r subtract two pointers *)
    7071  | Ocmpp: comparison → binary_operation.  (**r compare pointers *)
    7172
     
    197198  ].
    198199
    199 (* TODO: add zero to null? *)
    200200definition ev_add ≝ λv1,v2: val.
    201201  match v1 with
    202202  [ Vint n1 ⇒ match v2 with
    203203    [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2))
    204     | Vptr r b2 p ofs2 ⇒ Some ? (Vptr r b2 p (shift_offset ofs2 n1))
    205     | _ ⇒ None ? ]
    206   | Vptr r b1 p ofs1 ⇒ match v2 with
     204    | _ ⇒ None ? ]
     205  | _ ⇒ None ? ].
     206
     207definition ev_sub ≝ λv1,v2: val.
     208  match v1 with
     209  [ Vint n1 ⇒ match v2 with
     210    [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2))
     211    | _ ⇒ None ? ]
     212  | _ ⇒ None ? ].
     213
     214(* NB: requires arguments to be presented pointer first. *)
     215definition ev_addp ≝ λv1,v2: val.
     216  match v1 with
     217  [ Vptr r b1 p ofs1 ⇒ match v2 with
    207218    [ Vint n2 ⇒ Some ? (Vptr r b1 p (shift_offset ofs1 n2))
    208219    | _ ⇒ None ? ]
    209   | _ ⇒ None ? ].
    210 
    211 definition ev_sub ≝ λv1,v2: val.
    212   match v1 with
    213   [ Vint n1 ⇒ match v2 with
    214     [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2))
    215     | _ ⇒ None ? ]
    216   | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     220  | Vnull r ⇒ match v2 with
     221    [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?
     222    | _ ⇒ None ?
     223    ]
     224  | _ ⇒ None ? ].
     225
     226definition ev_subpi ≝ λv1,v2: val.
     227  match v1 with
     228  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    217229    [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 n2))
    218     | Vptr r2 b2 p2 ofs2 ⇒
     230    | _ ⇒ None ? ]
     231  | Vnull r ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
     232  | _ ⇒ None ? ].
     233
     234definition ev_subpp ≝ λv1,v2: val.
     235  match v1 with
     236  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     237    [ Vptr r2 b2 p2 ofs2 ⇒
    219238        if eq_block b1 b2 then Some ? (Vint (sub_offset ofs1 ofs2)) else None ?
    220239    | _ ⇒ None ? ]
     
    398417    [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
    399418    | _ ⇒ None ? ]
    400   | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     419  | _ ⇒ None ? ].
     420
     421definition ev_cmpp ≝ λc: comparison. λv1,v2: val.
     422  match v1 with
     423  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    401424    [ Vptr r2 b2 p2 ofs2 ⇒
    402425        if eq_block b1 b2
     
    450473  | Ocmpu c ⇒ ev_cmpu c
    451474  | Ocmpf c ⇒ ev_cmpf c
    452   (* FIXME: it doesn't make sense to use the same operation for ints and ptrs. *)
    453   | Oaddp ⇒ ev_add
    454   | Osubp ⇒ ev_sub
    455   | Ocmpp c ⇒ ev_cmp c
    456   ].
    457 
     475  | Oaddp ⇒ ev_addp
     476  | Osubpi ⇒ ev_subpi
     477  | Osubpp ⇒ ev_subpp
     478  | Ocmpp c ⇒ ev_cmpp c
     479  ].
     480
Note: See TracChangeset for help on using the changeset viewer.