Ignore:
Timestamp:
Feb 11, 2011, 4:45:28 PM (10 years ago)
Author:
campbell
Message:

First pass at moving regions to block type.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Values.ma

    r487 r496  
    2424include "basics/logic.ma".
    2525
    26 definition block ≝ Z.
    27 (*definition eq_block ≝ zeq.*)
     26definition block ≝ region × Z.
     27
     28definition eq_block ≝
     29λb1,b2.
     30match b1 with [ pair r1 i1 ⇒
     31match b2 with [ pair r2 i2 ⇒
     32  eq_region r1 r2 ∧ eqZb i1 i2
     33] ].
     34
     35lemma eq_block_elim : ∀P:bool → Prop. ∀b1,b2.
     36  (b1 = b2 → P true) → (b1 ≠ b2 → P false) →
     37  P (eq_block b1 b2).
     38#P * #r1 #i1 * #r2 #i2 #H1 #H2
     39whd in ⊢ (?%) @eq_region_elim #H3
     40[ whd in ⊢ (?%) @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
     41| @H2 % #E destruct elim H3 /2/
     42] qed.
    2843
    2944(* * A value is either:
     
    201216    [ Vint n2 ⇒ Vptr pty1 b1 (sub ofs1 n2)
    202217    | Vptr pty2 b2 ofs2 ⇒
    203         if eqZb b1 b2 then Vint (sub ofs1 ofs2) else Vundef
     218        if eq_block b1 b2 then Vint (sub ofs1 ofs2) else Vundef
    204219    | _ ⇒ Vundef ]
    205220  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero | _ ⇒ Vundef ]
     
    372387  | Vptr r1 b1 ofs1 ⇒ match v2 with
    373388    [ Vptr r2 b2 ofs2 ⇒
    374         if eqZb b1 b2
     389        if eq_block b1 b2
    375390        then of_bool (cmp c ofs1 ofs2)
    376391        else cmp_mismatch c
     
    391406  | Vptr r1 b1 ofs1 ⇒ match v2 with
    392407    [ Vptr r2 b2 ofs2 ⇒
    393         if eqZb b1 b2
     408        if eq_block b1 b2
    394409        then of_bool (cmpu c ofs1 ofs2)
    395410        else cmp_mismatch c
Note: See TracChangeset for help on using the changeset viewer.