Changeset 2649 for extracted/genMem.ml


Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/genMem.ml

    r2601 r2649  
    3535open Deqsets
    3636
     37open ErrorMessages
     38
    3739open PreIdentifiers
    3840
     
    4951open Identifiers
    5052
    51 open Coqlib
    52 
    53 open Floats
    54 
    5553open Integers
    5654
     
    6058
    6159open Arithmetic
    62 
    63 open Char
    64 
    65 open String
    6660
    6761open Extranat
     
    10498(** val block_contents_rect_Type4 :
    10599    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    106 let rec block_contents_rect_Type4 h_mk_block_contents x_5450 =
    107   let { low = low0; high = high0; contents = contents0 } = x_5450 in
     100let rec block_contents_rect_Type4 h_mk_block_contents x_4887 =
     101  let { low = low0; high = high0; contents = contents0 } = x_4887 in
    108102  h_mk_block_contents low0 high0 contents0
    109103
    110104(** val block_contents_rect_Type5 :
    111105    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    112 let rec block_contents_rect_Type5 h_mk_block_contents x_5452 =
    113   let { low = low0; high = high0; contents = contents0 } = x_5452 in
     106let rec block_contents_rect_Type5 h_mk_block_contents x_4889 =
     107  let { low = low0; high = high0; contents = contents0 } = x_4889 in
    114108  h_mk_block_contents low0 high0 contents0
    115109
    116110(** val block_contents_rect_Type3 :
    117111    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    118 let rec block_contents_rect_Type3 h_mk_block_contents x_5454 =
    119   let { low = low0; high = high0; contents = contents0 } = x_5454 in
     112let rec block_contents_rect_Type3 h_mk_block_contents x_4891 =
     113  let { low = low0; high = high0; contents = contents0 } = x_4891 in
    120114  h_mk_block_contents low0 high0 contents0
    121115
    122116(** val block_contents_rect_Type2 :
    123117    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    124 let rec block_contents_rect_Type2 h_mk_block_contents x_5456 =
    125   let { low = low0; high = high0; contents = contents0 } = x_5456 in
     118let rec block_contents_rect_Type2 h_mk_block_contents x_4893 =
     119  let { low = low0; high = high0; contents = contents0 } = x_4893 in
    126120  h_mk_block_contents low0 high0 contents0
    127121
    128122(** val block_contents_rect_Type1 :
    129123    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    130 let rec block_contents_rect_Type1 h_mk_block_contents x_5458 =
    131   let { low = low0; high = high0; contents = contents0 } = x_5458 in
     124let rec block_contents_rect_Type1 h_mk_block_contents x_4895 =
     125  let { low = low0; high = high0; contents = contents0 } = x_4895 in
    132126  h_mk_block_contents low0 high0 contents0
    133127
    134128(** val block_contents_rect_Type0 :
    135129    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    136 let rec block_contents_rect_Type0 h_mk_block_contents x_5460 =
    137   let { low = low0; high = high0; contents = contents0 } = x_5460 in
     130let rec block_contents_rect_Type0 h_mk_block_contents x_4897 =
     131  let { low = low0; high = high0; contents = contents0 } = x_4897 in
    138132  h_mk_block_contents low0 high0 contents0
    139133
     
    191185(** val mem_rect_Type4 :
    192186    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    193 let rec mem_rect_Type4 h_mk_mem x_5476 =
    194   let { blocks = blocks0; nextblock = nextblock0 } = x_5476 in
     187let rec mem_rect_Type4 h_mk_mem x_4913 =
     188  let { blocks = blocks0; nextblock = nextblock0 } = x_4913 in
    195189  h_mk_mem blocks0 nextblock0 __
    196190
    197191(** val mem_rect_Type5 :
    198192    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    199 let rec mem_rect_Type5 h_mk_mem x_5478 =
    200   let { blocks = blocks0; nextblock = nextblock0 } = x_5478 in
     193let rec mem_rect_Type5 h_mk_mem x_4915 =
     194  let { blocks = blocks0; nextblock = nextblock0 } = x_4915 in
    201195  h_mk_mem blocks0 nextblock0 __
    202196
    203197(** val mem_rect_Type3 :
    204198    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    205 let rec mem_rect_Type3 h_mk_mem x_5480 =
    206   let { blocks = blocks0; nextblock = nextblock0 } = x_5480 in
     199let rec mem_rect_Type3 h_mk_mem x_4917 =
     200  let { blocks = blocks0; nextblock = nextblock0 } = x_4917 in
    207201  h_mk_mem blocks0 nextblock0 __
    208202
    209203(** val mem_rect_Type2 :
    210204    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    211 let rec mem_rect_Type2 h_mk_mem x_5482 =
    212   let { blocks = blocks0; nextblock = nextblock0 } = x_5482 in
     205let rec mem_rect_Type2 h_mk_mem x_4919 =
     206  let { blocks = blocks0; nextblock = nextblock0 } = x_4919 in
    213207  h_mk_mem blocks0 nextblock0 __
    214208
    215209(** val mem_rect_Type1 :
    216210    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    217 let rec mem_rect_Type1 h_mk_mem x_5484 =
    218   let { blocks = blocks0; nextblock = nextblock0 } = x_5484 in
     211let rec mem_rect_Type1 h_mk_mem x_4921 =
     212  let { blocks = blocks0; nextblock = nextblock0 } = x_4921 in
    219213  h_mk_mem blocks0 nextblock0 __
    220214
    221215(** val mem_rect_Type0 :
    222216    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    223 let rec mem_rect_Type0 h_mk_mem x_5486 =
    224   let { blocks = blocks0; nextblock = nextblock0 } = x_5486 in
     217let rec mem_rect_Type0 h_mk_mem x_4923 =
     218  let { blocks = blocks0; nextblock = nextblock0 } = x_4923 in
    225219  h_mk_mem blocks0 nextblock0 __
    226220
     
    288282    Positive.One) }
    289283
    290 (** val alloc :
    291     mem1 -> Z.z -> Z.z -> AST.region -> (mem1, Pointers.block Types.sig0)
    292     Types.prod **)
    293 let rec alloc m lo hi r =
    294   let b = { Pointers.block_region = r; Pointers.block_id = m.nextblock } in
     284(** val alloc : mem1 -> Z.z -> Z.z -> (mem1, Pointers.block) Types.prod **)
     285let rec alloc m lo hi =
     286  let b = m.nextblock in
    295287  { Types.fst = { blocks = (update_block b (empty_block lo hi) m.blocks);
    296288  nextblock = (Z.zsucc m.nextblock) }; Types.snd = b }
     
    316308(** val block_region0 : mem1 -> Pointers.block -> AST.region **)
    317309let block_region0 m b =
    318   b.Pointers.block_region
     310  Pointers.block_region b
    319311
    320312(** val do_if_in_bounds :
     
    323315let do_if_in_bounds m ptr f =
    324316  let b = ptr.Pointers.pblock in
    325   (match Z.zltb b.Pointers.block_id m.nextblock with
     317  (match Z.zltb (Pointers.block_id b) m.nextblock with
    326318   | Bool.True ->
    327319     let content = m.blocks b in
Note: See TracChangeset for help on using the changeset viewer.