Changeset 2717 for extracted/pointers.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 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/pointers.ml

    r2649 r2717  
    22
    33open Division
     4
     5open Exp
    46
    57open Arithmetic
     
    7880
    7981(** val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1 **)
    80 let rec block_rect_Type4 h_mk_block x_2388 =
    81   let block_id = x_2388 in h_mk_block block_id
     82let rec block_rect_Type4 h_mk_block x_4950 =
     83  let block_id = x_4950 in h_mk_block block_id
    8284
    8385(** val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1 **)
    84 let rec block_rect_Type5 h_mk_block x_2390 =
    85   let block_id = x_2390 in h_mk_block block_id
     86let rec block_rect_Type5 h_mk_block x_4952 =
     87  let block_id = x_4952 in h_mk_block block_id
    8688
    8789(** val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1 **)
    88 let rec block_rect_Type3 h_mk_block x_2392 =
    89   let block_id = x_2392 in h_mk_block block_id
     90let rec block_rect_Type3 h_mk_block x_4954 =
     91  let block_id = x_4954 in h_mk_block block_id
    9092
    9193(** val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1 **)
    92 let rec block_rect_Type2 h_mk_block x_2394 =
    93   let block_id = x_2394 in h_mk_block block_id
     94let rec block_rect_Type2 h_mk_block x_4956 =
     95  let block_id = x_4956 in h_mk_block block_id
    9496
    9597(** val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1 **)
    96 let rec block_rect_Type1 h_mk_block x_2396 =
    97   let block_id = x_2396 in h_mk_block block_id
     98let rec block_rect_Type1 h_mk_block x_4958 =
     99  let block_id = x_4958 in h_mk_block block_id
    98100
    99101(** val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1 **)
    100 let rec block_rect_Type0 h_mk_block x_2398 =
    101   let block_id = x_2398 in h_mk_block block_id
     102let rec block_rect_Type0 h_mk_block x_4960 =
     103  let block_id = x_4960 in h_mk_block block_id
    102104
    103105(** val block_id : block -> Z.z **)
     
    161163
    162164(** val offset_rect_Type4 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    163 let rec offset_rect_Type4 h_mk_offset x_2414 =
    164   let offv = x_2414 in h_mk_offset offv
     165let rec offset_rect_Type4 h_mk_offset x_4976 =
     166  let offv = x_4976 in h_mk_offset offv
    165167
    166168(** val offset_rect_Type5 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    167 let rec offset_rect_Type5 h_mk_offset x_2416 =
    168   let offv = x_2416 in h_mk_offset offv
     169let rec offset_rect_Type5 h_mk_offset x_4978 =
     170  let offv = x_4978 in h_mk_offset offv
    169171
    170172(** val offset_rect_Type3 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    171 let rec offset_rect_Type3 h_mk_offset x_2418 =
    172   let offv = x_2418 in h_mk_offset offv
     173let rec offset_rect_Type3 h_mk_offset x_4980 =
     174  let offv = x_4980 in h_mk_offset offv
    173175
    174176(** val offset_rect_Type2 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    175 let rec offset_rect_Type2 h_mk_offset x_2420 =
    176   let offv = x_2420 in h_mk_offset offv
     177let rec offset_rect_Type2 h_mk_offset x_4982 =
     178  let offv = x_4982 in h_mk_offset offv
    177179
    178180(** val offset_rect_Type1 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    179 let rec offset_rect_Type1 h_mk_offset x_2422 =
    180   let offv = x_2422 in h_mk_offset offv
     181let rec offset_rect_Type1 h_mk_offset x_4984 =
     182  let offv = x_4984 in h_mk_offset offv
    181183
    182184(** val offset_rect_Type0 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    183 let rec offset_rect_Type0 h_mk_offset x_2424 =
    184   let offv = x_2424 in h_mk_offset offv
     185let rec offset_rect_Type0 h_mk_offset x_4986 =
     186  let offv = x_4986 in h_mk_offset offv
    185187
    186188(** val offv : offset -> BitVector.bitVector **)
     
    278280
    279281(** val pointer_rect_Type4 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    280 let rec pointer_rect_Type4 h_mk_pointer x_2440 =
    281   let { pblock = pblock0; poff = poff0 } = x_2440 in
     282let rec pointer_rect_Type4 h_mk_pointer x_5002 =
     283  let { pblock = pblock0; poff = poff0 } = x_5002 in
    282284  h_mk_pointer pblock0 poff0
    283285
    284286(** val pointer_rect_Type5 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    285 let rec pointer_rect_Type5 h_mk_pointer x_2442 =
    286   let { pblock = pblock0; poff = poff0 } = x_2442 in
     287let rec pointer_rect_Type5 h_mk_pointer x_5004 =
     288  let { pblock = pblock0; poff = poff0 } = x_5004 in
    287289  h_mk_pointer pblock0 poff0
    288290
    289291(** val pointer_rect_Type3 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    290 let rec pointer_rect_Type3 h_mk_pointer x_2444 =
    291   let { pblock = pblock0; poff = poff0 } = x_2444 in
     292let rec pointer_rect_Type3 h_mk_pointer x_5006 =
     293  let { pblock = pblock0; poff = poff0 } = x_5006 in
    292294  h_mk_pointer pblock0 poff0
    293295
    294296(** val pointer_rect_Type2 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    295 let rec pointer_rect_Type2 h_mk_pointer x_2446 =
    296   let { pblock = pblock0; poff = poff0 } = x_2446 in
     297let rec pointer_rect_Type2 h_mk_pointer x_5008 =
     298  let { pblock = pblock0; poff = poff0 } = x_5008 in
    297299  h_mk_pointer pblock0 poff0
    298300
    299301(** val pointer_rect_Type1 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    300 let rec pointer_rect_Type1 h_mk_pointer x_2448 =
    301   let { pblock = pblock0; poff = poff0 } = x_2448 in
     302let rec pointer_rect_Type1 h_mk_pointer x_5010 =
     303  let { pblock = pblock0; poff = poff0 } = x_5010 in
    302304  h_mk_pointer pblock0 poff0
    303305
    304306(** val pointer_rect_Type0 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    305 let rec pointer_rect_Type0 h_mk_pointer x_2450 =
    306   let { pblock = pblock0; poff = poff0 } = x_2450 in
     307let rec pointer_rect_Type0 h_mk_pointer x_5012 =
     308  let { pblock = pblock0; poff = poff0 } = x_5012 in
    307309  h_mk_pointer pblock0 poff0
    308310
Note: See TracChangeset for help on using the changeset viewer.