Changeset 2773 for extracted/pointers.ml


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 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/pointers.ml

    r2743 r2773  
    77open Arithmetic
    88
     9open Setoids
     10
     11open Monad
     12
     13open Option
     14
    915open Extranat
    1016
     
    6066
    6167open Extralib
    62 
    63 open Setoids
    64 
    65 open Monad
    66 
    67 open Option
    6868
    6969open Lists
     
    8080
    8181(** val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1 **)
    82 let rec block_rect_Type4 h_mk_block x_4976 =
    83   let block_id = x_4976 in h_mk_block block_id
     82let rec block_rect_Type4 h_mk_block x_4326 =
     83  let block_id = x_4326 in h_mk_block block_id
    8484
    8585(** val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1 **)
    86 let rec block_rect_Type5 h_mk_block x_4978 =
    87   let block_id = x_4978 in h_mk_block block_id
     86let rec block_rect_Type5 h_mk_block x_4328 =
     87  let block_id = x_4328 in h_mk_block block_id
    8888
    8989(** val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1 **)
    90 let rec block_rect_Type3 h_mk_block x_4980 =
    91   let block_id = x_4980 in h_mk_block block_id
     90let rec block_rect_Type3 h_mk_block x_4330 =
     91  let block_id = x_4330 in h_mk_block block_id
    9292
    9393(** val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1 **)
    94 let rec block_rect_Type2 h_mk_block x_4982 =
    95   let block_id = x_4982 in h_mk_block block_id
     94let rec block_rect_Type2 h_mk_block x_4332 =
     95  let block_id = x_4332 in h_mk_block block_id
    9696
    9797(** val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1 **)
    98 let rec block_rect_Type1 h_mk_block x_4984 =
    99   let block_id = x_4984 in h_mk_block block_id
     98let rec block_rect_Type1 h_mk_block x_4334 =
     99  let block_id = x_4334 in h_mk_block block_id
    100100
    101101(** val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1 **)
    102 let rec block_rect_Type0 h_mk_block x_4986 =
    103   let block_id = x_4986 in h_mk_block block_id
     102let rec block_rect_Type0 h_mk_block x_4336 =
     103  let block_id = x_4336 in h_mk_block block_id
    104104
    105105(** val block_id : block -> Z.z **)
     
    163163
    164164(** val offset_rect_Type4 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    165 let rec offset_rect_Type4 h_mk_offset x_5002 =
    166   let offv = x_5002 in h_mk_offset offv
     165let rec offset_rect_Type4 h_mk_offset x_4352 =
     166  let offv = x_4352 in h_mk_offset offv
    167167
    168168(** val offset_rect_Type5 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    169 let rec offset_rect_Type5 h_mk_offset x_5004 =
    170   let offv = x_5004 in h_mk_offset offv
     169let rec offset_rect_Type5 h_mk_offset x_4354 =
     170  let offv = x_4354 in h_mk_offset offv
    171171
    172172(** val offset_rect_Type3 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    173 let rec offset_rect_Type3 h_mk_offset x_5006 =
    174   let offv = x_5006 in h_mk_offset offv
     173let rec offset_rect_Type3 h_mk_offset x_4356 =
     174  let offv = x_4356 in h_mk_offset offv
    175175
    176176(** val offset_rect_Type2 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    177 let rec offset_rect_Type2 h_mk_offset x_5008 =
    178   let offv = x_5008 in h_mk_offset offv
     177let rec offset_rect_Type2 h_mk_offset x_4358 =
     178  let offv = x_4358 in h_mk_offset offv
    179179
    180180(** val offset_rect_Type1 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    181 let rec offset_rect_Type1 h_mk_offset x_5010 =
    182   let offv = x_5010 in h_mk_offset offv
     181let rec offset_rect_Type1 h_mk_offset x_4360 =
     182  let offv = x_4360 in h_mk_offset offv
    183183
    184184(** val offset_rect_Type0 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    185 let rec offset_rect_Type0 h_mk_offset x_5012 =
    186   let offv = x_5012 in h_mk_offset offv
     185let rec offset_rect_Type0 h_mk_offset x_4362 =
     186  let offv = x_4362 in h_mk_offset offv
    187187
    188188(** val offv : offset -> BitVector.bitVector **)
     
    228228
    229229(** val offset_of_Z : Z.z -> offset **)
    230 let offset_of_Z z0 =
    231   BitVectorZ.bitvector_of_Z offset_size z0
     230let offset_of_Z z =
     231  BitVectorZ.bitvector_of_Z offset_size z
    232232
    233233(** val shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset **)
     
    280280
    281281(** val pointer_rect_Type4 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    282 let rec pointer_rect_Type4 h_mk_pointer x_5028 =
    283   let { pblock = pblock0; poff = poff0 } = x_5028 in
     282let rec pointer_rect_Type4 h_mk_pointer x_4378 =
     283  let { pblock = pblock0; poff = poff0 } = x_4378 in
    284284  h_mk_pointer pblock0 poff0
    285285
    286286(** val pointer_rect_Type5 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    287 let rec pointer_rect_Type5 h_mk_pointer x_5030 =
    288   let { pblock = pblock0; poff = poff0 } = x_5030 in
     287let rec pointer_rect_Type5 h_mk_pointer x_4380 =
     288  let { pblock = pblock0; poff = poff0 } = x_4380 in
    289289  h_mk_pointer pblock0 poff0
    290290
    291291(** val pointer_rect_Type3 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    292 let rec pointer_rect_Type3 h_mk_pointer x_5032 =
    293   let { pblock = pblock0; poff = poff0 } = x_5032 in
     292let rec pointer_rect_Type3 h_mk_pointer x_4382 =
     293  let { pblock = pblock0; poff = poff0 } = x_4382 in
    294294  h_mk_pointer pblock0 poff0
    295295
    296296(** val pointer_rect_Type2 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    297 let rec pointer_rect_Type2 h_mk_pointer x_5034 =
    298   let { pblock = pblock0; poff = poff0 } = x_5034 in
     297let rec pointer_rect_Type2 h_mk_pointer x_4384 =
     298  let { pblock = pblock0; poff = poff0 } = x_4384 in
    299299  h_mk_pointer pblock0 poff0
    300300
    301301(** val pointer_rect_Type1 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    302 let rec pointer_rect_Type1 h_mk_pointer x_5036 =
    303   let { pblock = pblock0; poff = poff0 } = x_5036 in
     302let rec pointer_rect_Type1 h_mk_pointer x_4386 =
     303  let { pblock = pblock0; poff = poff0 } = x_4386 in
    304304  h_mk_pointer pblock0 poff0
    305305
    306306(** val pointer_rect_Type0 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    307 let rec pointer_rect_Type0 h_mk_pointer x_5038 =
    308   let { pblock = pblock0; poff = poff0 } = x_5038 in
     307let rec pointer_rect_Type0 h_mk_pointer x_4388 =
     308  let { pblock = pblock0; poff = poff0 } = x_4388 in
    309309  h_mk_pointer pblock0 poff0
    310310
     
    381381
    382382(** val eq_pointer : pointer -> pointer -> Bool.bool **)
    383 let eq_pointer p3 p4 =
    384   Bool.andb (eq_block p3.pblock p4.pblock) (eq_offset p3.poff p4.poff)
    385 
     383let eq_pointer p1 p2 =
     384  Bool.andb (eq_block p1.pblock p2.pblock) (eq_offset p1.poff p2.poff)
     385
Note: See TracChangeset for help on using the changeset viewer.