Changeset 744 for src/common/FrontEndOps.ma
 Timestamp:
 Apr 7, 2011, 6:53:59 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FrontEndOps.ma
r727 r744 171 171 ]. 172 172 173 (* FIXME: switch to alias, or rename, or … *)174 definition int_eq : int → int → bool ≝ eq.175 173 definition ev_notbool : val → option val ≝ λv. 176 174 match v with … … 181 179 ]. 182 180 183 definition ev_zero_ext ≝ λnbits: Z. λv: val.181 definition ev_zero_ext ≝ λnbits: nat. λv: val. 184 182 match v with 185 183 [ Vint n ⇒ Some ? (Vint (zero_ext nbits n)) … … 187 185 ]. 188 186 189 definition ev_sign_ext ≝ λnbits: Z. λv:val.187 definition ev_sign_ext ≝ λnbits:nat. λv:val. 190 188 match v with 191 189 [ Vint i ⇒ Some ? (Vint (sign_ext nbits i)) … … 203 201 match v1 with 204 202 [ Vint n1 ⇒ match v2 with 205 [ Vint n2 ⇒ Some ? (Vint (add n1 n2))203 [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2)) 206 204  Vptr r b2 p ofs2 ⇒ Some ? (Vptr r b2 p (shift_offset ofs2 n1)) 207 205  _ ⇒ None ? ] … … 214 212 match v1 with 215 213 [ Vint n1 ⇒ match v2 with 216 [ Vint n2 ⇒ Some ? (Vint (sub n1 n2))214 [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2)) 217 215  _ ⇒ None ? ] 218 216  Vptr r1 b1 p1 ofs1 ⇒ match v2 with … … 234 232 match v1 with 235 233 [ Vint n1 ⇒ match v2 with 236 [ Vint n2 ⇒ Some ? (Vint (divs n1 n2))234 [ Vint n2 ⇒ option_map ?? Vint (division_s ? n1 n2) 237 235  _ ⇒ None ? ] 238 236  _ ⇒ None ? ]. … … 241 239 match v1 with 242 240 [ 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) 245 242  _ ⇒ None ? 246 243 ] … … 251 248 match v1 with 252 249 [ 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) 255 251  _ ⇒ None ? 256 252 ] … … 261 257 match v1 with 262 258 [ 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) 265 260  _ ⇒ None ? 266 261 ]
Note: See TracChangeset
for help on using the changeset viewer.