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/classifyOp.ml

    r2743 r2773  
    11open Preamble
    22
    3 open BitVectorTrie
    4 
    53open CostLabel
    64
     
    2119open Extralib
    2220
     21open Lists
     22
     23open Positive
     24
     25open Identifiers
     26
     27open Exp
     28
     29open Arithmetic
     30
     31open Vector
     32
     33open Div_and_mod
     34
     35open Util
     36
     37open FoldStuff
     38
     39open BitVector
     40
     41open Jmeq
     42
     43open Russell
     44
     45open List
     46
    2347open Setoids
    2448
     
    2650
    2751open Option
    28 
    29 open Lists
    30 
    31 open Positive
    32 
    33 open Identifiers
    34 
    35 open Exp
    36 
    37 open Arithmetic
    38 
    39 open Vector
    40 
    41 open Div_and_mod
    42 
    43 open Jmeq
    44 
    45 open Russell
    46 
    47 open List
    48 
    49 open Util
    50 
    51 open FoldStuff
    52 
    53 open BitVector
    5452
    5553open Extranat
     
    9896    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    9997    -> classify_add_cases -> 'a1 **)
    100 let rec classify_add_cases_rect_Type4 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7350 x_7349 = function
     98let rec classify_add_cases_rect_Type4 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_2428 x_2427 = function
    10199| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    102100| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    110108    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    111109    -> classify_add_cases -> 'a1 **)
    112 let rec classify_add_cases_rect_Type5 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7357 x_7356 = function
     110let rec classify_add_cases_rect_Type5 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_2435 x_2434 = function
    113111| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    114112| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    122120    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    123121    -> classify_add_cases -> 'a1 **)
    124 let rec classify_add_cases_rect_Type3 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7364 x_7363 = function
     122let rec classify_add_cases_rect_Type3 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_2442 x_2441 = function
    125123| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    126124| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    134132    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    135133    -> classify_add_cases -> 'a1 **)
    136 let rec classify_add_cases_rect_Type2 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7371 x_7370 = function
     134let rec classify_add_cases_rect_Type2 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_2449 x_2448 = function
    137135| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    138136| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    146144    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    147145    -> classify_add_cases -> 'a1 **)
    148 let rec classify_add_cases_rect_Type1 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7378 x_7377 = function
     146let rec classify_add_cases_rect_Type1 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_2456 x_2455 = function
    149147| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    150148| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    158156    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    159157    -> classify_add_cases -> 'a1 **)
    160 let rec classify_add_cases_rect_Type0 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7385 x_7384 = function
     158let rec classify_add_cases_rect_Type0 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_2463 x_2462 = function
    161159| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    162160| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    321319    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    322320    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    323 let rec classify_sub_cases_rect_Type4 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7441 x_7440 = function
     321let rec classify_sub_cases_rect_Type4 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_2519 x_2518 = function
    324322| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    325323| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    333331    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    334332    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    335 let rec classify_sub_cases_rect_Type5 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7448 x_7447 = function
     333let rec classify_sub_cases_rect_Type5 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_2526 x_2525 = function
    336334| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    337335| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    345343    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    346344    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    347 let rec classify_sub_cases_rect_Type3 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7455 x_7454 = function
     345let rec classify_sub_cases_rect_Type3 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_2533 x_2532 = function
    348346| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    349347| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    357355    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    358356    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    359 let rec classify_sub_cases_rect_Type2 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7462 x_7461 = function
     357let rec classify_sub_cases_rect_Type2 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_2540 x_2539 = function
    360358| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    361359| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    369367    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    370368    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    371 let rec classify_sub_cases_rect_Type1 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7469 x_7468 = function
     369let rec classify_sub_cases_rect_Type1 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_2547 x_2546 = function
    372370| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    373371| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    381379    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    382380    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    383 let rec classify_sub_cases_rect_Type0 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7476 x_7475 = function
     381let rec classify_sub_cases_rect_Type0 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_2554 x_2553 = function
    384382| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    385383| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    521519    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    522520    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    523 let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_7530 x_7529 = function
     521let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_2608 x_2607 = function
    524522| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    525523| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    528526    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    529527    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    530 let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_7535 x_7534 = function
     528let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_2613 x_2612 = function
    531529| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    532530| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    535533    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    536534    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    537 let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_7540 x_7539 = function
     535let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_2618 x_2617 = function
    538536| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    539537| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    542540    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    543541    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    544 let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_7545 x_7544 = function
     542let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_2623 x_2622 = function
    545543| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    546544| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    549547    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    550548    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    551 let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_7550 x_7549 = function
     549let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_2628 x_2627 = function
    552550| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    553551| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    556554    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    557555    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    558 let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_7555 x_7554 = function
     556let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_2633 x_2632 = function
    559557| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    560558| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    638636    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    639637    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    640 let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7596 x_7595 = function
     638let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_2674 x_2673 = function
    641639| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    642640| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    647645    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    648646    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    649 let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7602 x_7601 = function
     647let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_2680 x_2679 = function
    650648| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    651649| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    656654    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    657655    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    658 let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7608 x_7607 = function
     656let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_2686 x_2685 = function
    659657| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    660658| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    665663    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    666664    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    667 let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7614 x_7613 = function
     665let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_2692 x_2691 = function
    668666| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    669667| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    674672    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    675673    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    676 let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7620 x_7619 = function
     674let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_2698 x_2697 = function
    677675| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    678676| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    683681    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    684682    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    685 let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7626 x_7625 = function
     683let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_2704 x_2703 = function
    686684| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    687685| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    782780    -> 'a1 **)
    783781let rec classify_fun_cases_rect_Type4 h_fun_case_f h_fun_default = function
    784 | Fun_case_f (x_7674, x_7673) -> h_fun_case_f x_7674 x_7673
     782| Fun_case_f (x_2752, x_2751) -> h_fun_case_f x_2752 x_2751
    785783| Fun_default -> h_fun_default
    786784
     
    789787    -> 'a1 **)
    790788let rec classify_fun_cases_rect_Type5 h_fun_case_f h_fun_default = function
    791 | Fun_case_f (x_7679, x_7678) -> h_fun_case_f x_7679 x_7678
     789| Fun_case_f (x_2757, x_2756) -> h_fun_case_f x_2757 x_2756
    792790| Fun_default -> h_fun_default
    793791
     
    796794    -> 'a1 **)
    797795let rec classify_fun_cases_rect_Type3 h_fun_case_f h_fun_default = function
    798 | Fun_case_f (x_7684, x_7683) -> h_fun_case_f x_7684 x_7683
     796| Fun_case_f (x_2762, x_2761) -> h_fun_case_f x_2762 x_2761
    799797| Fun_default -> h_fun_default
    800798
     
    803801    -> 'a1 **)
    804802let rec classify_fun_cases_rect_Type2 h_fun_case_f h_fun_default = function
    805 | Fun_case_f (x_7689, x_7688) -> h_fun_case_f x_7689 x_7688
     803| Fun_case_f (x_2767, x_2766) -> h_fun_case_f x_2767 x_2766
    806804| Fun_default -> h_fun_default
    807805
     
    810808    -> 'a1 **)
    811809let rec classify_fun_cases_rect_Type1 h_fun_case_f h_fun_default = function
    812 | Fun_case_f (x_7694, x_7693) -> h_fun_case_f x_7694 x_7693
     810| Fun_case_f (x_2772, x_2771) -> h_fun_case_f x_2772 x_2771
    813811| Fun_default -> h_fun_default
    814812
     
    817815    -> 'a1 **)
    818816let rec classify_fun_cases_rect_Type0 h_fun_case_f h_fun_default = function
    819 | Fun_case_f (x_7699, x_7698) -> h_fun_case_f x_7699 x_7698
     817| Fun_case_f (x_2777, x_2776) -> h_fun_case_f x_2777 x_2776
    820818| Fun_default -> h_fun_default
    821819
     
    876874   | Csyntax.Tpointer x -> Fun_default
    877875   | Csyntax.Tarray (x, x0) -> Fun_default
    878    | Csyntax.Tfunction (args, res1) -> Fun_case_f (args, res1)
     876   | Csyntax.Tfunction (args, res) -> Fun_case_f (args, res)
    879877   | Csyntax.Tstruct (x, x0) -> Fun_default
    880878   | Csyntax.Tunion (x, x0) -> Fun_default
    881879   | Csyntax.Tcomp_ptr x -> Fun_default)
    882880| Csyntax.Tarray (x, x0) -> Fun_default
    883 | Csyntax.Tfunction (args, res1) -> Fun_case_f (args, res1)
     881| Csyntax.Tfunction (args, res) -> Fun_case_f (args, res)
    884882| Csyntax.Tstruct (x, x0) -> Fun_default
    885883| Csyntax.Tunion (x, x0) -> Fun_default
Note: See TracChangeset for help on using the changeset viewer.