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

    r2649 r2717  
    3030
    3131open Division
     32
     33open Exp
    3234
    3335open Arithmetic
     
    8789    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    8890    'a1 **)
    89 let rec program_counter_rect_Type4 h_mk_program_counter x_4510 =
    90   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4510 in
     91let rec program_counter_rect_Type4 h_mk_program_counter x_6074 =
     92  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6074 in
    9193  h_mk_program_counter pc_block0 pc_offset0
    9294
     
    9496    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    9597    'a1 **)
    96 let rec program_counter_rect_Type5 h_mk_program_counter x_4512 =
    97   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4512 in
     98let rec program_counter_rect_Type5 h_mk_program_counter x_6076 =
     99  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6076 in
    98100  h_mk_program_counter pc_block0 pc_offset0
    99101
     
    101103    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    102104    'a1 **)
    103 let rec program_counter_rect_Type3 h_mk_program_counter x_4514 =
    104   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4514 in
     105let rec program_counter_rect_Type3 h_mk_program_counter x_6078 =
     106  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6078 in
    105107  h_mk_program_counter pc_block0 pc_offset0
    106108
     
    108110    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    109111    'a1 **)
    110 let rec program_counter_rect_Type2 h_mk_program_counter x_4516 =
    111   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4516 in
     112let rec program_counter_rect_Type2 h_mk_program_counter x_6080 =
     113  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6080 in
    112114  h_mk_program_counter pc_block0 pc_offset0
    113115
     
    115117    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    116118    'a1 **)
    117 let rec program_counter_rect_Type1 h_mk_program_counter x_4518 =
    118   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4518 in
     119let rec program_counter_rect_Type1 h_mk_program_counter x_6082 =
     120  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6082 in
    119121  h_mk_program_counter pc_block0 pc_offset0
    120122
     
    122124    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    123125    'a1 **)
    124 let rec program_counter_rect_Type0 h_mk_program_counter x_4520 =
    125   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4520 in
     126let rec program_counter_rect_Type0 h_mk_program_counter x_6084 =
     127  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6084 in
    126128  h_mk_program_counter pc_block0 pc_offset0
    127129
     
    213215
    214216(** val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    215 let rec part_rect_Type4 h_mk_part x_4536 =
    216   let part_no = x_4536 in h_mk_part part_no __
     217let rec part_rect_Type4 h_mk_part x_6100 =
     218  let part_no = x_6100 in h_mk_part part_no __
    217219
    218220(** val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    219 let rec part_rect_Type5 h_mk_part x_4538 =
    220   let part_no = x_4538 in h_mk_part part_no __
     221let rec part_rect_Type5 h_mk_part x_6102 =
     222  let part_no = x_6102 in h_mk_part part_no __
    221223
    222224(** val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    223 let rec part_rect_Type3 h_mk_part x_4540 =
    224   let part_no = x_4540 in h_mk_part part_no __
     225let rec part_rect_Type3 h_mk_part x_6104 =
     226  let part_no = x_6104 in h_mk_part part_no __
    225227
    226228(** val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    227 let rec part_rect_Type2 h_mk_part x_4542 =
    228   let part_no = x_4542 in h_mk_part part_no __
     229let rec part_rect_Type2 h_mk_part x_6106 =
     230  let part_no = x_6106 in h_mk_part part_no __
    229231
    230232(** val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    231 let rec part_rect_Type1 h_mk_part x_4544 =
    232   let part_no = x_4544 in h_mk_part part_no __
     233let rec part_rect_Type1 h_mk_part x_6108 =
     234  let part_no = x_6108 in h_mk_part part_no __
    233235
    234236(** val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    235 let rec part_rect_Type0 h_mk_part x_4546 =
    236   let part_no = x_4546 in h_mk_part part_no __
     237let rec part_rect_Type0 h_mk_part x_6110 =
     238  let part_no = x_6110 in h_mk_part part_no __
    237239
    238240(** val part_no : part -> Nat.nat **)
     
    324326| BVundef -> h_BVundef
    325327| BVnonzero -> h_BVnonzero
    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
     328| BVXor (x_6144, x_6143, x_6142) -> h_BVXor x_6144 x_6143 x_6142
     329| BVByte x_6145 -> h_BVByte x_6145
     330| BVnull x_6146 -> h_BVnull x_6146
     331| BVptr (x_6148, x_6147) -> h_BVptr x_6148 x_6147
     332| BVpc (x_6150, x_6149) -> h_BVpc x_6150 x_6149
    331333
    332334(** val beval_rect_Type5 :
     
    338340| BVundef -> h_BVundef
    339341| BVnonzero -> h_BVnonzero
    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
     342| BVXor (x_6161, x_6160, x_6159) -> h_BVXor x_6161 x_6160 x_6159
     343| BVByte x_6162 -> h_BVByte x_6162
     344| BVnull x_6163 -> h_BVnull x_6163
     345| BVptr (x_6165, x_6164) -> h_BVptr x_6165 x_6164
     346| BVpc (x_6167, x_6166) -> h_BVpc x_6167 x_6166
    345347
    346348(** val beval_rect_Type3 :
     
    352354| BVundef -> h_BVundef
    353355| BVnonzero -> h_BVnonzero
    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
     356| BVXor (x_6178, x_6177, x_6176) -> h_BVXor x_6178 x_6177 x_6176
     357| BVByte x_6179 -> h_BVByte x_6179
     358| BVnull x_6180 -> h_BVnull x_6180
     359| BVptr (x_6182, x_6181) -> h_BVptr x_6182 x_6181
     360| BVpc (x_6184, x_6183) -> h_BVpc x_6184 x_6183
    359361
    360362(** val beval_rect_Type2 :
     
    366368| BVundef -> h_BVundef
    367369| BVnonzero -> h_BVnonzero
    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
     370| BVXor (x_6195, x_6194, x_6193) -> h_BVXor x_6195 x_6194 x_6193
     371| BVByte x_6196 -> h_BVByte x_6196
     372| BVnull x_6197 -> h_BVnull x_6197
     373| BVptr (x_6199, x_6198) -> h_BVptr x_6199 x_6198
     374| BVpc (x_6201, x_6200) -> h_BVpc x_6201 x_6200
    373375
    374376(** val beval_rect_Type1 :
     
    380382| BVundef -> h_BVundef
    381383| BVnonzero -> h_BVnonzero
    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
     384| BVXor (x_6212, x_6211, x_6210) -> h_BVXor x_6212 x_6211 x_6210
     385| BVByte x_6213 -> h_BVByte x_6213
     386| BVnull x_6214 -> h_BVnull x_6214
     387| BVptr (x_6216, x_6215) -> h_BVptr x_6216 x_6215
     388| BVpc (x_6218, x_6217) -> h_BVpc x_6218 x_6217
    387389
    388390(** val beval_rect_Type0 :
     
    394396| BVundef -> h_BVundef
    395397| BVnonzero -> h_BVnonzero
    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
     398| BVXor (x_6229, x_6228, x_6227) -> h_BVXor x_6229 x_6228 x_6227
     399| BVByte x_6230 -> h_BVByte x_6230
     400| BVnull x_6231 -> h_BVnull x_6231
     401| BVptr (x_6233, x_6232) -> h_BVptr x_6233 x_6232
     402| BVpc (x_6235, x_6234) -> h_BVpc x_6235 x_6234
    401403
    402404(** val beval_inv_rect_Type4 :
     
    737739    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    738740let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function
    739 | BBbit x_4790 -> h_BBbit x_4790
     741| BBbit x_6354 -> h_BBbit x_6354
    740742| BBundef -> h_BBundef
    741 | BBptrcarry (x_4793, x_4792, p, x_4791) ->
    742   h_BBptrcarry x_4793 x_4792 p x_4791
     743| BBptrcarry (x_6357, x_6356, p, x_6355) ->
     744  h_BBptrcarry x_6357 x_6356 p x_6355
    743745
    744746(** val bebit_rect_Type5 :
     
    746748    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    747749let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
    748 | BBbit x_4798 -> h_BBbit x_4798
     750| BBbit x_6362 -> h_BBbit x_6362
    749751| BBundef -> h_BBundef
    750 | BBptrcarry (x_4801, x_4800, p, x_4799) ->
    751   h_BBptrcarry x_4801 x_4800 p x_4799
     752| BBptrcarry (x_6365, x_6364, p, x_6363) ->
     753  h_BBptrcarry x_6365 x_6364 p x_6363
    752754
    753755(** val bebit_rect_Type3 :
     
    755757    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    756758let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
    757 | BBbit x_4806 -> h_BBbit x_4806
     759| BBbit x_6370 -> h_BBbit x_6370
    758760| BBundef -> h_BBundef
    759 | BBptrcarry (x_4809, x_4808, p, x_4807) ->
    760   h_BBptrcarry x_4809 x_4808 p x_4807
     761| BBptrcarry (x_6373, x_6372, p, x_6371) ->
     762  h_BBptrcarry x_6373 x_6372 p x_6371
    761763
    762764(** val bebit_rect_Type2 :
     
    764766    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    765767let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
    766 | BBbit x_4814 -> h_BBbit x_4814
     768| BBbit x_6378 -> h_BBbit x_6378
    767769| BBundef -> h_BBundef
    768 | BBptrcarry (x_4817, x_4816, p, x_4815) ->
    769   h_BBptrcarry x_4817 x_4816 p x_4815
     770| BBptrcarry (x_6381, x_6380, p, x_6379) ->
     771  h_BBptrcarry x_6381 x_6380 p x_6379
    770772
    771773(** val bebit_rect_Type1 :
     
    773775    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    774776let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
    775 | BBbit x_4822 -> h_BBbit x_4822
     777| BBbit x_6386 -> h_BBbit x_6386
    776778| BBundef -> h_BBundef
    777 | BBptrcarry (x_4825, x_4824, p, x_4823) ->
    778   h_BBptrcarry x_4825 x_4824 p x_4823
     779| BBptrcarry (x_6389, x_6388, p, x_6387) ->
     780  h_BBptrcarry x_6389 x_6388 p x_6387
    779781
    780782(** val bebit_rect_Type0 :
     
    782784    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    783785let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
    784 | BBbit x_4830 -> h_BBbit x_4830
     786| BBbit x_6394 -> h_BBbit x_6394
    785787| BBundef -> h_BBundef
    786 | BBptrcarry (x_4833, x_4832, p, x_4831) ->
    787   h_BBptrcarry x_4833 x_4832 p x_4831
     788| BBptrcarry (x_6397, x_6396, p, x_6395) ->
     789  h_BBptrcarry x_6397 x_6396 p x_6395
    788790
    789791(** val bebit_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.