Ignore:
Timestamp:
Nov 23, 2011, 6:03:07 PM (9 years ago)
Author:
campbell
Message:

Use pointer record in front-end.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r1516 r1545  
    8484      match find_symbol s with
    8585      [ 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))))
    8787      ]
    8888  | 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))))
    9090  ]. cases sp // qed.
    9191
     
    102102      match arg with
    103103      [ 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 ?))
    105105      | Vnull _ ⇒ Some ? (Vint sz (repr ? 1))
    106106      | _ ⇒ None ?
     
    125125[ ASTint sz sg ⇒ ∀i.P (Vint sz i)
    126126| 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))
    128128] →
    129129P v.
     
    197197definition ev_addp ≝ λv1,v2: val.
    198198  match v1 with
    199   [ Vptr r b1 p ofs1 ⇒ match v2 with
    200     [ 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))
    201201    | _ ⇒ None ? ]
    202202  | Vnull r ⇒ match v2 with
     
    208208definition ev_subpi ≝ λv1,v2: val.
    209209  match v1 with
    210   [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    211     [ 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))
    212212    | _ ⇒ None ? ]
    213213  | Vnull r ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
     
    216216definition ev_subpp ≝ λsz. λv1,v2: val.
    217217  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 ?
    221223    | _ ⇒ None ? ]
    222224  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
     
    384386definition ev_cmpp ≝ λc: comparison. λv1,v2: val.
    385387  match v1 with
    386   [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    387     [ Vptr r2 b2 p2 ofs2 ⇒
    388         if eq_block b1 b2
    389         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)))
    390392        else ev_cmp_mismatch c
    391393    | Vnull r2 ⇒ ev_cmp_mismatch c
    392394    | _ ⇒ None ? ]
    393395  | Vnull r1 ⇒ match v2 with
    394     [ Vptr _ _ _ _ ⇒ ev_cmp_mismatch c
     396    [ Vptr _ ⇒ ev_cmp_mismatch c
    395397    | Vnull r2 ⇒ ev_cmp_match c
    396398    | _ ⇒ None ?
Note: See TracChangeset for help on using the changeset viewer.