Changeset 2717 for extracted/genMem.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (8 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/genMem.ml

    r2649 r2717  
    5656
    5757open Division
     58
     59open Exp
    5860
    5961open Arithmetic
     
    98100(** val block_contents_rect_Type4 :
    99101    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    100 let rec block_contents_rect_Type4 h_mk_block_contents x_4887 =
    101   let { low = low0; high = high0; contents = contents0 } = x_4887 in
     102let rec block_contents_rect_Type4 h_mk_block_contents x_6451 =
     103  let { low = low0; high = high0; contents = contents0 } = x_6451 in
    102104  h_mk_block_contents low0 high0 contents0
    103105
    104106(** val block_contents_rect_Type5 :
    105107    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    106 let rec block_contents_rect_Type5 h_mk_block_contents x_4889 =
    107   let { low = low0; high = high0; contents = contents0 } = x_4889 in
     108let rec block_contents_rect_Type5 h_mk_block_contents x_6453 =
     109  let { low = low0; high = high0; contents = contents0 } = x_6453 in
    108110  h_mk_block_contents low0 high0 contents0
    109111
    110112(** val block_contents_rect_Type3 :
    111113    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    112 let rec block_contents_rect_Type3 h_mk_block_contents x_4891 =
    113   let { low = low0; high = high0; contents = contents0 } = x_4891 in
     114let rec block_contents_rect_Type3 h_mk_block_contents x_6455 =
     115  let { low = low0; high = high0; contents = contents0 } = x_6455 in
    114116  h_mk_block_contents low0 high0 contents0
    115117
    116118(** val block_contents_rect_Type2 :
    117119    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    118 let rec block_contents_rect_Type2 h_mk_block_contents x_4893 =
    119   let { low = low0; high = high0; contents = contents0 } = x_4893 in
     120let rec block_contents_rect_Type2 h_mk_block_contents x_6457 =
     121  let { low = low0; high = high0; contents = contents0 } = x_6457 in
    120122  h_mk_block_contents low0 high0 contents0
    121123
    122124(** val block_contents_rect_Type1 :
    123125    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    124 let rec block_contents_rect_Type1 h_mk_block_contents x_4895 =
    125   let { low = low0; high = high0; contents = contents0 } = x_4895 in
     126let rec block_contents_rect_Type1 h_mk_block_contents x_6459 =
     127  let { low = low0; high = high0; contents = contents0 } = x_6459 in
    126128  h_mk_block_contents low0 high0 contents0
    127129
    128130(** val block_contents_rect_Type0 :
    129131    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    130 let rec block_contents_rect_Type0 h_mk_block_contents x_4897 =
    131   let { low = low0; high = high0; contents = contents0 } = x_4897 in
     132let rec block_contents_rect_Type0 h_mk_block_contents x_6461 =
     133  let { low = low0; high = high0; contents = contents0 } = x_6461 in
    132134  h_mk_block_contents low0 high0 contents0
    133135
     
    185187(** val mem_rect_Type4 :
    186188    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    187 let rec mem_rect_Type4 h_mk_mem x_4913 =
    188   let { blocks = blocks0; nextblock = nextblock0 } = x_4913 in
     189let rec mem_rect_Type4 h_mk_mem x_6477 =
     190  let { blocks = blocks0; nextblock = nextblock0 } = x_6477 in
    189191  h_mk_mem blocks0 nextblock0 __
    190192
    191193(** val mem_rect_Type5 :
    192194    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    193 let rec mem_rect_Type5 h_mk_mem x_4915 =
    194   let { blocks = blocks0; nextblock = nextblock0 } = x_4915 in
     195let rec mem_rect_Type5 h_mk_mem x_6479 =
     196  let { blocks = blocks0; nextblock = nextblock0 } = x_6479 in
    195197  h_mk_mem blocks0 nextblock0 __
    196198
    197199(** val mem_rect_Type3 :
    198200    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    199 let rec mem_rect_Type3 h_mk_mem x_4917 =
    200   let { blocks = blocks0; nextblock = nextblock0 } = x_4917 in
     201let rec mem_rect_Type3 h_mk_mem x_6481 =
     202  let { blocks = blocks0; nextblock = nextblock0 } = x_6481 in
    201203  h_mk_mem blocks0 nextblock0 __
    202204
    203205(** val mem_rect_Type2 :
    204206    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    205 let rec mem_rect_Type2 h_mk_mem x_4919 =
    206   let { blocks = blocks0; nextblock = nextblock0 } = x_4919 in
     207let rec mem_rect_Type2 h_mk_mem x_6483 =
     208  let { blocks = blocks0; nextblock = nextblock0 } = x_6483 in
    207209  h_mk_mem blocks0 nextblock0 __
    208210
    209211(** val mem_rect_Type1 :
    210212    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    211 let rec mem_rect_Type1 h_mk_mem x_4921 =
    212   let { blocks = blocks0; nextblock = nextblock0 } = x_4921 in
     213let rec mem_rect_Type1 h_mk_mem x_6485 =
     214  let { blocks = blocks0; nextblock = nextblock0 } = x_6485 in
    213215  h_mk_mem blocks0 nextblock0 __
    214216
    215217(** val mem_rect_Type0 :
    216218    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
    217 let rec mem_rect_Type0 h_mk_mem x_4923 =
    218   let { blocks = blocks0; nextblock = nextblock0 } = x_4923 in
     219let rec mem_rect_Type0 h_mk_mem x_6487 =
     220  let { blocks = blocks0; nextblock = nextblock0 } = x_6487 in
    219221  h_mk_mem blocks0 nextblock0 __
    220222
Note: See TracChangeset for help on using the changeset viewer.