Changeset 2773 for extracted/genMem.ml


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (8 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/genMem.ml

    r2743 r2773  
    4141open Errors
    4242
     43open Lists
     44
     45open Identifiers
     46
     47open Integers
     48
     49open AST
     50
     51open Division
     52
     53open Exp
     54
     55open Arithmetic
     56
    4357open Setoids
    4458
     
    4761open Option
    4862
    49 open Lists
    50 
    51 open Identifiers
    52 
    53 open Integers
    54 
    55 open AST
    56 
    57 open Division
    58 
    59 open Exp
    60 
    61 open Arithmetic
    62 
    6363open Extranat
    6464
     
    8181open ByteValues
    8282
    83 (** val update1 : Z.z -> 'a1 -> (Z.z -> 'a1) -> Z.z -> 'a1 **)
    84 let update1 x v f y =
     83(** val update : Z.z -> 'a1 -> (Z.z -> 'a1) -> Z.z -> 'a1 **)
     84let update x v f y =
    8585  match Z.eqZb y x with
    8686  | Bool.True -> v
     
    100100(** val block_contents_rect_Type4 :
    101101    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    102 let rec block_contents_rect_Type4 h_mk_block_contents x_6477 =
    103   let { low = low0; high = high0; contents = contents0 } = x_6477 in
     102let rec block_contents_rect_Type4 h_mk_block_contents x_4781 =
     103  let { low = low0; high = high0; contents = contents0 } = x_4781 in
    104104  h_mk_block_contents low0 high0 contents0
    105105
    106106(** val block_contents_rect_Type5 :
    107107    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    108 let rec block_contents_rect_Type5 h_mk_block_contents x_6479 =
    109   let { low = low0; high = high0; contents = contents0 } = x_6479 in
     108let rec block_contents_rect_Type5 h_mk_block_contents x_4783 =
     109  let { low = low0; high = high0; contents = contents0 } = x_4783 in
    110110  h_mk_block_contents low0 high0 contents0
    111111
    112112(** val block_contents_rect_Type3 :
    113113    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    114 let rec block_contents_rect_Type3 h_mk_block_contents x_6481 =
    115   let { low = low0; high = high0; contents = contents0 } = x_6481 in
     114let rec block_contents_rect_Type3 h_mk_block_contents x_4785 =
     115  let { low = low0; high = high0; contents = contents0 } = x_4785 in
    116116  h_mk_block_contents low0 high0 contents0
    117117
    118118(** val block_contents_rect_Type2 :
    119119    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    120 let rec block_contents_rect_Type2 h_mk_block_contents x_6483 =
    121   let { low = low0; high = high0; contents = contents0 } = x_6483 in
     120let rec block_contents_rect_Type2 h_mk_block_contents x_4787 =
     121  let { low = low0; high = high0; contents = contents0 } = x_4787 in
    122122  h_mk_block_contents low0 high0 contents0
    123123
    124124(** val block_contents_rect_Type1 :
    125125    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    126 let rec block_contents_rect_Type1 h_mk_block_contents x_6485 =
    127   let { low = low0; high = high0; contents = contents0 } = x_6485 in
     126let rec block_contents_rect_Type1 h_mk_block_contents x_4789 =
     127  let { low = low0; high = high0; contents = contents0 } = x_4789 in
    128128  h_mk_block_contents low0 high0 contents0
    129129
    130130(** val block_contents_rect_Type0 :
    131131    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    132 let rec block_contents_rect_Type0 h_mk_block_contents x_6487 =
    133   let { low = low0; high = high0; contents = contents0 } = x_6487 in
     132let rec block_contents_rect_Type0 h_mk_block_contents x_4791 =
     133  let { low = low0; high = high0; contents = contents0 } = x_4791 in
    134134  h_mk_block_contents low0 high0 contents0
    135135
     
    183183    Obj.magic (fun _ dH -> dH __ __ __)) y
    184184
    185 type mem1 = { blocks : (Pointers.block -> block_contents); nextblock : Z.z }
     185type mem = { blocks : (Pointers.block -> block_contents); nextblock : Z.z }
    186186
    187187(** val mem_rect_Type4 :
    188     ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    189 let rec mem_rect_Type4 h_mk_mem x_6503 =
    190   let { blocks = blocks0; nextblock = nextblock0 } = x_6503 in
     188    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
     189let rec mem_rect_Type4 h_mk_mem x_4807 =
     190  let { blocks = blocks0; nextblock = nextblock0 } = x_4807 in
    191191  h_mk_mem blocks0 nextblock0 __
    192192
    193193(** val mem_rect_Type5 :
    194     ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    195 let rec mem_rect_Type5 h_mk_mem x_6505 =
    196   let { blocks = blocks0; nextblock = nextblock0 } = x_6505 in
     194    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
     195let rec mem_rect_Type5 h_mk_mem x_4809 =
     196  let { blocks = blocks0; nextblock = nextblock0 } = x_4809 in
    197197  h_mk_mem blocks0 nextblock0 __
    198198
    199199(** val mem_rect_Type3 :
    200     ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    201 let rec mem_rect_Type3 h_mk_mem x_6507 =
    202   let { blocks = blocks0; nextblock = nextblock0 } = x_6507 in
     200    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
     201let rec mem_rect_Type3 h_mk_mem x_4811 =
     202  let { blocks = blocks0; nextblock = nextblock0 } = x_4811 in
    203203  h_mk_mem blocks0 nextblock0 __
    204204
    205205(** val mem_rect_Type2 :
    206     ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    207 let rec mem_rect_Type2 h_mk_mem x_6509 =
    208   let { blocks = blocks0; nextblock = nextblock0 } = x_6509 in
     206    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
     207let rec mem_rect_Type2 h_mk_mem x_4813 =
     208  let { blocks = blocks0; nextblock = nextblock0 } = x_4813 in
    209209  h_mk_mem blocks0 nextblock0 __
    210210
    211211(** val mem_rect_Type1 :
    212     ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    213 let rec mem_rect_Type1 h_mk_mem x_6511 =
    214   let { blocks = blocks0; nextblock = nextblock0 } = x_6511 in
     212    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
     213let rec mem_rect_Type1 h_mk_mem x_4815 =
     214  let { blocks = blocks0; nextblock = nextblock0 } = x_4815 in
    215215  h_mk_mem blocks0 nextblock0 __
    216216
    217217(** val mem_rect_Type0 :
    218     ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    219 let rec mem_rect_Type0 h_mk_mem x_6513 =
    220   let { blocks = blocks0; nextblock = nextblock0 } = x_6513 in
    221   h_mk_mem blocks0 nextblock0 __
    222 
    223 (** val blocks : mem1 -> Pointers.block -> block_contents **)
     218    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
     219let rec mem_rect_Type0 h_mk_mem x_4817 =
     220  let { blocks = blocks0; nextblock = nextblock0 } = x_4817 in
     221  h_mk_mem blocks0 nextblock0 __
     222
     223(** val blocks : mem -> Pointers.block -> block_contents **)
    224224let rec blocks xxx =
    225225  xxx.blocks
    226226
    227 (** val nextblock : mem1 -> Z.z **)
     227(** val nextblock : mem -> Z.z **)
    228228let rec nextblock xxx =
    229229  xxx.nextblock
    230230
    231231(** val mem_inv_rect_Type4 :
    232     mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
     232    mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
    233233    'a1 **)
    234234let mem_inv_rect_Type4 hterm h1 =
     
    236236
    237237(** val mem_inv_rect_Type3 :
    238     mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
     238    mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
    239239    'a1 **)
    240240let mem_inv_rect_Type3 hterm h1 =
     
    242242
    243243(** val mem_inv_rect_Type2 :
    244     mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
     244    mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
    245245    'a1 **)
    246246let mem_inv_rect_Type2 hterm h1 =
     
    248248
    249249(** val mem_inv_rect_Type1 :
    250     mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
     250    mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
    251251    'a1 **)
    252252let mem_inv_rect_Type1 hterm h1 =
     
    254254
    255255(** val mem_inv_rect_Type0 :
    256     mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
     256    mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
    257257    'a1 **)
    258258let mem_inv_rect_Type0 hterm h1 =
    259259  let hcut = mem_rect_Type0 h1 hterm in hcut __
    260260
    261 (** val mem_discr : mem1 -> mem1 -> __ **)
     261(** val mem_discr : mem -> mem -> __ **)
    262262let mem_discr x y =
    263263  Logic.eq_rect_Type2 x
     
    265265    Obj.magic (fun _ dH -> dH __ __ __)) y
    266266
    267 (** val mem_jmdiscr : mem1 -> mem1 -> __ **)
     267(** val mem_jmdiscr : mem -> mem -> __ **)
    268268let mem_jmdiscr x y =
    269269  Logic.eq_rect_Type2 x
     
    279279  { low = lo; high = hi; contents = (fun y -> ByteValues.BVundef) }
    280280
    281 (** val empty : mem1 **)
     281(** val empty : mem **)
    282282let empty =
    283283  { blocks = (fun x -> empty_block Z.OZ Z.OZ); nextblock = (Z.Pos
    284284    Positive.One) }
    285285
    286 (** val alloc : mem1 -> Z.z -> Z.z -> (mem1, Pointers.block) Types.prod **)
     286(** val alloc : mem -> Z.z -> Z.z -> (mem, Pointers.block) Types.prod **)
    287287let rec alloc m lo hi =
    288288  let b = m.nextblock in
     
    290290  nextblock = (Z.zsucc m.nextblock) }; Types.snd = b }
    291291
    292 (** val free : mem1 -> Pointers.block -> mem1 **)
     292(** val free : mem -> Pointers.block -> mem **)
    293293let free m b =
    294294  { blocks =
     
    296296    nextblock = m.nextblock }
    297297
    298 (** val free_list : mem1 -> Pointers.block List.list -> mem1 **)
     298(** val free_list : mem -> Pointers.block List.list -> mem **)
    299299let free_list m l =
    300300  List.foldr (fun b m0 -> free m0 b) m l
    301301
    302 (** val low_bound : mem1 -> Pointers.block -> Z.z **)
     302(** val low_bound : mem -> Pointers.block -> Z.z **)
    303303let low_bound m b =
    304304  (m.blocks b).low
    305305
    306 (** val high_bound : mem1 -> Pointers.block -> Z.z **)
     306(** val high_bound : mem -> Pointers.block -> Z.z **)
    307307let high_bound m b =
    308308  (m.blocks b).high
    309309
    310 (** val block_region0 : mem1 -> Pointers.block -> AST.region **)
    311 let block_region0 m b =
     310(** val block_region : mem -> Pointers.block -> AST.region **)
     311let block_region m b =
    312312  Pointers.block_region b
    313313
    314314(** val do_if_in_bounds :
    315     mem1 -> Pointers.pointer -> (Pointers.block -> block_contents -> Z.z ->
     315    mem -> Pointers.pointer -> (Pointers.block -> block_contents -> Z.z ->
    316316    'a1) -> 'a1 Types.option **)
    317317let do_if_in_bounds m ptr f =
     
    330330
    331331(** val beloadv :
    332     mem1 -> Pointers.pointer -> ByteValues.beval Types.option **)
     332    mem -> Pointers.pointer -> ByteValues.beval Types.option **)
    333333let beloadv m ptr =
    334334  do_if_in_bounds m ptr (fun b content off -> content.contents off)
    335335
    336336(** val bestorev :
    337     mem1 -> Pointers.pointer -> ByteValues.beval -> mem1 Types.option **)
     337    mem -> Pointers.pointer -> ByteValues.beval -> mem Types.option **)
    338338let bestorev m ptr v =
    339339  do_if_in_bounds m ptr (fun b content off ->
    340     let contents0 = update1 off v content.contents in
     340    let contents0 = update off v content.contents in
    341341    let content0 = { low = content.low; high = content.high; contents =
    342342      contents0 }
Note: See TracChangeset for help on using the changeset viewer.