Changeset 727 for src/common
 Timestamp:
 Mar 31, 2011, 5:20:00 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FrontEndOps.ma
r702 r727 40 40  Ointuoffloat: unary_operation (**r unsigned integer to float *) 41 41  Ofloatofint: unary_operation (**r float to signed integer *) 42  Ofloatofintu: unary_operation. (**r float to unsigned integer *) 42  Ofloatofintu: unary_operation (**r float to unsigned integer *) 43  Oid: unary_operation (**r identity (used to move between registers *) 44  Optrofint: region → unary_operation (**r int to pointer with given representation *) 45  Ointofptr: unary_operation. (**r pointer to int *) 43 46 44 47 inductive binary_operation : Type[0] ≝ … … 62 65  Ocmp: comparison > binary_operation (**r integer signed comparison *) 63 66  Ocmpu: comparison > binary_operation (**r integer unsigned comparison *) 64  Ocmpf: comparison > binary_operation. (**r float comparison *) 67  Ocmpf: comparison > binary_operation (**r float comparison *) 68  Oaddp: binary_operation (**r add an integer to a pointer *) 69  Osubp: binary_operation (**r subtract two pointers *) 70  Ocmpp: comparison → binary_operation. (**r compare pointers *) 65 71 66 72 … … 105 111  Ofloatofint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofint n1))  _ ⇒ None ? ] 106 112  Ofloatofintu ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofintu n1))  _ ⇒ None ? ] 113  Oid ⇒ Some ? arg (* XXX should we restricted the values allowed? *) 114 (* Only conversion of null pointers is specified. *) 115  Optrofint r ⇒ match arg with [ Vint n1 ⇒ if eq n1 zero then Some ? (Vnull r) else None ?  _ ⇒ None ? ] 116  Ointofptr ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint zero)  _ ⇒ None ? ] 107 117 ]. 108 118 … … 445 455  Ocmpu c ⇒ ev_cmpu c 446 456  Ocmpf c ⇒ ev_cmpf c 447 ]. 448 457 (* FIXME: it doesn't make sense to use the same operation for ints and ptrs. *) 458  Oaddp ⇒ ev_add 459  Osubp ⇒ ev_sub 460  Ocmpp c ⇒ ev_cmp c 461 ]. 462
Note: See TracChangeset
for help on using the changeset viewer.