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/byteValues.ml

    r2743 r2773  
    1515open Extralib
    1616
     17open Lists
     18
     19open Identifiers
     20
     21open Integers
     22
     23open AST
     24
     25open Division
     26
     27open Exp
     28
     29open Arithmetic
     30
    1731open Setoids
    1832
     
    2034
    2135open Option
    22 
    23 open Lists
    24 
    25 open Identifiers
    26 
    27 open Integers
    28 
    29 open AST
    30 
    31 open Division
    32 
    33 open Exp
    34 
    35 open Arithmetic
    3636
    3737open Extranat
     
    8989    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    9090    'a1 **)
    91 let rec program_counter_rect_Type4 h_mk_program_counter x_6100 =
    92   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6100 in
     91let rec program_counter_rect_Type4 h_mk_program_counter x_4404 =
     92  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4404 in
    9393  h_mk_program_counter pc_block0 pc_offset0
    9494
     
    9696    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    9797    'a1 **)
    98 let rec program_counter_rect_Type5 h_mk_program_counter x_6102 =
    99   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6102 in
     98let rec program_counter_rect_Type5 h_mk_program_counter x_4406 =
     99  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4406 in
    100100  h_mk_program_counter pc_block0 pc_offset0
    101101
     
    103103    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    104104    'a1 **)
    105 let rec program_counter_rect_Type3 h_mk_program_counter x_6104 =
    106   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6104 in
     105let rec program_counter_rect_Type3 h_mk_program_counter x_4408 =
     106  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4408 in
    107107  h_mk_program_counter pc_block0 pc_offset0
    108108
     
    110110    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    111111    'a1 **)
    112 let rec program_counter_rect_Type2 h_mk_program_counter x_6106 =
    113   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6106 in
     112let rec program_counter_rect_Type2 h_mk_program_counter x_4410 =
     113  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4410 in
    114114  h_mk_program_counter pc_block0 pc_offset0
    115115
     
    117117    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    118118    'a1 **)
    119 let rec program_counter_rect_Type1 h_mk_program_counter x_6108 =
    120   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6108 in
     119let rec program_counter_rect_Type1 h_mk_program_counter x_4412 =
     120  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4412 in
    121121  h_mk_program_counter pc_block0 pc_offset0
    122122
     
    124124    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    125125    'a1 **)
    126 let rec program_counter_rect_Type0 h_mk_program_counter x_6110 =
    127   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6110 in
     126let rec program_counter_rect_Type0 h_mk_program_counter x_4414 =
     127  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4414 in
    128128  h_mk_program_counter pc_block0 pc_offset0
    129129
     
    184184  Bool.andb
    185185    (Pointers.eq_block (Types.pi1 pc1.pc_block) (Types.pi1 pc2.pc_block))
    186     (Positive.eqb0 pc1.pc_offset pc2.pc_offset)
     186    (Positive.eqb pc1.pc_offset pc2.pc_offset)
    187187
    188188(** val bitvector_from_pos :
     
    202202let cpointer_of_pc pc =
    203203  let pc_off = pc.pc_offset in
    204   (match Positive.leb0 pc_off (Positive.two_power_nat Pointers.offset_size) with
     204  (match Positive.leb pc_off (Positive.two_power_nat Pointers.offset_size) with
    205205   | Bool.True ->
    206206     Obj.magic
    207        (Monad.m_return0 (Monad.max_def Option.option0) { Pointers.pblock =
     207       (Monad.m_return0 (Monad.max_def Option.option) { Pointers.pblock =
    208208         (Types.pi1 pc.pc_block); Pointers.poff =
    209209         (bitvector_from_pos Pointers.offset_size pc_off) })
     
    215215
    216216(** val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    217 let rec part_rect_Type4 h_mk_part x_6126 =
    218   let part_no = x_6126 in h_mk_part part_no __
     217let rec part_rect_Type4 h_mk_part x_4430 =
     218  let part_no = x_4430 in h_mk_part part_no __
    219219
    220220(** val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    221 let rec part_rect_Type5 h_mk_part x_6128 =
    222   let part_no = x_6128 in h_mk_part part_no __
     221let rec part_rect_Type5 h_mk_part x_4432 =
     222  let part_no = x_4432 in h_mk_part part_no __
    223223
    224224(** val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    225 let rec part_rect_Type3 h_mk_part x_6130 =
    226   let part_no = x_6130 in h_mk_part part_no __
     225let rec part_rect_Type3 h_mk_part x_4434 =
     226  let part_no = x_4434 in h_mk_part part_no __
    227227
    228228(** val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    229 let rec part_rect_Type2 h_mk_part x_6132 =
    230   let part_no = x_6132 in h_mk_part part_no __
     229let rec part_rect_Type2 h_mk_part x_4436 =
     230  let part_no = x_4436 in h_mk_part part_no __
    231231
    232232(** val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    233 let rec part_rect_Type1 h_mk_part x_6134 =
    234   let part_no = x_6134 in h_mk_part part_no __
     233let rec part_rect_Type1 h_mk_part x_4438 =
     234  let part_no = x_4438 in h_mk_part part_no __
    235235
    236236(** val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    237 let rec part_rect_Type0 h_mk_part x_6136 =
    238   let part_no = x_6136 in h_mk_part part_no __
     237let rec part_rect_Type0 h_mk_part x_4440 =
     238  let part_no = x_4440 in h_mk_part part_no __
    239239
    240240(** val part_no : part -> Nat.nat **)
     
    486486| BVundef -> h_BVundef
    487487| BVnonzero -> h_BVnonzero
    488 | BVXor (x_6170, x_6169, x_6168) -> h_BVXor x_6170 x_6169 x_6168
    489 | BVByte x_6171 -> h_BVByte x_6171
    490 | BVnull x_6172 -> h_BVnull x_6172
    491 | BVptr (x_6174, x_6173) -> h_BVptr x_6174 x_6173
    492 | BVpc (x_6176, x_6175) -> h_BVpc x_6176 x_6175
     488| BVXor (x_4474, x_4473, x_4472) -> h_BVXor x_4474 x_4473 x_4472
     489| BVByte x_4475 -> h_BVByte x_4475
     490| BVnull x_4476 -> h_BVnull x_4476
     491| BVptr (x_4478, x_4477) -> h_BVptr x_4478 x_4477
     492| BVpc (x_4480, x_4479) -> h_BVpc x_4480 x_4479
    493493
    494494(** val beval_rect_Type5 :
     
    500500| BVundef -> h_BVundef
    501501| BVnonzero -> h_BVnonzero
    502 | BVXor (x_6187, x_6186, x_6185) -> h_BVXor x_6187 x_6186 x_6185
    503 | BVByte x_6188 -> h_BVByte x_6188
    504 | BVnull x_6189 -> h_BVnull x_6189
    505 | BVptr (x_6191, x_6190) -> h_BVptr x_6191 x_6190
    506 | BVpc (x_6193, x_6192) -> h_BVpc x_6193 x_6192
     502| BVXor (x_4491, x_4490, x_4489) -> h_BVXor x_4491 x_4490 x_4489
     503| BVByte x_4492 -> h_BVByte x_4492
     504| BVnull x_4493 -> h_BVnull x_4493
     505| BVptr (x_4495, x_4494) -> h_BVptr x_4495 x_4494
     506| BVpc (x_4497, x_4496) -> h_BVpc x_4497 x_4496
    507507
    508508(** val beval_rect_Type3 :
     
    514514| BVundef -> h_BVundef
    515515| BVnonzero -> h_BVnonzero
    516 | BVXor (x_6204, x_6203, x_6202) -> h_BVXor x_6204 x_6203 x_6202
    517 | BVByte x_6205 -> h_BVByte x_6205
    518 | BVnull x_6206 -> h_BVnull x_6206
    519 | BVptr (x_6208, x_6207) -> h_BVptr x_6208 x_6207
    520 | BVpc (x_6210, x_6209) -> h_BVpc x_6210 x_6209
     516| BVXor (x_4508, x_4507, x_4506) -> h_BVXor x_4508 x_4507 x_4506
     517| BVByte x_4509 -> h_BVByte x_4509
     518| BVnull x_4510 -> h_BVnull x_4510
     519| BVptr (x_4512, x_4511) -> h_BVptr x_4512 x_4511
     520| BVpc (x_4514, x_4513) -> h_BVpc x_4514 x_4513
    521521
    522522(** val beval_rect_Type2 :
     
    528528| BVundef -> h_BVundef
    529529| BVnonzero -> h_BVnonzero
    530 | BVXor (x_6221, x_6220, x_6219) -> h_BVXor x_6221 x_6220 x_6219
    531 | BVByte x_6222 -> h_BVByte x_6222
    532 | BVnull x_6223 -> h_BVnull x_6223
    533 | BVptr (x_6225, x_6224) -> h_BVptr x_6225 x_6224
    534 | BVpc (x_6227, x_6226) -> h_BVpc x_6227 x_6226
     530| BVXor (x_4525, x_4524, x_4523) -> h_BVXor x_4525 x_4524 x_4523
     531| BVByte x_4526 -> h_BVByte x_4526
     532| BVnull x_4527 -> h_BVnull x_4527
     533| BVptr (x_4529, x_4528) -> h_BVptr x_4529 x_4528
     534| BVpc (x_4531, x_4530) -> h_BVpc x_4531 x_4530
    535535
    536536(** val beval_rect_Type1 :
     
    542542| BVundef -> h_BVundef
    543543| BVnonzero -> h_BVnonzero
    544 | BVXor (x_6238, x_6237, x_6236) -> h_BVXor x_6238 x_6237 x_6236
    545 | BVByte x_6239 -> h_BVByte x_6239
    546 | BVnull x_6240 -> h_BVnull x_6240
    547 | BVptr (x_6242, x_6241) -> h_BVptr x_6242 x_6241
    548 | BVpc (x_6244, x_6243) -> h_BVpc x_6244 x_6243
     544| BVXor (x_4542, x_4541, x_4540) -> h_BVXor x_4542 x_4541 x_4540
     545| BVByte x_4543 -> h_BVByte x_4543
     546| BVnull x_4544 -> h_BVnull x_4544
     547| BVptr (x_4546, x_4545) -> h_BVptr x_4546 x_4545
     548| BVpc (x_4548, x_4547) -> h_BVpc x_4548 x_4547
    549549
    550550(** val beval_rect_Type0 :
     
    556556| BVundef -> h_BVundef
    557557| BVnonzero -> h_BVnonzero
    558 | BVXor (x_6255, x_6254, x_6253) -> h_BVXor x_6255 x_6254 x_6253
    559 | BVByte x_6256 -> h_BVByte x_6256
    560 | BVnull x_6257 -> h_BVnull x_6257
    561 | BVptr (x_6259, x_6258) -> h_BVptr x_6259 x_6258
    562 | BVpc (x_6261, x_6260) -> h_BVpc x_6261 x_6260
     558| BVXor (x_4559, x_4558, x_4557) -> h_BVXor x_4559 x_4558 x_4557
     559| BVByte x_4560 -> h_BVByte x_4560
     560| BVnull x_4561 -> h_BVnull x_4561
     561| BVptr (x_4563, x_4562) -> h_BVptr x_4563 x_4562
     562| BVpc (x_4565, x_4564) -> h_BVpc x_4565 x_4564
    563563
    564564(** val beval_inv_rect_Type4 :
     
    663663           Errors.Error (List.Cons ((Errors.MSG
    664664             ErrorMessages.CorruptedPointer), List.Nil))
    665          | BVptr (ptr1, p3) ->
     665         | BVptr (ptr1, p1) ->
    666666           (match bv2 with
    667667            | BVundef ->
     
    680680              Errors.Error (List.Cons ((Errors.MSG
    681681                ErrorMessages.CorruptedPointer), List.Nil))
    682             | BVptr (ptr2, p4) ->
     682            | BVptr (ptr2, p2) ->
    683683              (match Bool.andb
    684684                       (Bool.andb
    685                          (Bool.andb (Nat.eqb (part_no p3) Nat.O)
    686                            (Nat.eqb (part_no p4) (Nat.S Nat.O)))
     685                         (Bool.andb (Nat.eqb (part_no p1) Nat.O)
     686                           (Nat.eqb (part_no p2) (Nat.S Nat.O)))
    687687                         (Pointers.eq_block ptr1.Pointers.pblock
    688688                           ptr2.Pointers.pblock))
     
    741741           Errors.Error (List.Cons ((Errors.MSG
    742742             ErrorMessages.CorruptedPointer), List.Nil))
    743          | BVpc (ptr1, p3) ->
     743         | BVpc (ptr1, p1) ->
    744744           (match bv2 with
    745745            | BVundef ->
     
    761761              Errors.Error (List.Cons ((Errors.MSG
    762762                ErrorMessages.CorruptedPointer), List.Nil))
    763             | BVpc (ptr2, p4) ->
     763            | BVpc (ptr2, p2) ->
    764764              (match Bool.andb
    765                        (Bool.andb (Nat.eqb (part_no p3) Nat.O)
    766                          (Nat.eqb (part_no p4) (Nat.S Nat.O)))
     765                       (Bool.andb (Nat.eqb (part_no p1) Nat.O)
     766                         (Nat.eqb (part_no p2) (Nat.S Nat.O)))
    767767                       (eq_program_counter ptr1 ptr2) with
    768768               | Bool.True ->
     
    856856      Obj.magic (Errors.Error (List.Cons ((Errors.MSG
    857857        ErrorMessages.NotAnInt32Val), List.Nil)))
    858     | List.Cons (hd0, tl) ->
     858    | List.Cons (hd, tl) ->
    859859      Monad.m_bind0 (Monad.max_def Errors.res0)
    860         (Obj.magic (byte_of_val ErrorMessages.NotAnInt32Val hd0)) (fun b ->
     860        (Obj.magic (byte_of_val ErrorMessages.NotAnInt32Val hd)) (fun b ->
    861861        Obj.magic (Errors.OK { Types.fst = b; Types.snd = tl }))
    862862  in
     
    871871            | List.Nil ->
    872872              Obj.magic (Errors.OK
    873                 (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     873                (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    874874                  (Nat.S (Nat.S Nat.O))))))))
    875875                  (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    878878                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
    879879                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) b4
    880                   (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     880                  (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    881881                    (Nat.S (Nat.S Nat.O))))))))
    882882                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    883883                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
    884884                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) b3
    885                     (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     885                    (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    886886                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
    887887                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 b1))))
     
    899899    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    900900let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function
    901 | BBbit x_6380 -> h_BBbit x_6380
     901| BBbit x_4684 -> h_BBbit x_4684
    902902| BBundef -> h_BBundef
    903 | BBptrcarry (x_6383, x_6382, p, x_6381) ->
    904   h_BBptrcarry x_6383 x_6382 p x_6381
     903| BBptrcarry (x_4687, x_4686, p, x_4685) ->
     904  h_BBptrcarry x_4687 x_4686 p x_4685
    905905
    906906(** val bebit_rect_Type5 :
     
    908908    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    909909let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
    910 | BBbit x_6388 -> h_BBbit x_6388
     910| BBbit x_4692 -> h_BBbit x_4692
    911911| BBundef -> h_BBundef
    912 | BBptrcarry (x_6391, x_6390, p, x_6389) ->
    913   h_BBptrcarry x_6391 x_6390 p x_6389
     912| BBptrcarry (x_4695, x_4694, p, x_4693) ->
     913  h_BBptrcarry x_4695 x_4694 p x_4693
    914914
    915915(** val bebit_rect_Type3 :
     
    917917    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    918918let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
    919 | BBbit x_6396 -> h_BBbit x_6396
     919| BBbit x_4700 -> h_BBbit x_4700
    920920| BBundef -> h_BBundef
    921 | BBptrcarry (x_6399, x_6398, p, x_6397) ->
    922   h_BBptrcarry x_6399 x_6398 p x_6397
     921| BBptrcarry (x_4703, x_4702, p, x_4701) ->
     922  h_BBptrcarry x_4703 x_4702 p x_4701
    923923
    924924(** val bebit_rect_Type2 :
     
    926926    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    927927let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
    928 | BBbit x_6404 -> h_BBbit x_6404
     928| BBbit x_4708 -> h_BBbit x_4708
    929929| BBundef -> h_BBundef
    930 | BBptrcarry (x_6407, x_6406, p, x_6405) ->
    931   h_BBptrcarry x_6407 x_6406 p x_6405
     930| BBptrcarry (x_4711, x_4710, p, x_4709) ->
     931  h_BBptrcarry x_4711 x_4710 p x_4709
    932932
    933933(** val bebit_rect_Type1 :
     
    935935    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    936936let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
    937 | BBbit x_6412 -> h_BBbit x_6412
     937| BBbit x_4716 -> h_BBbit x_4716
    938938| BBundef -> h_BBundef
    939 | BBptrcarry (x_6415, x_6414, p, x_6413) ->
    940   h_BBptrcarry x_6415 x_6414 p x_6413
     939| BBptrcarry (x_4719, x_4718, p, x_4717) ->
     940  h_BBptrcarry x_4719 x_4718 p x_4717
    941941
    942942(** val bebit_rect_Type0 :
     
    944944    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    945945let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
    946 | BBbit x_6420 -> h_BBbit x_6420
     946| BBbit x_4724 -> h_BBbit x_4724
    947947| BBundef -> h_BBundef
    948 | BBptrcarry (x_6423, x_6422, p, x_6421) ->
    949   h_BBptrcarry x_6423 x_6422 p x_6421
     948| BBptrcarry (x_4727, x_4726, p, x_4725) ->
     949  h_BBptrcarry x_4727 x_4726 p x_4725
    950950
    951951(** val bebit_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.