Changeset 2743 for extracted/genMem.ml


Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (7 years ago)
Author:
sacerdot
Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/genMem.ml

    r2730 r2743  
    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_1100 =
    103   let { low = low0; high = high0; contents = contents0 } = x_1100 in
     102let rec block_contents_rect_Type4 h_mk_block_contents x_6477 =
     103  let { low = low0; high = high0; contents = contents0 } = x_6477 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_1102 =
    109   let { low = low0; high = high0; contents = contents0 } = x_1102 in
     108let rec block_contents_rect_Type5 h_mk_block_contents x_6479 =
     109  let { low = low0; high = high0; contents = contents0 } = x_6479 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_1104 =
    115   let { low = low0; high = high0; contents = contents0 } = x_1104 in
     114let rec block_contents_rect_Type3 h_mk_block_contents x_6481 =
     115  let { low = low0; high = high0; contents = contents0 } = x_6481 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_1106 =
    121   let { low = low0; high = high0; contents = contents0 } = x_1106 in
     120let rec block_contents_rect_Type2 h_mk_block_contents x_6483 =
     121  let { low = low0; high = high0; contents = contents0 } = x_6483 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_1108 =
    127   let { low = low0; high = high0; contents = contents0 } = x_1108 in
     126let rec block_contents_rect_Type1 h_mk_block_contents x_6485 =
     127  let { low = low0; high = high0; contents = contents0 } = x_6485 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_1110 =
    133   let { low = low0; high = high0; contents = contents0 } = x_1110 in
     132let rec block_contents_rect_Type0 h_mk_block_contents x_6487 =
     133  let { low = low0; high = high0; contents = contents0 } = x_6487 in
    134134  h_mk_block_contents low0 high0 contents0
    135135
     
    187187(** val mem_rect_Type4 :
    188188    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    189 let rec mem_rect_Type4 h_mk_mem x_1126 =
    190   let { blocks = blocks0; nextblock = nextblock0 } = x_1126 in
     189let rec mem_rect_Type4 h_mk_mem x_6503 =
     190  let { blocks = blocks0; nextblock = nextblock0 } = x_6503 in
    191191  h_mk_mem blocks0 nextblock0 __
    192192
    193193(** val mem_rect_Type5 :
    194194    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    195 let rec mem_rect_Type5 h_mk_mem x_1128 =
    196   let { blocks = blocks0; nextblock = nextblock0 } = x_1128 in
     195let rec mem_rect_Type5 h_mk_mem x_6505 =
     196  let { blocks = blocks0; nextblock = nextblock0 } = x_6505 in
    197197  h_mk_mem blocks0 nextblock0 __
    198198
    199199(** val mem_rect_Type3 :
    200200    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    201 let rec mem_rect_Type3 h_mk_mem x_1130 =
    202   let { blocks = blocks0; nextblock = nextblock0 } = x_1130 in
     201let rec mem_rect_Type3 h_mk_mem x_6507 =
     202  let { blocks = blocks0; nextblock = nextblock0 } = x_6507 in
    203203  h_mk_mem blocks0 nextblock0 __
    204204
    205205(** val mem_rect_Type2 :
    206206    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    207 let rec mem_rect_Type2 h_mk_mem x_1132 =
    208   let { blocks = blocks0; nextblock = nextblock0 } = x_1132 in
     207let rec mem_rect_Type2 h_mk_mem x_6509 =
     208  let { blocks = blocks0; nextblock = nextblock0 } = x_6509 in
    209209  h_mk_mem blocks0 nextblock0 __
    210210
    211211(** val mem_rect_Type1 :
    212212    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    213 let rec mem_rect_Type1 h_mk_mem x_1134 =
    214   let { blocks = blocks0; nextblock = nextblock0 } = x_1134 in
     213let rec mem_rect_Type1 h_mk_mem x_6511 =
     214  let { blocks = blocks0; nextblock = nextblock0 } = x_6511 in
    215215  h_mk_mem blocks0 nextblock0 __
    216216
    217217(** val mem_rect_Type0 :
    218218    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    219 let rec mem_rect_Type0 h_mk_mem x_1136 =
    220   let { blocks = blocks0; nextblock = nextblock0 } = x_1136 in
     219let rec mem_rect_Type0 h_mk_mem x_6513 =
     220  let { blocks = blocks0; nextblock = nextblock0 } = x_6513 in
    221221  h_mk_mem blocks0 nextblock0 __
    222222
Note: See TracChangeset for help on using the changeset viewer.