Ignore:
Timestamp:
Feb 25, 2013, 9:54:49 PM (8 years ago)
Author:
sacerdot
Message:

Exported again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint_LTL_LIN.ml

    r2717 r2730  
    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_18077, x_18076) -> h_from_acc x_18077 x_18076
    119 | To_acc (x_18079, x_18078) -> h_to_acc x_18079 x_18078
    120 | Int_to_reg (x_18081, x_18080) -> h_int_to_reg x_18081 x_18080
    121 | Int_to_acc (x_18083, x_18082) -> h_int_to_acc x_18083 x_18082
     118| From_acc (x_7486, x_7485) -> h_from_acc x_7486 x_7485
     119| To_acc (x_7488, x_7487) -> h_to_acc x_7488 x_7487
     120| Int_to_reg (x_7490, x_7489) -> h_int_to_reg x_7490 x_7489
     121| Int_to_acc (x_7492, x_7491) -> h_int_to_acc x_7492 x_7491
    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_18090, x_18089) -> h_from_acc x_18090 x_18089
    129 | To_acc (x_18092, x_18091) -> h_to_acc x_18092 x_18091
    130 | Int_to_reg (x_18094, x_18093) -> h_int_to_reg x_18094 x_18093
    131 | Int_to_acc (x_18096, x_18095) -> h_int_to_acc x_18096 x_18095
     128| From_acc (x_7499, x_7498) -> h_from_acc x_7499 x_7498
     129| To_acc (x_7501, x_7500) -> h_to_acc x_7501 x_7500
     130| Int_to_reg (x_7503, x_7502) -> h_int_to_reg x_7503 x_7502
     131| Int_to_acc (x_7505, x_7504) -> h_int_to_acc x_7505 x_7504
    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_18103, x_18102) -> h_from_acc x_18103 x_18102
    139 | To_acc (x_18105, x_18104) -> h_to_acc x_18105 x_18104
    140 | Int_to_reg (x_18107, x_18106) -> h_int_to_reg x_18107 x_18106
    141 | Int_to_acc (x_18109, x_18108) -> h_int_to_acc x_18109 x_18108
     138| From_acc (x_7512, x_7511) -> h_from_acc x_7512 x_7511
     139| To_acc (x_7514, x_7513) -> h_to_acc x_7514 x_7513
     140| Int_to_reg (x_7516, x_7515) -> h_int_to_reg x_7516 x_7515
     141| Int_to_acc (x_7518, x_7517) -> h_int_to_acc x_7518 x_7517
    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_18116, x_18115) -> h_from_acc x_18116 x_18115
    149 | To_acc (x_18118, x_18117) -> h_to_acc x_18118 x_18117
    150 | Int_to_reg (x_18120, x_18119) -> h_int_to_reg x_18120 x_18119
    151 | Int_to_acc (x_18122, x_18121) -> h_int_to_acc x_18122 x_18121
     148| From_acc (x_7525, x_7524) -> h_from_acc x_7525 x_7524
     149| To_acc (x_7527, x_7526) -> h_to_acc x_7527 x_7526
     150| Int_to_reg (x_7529, x_7528) -> h_int_to_reg x_7529 x_7528
     151| Int_to_acc (x_7531, x_7530) -> h_int_to_acc x_7531 x_7530
    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_18129, x_18128) -> h_from_acc x_18129 x_18128
    159 | To_acc (x_18131, x_18130) -> h_to_acc x_18131 x_18130
    160 | Int_to_reg (x_18133, x_18132) -> h_int_to_reg x_18133 x_18132
    161 | Int_to_acc (x_18135, x_18134) -> h_int_to_acc x_18135 x_18134
     158| From_acc (x_7538, x_7537) -> h_from_acc x_7538 x_7537
     159| To_acc (x_7540, x_7539) -> h_to_acc x_7540 x_7539
     160| Int_to_reg (x_7542, x_7541) -> h_int_to_reg x_7542 x_7541
     161| Int_to_acc (x_7544, x_7543) -> h_int_to_acc x_7544 x_7543
    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_18142, x_18141) -> h_from_acc x_18142 x_18141
    169 | To_acc (x_18144, x_18143) -> h_to_acc x_18144 x_18143
    170 | Int_to_reg (x_18146, x_18145) -> h_int_to_reg x_18146 x_18145
    171 | Int_to_acc (x_18148, x_18147) -> h_int_to_acc x_18148 x_18147
     168| From_acc (x_7551, x_7550) -> h_from_acc x_7551 x_7550
     169| To_acc (x_7553, x_7552) -> h_to_acc x_7553 x_7552
     170| Int_to_reg (x_7555, x_7554) -> h_int_to_reg x_7555 x_7554
     171| Int_to_acc (x_7557, x_7556) -> h_int_to_acc x_7557 x_7556
    172172
    173173(** val registers_move_inv_rect_Type4 :
     
    241241| SAVE_CARRY -> h_SAVE_CARRY
    242242| RESTORE_CARRY -> h_RESTORE_CARRY
    243 | LOW_ADDRESS (x_18242, x_18241) -> h_LOW_ADDRESS x_18242 x_18241
    244 | HIGH_ADDRESS (x_18244, x_18243) -> h_HIGH_ADDRESS x_18244 x_18243
     243| LOW_ADDRESS (x_7651, x_7650) -> h_LOW_ADDRESS x_7651 x_7650
     244| HIGH_ADDRESS (x_7653, x_7652) -> h_HIGH_ADDRESS x_7653 x_7652
    245245
    246246(** val ltl_lin_seq_rect_Type5 :
     
    250250| SAVE_CARRY -> h_SAVE_CARRY
    251251| RESTORE_CARRY -> h_RESTORE_CARRY
    252 | LOW_ADDRESS (x_18251, x_18250) -> h_LOW_ADDRESS x_18251 x_18250
    253 | HIGH_ADDRESS (x_18253, x_18252) -> h_HIGH_ADDRESS x_18253 x_18252
     252| LOW_ADDRESS (x_7660, x_7659) -> h_LOW_ADDRESS x_7660 x_7659
     253| HIGH_ADDRESS (x_7662, x_7661) -> h_HIGH_ADDRESS x_7662 x_7661
    254254
    255255(** val ltl_lin_seq_rect_Type3 :
     
    259259| SAVE_CARRY -> h_SAVE_CARRY
    260260| RESTORE_CARRY -> h_RESTORE_CARRY
    261 | LOW_ADDRESS (x_18260, x_18259) -> h_LOW_ADDRESS x_18260 x_18259
    262 | HIGH_ADDRESS (x_18262, x_18261) -> h_HIGH_ADDRESS x_18262 x_18261
     261| LOW_ADDRESS (x_7669, x_7668) -> h_LOW_ADDRESS x_7669 x_7668
     262| HIGH_ADDRESS (x_7671, x_7670) -> h_HIGH_ADDRESS x_7671 x_7670
    263263
    264264(** val ltl_lin_seq_rect_Type2 :
     
    268268| SAVE_CARRY -> h_SAVE_CARRY
    269269| RESTORE_CARRY -> h_RESTORE_CARRY
    270 | LOW_ADDRESS (x_18269, x_18268) -> h_LOW_ADDRESS x_18269 x_18268
    271 | HIGH_ADDRESS (x_18271, x_18270) -> h_HIGH_ADDRESS x_18271 x_18270
     270| LOW_ADDRESS (x_7678, x_7677) -> h_LOW_ADDRESS x_7678 x_7677
     271| HIGH_ADDRESS (x_7680, x_7679) -> h_HIGH_ADDRESS x_7680 x_7679
    272272
    273273(** val ltl_lin_seq_rect_Type1 :
     
    277277| SAVE_CARRY -> h_SAVE_CARRY
    278278| RESTORE_CARRY -> h_RESTORE_CARRY
    279 | LOW_ADDRESS (x_18278, x_18277) -> h_LOW_ADDRESS x_18278 x_18277
    280 | HIGH_ADDRESS (x_18280, x_18279) -> h_HIGH_ADDRESS x_18280 x_18279
     279| LOW_ADDRESS (x_7687, x_7686) -> h_LOW_ADDRESS x_7687 x_7686
     280| HIGH_ADDRESS (x_7689, x_7688) -> h_HIGH_ADDRESS x_7689 x_7688
    281281
    282282(** val ltl_lin_seq_rect_Type0 :
     
    286286| SAVE_CARRY -> h_SAVE_CARRY
    287287| RESTORE_CARRY -> h_RESTORE_CARRY
    288 | LOW_ADDRESS (x_18287, x_18286) -> h_LOW_ADDRESS x_18287 x_18286
    289 | HIGH_ADDRESS (x_18289, x_18288) -> h_HIGH_ADDRESS x_18289 x_18288
     288| LOW_ADDRESS (x_7696, x_7695) -> h_LOW_ADDRESS x_7696 x_7695
     289| HIGH_ADDRESS (x_7698, x_7697) -> h_HIGH_ADDRESS x_7698 x_7697
    290290
    291291(** val ltl_lin_seq_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.