Ignore:
Timestamp:
Apr 2, 2013, 1:25:09 AM (7 years ago)
Author:
sacerdot
Message:

New extraction

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint_LTL_LIN.ml

    r3043 r3059  
    130130    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    131131let rec registers_move_rect_Type4 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    132 | From_acc (x_18694, x_18693) -> h_from_acc x_18694 x_18693
    133 | To_acc (x_18696, x_18695) -> h_to_acc x_18696 x_18695
    134 | Int_to_reg (x_18698, x_18697) -> h_int_to_reg x_18698 x_18697
    135 | Int_to_acc (x_18700, x_18699) -> h_int_to_acc x_18700 x_18699
     132| From_acc (x_18638, x_18637) -> h_from_acc x_18638 x_18637
     133| To_acc (x_18640, x_18639) -> h_to_acc x_18640 x_18639
     134| Int_to_reg (x_18642, x_18641) -> h_int_to_reg x_18642 x_18641
     135| Int_to_acc (x_18644, x_18643) -> h_int_to_acc x_18644 x_18643
    136136
    137137(** val registers_move_rect_Type5 :
     
    140140    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    141141let rec registers_move_rect_Type5 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    142 | From_acc (x_18707, x_18706) -> h_from_acc x_18707 x_18706
    143 | To_acc (x_18709, x_18708) -> h_to_acc x_18709 x_18708
    144 | Int_to_reg (x_18711, x_18710) -> h_int_to_reg x_18711 x_18710
    145 | Int_to_acc (x_18713, x_18712) -> h_int_to_acc x_18713 x_18712
     142| From_acc (x_18651, x_18650) -> h_from_acc x_18651 x_18650
     143| To_acc (x_18653, x_18652) -> h_to_acc x_18653 x_18652
     144| Int_to_reg (x_18655, x_18654) -> h_int_to_reg x_18655 x_18654
     145| Int_to_acc (x_18657, x_18656) -> h_int_to_acc x_18657 x_18656
    146146
    147147(** val registers_move_rect_Type3 :
     
    150150    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    151151let rec registers_move_rect_Type3 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    152 | From_acc (x_18720, x_18719) -> h_from_acc x_18720 x_18719
    153 | To_acc (x_18722, x_18721) -> h_to_acc x_18722 x_18721
    154 | Int_to_reg (x_18724, x_18723) -> h_int_to_reg x_18724 x_18723
    155 | Int_to_acc (x_18726, x_18725) -> h_int_to_acc x_18726 x_18725
     152| From_acc (x_18664, x_18663) -> h_from_acc x_18664 x_18663
     153| To_acc (x_18666, x_18665) -> h_to_acc x_18666 x_18665
     154| Int_to_reg (x_18668, x_18667) -> h_int_to_reg x_18668 x_18667
     155| Int_to_acc (x_18670, x_18669) -> h_int_to_acc x_18670 x_18669
    156156
    157157(** val registers_move_rect_Type2 :
     
    160160    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    161161let rec registers_move_rect_Type2 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    162 | From_acc (x_18733, x_18732) -> h_from_acc x_18733 x_18732
    163 | To_acc (x_18735, x_18734) -> h_to_acc x_18735 x_18734
    164 | Int_to_reg (x_18737, x_18736) -> h_int_to_reg x_18737 x_18736
    165 | Int_to_acc (x_18739, x_18738) -> h_int_to_acc x_18739 x_18738
     162| From_acc (x_18677, x_18676) -> h_from_acc x_18677 x_18676
     163| To_acc (x_18679, x_18678) -> h_to_acc x_18679 x_18678
     164| Int_to_reg (x_18681, x_18680) -> h_int_to_reg x_18681 x_18680
     165| Int_to_acc (x_18683, x_18682) -> h_int_to_acc x_18683 x_18682
    166166
    167167(** val registers_move_rect_Type1 :
     
    170170    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    171171let rec registers_move_rect_Type1 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    172 | From_acc (x_18746, x_18745) -> h_from_acc x_18746 x_18745
    173 | To_acc (x_18748, x_18747) -> h_to_acc x_18748 x_18747
    174 | Int_to_reg (x_18750, x_18749) -> h_int_to_reg x_18750 x_18749
    175 | Int_to_acc (x_18752, x_18751) -> h_int_to_acc x_18752 x_18751
     172| From_acc (x_18690, x_18689) -> h_from_acc x_18690 x_18689
     173| To_acc (x_18692, x_18691) -> h_to_acc x_18692 x_18691
     174| Int_to_reg (x_18694, x_18693) -> h_int_to_reg x_18694 x_18693
     175| Int_to_acc (x_18696, x_18695) -> h_int_to_acc x_18696 x_18695
    176176
    177177(** val registers_move_rect_Type0 :
     
    180180    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    181181let rec registers_move_rect_Type0 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    182 | From_acc (x_18759, x_18758) -> h_from_acc x_18759 x_18758
    183 | To_acc (x_18761, x_18760) -> h_to_acc x_18761 x_18760
    184 | Int_to_reg (x_18763, x_18762) -> h_int_to_reg x_18763 x_18762
    185 | Int_to_acc (x_18765, x_18764) -> h_int_to_acc x_18765 x_18764
     182| From_acc (x_18703, x_18702) -> h_from_acc x_18703 x_18702
     183| To_acc (x_18705, x_18704) -> h_to_acc x_18705 x_18704
     184| Int_to_reg (x_18707, x_18706) -> h_int_to_reg x_18707 x_18706
     185| Int_to_acc (x_18709, x_18708) -> h_int_to_acc x_18709 x_18708
    186186
    187187(** val registers_move_inv_rect_Type4 :
     
    255255| SAVE_CARRY -> h_SAVE_CARRY
    256256| RESTORE_CARRY -> h_RESTORE_CARRY
    257 | LOW_ADDRESS x_18856 -> h_LOW_ADDRESS x_18856
    258 | HIGH_ADDRESS x_18857 -> h_HIGH_ADDRESS x_18857
     257| LOW_ADDRESS x_18800 -> h_LOW_ADDRESS x_18800
     258| HIGH_ADDRESS x_18801 -> h_HIGH_ADDRESS x_18801
    259259
    260260(** val ltl_lin_seq_rect_Type5 :
     
    264264| SAVE_CARRY -> h_SAVE_CARRY
    265265| RESTORE_CARRY -> h_RESTORE_CARRY
    266 | LOW_ADDRESS x_18863 -> h_LOW_ADDRESS x_18863
    267 | HIGH_ADDRESS x_18864 -> h_HIGH_ADDRESS x_18864
     266| LOW_ADDRESS x_18807 -> h_LOW_ADDRESS x_18807
     267| HIGH_ADDRESS x_18808 -> h_HIGH_ADDRESS x_18808
    268268
    269269(** val ltl_lin_seq_rect_Type3 :
     
    273273| SAVE_CARRY -> h_SAVE_CARRY
    274274| RESTORE_CARRY -> h_RESTORE_CARRY
    275 | LOW_ADDRESS x_18870 -> h_LOW_ADDRESS x_18870
    276 | HIGH_ADDRESS x_18871 -> h_HIGH_ADDRESS x_18871
     275| LOW_ADDRESS x_18814 -> h_LOW_ADDRESS x_18814
     276| HIGH_ADDRESS x_18815 -> h_HIGH_ADDRESS x_18815
    277277
    278278(** val ltl_lin_seq_rect_Type2 :
     
    282282| SAVE_CARRY -> h_SAVE_CARRY
    283283| RESTORE_CARRY -> h_RESTORE_CARRY
    284 | LOW_ADDRESS x_18877 -> h_LOW_ADDRESS x_18877
    285 | HIGH_ADDRESS x_18878 -> h_HIGH_ADDRESS x_18878
     284| LOW_ADDRESS x_18821 -> h_LOW_ADDRESS x_18821
     285| HIGH_ADDRESS x_18822 -> h_HIGH_ADDRESS x_18822
    286286
    287287(** val ltl_lin_seq_rect_Type1 :
     
    291291| SAVE_CARRY -> h_SAVE_CARRY
    292292| RESTORE_CARRY -> h_RESTORE_CARRY
    293 | LOW_ADDRESS x_18884 -> h_LOW_ADDRESS x_18884
    294 | HIGH_ADDRESS x_18885 -> h_HIGH_ADDRESS x_18885
     293| LOW_ADDRESS x_18828 -> h_LOW_ADDRESS x_18828
     294| HIGH_ADDRESS x_18829 -> h_HIGH_ADDRESS x_18829
    295295
    296296(** val ltl_lin_seq_rect_Type0 :
     
    300300| SAVE_CARRY -> h_SAVE_CARRY
    301301| RESTORE_CARRY -> h_RESTORE_CARRY
    302 | LOW_ADDRESS x_18891 -> h_LOW_ADDRESS x_18891
    303 | HIGH_ADDRESS x_18892 -> h_HIGH_ADDRESS x_18892
     302| LOW_ADDRESS x_18835 -> h_LOW_ADDRESS x_18835
     303| HIGH_ADDRESS x_18836 -> h_HIGH_ADDRESS x_18836
    304304
    305305(** val ltl_lin_seq_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.