Ignore:
Timestamp:
Apr 4, 2012, 6:48:25 PM (9 years ago)
Author:
campbell
Message:

First cut at using back-end memory model throughout.
Note the correction to BEValues.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndVal.ma

    r1873 r1874  
    11include "common/Values.ma".
    22include "joint/BEValues.ma".
    3 include "common/Mem.ma".
    43
    54(* Transform between lists of "back-end" (i.e., byte by byte) values and the
     
    76   resolve the sizes; they are not strictly checked. *)
    87
    9 let rec make_parts (r:region) (n:nat) (H:le n (size_pointer r)) on n : list (part r) ≝
    10 match n return λn.le n ? → ? with
    11 [ O ⇒ λ_. [ ]
    12 | S m ⇒ λH'. mk_part r n H::(make_parts r m ?)
     8let rec make_parts_aux (r:region) (n:nat) (H:lt n (size_pointer r)) (tl:list (part r)) on n : list (part r) ≝
     9match n return λn.lt n ? → ? with
     10[ O ⇒ λH'. (mk_part r O H')::tl
     11| S m ⇒ λH'. make_parts_aux r m ? ((mk_part r n H)::tl)
    1312] H.
    1413/2/
    1514qed.
    1615
    17 definition make_be_null : region → list beval
    18 λr. map ?? (λp. BVnull r p) (make_parts r (size_pointer r) ?).
     16definition make_parts : ∀r:region. list (part r)
     17λr. make_parts_aux r (pred (size_pointer r)) ? [ ].
    1918//
    2019qed.
     20
     21definition make_be_null : region → list beval ≝
     22λr. map ?? (λp. BVnull r p) (make_parts r).
    2123
    2224let rec bytes_of_bitvector (n:nat) (v:BitVector (times n 8)) : list Byte ≝
Note: See TracChangeset for help on using the changeset viewer.