Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint_LTL_LIN.ml

    r2743 r2773  
    99open LabelledObjects
    1010
     11open BitVectorTrie
     12
    1113open Graphs
    1214
     
    1719open Registers
    1820
    19 open BitVectorTrie
    20 
    2121open CostLabel
    2222
     
    3737open Extralib
    3838
     39open Lists
     40
     41open Identifiers
     42
     43open Integers
     44
     45open AST
     46
     47open Division
     48
     49open Exp
     50
     51open Arithmetic
     52
    3953open Setoids
    4054
     
    4256
    4357open Option
    44 
    45 open Lists
    46 
    47 open Identifiers
    48 
    49 open Integers
    50 
    51 open AST
    52 
    53 open Division
    54 
    55 open Exp
    56 
    57 open Arithmetic
    5858
    5959open Extranat
     
    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_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
     118| From_acc (x_16467, x_16466) -> h_from_acc x_16467 x_16466
     119| To_acc (x_16469, x_16468) -> h_to_acc x_16469 x_16468
     120| Int_to_reg (x_16471, x_16470) -> h_int_to_reg x_16471 x_16470
     121| Int_to_acc (x_16473, x_16472) -> h_int_to_acc x_16473 x_16472
    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_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
     128| From_acc (x_16480, x_16479) -> h_from_acc x_16480 x_16479
     129| To_acc (x_16482, x_16481) -> h_to_acc x_16482 x_16481
     130| Int_to_reg (x_16484, x_16483) -> h_int_to_reg x_16484 x_16483
     131| Int_to_acc (x_16486, x_16485) -> h_int_to_acc x_16486 x_16485
    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_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
     138| From_acc (x_16493, x_16492) -> h_from_acc x_16493 x_16492
     139| To_acc (x_16495, x_16494) -> h_to_acc x_16495 x_16494
     140| Int_to_reg (x_16497, x_16496) -> h_int_to_reg x_16497 x_16496
     141| Int_to_acc (x_16499, x_16498) -> h_int_to_acc x_16499 x_16498
    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_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
     148| From_acc (x_16506, x_16505) -> h_from_acc x_16506 x_16505
     149| To_acc (x_16508, x_16507) -> h_to_acc x_16508 x_16507
     150| Int_to_reg (x_16510, x_16509) -> h_int_to_reg x_16510 x_16509
     151| Int_to_acc (x_16512, x_16511) -> h_int_to_acc x_16512 x_16511
    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_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
     158| From_acc (x_16519, x_16518) -> h_from_acc x_16519 x_16518
     159| To_acc (x_16521, x_16520) -> h_to_acc x_16521 x_16520
     160| Int_to_reg (x_16523, x_16522) -> h_int_to_reg x_16523 x_16522
     161| Int_to_acc (x_16525, x_16524) -> h_int_to_acc x_16525 x_16524
    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_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
     168| From_acc (x_16532, x_16531) -> h_from_acc x_16532 x_16531
     169| To_acc (x_16534, x_16533) -> h_to_acc x_16534 x_16533
     170| Int_to_reg (x_16536, x_16535) -> h_int_to_reg x_16536 x_16535
     171| Int_to_acc (x_16538, x_16537) -> h_int_to_acc x_16538 x_16537
    172172
    173173(** val registers_move_inv_rect_Type4 :
     
    241241| SAVE_CARRY -> h_SAVE_CARRY
    242242| RESTORE_CARRY -> h_RESTORE_CARRY
    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
     243| LOW_ADDRESS (x_16632, x_16631) -> h_LOW_ADDRESS x_16632 x_16631
     244| HIGH_ADDRESS (x_16634, x_16633) -> h_HIGH_ADDRESS x_16634 x_16633
    245245
    246246(** val ltl_lin_seq_rect_Type5 :
     
    250250| SAVE_CARRY -> h_SAVE_CARRY
    251251| RESTORE_CARRY -> h_RESTORE_CARRY
    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
     252| LOW_ADDRESS (x_16641, x_16640) -> h_LOW_ADDRESS x_16641 x_16640
     253| HIGH_ADDRESS (x_16643, x_16642) -> h_HIGH_ADDRESS x_16643 x_16642
    254254
    255255(** val ltl_lin_seq_rect_Type3 :
     
    259259| SAVE_CARRY -> h_SAVE_CARRY
    260260| RESTORE_CARRY -> h_RESTORE_CARRY
    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
     261| LOW_ADDRESS (x_16650, x_16649) -> h_LOW_ADDRESS x_16650 x_16649
     262| HIGH_ADDRESS (x_16652, x_16651) -> h_HIGH_ADDRESS x_16652 x_16651
    263263
    264264(** val ltl_lin_seq_rect_Type2 :
     
    268268| SAVE_CARRY -> h_SAVE_CARRY
    269269| RESTORE_CARRY -> h_RESTORE_CARRY
    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
     270| LOW_ADDRESS (x_16659, x_16658) -> h_LOW_ADDRESS x_16659 x_16658
     271| HIGH_ADDRESS (x_16661, x_16660) -> h_HIGH_ADDRESS x_16661 x_16660
    272272
    273273(** val ltl_lin_seq_rect_Type1 :
     
    277277| SAVE_CARRY -> h_SAVE_CARRY
    278278| RESTORE_CARRY -> h_RESTORE_CARRY
    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
     279| LOW_ADDRESS (x_16668, x_16667) -> h_LOW_ADDRESS x_16668 x_16667
     280| HIGH_ADDRESS (x_16670, x_16669) -> h_HIGH_ADDRESS x_16670 x_16669
    281281
    282282(** val ltl_lin_seq_rect_Type0 :
     
    286286| SAVE_CARRY -> h_SAVE_CARRY
    287287| RESTORE_CARRY -> h_RESTORE_CARRY
    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
     288| LOW_ADDRESS (x_16677, x_16676) -> h_LOW_ADDRESS x_16677 x_16676
     289| HIGH_ADDRESS (x_16679, x_16678) -> h_HIGH_ADDRESS x_16679 x_16678
    290290
    291291(** val ltl_lin_seq_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.