Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (7 years ago)
Author:
sacerdot
Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint_LTL_LIN.ml

    r2730 r2743  
    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_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
     118| From_acc (x_21157, x_21156) -> h_from_acc x_21157 x_21156
     119| To_acc (x_21159, x_21158) -> h_to_acc x_21159 x_21158
     120| Int_to_reg (x_21161, x_21160) -> h_int_to_reg x_21161 x_21160
     121| Int_to_acc (x_21163, x_21162) -> h_int_to_acc x_21163 x_21162
    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_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
     128| From_acc (x_21170, x_21169) -> h_from_acc x_21170 x_21169
     129| To_acc (x_21172, x_21171) -> h_to_acc x_21172 x_21171
     130| Int_to_reg (x_21174, x_21173) -> h_int_to_reg x_21174 x_21173
     131| Int_to_acc (x_21176, x_21175) -> h_int_to_acc x_21176 x_21175
    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_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
     138| From_acc (x_21183, x_21182) -> h_from_acc x_21183 x_21182
     139| To_acc (x_21185, x_21184) -> h_to_acc x_21185 x_21184
     140| Int_to_reg (x_21187, x_21186) -> h_int_to_reg x_21187 x_21186
     141| Int_to_acc (x_21189, x_21188) -> h_int_to_acc x_21189 x_21188
    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_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
     148| From_acc (x_21196, x_21195) -> h_from_acc x_21196 x_21195
     149| To_acc (x_21198, x_21197) -> h_to_acc x_21198 x_21197
     150| Int_to_reg (x_21200, x_21199) -> h_int_to_reg x_21200 x_21199
     151| Int_to_acc (x_21202, x_21201) -> h_int_to_acc x_21202 x_21201
    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_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
     158| From_acc (x_21209, x_21208) -> h_from_acc x_21209 x_21208
     159| To_acc (x_21211, x_21210) -> h_to_acc x_21211 x_21210
     160| Int_to_reg (x_21213, x_21212) -> h_int_to_reg x_21213 x_21212
     161| Int_to_acc (x_21215, x_21214) -> h_int_to_acc x_21215 x_21214
    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_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
     168| From_acc (x_21222, x_21221) -> h_from_acc x_21222 x_21221
     169| To_acc (x_21224, x_21223) -> h_to_acc x_21224 x_21223
     170| Int_to_reg (x_21226, x_21225) -> h_int_to_reg x_21226 x_21225
     171| Int_to_acc (x_21228, x_21227) -> h_int_to_acc x_21228 x_21227
    172172
    173173(** val registers_move_inv_rect_Type4 :
     
    241241| SAVE_CARRY -> h_SAVE_CARRY
    242242| RESTORE_CARRY -> h_RESTORE_CARRY
    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
     243| LOW_ADDRESS (x_21322, x_21321) -> h_LOW_ADDRESS x_21322 x_21321
     244| HIGH_ADDRESS (x_21324, x_21323) -> h_HIGH_ADDRESS x_21324 x_21323
    245245
    246246(** val ltl_lin_seq_rect_Type5 :
     
    250250| SAVE_CARRY -> h_SAVE_CARRY
    251251| RESTORE_CARRY -> h_RESTORE_CARRY
    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
     252| LOW_ADDRESS (x_21331, x_21330) -> h_LOW_ADDRESS x_21331 x_21330
     253| HIGH_ADDRESS (x_21333, x_21332) -> h_HIGH_ADDRESS x_21333 x_21332
    254254
    255255(** val ltl_lin_seq_rect_Type3 :
     
    259259| SAVE_CARRY -> h_SAVE_CARRY
    260260| RESTORE_CARRY -> h_RESTORE_CARRY
    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
     261| LOW_ADDRESS (x_21340, x_21339) -> h_LOW_ADDRESS x_21340 x_21339
     262| HIGH_ADDRESS (x_21342, x_21341) -> h_HIGH_ADDRESS x_21342 x_21341
    263263
    264264(** val ltl_lin_seq_rect_Type2 :
     
    268268| SAVE_CARRY -> h_SAVE_CARRY
    269269| RESTORE_CARRY -> h_RESTORE_CARRY
    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
     270| LOW_ADDRESS (x_21349, x_21348) -> h_LOW_ADDRESS x_21349 x_21348
     271| HIGH_ADDRESS (x_21351, x_21350) -> h_HIGH_ADDRESS x_21351 x_21350
    272272
    273273(** val ltl_lin_seq_rect_Type1 :
     
    277277| SAVE_CARRY -> h_SAVE_CARRY
    278278| RESTORE_CARRY -> h_RESTORE_CARRY
    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
     279| LOW_ADDRESS (x_21358, x_21357) -> h_LOW_ADDRESS x_21358 x_21357
     280| HIGH_ADDRESS (x_21360, x_21359) -> h_HIGH_ADDRESS x_21360 x_21359
    281281
    282282(** val ltl_lin_seq_rect_Type0 :
     
    286286| SAVE_CARRY -> h_SAVE_CARRY
    287287| RESTORE_CARRY -> h_RESTORE_CARRY
    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
     288| LOW_ADDRESS (x_21367, x_21366) -> h_LOW_ADDRESS x_21367 x_21366
     289| HIGH_ADDRESS (x_21369, x_21368) -> h_HIGH_ADDRESS x_21369 x_21368
    290290
    291291(** val ltl_lin_seq_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.