Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/byteValues.ml

    r2601 r2649  
    77open Deqsets
    88
     9open ErrorMessages
     10
    911open PreIdentifiers
    1012
     
    2325open Identifiers
    2426
    25 open Coqlib
    26 
    27 open Floats
    28 
    2927open Integers
    3028
     
    3432
    3533open Arithmetic
    36 
    37 open Char
    38 
    39 open String
    4034
    4135open Extranat
     
    9387    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    9488    'a1 **)
    95 let rec program_counter_rect_Type4 h_mk_program_counter x_5073 =
    96   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5073 in
     89let rec program_counter_rect_Type4 h_mk_program_counter x_4510 =
     90  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4510 in
    9791  h_mk_program_counter pc_block0 pc_offset0
    9892
     
    10094    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    10195    'a1 **)
    102 let rec program_counter_rect_Type5 h_mk_program_counter x_5075 =
    103   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5075 in
     96let rec program_counter_rect_Type5 h_mk_program_counter x_4512 =
     97  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4512 in
    10498  h_mk_program_counter pc_block0 pc_offset0
    10599
     
    107101    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    108102    'a1 **)
    109 let rec program_counter_rect_Type3 h_mk_program_counter x_5077 =
    110   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5077 in
     103let rec program_counter_rect_Type3 h_mk_program_counter x_4514 =
     104  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4514 in
    111105  h_mk_program_counter pc_block0 pc_offset0
    112106
     
    114108    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    115109    'a1 **)
    116 let rec program_counter_rect_Type2 h_mk_program_counter x_5079 =
    117   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5079 in
     110let rec program_counter_rect_Type2 h_mk_program_counter x_4516 =
     111  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4516 in
    118112  h_mk_program_counter pc_block0 pc_offset0
    119113
     
    121115    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    122116    'a1 **)
    123 let rec program_counter_rect_Type1 h_mk_program_counter x_5081 =
    124   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5081 in
     117let rec program_counter_rect_Type1 h_mk_program_counter x_4518 =
     118  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4518 in
    125119  h_mk_program_counter pc_block0 pc_offset0
    126120
     
    128122    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    129123    'a1 **)
    130 let rec program_counter_rect_Type0 h_mk_program_counter x_5083 =
    131   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5083 in
     124let rec program_counter_rect_Type0 h_mk_program_counter x_4520 =
     125  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4520 in
    132126  h_mk_program_counter pc_block0 pc_offset0
    133127
     
    219213
    220214(** val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    221 let rec part_rect_Type4 h_mk_part x_5099 =
    222   let part_no = x_5099 in h_mk_part part_no __
     215let rec part_rect_Type4 h_mk_part x_4536 =
     216  let part_no = x_4536 in h_mk_part part_no __
    223217
    224218(** val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    225 let rec part_rect_Type5 h_mk_part x_5101 =
    226   let part_no = x_5101 in h_mk_part part_no __
     219let rec part_rect_Type5 h_mk_part x_4538 =
     220  let part_no = x_4538 in h_mk_part part_no __
    227221
    228222(** val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    229 let rec part_rect_Type3 h_mk_part x_5103 =
    230   let part_no = x_5103 in h_mk_part part_no __
     223let rec part_rect_Type3 h_mk_part x_4540 =
     224  let part_no = x_4540 in h_mk_part part_no __
    231225
    232226(** val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    233 let rec part_rect_Type2 h_mk_part x_5105 =
    234   let part_no = x_5105 in h_mk_part part_no __
     227let rec part_rect_Type2 h_mk_part x_4542 =
     228  let part_no = x_4542 in h_mk_part part_no __
    235229
    236230(** val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    237 let rec part_rect_Type1 h_mk_part x_5107 =
    238   let part_no = x_5107 in h_mk_part part_no __
     231let rec part_rect_Type1 h_mk_part x_4544 =
     232  let part_no = x_4544 in h_mk_part part_no __
    239233
    240234(** val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    241 let rec part_rect_Type0 h_mk_part x_5109 =
    242   let part_no = x_5109 in h_mk_part part_no __
     235let rec part_rect_Type0 h_mk_part x_4546 =
     236  let part_no = x_4546 in h_mk_part part_no __
    243237
    244238(** val part_no : part -> Nat.nat **)
     
    330324| BVundef -> h_BVundef
    331325| BVnonzero -> h_BVnonzero
    332 | BVXor (x_5143, x_5142, x_5141) -> h_BVXor x_5143 x_5142 x_5141
    333 | BVByte x_5144 -> h_BVByte x_5144
    334 | BVnull x_5145 -> h_BVnull x_5145
    335 | BVptr (x_5147, x_5146) -> h_BVptr x_5147 x_5146
    336 | BVpc (x_5149, x_5148) -> h_BVpc x_5149 x_5148
     326| BVXor (x_4580, x_4579, x_4578) -> h_BVXor x_4580 x_4579 x_4578
     327| BVByte x_4581 -> h_BVByte x_4581
     328| BVnull x_4582 -> h_BVnull x_4582
     329| BVptr (x_4584, x_4583) -> h_BVptr x_4584 x_4583
     330| BVpc (x_4586, x_4585) -> h_BVpc x_4586 x_4585
    337331
    338332(** val beval_rect_Type5 :
     
    344338| BVundef -> h_BVundef
    345339| BVnonzero -> h_BVnonzero
    346 | BVXor (x_5160, x_5159, x_5158) -> h_BVXor x_5160 x_5159 x_5158
    347 | BVByte x_5161 -> h_BVByte x_5161
    348 | BVnull x_5162 -> h_BVnull x_5162
    349 | BVptr (x_5164, x_5163) -> h_BVptr x_5164 x_5163
    350 | BVpc (x_5166, x_5165) -> h_BVpc x_5166 x_5165
     340| BVXor (x_4597, x_4596, x_4595) -> h_BVXor x_4597 x_4596 x_4595
     341| BVByte x_4598 -> h_BVByte x_4598
     342| BVnull x_4599 -> h_BVnull x_4599
     343| BVptr (x_4601, x_4600) -> h_BVptr x_4601 x_4600
     344| BVpc (x_4603, x_4602) -> h_BVpc x_4603 x_4602
    351345
    352346(** val beval_rect_Type3 :
     
    358352| BVundef -> h_BVundef
    359353| BVnonzero -> h_BVnonzero
    360 | BVXor (x_5177, x_5176, x_5175) -> h_BVXor x_5177 x_5176 x_5175
    361 | BVByte x_5178 -> h_BVByte x_5178
    362 | BVnull x_5179 -> h_BVnull x_5179
    363 | BVptr (x_5181, x_5180) -> h_BVptr x_5181 x_5180
    364 | BVpc (x_5183, x_5182) -> h_BVpc x_5183 x_5182
     354| BVXor (x_4614, x_4613, x_4612) -> h_BVXor x_4614 x_4613 x_4612
     355| BVByte x_4615 -> h_BVByte x_4615
     356| BVnull x_4616 -> h_BVnull x_4616
     357| BVptr (x_4618, x_4617) -> h_BVptr x_4618 x_4617
     358| BVpc (x_4620, x_4619) -> h_BVpc x_4620 x_4619
    365359
    366360(** val beval_rect_Type2 :
     
    372366| BVundef -> h_BVundef
    373367| BVnonzero -> h_BVnonzero
    374 | BVXor (x_5194, x_5193, x_5192) -> h_BVXor x_5194 x_5193 x_5192
    375 | BVByte x_5195 -> h_BVByte x_5195
    376 | BVnull x_5196 -> h_BVnull x_5196
    377 | BVptr (x_5198, x_5197) -> h_BVptr x_5198 x_5197
    378 | BVpc (x_5200, x_5199) -> h_BVpc x_5200 x_5199
     368| BVXor (x_4631, x_4630, x_4629) -> h_BVXor x_4631 x_4630 x_4629
     369| BVByte x_4632 -> h_BVByte x_4632
     370| BVnull x_4633 -> h_BVnull x_4633
     371| BVptr (x_4635, x_4634) -> h_BVptr x_4635 x_4634
     372| BVpc (x_4637, x_4636) -> h_BVpc x_4637 x_4636
    379373
    380374(** val beval_rect_Type1 :
     
    386380| BVundef -> h_BVundef
    387381| BVnonzero -> h_BVnonzero
    388 | BVXor (x_5211, x_5210, x_5209) -> h_BVXor x_5211 x_5210 x_5209
    389 | BVByte x_5212 -> h_BVByte x_5212
    390 | BVnull x_5213 -> h_BVnull x_5213
    391 | BVptr (x_5215, x_5214) -> h_BVptr x_5215 x_5214
    392 | BVpc (x_5217, x_5216) -> h_BVpc x_5217 x_5216
     382| BVXor (x_4648, x_4647, x_4646) -> h_BVXor x_4648 x_4647 x_4646
     383| BVByte x_4649 -> h_BVByte x_4649
     384| BVnull x_4650 -> h_BVnull x_4650
     385| BVptr (x_4652, x_4651) -> h_BVptr x_4652 x_4651
     386| BVpc (x_4654, x_4653) -> h_BVpc x_4654 x_4653
    393387
    394388(** val beval_rect_Type0 :
     
    400394| BVundef -> h_BVundef
    401395| BVnonzero -> h_BVnonzero
    402 | BVXor (x_5228, x_5227, x_5226) -> h_BVXor x_5228 x_5227 x_5226
    403 | BVByte x_5229 -> h_BVByte x_5229
    404 | BVnull x_5230 -> h_BVnull x_5230
    405 | BVptr (x_5232, x_5231) -> h_BVptr x_5232 x_5231
    406 | BVpc (x_5234, x_5233) -> h_BVpc x_5234 x_5233
     396| BVXor (x_4665, x_4664, x_4663) -> h_BVXor x_4665 x_4664 x_4663
     397| BVByte x_4666 -> h_BVByte x_4666
     398| BVnull x_4667 -> h_BVnull x_4667
     399| BVptr (x_4669, x_4668) -> h_BVptr x_4669 x_4668
     400| BVpc (x_4671, x_4670) -> h_BVpc x_4671 x_4670
    407401
    408402(** val beval_inv_rect_Type4 :
     
    477471  let b2 = (Vector.vsplit m p v2).Types.snd in BitVector.eq_bv p b1 b2
    478472
    479 (** val corruptedPointer : String.string **)
    480 let corruptedPointer = "corrupted pointer"
    481   (* failwith "AXIOM TO BE REALIZED" *)
    482 
    483473(** val pointer_of_bevals :
    484474    beval List.list -> Pointers.pointer Errors.res **)
    485475let pointer_of_bevals = function
    486476| List.Nil ->
    487   Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
     477  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
     478    List.Nil))
    488479| List.Cons (bv1, tl) ->
    489480  (match tl with
    490481   | List.Nil ->
    491      Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
     482     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
     483       List.Nil))
    492484   | List.Cons (bv2, tl') ->
    493485     (match tl' with
     
    495487        (match bv1 with
    496488         | BVundef ->
    497            Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
     489           Errors.Error (List.Cons ((Errors.MSG
     490             ErrorMessages.CorruptedPointer), List.Nil))
    498491         | BVnonzero ->
    499            Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
     492           Errors.Error (List.Cons ((Errors.MSG
     493             ErrorMessages.CorruptedPointer), List.Nil))
    500494         | BVXor (x, x0, x1) ->
    501            Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
     495           Errors.Error (List.Cons ((Errors.MSG
     496             ErrorMessages.CorruptedPointer), List.Nil))
    502497         | BVByte x ->
    503            Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
     498           Errors.Error (List.Cons ((Errors.MSG
     499             ErrorMessages.CorruptedPointer), List.Nil))
    504500         | BVnull x ->
    505            Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
     501           Errors.Error (List.Cons ((Errors.MSG
     502             ErrorMessages.CorruptedPointer), List.Nil))
    506503         | BVptr (ptr1, p3) ->
    507504           (match bv2 with
    508505            | BVundef ->
    509               Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
    510                 List.Nil))
     506              Errors.Error (List.Cons ((Errors.MSG
     507                ErrorMessages.CorruptedPointer), List.Nil))
    511508            | BVnonzero ->
    512               Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
    513                 List.Nil))
     509              Errors.Error (List.Cons ((Errors.MSG
     510                ErrorMessages.CorruptedPointer), List.Nil))
    514511            | BVXor (x, x0, x1) ->
    515               Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
    516                 List.Nil))
     512              Errors.Error (List.Cons ((Errors.MSG
     513                ErrorMessages.CorruptedPointer), List.Nil))
    517514            | BVByte x ->
    518               Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
    519                 List.Nil))
     515              Errors.Error (List.Cons ((Errors.MSG
     516                ErrorMessages.CorruptedPointer), List.Nil))
    520517            | BVnull x ->
    521               Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
    522                 List.Nil))
     518              Errors.Error (List.Cons ((Errors.MSG
     519                ErrorMessages.CorruptedPointer), List.Nil))
    523520            | BVptr (ptr2, p4) ->
    524521              (match Bool.andb
     
    538535                 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2)
    539536               | Bool.False ->
    540                  Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
    541                    List.Nil)))
     537                 Errors.Error (List.Cons ((Errors.MSG
     538                   ErrorMessages.CorruptedPointer), List.Nil)))
    542539            | BVpc (x, x0) ->
    543               Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
    544                 List.Nil)))
     540              Errors.Error (List.Cons ((Errors.MSG
     541                ErrorMessages.CorruptedPointer), List.Nil)))
    545542         | BVpc (x, x0) ->
    546            Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)))
     543           Errors.Error (List.Cons ((Errors.MSG
     544             ErrorMessages.CorruptedPointer), List.Nil)))
    547545      | List.Cons (x, x0) ->
    548         Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))))
     546        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
     547          List.Nil))))
    549548
    550549(** val pc_of_bevals : beval List.list -> program_counter Errors.res **)
    551550let pc_of_bevals = function
    552551| List.Nil ->
    553   Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
     552  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
     553    List.Nil))
    554554| List.Cons (bv1, tl) ->
    555555  (match tl with
    556556   | List.Nil ->
    557      Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
     557     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
     558       List.Nil))
    558559   | List.Cons (bv2, tl') ->
    559560     (match tl' with
     
    561562        (match bv1 with
    562563         | BVundef ->
    563            Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
     564           Errors.Error (List.Cons ((Errors.MSG
     565             ErrorMessages.CorruptedPointer), List.Nil))
    564566         | BVnonzero ->
    565            Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
     567           Errors.Error (List.Cons ((Errors.MSG
     568             ErrorMessages.CorruptedPointer), List.Nil))
    566569         | BVXor (x, x0, x1) ->
    567            Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
     570           Errors.Error (List.Cons ((Errors.MSG
     571             ErrorMessages.CorruptedPointer), List.Nil))
    568572         | BVByte x ->
    569            Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
     573           Errors.Error (List.Cons ((Errors.MSG
     574             ErrorMessages.CorruptedPointer), List.Nil))
    570575         | BVnull x ->
    571            Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
     576           Errors.Error (List.Cons ((Errors.MSG
     577             ErrorMessages.CorruptedPointer), List.Nil))
    572578         | BVptr (x, x0) ->
    573            Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
     579           Errors.Error (List.Cons ((Errors.MSG
     580             ErrorMessages.CorruptedPointer), List.Nil))
    574581         | BVpc (ptr1, p3) ->
    575582           (match bv2 with
    576583            | BVundef ->
    577               Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
    578                 List.Nil))
     584              Errors.Error (List.Cons ((Errors.MSG
     585                ErrorMessages.CorruptedPointer), List.Nil))
    579586            | BVnonzero ->
    580               Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
    581                 List.Nil))
     587              Errors.Error (List.Cons ((Errors.MSG
     588                ErrorMessages.CorruptedPointer), List.Nil))
    582589            | BVXor (x, x0, x1) ->
    583               Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
    584                 List.Nil))
     590              Errors.Error (List.Cons ((Errors.MSG
     591                ErrorMessages.CorruptedPointer), List.Nil))
    585592            | BVByte x ->
    586               Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
    587                 List.Nil))
     593              Errors.Error (List.Cons ((Errors.MSG
     594                ErrorMessages.CorruptedPointer), List.Nil))
    588595            | BVnull x ->
    589               Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
    590                 List.Nil))
     596              Errors.Error (List.Cons ((Errors.MSG
     597                ErrorMessages.CorruptedPointer), List.Nil))
    591598            | BVptr (x, x0) ->
    592               Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
    593                 List.Nil))
     599              Errors.Error (List.Cons ((Errors.MSG
     600                ErrorMessages.CorruptedPointer), List.Nil))
    594601            | BVpc (ptr2, p4) ->
    595602              (match Bool.andb
     
    600607                 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2)
    601608               | Bool.False ->
    602                  Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
    603                    List.Nil)))))
     609                 Errors.Error (List.Cons ((Errors.MSG
     610                   ErrorMessages.CorruptedPointer), List.Nil)))))
    604611      | List.Cons (x, x0) ->
    605         Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))))
     612        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
     613          List.Nil))))
    606614
    607615(** val bevals_of_pointer : Pointers.pointer -> beval List.list **)
     
    638646    __
    639647
    640 (** val notATwoBytesPointer : String.string **)
    641 let notATwoBytesPointer = "not a two bytes pointer"
    642   (* failwith "AXIOM TO BE REALIZED" *)
    643 
    644648(** val beval_pair_of_pointer :
    645649    Pointers.pointer -> (beval, beval) Types.prod **)
     
    651655  list_to_pair (bevals_of_pc p)
    652656
    653 (** val valueNotABoolean : String.string **)
    654 let valueNotABoolean = "value not a boolean"
    655   (* failwith "AXIOM TO BE REALIZED" *)
    656 
    657657(** val bool_of_beval : beval -> Bool.bool Errors.res **)
    658658let bool_of_beval = function
    659659| BVundef ->
    660   Errors.Error (List.Cons ((Errors.MSG valueNotABoolean), List.Nil))
     660  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
     661    List.Nil))
    661662| BVnonzero -> Errors.OK Bool.True
    662663| BVXor (x, x0, x1) ->
    663   Errors.Error (List.Cons ((Errors.MSG valueNotABoolean), List.Nil))
     664  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
     665    List.Nil))
    664666| BVByte b ->
    665667  Errors.OK
     
    671673| BVptr (x, x0) -> Errors.OK Bool.True
    672674| BVpc (x, x0) ->
    673   Errors.Error (List.Cons ((Errors.MSG valueNotABoolean), List.Nil))
    674 
    675 (** val byte_of_val : String.string -> beval -> BitVector.byte Errors.res **)
     675  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
     676    List.Nil))
     677
     678(** val byte_of_val :
     679    ErrorMessages.errorMessage -> beval -> BitVector.byte Errors.res **)
    676680let byte_of_val err = function
    677681| BVundef -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
     
    683687| BVpc (x, x0) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
    684688
    685 (** val notAnInt32Val : String.string **)
    686 let notAnInt32Val = "not an int32 val"
    687   (* failwith "AXIOM TO BE REALIZED" *)
    688 
    689689(** val word_of_list_beval : beval List.list -> Integers.int Errors.res **)
    690690let word_of_list_beval l =
     
    692692    match l0 with
    693693    | List.Nil ->
    694       Obj.magic (Errors.Error (List.Cons ((Errors.MSG notAnInt32Val),
    695         List.Nil)))
     694      Obj.magic (Errors.Error (List.Cons ((Errors.MSG
     695        ErrorMessages.NotAnInt32Val), List.Nil)))
    696696    | List.Cons (hd0, tl) ->
    697697      Monad.m_bind0 (Monad.max_def Errors.res0)
    698         (Obj.magic (byte_of_val notAnInt32Val hd0)) (fun b ->
     698        (Obj.magic (byte_of_val ErrorMessages.NotAnInt32Val hd0)) (fun b ->
    699699        Obj.magic (Errors.OK { Types.fst = b; Types.snd = tl }))
    700700  in
     
    725725                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 b1))))
    726726            | List.Cons (x, x0) ->
    727               Obj.magic (Errors.Error (List.Cons ((Errors.MSG notAnInt32Val),
    728                 List.Nil))))))))
     727              Obj.magic (Errors.Error (List.Cons ((Errors.MSG
     728                ErrorMessages.NotAnInt32Val), List.Nil))))))))
    729729
    730730type bebit =
     
    737737    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    738738let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function
    739 | BBbit x_5353 -> h_BBbit x_5353
     739| BBbit x_4790 -> h_BBbit x_4790
    740740| BBundef -> h_BBundef
    741 | BBptrcarry (x_5356, x_5355, p, x_5354) ->
    742   h_BBptrcarry x_5356 x_5355 p x_5354
     741| BBptrcarry (x_4793, x_4792, p, x_4791) ->
     742  h_BBptrcarry x_4793 x_4792 p x_4791
    743743
    744744(** val bebit_rect_Type5 :
     
    746746    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    747747let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
    748 | BBbit x_5361 -> h_BBbit x_5361
     748| BBbit x_4798 -> h_BBbit x_4798
    749749| BBundef -> h_BBundef
    750 | BBptrcarry (x_5364, x_5363, p, x_5362) ->
    751   h_BBptrcarry x_5364 x_5363 p x_5362
     750| BBptrcarry (x_4801, x_4800, p, x_4799) ->
     751  h_BBptrcarry x_4801 x_4800 p x_4799
    752752
    753753(** val bebit_rect_Type3 :
     
    755755    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    756756let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
    757 | BBbit x_5369 -> h_BBbit x_5369
     757| BBbit x_4806 -> h_BBbit x_4806
    758758| BBundef -> h_BBundef
    759 | BBptrcarry (x_5372, x_5371, p, x_5370) ->
    760   h_BBptrcarry x_5372 x_5371 p x_5370
     759| BBptrcarry (x_4809, x_4808, p, x_4807) ->
     760  h_BBptrcarry x_4809 x_4808 p x_4807
    761761
    762762(** val bebit_rect_Type2 :
     
    764764    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    765765let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
    766 | BBbit x_5377 -> h_BBbit x_5377
     766| BBbit x_4814 -> h_BBbit x_4814
    767767| BBundef -> h_BBundef
    768 | BBptrcarry (x_5380, x_5379, p, x_5378) ->
    769   h_BBptrcarry x_5380 x_5379 p x_5378
     768| BBptrcarry (x_4817, x_4816, p, x_4815) ->
     769  h_BBptrcarry x_4817 x_4816 p x_4815
    770770
    771771(** val bebit_rect_Type1 :
     
    773773    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    774774let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
    775 | BBbit x_5385 -> h_BBbit x_5385
     775| BBbit x_4822 -> h_BBbit x_4822
    776776| BBundef -> h_BBundef
    777 | BBptrcarry (x_5388, x_5387, p, x_5386) ->
    778   h_BBptrcarry x_5388 x_5387 p x_5386
     777| BBptrcarry (x_4825, x_4824, p, x_4823) ->
     778  h_BBptrcarry x_4825 x_4824 p x_4823
    779779
    780780(** val bebit_rect_Type0 :
     
    782782    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    783783let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
    784 | BBbit x_5393 -> h_BBbit x_5393
     784| BBbit x_4830 -> h_BBbit x_4830
    785785| BBundef -> h_BBundef
    786 | BBptrcarry (x_5396, x_5395, p, x_5394) ->
    787   h_BBptrcarry x_5396 x_5395 p x_5394
     786| BBptrcarry (x_4833, x_4832, p, x_4831) ->
     787  h_BBptrcarry x_4833 x_4832 p x_4831
    788788
    789789(** val bebit_inv_rect_Type4 :
     
    835835    y
    836836
    837 (** val bit_of_val : String.string -> bebit -> BitVector.bit Errors.res **)
     837(** val bit_of_val :
     838    ErrorMessages.errorMessage -> bebit -> BitVector.bit Errors.res **)
    838839let bit_of_val err = function
    839840| BBbit b0 -> Errors.OK b0
Note: See TracChangeset for help on using the changeset viewer.