Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/classifyOp.ml

    r2649 r2717  
    11open Preamble
    22
     3open BitVectorTrie
     4
    35open CostLabel
    46
     
    3032
    3133open Identifiers
     34
     35open Exp
    3236
    3337open Arithmetic
     
    9498    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    9599    -> classify_add_cases -> 'a1 **)
    96 let 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
     100let rec classify_add_cases_rect_Type4 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7324 x_7323 = function
    97101| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    98102| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    106110    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    107111    -> classify_add_cases -> 'a1 **)
    108 let 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
     112let rec classify_add_cases_rect_Type5 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7331 x_7330 = function
    109113| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    110114| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    118122    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    119123    -> classify_add_cases -> 'a1 **)
    120 let 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
     124let rec classify_add_cases_rect_Type3 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7338 x_7337 = function
    121125| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    122126| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    130134    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    131135    -> classify_add_cases -> 'a1 **)
    132 let 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
     136let rec classify_add_cases_rect_Type2 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7345 x_7344 = function
    133137| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    134138| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    142146    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    143147    -> classify_add_cases -> 'a1 **)
    144 let 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
     148let rec classify_add_cases_rect_Type1 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7352 x_7351 = function
    145149| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    146150| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    154158    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    155159    -> classify_add_cases -> 'a1 **)
    156 let 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
     160let rec classify_add_cases_rect_Type0 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7359 x_7358 = function
    157161| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    158162| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    317321    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    318322    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    319 let 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
     323let rec classify_sub_cases_rect_Type4 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7415 x_7414 = function
    320324| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    321325| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    329333    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    330334    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    331 let 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
     335let rec classify_sub_cases_rect_Type5 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7422 x_7421 = function
    332336| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    333337| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    341345    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    342346    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    343 let 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
     347let rec classify_sub_cases_rect_Type3 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7429 x_7428 = function
    344348| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    345349| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    353357    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    354358    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    355 let 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
     359let rec classify_sub_cases_rect_Type2 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7436 x_7435 = function
    356360| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    357361| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    365369    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    366370    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    367 let 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
     371let rec classify_sub_cases_rect_Type1 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7443 x_7442 = function
    368372| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    369373| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    377381    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    378382    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    379 let 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
     383let rec classify_sub_cases_rect_Type0 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7450 x_7449 = function
    380384| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    381385| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    517521    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    518522    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    519 let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_3575 x_3574 = function
     523let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_7504 x_7503 = function
    520524| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    521525| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    524528    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    525529    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    526 let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_3580 x_3579 = function
     530let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_7509 x_7508 = function
    527531| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    528532| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    531535    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    532536    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    533 let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_3585 x_3584 = function
     537let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_7514 x_7513 = function
    534538| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    535539| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    538542    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    539543    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    540 let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_3590 x_3589 = function
     544let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_7519 x_7518 = function
    541545| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    542546| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    545549    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    546550    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    547 let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_3595 x_3594 = function
     551let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_7524 x_7523 = function
    548552| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    549553| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    552556    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    553557    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    554 let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_3600 x_3599 = function
     558let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_7529 x_7528 = function
    555559| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    556560| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    634638    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    635639    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    636 let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_3641 x_3640 = function
     640let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7570 x_7569 = function
    637641| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    638642| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    643647    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    644648    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    645 let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_3647 x_3646 = function
     649let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7576 x_7575 = function
    646650| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    647651| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    652656    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    653657    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    654 let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_3653 x_3652 = function
     658let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7582 x_7581 = function
    655659| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    656660| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    661665    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    662666    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    663 let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_3659 x_3658 = function
     667let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7588 x_7587 = function
    664668| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    665669| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    670674    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    671675    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    672 let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_3665 x_3664 = function
     676let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7594 x_7593 = function
    673677| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    674678| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    679683    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    680684    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    681 let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_3671 x_3670 = function
     685let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7600 x_7599 = function
    682686| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    683687| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    778782    -> 'a1 **)
    779783let rec classify_fun_cases_rect_Type4 h_fun_case_f h_fun_default = function
    780 | Fun_case_f (x_3719, x_3718) -> h_fun_case_f x_3719 x_3718
     784| Fun_case_f (x_7648, x_7647) -> h_fun_case_f x_7648 x_7647
    781785| Fun_default -> h_fun_default
    782786
     
    785789    -> 'a1 **)
    786790let rec classify_fun_cases_rect_Type5 h_fun_case_f h_fun_default = function
    787 | Fun_case_f (x_3724, x_3723) -> h_fun_case_f x_3724 x_3723
     791| Fun_case_f (x_7653, x_7652) -> h_fun_case_f x_7653 x_7652
    788792| Fun_default -> h_fun_default
    789793
     
    792796    -> 'a1 **)
    793797let rec classify_fun_cases_rect_Type3 h_fun_case_f h_fun_default = function
    794 | Fun_case_f (x_3729, x_3728) -> h_fun_case_f x_3729 x_3728
     798| Fun_case_f (x_7658, x_7657) -> h_fun_case_f x_7658 x_7657
    795799| Fun_default -> h_fun_default
    796800
     
    799803    -> 'a1 **)
    800804let rec classify_fun_cases_rect_Type2 h_fun_case_f h_fun_default = function
    801 | Fun_case_f (x_3734, x_3733) -> h_fun_case_f x_3734 x_3733
     805| Fun_case_f (x_7663, x_7662) -> h_fun_case_f x_7663 x_7662
    802806| Fun_default -> h_fun_default
    803807
     
    806810    -> 'a1 **)
    807811let rec classify_fun_cases_rect_Type1 h_fun_case_f h_fun_default = function
    808 | Fun_case_f (x_3739, x_3738) -> h_fun_case_f x_3739 x_3738
     812| Fun_case_f (x_7668, x_7667) -> h_fun_case_f x_7668 x_7667
    809813| Fun_default -> h_fun_default
    810814
     
    813817    -> 'a1 **)
    814818let rec classify_fun_cases_rect_Type0 h_fun_case_f h_fun_default = function
    815 | Fun_case_f (x_3744, x_3743) -> h_fun_case_f x_3744 x_3743
     819| Fun_case_f (x_7673, x_7672) -> h_fun_case_f x_7673 x_7672
    816820| Fun_default -> h_fun_default
    817821
Note: See TracChangeset for help on using the changeset viewer.