Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/classifyOp.ml

    r2827 r2951  
    9696    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    9797    -> classify_add_cases -> 'a1 **)
    98 let rec classify_add_cases_rect_Type4 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7389 x_7388 = function
     98let rec classify_add_cases_rect_Type4 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7428 x_7427 = function
    9999| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    100100| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    108108    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    109109    -> classify_add_cases -> 'a1 **)
    110 let rec classify_add_cases_rect_Type5 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7396 x_7395 = function
     110let rec classify_add_cases_rect_Type5 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7435 x_7434 = function
    111111| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    112112| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    120120    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    121121    -> classify_add_cases -> 'a1 **)
    122 let rec classify_add_cases_rect_Type3 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7403 x_7402 = function
     122let rec classify_add_cases_rect_Type3 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7442 x_7441 = function
    123123| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    124124| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    132132    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    133133    -> classify_add_cases -> 'a1 **)
    134 let rec classify_add_cases_rect_Type2 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7410 x_7409 = function
     134let rec classify_add_cases_rect_Type2 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7449 x_7448 = function
    135135| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    136136| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    144144    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    145145    -> classify_add_cases -> 'a1 **)
    146 let rec classify_add_cases_rect_Type1 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7417 x_7416 = function
     146let rec classify_add_cases_rect_Type1 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7456 x_7455 = function
    147147| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    148148| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    156156    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    157157    -> classify_add_cases -> 'a1 **)
    158 let rec classify_add_cases_rect_Type0 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7424 x_7423 = function
     158let rec classify_add_cases_rect_Type0 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7463 x_7462 = function
    159159| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    160160| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    319319    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    320320    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    321 let rec classify_sub_cases_rect_Type4 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7480 x_7479 = function
     321let rec classify_sub_cases_rect_Type4 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7519 x_7518 = function
    322322| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    323323| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    331331    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    332332    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    333 let rec classify_sub_cases_rect_Type5 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7487 x_7486 = function
     333let rec classify_sub_cases_rect_Type5 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7526 x_7525 = function
    334334| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    335335| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    343343    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    344344    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    345 let rec classify_sub_cases_rect_Type3 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7494 x_7493 = function
     345let rec classify_sub_cases_rect_Type3 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7533 x_7532 = function
    346346| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    347347| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    355355    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    356356    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    357 let rec classify_sub_cases_rect_Type2 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7501 x_7500 = function
     357let rec classify_sub_cases_rect_Type2 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7540 x_7539 = function
    358358| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    359359| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    367367    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    368368    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    369 let rec classify_sub_cases_rect_Type1 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7508 x_7507 = function
     369let rec classify_sub_cases_rect_Type1 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7547 x_7546 = function
    370370| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    371371| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    379379    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    380380    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    381 let rec classify_sub_cases_rect_Type0 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7515 x_7514 = function
     381let rec classify_sub_cases_rect_Type0 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7554 x_7553 = function
    382382| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    383383| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    519519    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    520520    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    521 let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_7569 x_7568 = function
     521let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_7608 x_7607 = function
    522522| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    523523| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    526526    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    527527    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    528 let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_7574 x_7573 = function
     528let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_7613 x_7612 = function
    529529| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    530530| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    533533    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    534534    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    535 let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_7579 x_7578 = function
     535let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_7618 x_7617 = function
    536536| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    537537| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    540540    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    541541    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    542 let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_7584 x_7583 = function
     542let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_7623 x_7622 = function
    543543| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    544544| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    547547    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    548548    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    549 let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_7589 x_7588 = function
     549let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_7628 x_7627 = function
    550550| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    551551| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    554554    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    555555    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    556 let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_7594 x_7593 = function
     556let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_7633 x_7632 = function
    557557| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    558558| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    636636    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    637637    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    638 let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7635 x_7634 = function
     638let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7674 x_7673 = function
    639639| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    640640| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    645645    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    646646    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    647 let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7641 x_7640 = function
     647let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7680 x_7679 = function
    648648| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    649649| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    654654    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    655655    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    656 let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7647 x_7646 = function
     656let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7686 x_7685 = function
    657657| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    658658| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    663663    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    664664    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    665 let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7653 x_7652 = function
     665let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7692 x_7691 = function
    666666| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    667667| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    672672    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    673673    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    674 let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7659 x_7658 = function
     674let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7698 x_7697 = function
    675675| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    676676| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    681681    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    682682    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    683 let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7665 x_7664 = function
     683let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7704 x_7703 = function
    684684| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    685685| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    780780    -> 'a1 **)
    781781let rec classify_fun_cases_rect_Type4 h_fun_case_f h_fun_default = function
    782 | Fun_case_f (x_7713, x_7712) -> h_fun_case_f x_7713 x_7712
     782| Fun_case_f (x_7752, x_7751) -> h_fun_case_f x_7752 x_7751
    783783| Fun_default -> h_fun_default
    784784
     
    787787    -> 'a1 **)
    788788let rec classify_fun_cases_rect_Type5 h_fun_case_f h_fun_default = function
    789 | Fun_case_f (x_7718, x_7717) -> h_fun_case_f x_7718 x_7717
     789| Fun_case_f (x_7757, x_7756) -> h_fun_case_f x_7757 x_7756
    790790| Fun_default -> h_fun_default
    791791
     
    794794    -> 'a1 **)
    795795let rec classify_fun_cases_rect_Type3 h_fun_case_f h_fun_default = function
    796 | Fun_case_f (x_7723, x_7722) -> h_fun_case_f x_7723 x_7722
     796| Fun_case_f (x_7762, x_7761) -> h_fun_case_f x_7762 x_7761
    797797| Fun_default -> h_fun_default
    798798
     
    801801    -> 'a1 **)
    802802let rec classify_fun_cases_rect_Type2 h_fun_case_f h_fun_default = function
    803 | Fun_case_f (x_7728, x_7727) -> h_fun_case_f x_7728 x_7727
     803| Fun_case_f (x_7767, x_7766) -> h_fun_case_f x_7767 x_7766
    804804| Fun_default -> h_fun_default
    805805
     
    808808    -> 'a1 **)
    809809let rec classify_fun_cases_rect_Type1 h_fun_case_f h_fun_default = function
    810 | Fun_case_f (x_7733, x_7732) -> h_fun_case_f x_7733 x_7732
     810| Fun_case_f (x_7772, x_7771) -> h_fun_case_f x_7772 x_7771
    811811| Fun_default -> h_fun_default
    812812
     
    815815    -> 'a1 **)
    816816let rec classify_fun_cases_rect_Type0 h_fun_case_f h_fun_default = function
    817 | Fun_case_f (x_7738, x_7737) -> h_fun_case_f x_7738 x_7737
     817| Fun_case_f (x_7777, x_7776) -> h_fun_case_f x_7777 x_7776
    818818| Fun_default -> h_fun_default
    819819
Note: See TracChangeset for help on using the changeset viewer.