Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (7 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/ByteValues.ma

    r1987 r2176  
    55include "common/Pointers.ma".
    66
    7 record part (r: region): Type[0] ≝
     7record part (*r: region*): Type[0] ≝
    88 { part_no:> nat
    9  ; part_no_ok: part_no < size_pointer r
     9 ; part_no_ok: part_no < size_pointer (*r*)
    1010 }.
    1111
     
    2525  | BVundef: beval
    2626  | BVByte: Byte → beval
    27   | BVnull: ∀r:region. part r → beval
    28   | BVptr: ∀p:pointer. part (ptype p) → beval.
     27  | BVnull: (*∀r:region.*) part → beval
     28  | BVptr: ∀p:pointer. part (*ptype p*) → beval.
    2929
    3030definition eq_beval: beval → beval → bool ≝
     
    3333   [ BVundef      ⇒ match v2 with [ BVundef      ⇒ true                           | _ ⇒ false ]
    3434   | BVByte b1    ⇒ match v2 with [ BVByte b2    ⇒ eq_bv … b1 b2                  | _ ⇒ false ]
    35    | BVnull r1 p1 ⇒ match v2 with [ BVnull r2 p2 ⇒ eq_region … r1 r2 ∧ eqb p1 p2  | _ ⇒ false ]
     35   | BVnull p1    ⇒ match v2 with [ BVnull p2    ⇒ eqb p1 p2                      | _ ⇒ false ]
    3636   | BVptr P1 p1  ⇒ match v2 with [ BVptr P2 p2  ⇒ eq_pointer … P1 P2 ∧ eqb p1 p2 | _ ⇒ false ]].
    3737
     
    4141 match l with
    4242  [ nil ⇒
    43      if eqb part (size_pointer (ptype p)) then
     43     if eqb part (size_pointer (*ptype p*)) then
    4444      OK … p
    4545     else
     
    7070(* CSC: use vectors in place of lists? Or even better products of tuples
    7171   (more easily pattern matchable in the finite case)? *)
    72 let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) (pr: plus part n = size_pointer (ptype p)) on n: list beval ≝
     72let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) (pr: plus part n = size_pointer (*ptype p*)) on n: list beval ≝
    7373 match n with
    7474  [ O ⇒ λ_.[]
     
    7777
    7878definition bevals_of_pointer: pointer → list beval ≝
    79  λp. bevals_of_pointer_aux p 0 (size_pointer (ptype p)) ….
     79 λp. bevals_of_pointer_aux p 0 (size_pointer (*ptype p*)) ….
    8080// qed.
    8181
    8282lemma pointer_of_bevals_bevals_of_pointer:
    8383 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p.
    84 * * #pbl #pok #poff
     84* #pbl #poff
    8585try %
    86 whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 1) [2,3: %]
    87 whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 2) %
     86whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 1) (*[2,3: %]*)
     87whd in ⊢ (??%?);(* >reflexive_eq_pointer >(eqb_n_n 2)*) %
    8888qed.
    8989
     
    9999(* Fails if the address is not representable as a pair *)
    100100definition beval_pair_of_pointer: pointer → res (beval × beval) ≝
     101 λp. OK … (list_to_pair … (bevals_of_pointer p) ?).
     102(*
    101103 λp. match p with [ mk_pointer pty pbl pok poff ⇒
    102104  match pty with
    103105   [ XData ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer XData pbl pok poff)) ?)
    104106   | Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?)
    105    | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].
     107   | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*)
    106108% qed.
    107109
    108110definition beval_pair_of_code_pointer: (Σp:pointer. ptype p = Code) → beval × beval ≝
     111 λp. list_to_pair ? (bevals_of_pointer p) ?.
     112(*
    109113 λp. match p return λp. ptype p = Code → ? with [ mk_pointer pty pbl pok poff ⇒
    110114  match pty return λpty. ? → pty = Code → ? with
    111115   [ Code ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer Code pbl ? poff)) ?
    112116   | _ ⇒ λpok'.λabs. ⊥] pok] ?.
    113 [@(pi2 … p) |7: // |8: %] destruct (abs)
     117[@(pi2 … p) |7: // |8: %] destruct (abs)*) %
    114118qed.
    115119
     
    131135  [ BVundef ⇒ Error … [MSG ValueNotABoolean]
    132136  | BVByte b ⇒ OK … (eq_bv … (zero …) b)
    133   | BVnull x y ⇒  OK … false
     137  | BVnull y ⇒  OK … false
    134138  | BVptr p q ⇒ OK ? true ].
    135139
Note: See TracChangeset for help on using the changeset viewer.