Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/classifyOp.ml

    r2601 r2649  
    33open CostLabel
    44
     5open Coqlib
     6
    57open Proper
    68
     
    911open Deqsets
    1012
     13open ErrorMessages
     14
    1115open PreIdentifiers
    1216
     
    2731open Identifiers
    2832
    29 open Coqlib
    30 
    31 open Floats
    32 
    3333open Arithmetic
    34 
    35 open Char
    36 
    37 open String
    3834
    3935open Vector
     
    9894    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    9995    -> 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_6323 x_6322 = function
     96let rec classify_add_cases_rect_Type4 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_3395 x_3394 = function
    10197| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    10298| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    110106    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    111107    -> 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_6330 x_6329 = function
     108let rec classify_add_cases_rect_Type5 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_3402 x_3401 = function
    113109| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    114110| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    122118    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    123119    -> 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_6337 x_6336 = function
     120let rec classify_add_cases_rect_Type3 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_3409 x_3408 = function
    125121| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    126122| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    134130    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    135131    -> 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_6344 x_6343 = function
     132let rec classify_add_cases_rect_Type2 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_3416 x_3415 = function
    137133| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    138134| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    146142    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    147143    -> 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_6351 x_6350 = function
     144let rec classify_add_cases_rect_Type1 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_3423 x_3422 = function
    149145| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    150146| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    158154    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    159155    -> 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_6358 x_6357 = function
     156let rec classify_add_cases_rect_Type0 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_3430 x_3429 = function
    161157| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    162158| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    321317    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    322318    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_6414 x_6413 = function
     319let rec classify_sub_cases_rect_Type4 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_3486 x_3485 = function
    324320| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    325321| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    333329    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    334330    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_6421 x_6420 = function
     331let rec classify_sub_cases_rect_Type5 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_3493 x_3492 = function
    336332| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    337333| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    345341    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    346342    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_6428 x_6427 = function
     343let rec classify_sub_cases_rect_Type3 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_3500 x_3499 = function
    348344| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    349345| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    357353    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    358354    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_6435 x_6434 = function
     355let rec classify_sub_cases_rect_Type2 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_3507 x_3506 = function
    360356| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    361357| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    369365    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    370366    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_6442 x_6441 = function
     367let rec classify_sub_cases_rect_Type1 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_3514 x_3513 = function
    372368| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    373369| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    381377    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    382378    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_6449 x_6448 = function
     379let rec classify_sub_cases_rect_Type0 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_3521 x_3520 = function
    384380| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    385381| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    521517    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    522518    -> '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_6503 x_6502 = function
     519let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_3575 x_3574 = function
    524520| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    525521| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    528524    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    529525    -> '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_6508 x_6507 = function
     526let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_3580 x_3579 = function
    531527| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    532528| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    535531    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    536532    -> '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_6513 x_6512 = function
     533let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_3585 x_3584 = function
    538534| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    539535| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    542538    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    543539    -> '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_6518 x_6517 = function
     540let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_3590 x_3589 = function
    545541| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    546542| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    549545    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    550546    -> '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_6523 x_6522 = function
     547let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_3595 x_3594 = function
    552548| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    553549| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    556552    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    557553    -> '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_6528 x_6527 = function
     554let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_3600 x_3599 = function
    559555| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    560556| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    638634    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    639635    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_6569 x_6568 = function
     636let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_3641 x_3640 = function
    641637| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    642638| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    647643    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    648644    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_6575 x_6574 = function
     645let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_3647 x_3646 = function
    650646| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    651647| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    656652    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    657653    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_6581 x_6580 = function
     654let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_3653 x_3652 = function
    659655| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    660656| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    665661    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    666662    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_6587 x_6586 = function
     663let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_3659 x_3658 = function
    668664| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    669665| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    674670    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    675671    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_6593 x_6592 = function
     672let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_3665 x_3664 = function
    677673| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    678674| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    683679    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    684680    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_6599 x_6598 = function
     681let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_3671 x_3670 = function
    686682| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    687683| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    782778    -> 'a1 **)
    783779let rec classify_fun_cases_rect_Type4 h_fun_case_f h_fun_default = function
    784 | Fun_case_f (x_6647, x_6646) -> h_fun_case_f x_6647 x_6646
     780| Fun_case_f (x_3719, x_3718) -> h_fun_case_f x_3719 x_3718
    785781| Fun_default -> h_fun_default
    786782
     
    789785    -> 'a1 **)
    790786let rec classify_fun_cases_rect_Type5 h_fun_case_f h_fun_default = function
    791 | Fun_case_f (x_6652, x_6651) -> h_fun_case_f x_6652 x_6651
     787| Fun_case_f (x_3724, x_3723) -> h_fun_case_f x_3724 x_3723
    792788| Fun_default -> h_fun_default
    793789
     
    796792    -> 'a1 **)
    797793let rec classify_fun_cases_rect_Type3 h_fun_case_f h_fun_default = function
    798 | Fun_case_f (x_6657, x_6656) -> h_fun_case_f x_6657 x_6656
     794| Fun_case_f (x_3729, x_3728) -> h_fun_case_f x_3729 x_3728
    799795| Fun_default -> h_fun_default
    800796
     
    803799    -> 'a1 **)
    804800let rec classify_fun_cases_rect_Type2 h_fun_case_f h_fun_default = function
    805 | Fun_case_f (x_6662, x_6661) -> h_fun_case_f x_6662 x_6661
     801| Fun_case_f (x_3734, x_3733) -> h_fun_case_f x_3734 x_3733
    806802| Fun_default -> h_fun_default
    807803
     
    810806    -> 'a1 **)
    811807let rec classify_fun_cases_rect_Type1 h_fun_case_f h_fun_default = function
    812 | Fun_case_f (x_6667, x_6666) -> h_fun_case_f x_6667 x_6666
     808| Fun_case_f (x_3739, x_3738) -> h_fun_case_f x_3739 x_3738
    813809| Fun_default -> h_fun_default
    814810
     
    817813    -> 'a1 **)
    818814let rec classify_fun_cases_rect_Type0 h_fun_case_f h_fun_default = function
    819 | Fun_case_f (x_6672, x_6671) -> h_fun_case_f x_6672 x_6671
     815| Fun_case_f (x_3744, x_3743) -> h_fun_case_f x_3744 x_3743
    820816| Fun_default -> h_fun_default
    821817
Note: See TracChangeset for help on using the changeset viewer.