Ignore:
Timestamp:
Mar 8, 2013, 9:07:28 PM (7 years ago)
Author:
sacerdot
Message:

Everything extracted again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint_LTL_LIN.ml

    r2797 r2827  
    116116    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    117117let rec registers_move_rect_Type4 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    118 | From_acc (x_21377, x_21376) -> h_from_acc x_21377 x_21376
    119 | To_acc (x_21379, x_21378) -> h_to_acc x_21379 x_21378
    120 | Int_to_reg (x_21381, x_21380) -> h_int_to_reg x_21381 x_21380
    121 | Int_to_acc (x_21383, x_21382) -> h_int_to_acc x_21383 x_21382
     118| From_acc (x_21503, x_21502) -> h_from_acc x_21503 x_21502
     119| To_acc (x_21505, x_21504) -> h_to_acc x_21505 x_21504
     120| Int_to_reg (x_21507, x_21506) -> h_int_to_reg x_21507 x_21506
     121| Int_to_acc (x_21509, x_21508) -> h_int_to_acc x_21509 x_21508
    122122
    123123(** val registers_move_rect_Type5 :
     
    126126    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    127127let rec registers_move_rect_Type5 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    128 | From_acc (x_21390, x_21389) -> h_from_acc x_21390 x_21389
    129 | To_acc (x_21392, x_21391) -> h_to_acc x_21392 x_21391
    130 | Int_to_reg (x_21394, x_21393) -> h_int_to_reg x_21394 x_21393
    131 | Int_to_acc (x_21396, x_21395) -> h_int_to_acc x_21396 x_21395
     128| From_acc (x_21516, x_21515) -> h_from_acc x_21516 x_21515
     129| To_acc (x_21518, x_21517) -> h_to_acc x_21518 x_21517
     130| Int_to_reg (x_21520, x_21519) -> h_int_to_reg x_21520 x_21519
     131| Int_to_acc (x_21522, x_21521) -> h_int_to_acc x_21522 x_21521
    132132
    133133(** val registers_move_rect_Type3 :
     
    136136    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    137137let rec registers_move_rect_Type3 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    138 | From_acc (x_21403, x_21402) -> h_from_acc x_21403 x_21402
    139 | To_acc (x_21405, x_21404) -> h_to_acc x_21405 x_21404
    140 | Int_to_reg (x_21407, x_21406) -> h_int_to_reg x_21407 x_21406
    141 | Int_to_acc (x_21409, x_21408) -> h_int_to_acc x_21409 x_21408
     138| From_acc (x_21529, x_21528) -> h_from_acc x_21529 x_21528
     139| To_acc (x_21531, x_21530) -> h_to_acc x_21531 x_21530
     140| Int_to_reg (x_21533, x_21532) -> h_int_to_reg x_21533 x_21532
     141| Int_to_acc (x_21535, x_21534) -> h_int_to_acc x_21535 x_21534
    142142
    143143(** val registers_move_rect_Type2 :
     
    146146    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    147147let rec registers_move_rect_Type2 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    148 | From_acc (x_21416, x_21415) -> h_from_acc x_21416 x_21415
    149 | To_acc (x_21418, x_21417) -> h_to_acc x_21418 x_21417
    150 | Int_to_reg (x_21420, x_21419) -> h_int_to_reg x_21420 x_21419
    151 | Int_to_acc (x_21422, x_21421) -> h_int_to_acc x_21422 x_21421
     148| From_acc (x_21542, x_21541) -> h_from_acc x_21542 x_21541
     149| To_acc (x_21544, x_21543) -> h_to_acc x_21544 x_21543
     150| Int_to_reg (x_21546, x_21545) -> h_int_to_reg x_21546 x_21545
     151| Int_to_acc (x_21548, x_21547) -> h_int_to_acc x_21548 x_21547
    152152
    153153(** val registers_move_rect_Type1 :
     
    156156    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    157157let rec registers_move_rect_Type1 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    158 | From_acc (x_21429, x_21428) -> h_from_acc x_21429 x_21428
    159 | To_acc (x_21431, x_21430) -> h_to_acc x_21431 x_21430
    160 | Int_to_reg (x_21433, x_21432) -> h_int_to_reg x_21433 x_21432
    161 | Int_to_acc (x_21435, x_21434) -> h_int_to_acc x_21435 x_21434
     158| From_acc (x_21555, x_21554) -> h_from_acc x_21555 x_21554
     159| To_acc (x_21557, x_21556) -> h_to_acc x_21557 x_21556
     160| Int_to_reg (x_21559, x_21558) -> h_int_to_reg x_21559 x_21558
     161| Int_to_acc (x_21561, x_21560) -> h_int_to_acc x_21561 x_21560
    162162
    163163(** val registers_move_rect_Type0 :
     
    166166    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    167167let rec registers_move_rect_Type0 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    168 | From_acc (x_21442, x_21441) -> h_from_acc x_21442 x_21441
    169 | To_acc (x_21444, x_21443) -> h_to_acc x_21444 x_21443
    170 | Int_to_reg (x_21446, x_21445) -> h_int_to_reg x_21446 x_21445
    171 | Int_to_acc (x_21448, x_21447) -> h_int_to_acc x_21448 x_21447
     168| From_acc (x_21568, x_21567) -> h_from_acc x_21568 x_21567
     169| To_acc (x_21570, x_21569) -> h_to_acc x_21570 x_21569
     170| Int_to_reg (x_21572, x_21571) -> h_int_to_reg x_21572 x_21571
     171| Int_to_acc (x_21574, x_21573) -> h_int_to_acc x_21574 x_21573
    172172
    173173(** val registers_move_inv_rect_Type4 :
     
    241241| SAVE_CARRY -> h_SAVE_CARRY
    242242| RESTORE_CARRY -> h_RESTORE_CARRY
    243 | LOW_ADDRESS (x_21542, x_21541) -> h_LOW_ADDRESS x_21542 x_21541
    244 | HIGH_ADDRESS (x_21544, x_21543) -> h_HIGH_ADDRESS x_21544 x_21543
     243| LOW_ADDRESS (x_21668, x_21667) -> h_LOW_ADDRESS x_21668 x_21667
     244| HIGH_ADDRESS (x_21670, x_21669) -> h_HIGH_ADDRESS x_21670 x_21669
    245245
    246246(** val ltl_lin_seq_rect_Type5 :
     
    250250| SAVE_CARRY -> h_SAVE_CARRY
    251251| RESTORE_CARRY -> h_RESTORE_CARRY
    252 | LOW_ADDRESS (x_21551, x_21550) -> h_LOW_ADDRESS x_21551 x_21550
    253 | HIGH_ADDRESS (x_21553, x_21552) -> h_HIGH_ADDRESS x_21553 x_21552
     252| LOW_ADDRESS (x_21677, x_21676) -> h_LOW_ADDRESS x_21677 x_21676
     253| HIGH_ADDRESS (x_21679, x_21678) -> h_HIGH_ADDRESS x_21679 x_21678
    254254
    255255(** val ltl_lin_seq_rect_Type3 :
     
    259259| SAVE_CARRY -> h_SAVE_CARRY
    260260| RESTORE_CARRY -> h_RESTORE_CARRY
    261 | LOW_ADDRESS (x_21560, x_21559) -> h_LOW_ADDRESS x_21560 x_21559
    262 | HIGH_ADDRESS (x_21562, x_21561) -> h_HIGH_ADDRESS x_21562 x_21561
     261| LOW_ADDRESS (x_21686, x_21685) -> h_LOW_ADDRESS x_21686 x_21685
     262| HIGH_ADDRESS (x_21688, x_21687) -> h_HIGH_ADDRESS x_21688 x_21687
    263263
    264264(** val ltl_lin_seq_rect_Type2 :
     
    268268| SAVE_CARRY -> h_SAVE_CARRY
    269269| RESTORE_CARRY -> h_RESTORE_CARRY
    270 | LOW_ADDRESS (x_21569, x_21568) -> h_LOW_ADDRESS x_21569 x_21568
    271 | HIGH_ADDRESS (x_21571, x_21570) -> h_HIGH_ADDRESS x_21571 x_21570
     270| LOW_ADDRESS (x_21695, x_21694) -> h_LOW_ADDRESS x_21695 x_21694
     271| HIGH_ADDRESS (x_21697, x_21696) -> h_HIGH_ADDRESS x_21697 x_21696
    272272
    273273(** val ltl_lin_seq_rect_Type1 :
     
    277277| SAVE_CARRY -> h_SAVE_CARRY
    278278| RESTORE_CARRY -> h_RESTORE_CARRY
    279 | LOW_ADDRESS (x_21578, x_21577) -> h_LOW_ADDRESS x_21578 x_21577
    280 | HIGH_ADDRESS (x_21580, x_21579) -> h_HIGH_ADDRESS x_21580 x_21579
     279| LOW_ADDRESS (x_21704, x_21703) -> h_LOW_ADDRESS x_21704 x_21703
     280| HIGH_ADDRESS (x_21706, x_21705) -> h_HIGH_ADDRESS x_21706 x_21705
    281281
    282282(** val ltl_lin_seq_rect_Type0 :
     
    286286| SAVE_CARRY -> h_SAVE_CARRY
    287287| RESTORE_CARRY -> h_RESTORE_CARRY
    288 | LOW_ADDRESS (x_21587, x_21586) -> h_LOW_ADDRESS x_21587 x_21586
    289 | HIGH_ADDRESS (x_21589, x_21588) -> h_HIGH_ADDRESS x_21589 x_21588
     288| LOW_ADDRESS (x_21713, x_21712) -> h_LOW_ADDRESS x_21713 x_21712
     289| HIGH_ADDRESS (x_21715, x_21714) -> h_HIGH_ADDRESS x_21715 x_21714
    290290
    291291(** val ltl_lin_seq_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.