Changeset 774 for src/common/FrontEndOps.ma
 Timestamp:
 Apr 26, 2011, 4:51:44 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FrontEndOps.ma
r744 r774 67 67  Ocmpf: comparison > binary_operation (**r float comparison *) 68 68  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 *) 70 71  Ocmpp: comparison → binary_operation. (**r compare pointers *) 71 72 … … 197 198 ]. 198 199 199 (* TODO: add zero to null? *)200 200 definition ev_add ≝ λv1,v2: val. 201 201 match v1 with 202 202 [ Vint n1 ⇒ match v2 with 203 203 [ 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 207 definition 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. *) 215 definition ev_addp ≝ λv1,v2: val. 216 match v1 with 217 [ Vptr r b1 p ofs1 ⇒ match v2 with 207 218 [ Vint n2 ⇒ Some ? (Vptr r b1 p (shift_offset ofs1 n2)) 208 219  _ ⇒ 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 226 definition ev_subpi ≝ λv1,v2: val. 227 match v1 with 228 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with 217 229 [ 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 234 definition ev_subpp ≝ λv1,v2: val. 235 match v1 with 236 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with 237 [ Vptr r2 b2 p2 ofs2 ⇒ 219 238 if eq_block b1 b2 then Some ? (Vint (sub_offset ofs1 ofs2)) else None ? 220 239  _ ⇒ None ? ] … … 398 417 [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2)) 399 418  _ ⇒ None ? ] 400  Vptr r1 b1 p1 ofs1 ⇒ match v2 with 419  _ ⇒ None ? ]. 420 421 definition ev_cmpp ≝ λc: comparison. λv1,v2: val. 422 match v1 with 423 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with 401 424 [ Vptr r2 b2 p2 ofs2 ⇒ 402 425 if eq_block b1 b2 … … 450 473  Ocmpu c ⇒ ev_cmpu c 451 474  Ocmpf c ⇒ ev_cmpf c 452 (* FIXME: it doesn't make sense to use the same operation for ints and ptrs. *)453  O addp ⇒ ev_add454  Osubp ⇒ ev_sub455  Ocmpp c ⇒ ev_cmp c456 ]. 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.