Changeset 1545 for src/common/FrontEndOps.ma
 Timestamp:
 Nov 23, 2011, 6:03:07 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FrontEndOps.ma
r1516 r1545 84 84 match find_symbol s with 85 85 [ None ⇒ None ? 86  Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset ? zero_offset (repr I16 ofs)))86  Some b ⇒ Some ? (Vptr (mk_pointer Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset ? zero_offset (repr I16 ofs)))) 87 87 ] 88 88  Oaddrstack ofs ⇒ 89 Some ? (Vptr Any sp ? (shift_offset ? zero_offset (repr I16 ofs)))89 Some ? (Vptr (mk_pointer Any sp ? (shift_offset ? zero_offset (repr I16 ofs)))) 90 90 ]. cases sp // qed. 91 91 … … 102 102 match arg with 103 103 [ Vint sz1 n1 ⇒ Some ? (Vint sz (if (eq_bv ? n1 (zero ?)) then (repr ? 1) else (zero ?))) 104  Vptr _ _ _ _⇒ Some ? (Vint sz (zero ?))104  Vptr _ ⇒ Some ? (Vint sz (zero ?)) 105 105  Vnull _ ⇒ Some ? (Vint sz (repr ? 1)) 106 106  _ ⇒ None ? … … 125 125 [ ASTint sz sg ⇒ ∀i.P (Vint sz i) 126 126  ASTfloat sz ⇒ ∀f.P (Vfloat f) 127  ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr r b c o)127  ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr (mk_pointer r b c o)) 128 128 ] → 129 129 P v. … … 197 197 definition ev_addp ≝ λv1,v2: val. 198 198 match v1 with 199 [ Vptr r b1 p ofs1 ⇒ match v2 with200 [ Vint sz2 n2 ⇒ Some ? (Vptr r b1 p (shift_offset ? ofs1 n2))199 [ Vptr ptr1 ⇒ match v2 with 200 [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer ? ptr1 n2)) 201 201  _ ⇒ None ? ] 202 202  Vnull r ⇒ match v2 with … … 208 208 definition ev_subpi ≝ λv1,v2: val. 209 209 match v1 with 210 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with211 [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2))210 [ Vptr ptr1 ⇒ match v2 with 211 [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer ? ptr1 n2)) 212 212  _ ⇒ None ? ] 213 213  Vnull r ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?  _ ⇒ None ? ] … … 216 216 definition ev_subpp ≝ λsz. λv1,v2: val. 217 217 match v1 with 218 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with 219 [ Vptr r2 b2 p2 ofs2 ⇒ 220 if eq_block b1 b2 then Some ? (Vint sz (sub_offset ? ofs1 ofs2)) else None ? 218 [ Vptr ptr1 ⇒ match v2 with 219 [ Vptr ptr2 ⇒ 220 if eq_block (pblock ptr1) (pblock ptr2) 221 then Some ? (Vint sz (sub_offset ? (poff ptr1) (poff ptr2))) 222 else None ? 221 223  _ ⇒ None ? ] 222 224  Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint sz (zero ?))  _ ⇒ None ? ] … … 384 386 definition ev_cmpp ≝ λc: comparison. λv1,v2: val. 385 387 match v1 with 386 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with387 [ Vptr r2 b2 p2 ofs2 ⇒388 if eq_block b1 b2389 then Some ? (of_bool (cmp_offset c ofs1 ofs2))388 [ Vptr ptr1 ⇒ match v2 with 389 [ Vptr ptr2 ⇒ 390 if eq_block (pblock ptr1) (pblock ptr2) 391 then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2))) 390 392 else ev_cmp_mismatch c 391 393  Vnull r2 ⇒ ev_cmp_mismatch c 392 394  _ ⇒ None ? ] 393 395  Vnull r1 ⇒ match v2 with 394 [ Vptr _ _ _ _⇒ ev_cmp_mismatch c396 [ Vptr _ ⇒ ev_cmp_mismatch c 395 397  Vnull r2 ⇒ ev_cmp_match c 396 398  _ ⇒ None ?
Note: See TracChangeset
for help on using the changeset viewer.