Changeset 2775 for extracted/aST.ml


Ignore:
Timestamp:
Mar 5, 2013, 9:52:39 PM (7 years ago)
Author:
sacerdot
Message:

The compiler now computes also the stack cost model.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/aST.ml

    r2773 r2775  
    418418    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    419419let rec typ_rect_Type4 h_ASTint h_ASTptr = function
    420 | ASTint (x_3766, x_3765) -> h_ASTint x_3766 x_3765
     420| ASTint (x_3519, x_3518) -> h_ASTint x_3519 x_3518
    421421| ASTptr -> h_ASTptr
    422422
     
    424424    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    425425let rec typ_rect_Type5 h_ASTint h_ASTptr = function
    426 | ASTint (x_3771, x_3770) -> h_ASTint x_3771 x_3770
     426| ASTint (x_3524, x_3523) -> h_ASTint x_3524 x_3523
    427427| ASTptr -> h_ASTptr
    428428
     
    430430    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    431431let rec typ_rect_Type3 h_ASTint h_ASTptr = function
    432 | ASTint (x_3776, x_3775) -> h_ASTint x_3776 x_3775
     432| ASTint (x_3529, x_3528) -> h_ASTint x_3529 x_3528
    433433| ASTptr -> h_ASTptr
    434434
     
    436436    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    437437let rec typ_rect_Type2 h_ASTint h_ASTptr = function
    438 | ASTint (x_3781, x_3780) -> h_ASTint x_3781 x_3780
     438| ASTint (x_3534, x_3533) -> h_ASTint x_3534 x_3533
    439439| ASTptr -> h_ASTptr
    440440
     
    442442    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    443443let rec typ_rect_Type1 h_ASTint h_ASTptr = function
    444 | ASTint (x_3786, x_3785) -> h_ASTint x_3786 x_3785
     444| ASTint (x_3539, x_3538) -> h_ASTint x_3539 x_3538
    445445| ASTptr -> h_ASTptr
    446446
     
    448448    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    449449let rec typ_rect_Type0 h_ASTint h_ASTptr = function
    450 | ASTint (x_3791, x_3790) -> h_ASTint x_3791 x_3790
     450| ASTint (x_3544, x_3543) -> h_ASTint x_3544 x_3543
    451451| ASTptr -> h_ASTptr
    452452
     
    877877(** val signature_rect_Type4 :
    878878    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    879 let rec signature_rect_Type4 h_mk_signature x_3826 =
    880   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3826 in
     879let rec signature_rect_Type4 h_mk_signature x_3579 =
     880  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3579 in
    881881  h_mk_signature sig_args0 sig_res0
    882882
    883883(** val signature_rect_Type5 :
    884884    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    885 let rec signature_rect_Type5 h_mk_signature x_3828 =
    886   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3828 in
     885let rec signature_rect_Type5 h_mk_signature x_3581 =
     886  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3581 in
    887887  h_mk_signature sig_args0 sig_res0
    888888
    889889(** val signature_rect_Type3 :
    890890    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    891 let rec signature_rect_Type3 h_mk_signature x_3830 =
    892   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3830 in
     891let rec signature_rect_Type3 h_mk_signature x_3583 =
     892  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3583 in
    893893  h_mk_signature sig_args0 sig_res0
    894894
    895895(** val signature_rect_Type2 :
    896896    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    897 let rec signature_rect_Type2 h_mk_signature x_3832 =
    898   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3832 in
     897let rec signature_rect_Type2 h_mk_signature x_3585 =
     898  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3585 in
    899899  h_mk_signature sig_args0 sig_res0
    900900
    901901(** val signature_rect_Type1 :
    902902    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    903 let rec signature_rect_Type1 h_mk_signature x_3834 =
    904   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3834 in
     903let rec signature_rect_Type1 h_mk_signature x_3587 =
     904  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3587 in
    905905  h_mk_signature sig_args0 sig_res0
    906906
    907907(** val signature_rect_Type0 :
    908908    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    909 let rec signature_rect_Type0 h_mk_signature x_3836 =
    910   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3836 in
     909let rec signature_rect_Type0 h_mk_signature x_3589 =
     910  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3589 in
    911911  h_mk_signature sig_args0 sig_res0
    912912
     
    984984    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    985985let rec init_data_rect_Type4 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    986 | Init_int8 x_3864 -> h_Init_int8 x_3864
    987 | Init_int16 x_3865 -> h_Init_int16 x_3865
    988 | Init_int32 x_3866 -> h_Init_int32 x_3866
    989 | Init_space x_3867 -> h_Init_space x_3867
     986| Init_int8 x_3617 -> h_Init_int8 x_3617
     987| Init_int16 x_3618 -> h_Init_int16 x_3618
     988| Init_int32 x_3619 -> h_Init_int32 x_3619
     989| Init_space x_3620 -> h_Init_space x_3620
    990990| Init_null -> h_Init_null
    991 | Init_addrof (x_3869, x_3868) -> h_Init_addrof x_3869 x_3868
     991| Init_addrof (x_3622, x_3621) -> h_Init_addrof x_3622 x_3621
    992992
    993993(** val init_data_rect_Type5 :
     
    995995    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    996996let rec init_data_rect_Type5 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    997 | Init_int8 x_3877 -> h_Init_int8 x_3877
    998 | Init_int16 x_3878 -> h_Init_int16 x_3878
    999 | Init_int32 x_3879 -> h_Init_int32 x_3879
    1000 | Init_space x_3880 -> h_Init_space x_3880
     997| Init_int8 x_3630 -> h_Init_int8 x_3630
     998| Init_int16 x_3631 -> h_Init_int16 x_3631
     999| Init_int32 x_3632 -> h_Init_int32 x_3632
     1000| Init_space x_3633 -> h_Init_space x_3633
    10011001| Init_null -> h_Init_null
    1002 | Init_addrof (x_3882, x_3881) -> h_Init_addrof x_3882 x_3881
     1002| Init_addrof (x_3635, x_3634) -> h_Init_addrof x_3635 x_3634
    10031003
    10041004(** val init_data_rect_Type3 :
     
    10061006    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10071007let rec init_data_rect_Type3 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1008 | Init_int8 x_3890 -> h_Init_int8 x_3890
    1009 | Init_int16 x_3891 -> h_Init_int16 x_3891
    1010 | Init_int32 x_3892 -> h_Init_int32 x_3892
    1011 | Init_space x_3893 -> h_Init_space x_3893
     1008| Init_int8 x_3643 -> h_Init_int8 x_3643
     1009| Init_int16 x_3644 -> h_Init_int16 x_3644
     1010| Init_int32 x_3645 -> h_Init_int32 x_3645
     1011| Init_space x_3646 -> h_Init_space x_3646
    10121012| Init_null -> h_Init_null
    1013 | Init_addrof (x_3895, x_3894) -> h_Init_addrof x_3895 x_3894
     1013| Init_addrof (x_3648, x_3647) -> h_Init_addrof x_3648 x_3647
    10141014
    10151015(** val init_data_rect_Type2 :
     
    10171017    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10181018let rec init_data_rect_Type2 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1019 | Init_int8 x_3903 -> h_Init_int8 x_3903
    1020 | Init_int16 x_3904 -> h_Init_int16 x_3904
    1021 | Init_int32 x_3905 -> h_Init_int32 x_3905
    1022 | Init_space x_3906 -> h_Init_space x_3906
     1019| Init_int8 x_3656 -> h_Init_int8 x_3656
     1020| Init_int16 x_3657 -> h_Init_int16 x_3657
     1021| Init_int32 x_3658 -> h_Init_int32 x_3658
     1022| Init_space x_3659 -> h_Init_space x_3659
    10231023| Init_null -> h_Init_null
    1024 | Init_addrof (x_3908, x_3907) -> h_Init_addrof x_3908 x_3907
     1024| Init_addrof (x_3661, x_3660) -> h_Init_addrof x_3661 x_3660
    10251025
    10261026(** val init_data_rect_Type1 :
     
    10281028    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10291029let rec init_data_rect_Type1 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1030 | Init_int8 x_3916 -> h_Init_int8 x_3916
    1031 | Init_int16 x_3917 -> h_Init_int16 x_3917
    1032 | Init_int32 x_3918 -> h_Init_int32 x_3918
    1033 | Init_space x_3919 -> h_Init_space x_3919
     1030| Init_int8 x_3669 -> h_Init_int8 x_3669
     1031| Init_int16 x_3670 -> h_Init_int16 x_3670
     1032| Init_int32 x_3671 -> h_Init_int32 x_3671
     1033| Init_space x_3672 -> h_Init_space x_3672
    10341034| Init_null -> h_Init_null
    1035 | Init_addrof (x_3921, x_3920) -> h_Init_addrof x_3921 x_3920
     1035| Init_addrof (x_3674, x_3673) -> h_Init_addrof x_3674 x_3673
    10361036
    10371037(** val init_data_rect_Type0 :
     
    10391039    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10401040let rec init_data_rect_Type0 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1041 | Init_int8 x_3929 -> h_Init_int8 x_3929
    1042 | Init_int16 x_3930 -> h_Init_int16 x_3930
    1043 | Init_int32 x_3931 -> h_Init_int32 x_3931
    1044 | Init_space x_3932 -> h_Init_space x_3932
     1041| Init_int8 x_3682 -> h_Init_int8 x_3682
     1042| Init_int16 x_3683 -> h_Init_int16 x_3683
     1043| Init_int32 x_3684 -> h_Init_int32 x_3684
     1044| Init_space x_3685 -> h_Init_space x_3685
    10451045| Init_null -> h_Init_null
    1046 | Init_addrof (x_3934, x_3933) -> h_Init_addrof x_3934 x_3933
     1046| Init_addrof (x_3687, x_3686) -> h_Init_addrof x_3687 x_3686
    10471047
    10481048(** val init_data_inv_rect_Type4 :
     
    11111111    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11121112    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1113 let rec program_rect_Type4 h_mk_program x_4021 =
     1113let rec program_rect_Type4 h_mk_program x_3774 =
    11141114  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1115     prog_main0 } = x_4021
     1115    prog_main0 } = x_3774
    11161116  in
    11171117  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11201120    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11211121    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1122 let rec program_rect_Type5 h_mk_program x_4023 =
     1122let rec program_rect_Type5 h_mk_program x_3776 =
    11231123  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1124     prog_main0 } = x_4023
     1124    prog_main0 } = x_3776
    11251125  in
    11261126  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11291129    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11301130    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1131 let rec program_rect_Type3 h_mk_program x_4025 =
     1131let rec program_rect_Type3 h_mk_program x_3778 =
    11321132  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1133     prog_main0 } = x_4025
     1133    prog_main0 } = x_3778
    11341134  in
    11351135  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11381138    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11391139    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1140 let rec program_rect_Type2 h_mk_program x_4027 =
     1140let rec program_rect_Type2 h_mk_program x_3780 =
    11411141  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1142     prog_main0 } = x_4027
     1142    prog_main0 } = x_3780
    11431143  in
    11441144  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11471147    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11481148    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1149 let rec program_rect_Type1 h_mk_program x_4029 =
     1149let rec program_rect_Type1 h_mk_program x_3782 =
    11501150  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1151     prog_main0 } = x_4029
     1151    prog_main0 } = x_3782
    11521152  in
    11531153  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11561156    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11571157    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1158 let rec program_rect_Type0 h_mk_program x_4031 =
     1158let rec program_rect_Type0 h_mk_program x_3784 =
    11591159  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1160     prog_main0 } = x_4031
     1160    prog_main0 } = x_3784
    11611161  in
    11621162  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    14771477(** val external_function_rect_Type4 :
    14781478    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1479 let rec external_function_rect_Type4 h_mk_external_function x_4235 =
    1480   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4235 in
     1479let rec external_function_rect_Type4 h_mk_external_function x_3988 =
     1480  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3988 in
    14811481  h_mk_external_function ef_id0 ef_sig0
    14821482
    14831483(** val external_function_rect_Type5 :
    14841484    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1485 let rec external_function_rect_Type5 h_mk_external_function x_4237 =
    1486   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4237 in
     1485let rec external_function_rect_Type5 h_mk_external_function x_3990 =
     1486  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3990 in
    14871487  h_mk_external_function ef_id0 ef_sig0
    14881488
    14891489(** val external_function_rect_Type3 :
    14901490    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1491 let rec external_function_rect_Type3 h_mk_external_function x_4239 =
    1492   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4239 in
     1491let rec external_function_rect_Type3 h_mk_external_function x_3992 =
     1492  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3992 in
    14931493  h_mk_external_function ef_id0 ef_sig0
    14941494
    14951495(** val external_function_rect_Type2 :
    14961496    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1497 let rec external_function_rect_Type2 h_mk_external_function x_4241 =
    1498   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4241 in
     1497let rec external_function_rect_Type2 h_mk_external_function x_3994 =
     1498  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3994 in
    14991499  h_mk_external_function ef_id0 ef_sig0
    15001500
    15011501(** val external_function_rect_Type1 :
    15021502    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1503 let rec external_function_rect_Type1 h_mk_external_function x_4243 =
    1504   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4243 in
     1503let rec external_function_rect_Type1 h_mk_external_function x_3996 =
     1504  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3996 in
    15051505  h_mk_external_function ef_id0 ef_sig0
    15061506
    15071507(** val external_function_rect_Type0 :
    15081508    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1509 let rec external_function_rect_Type0 h_mk_external_function x_4245 =
    1510   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4245 in
     1509let rec external_function_rect_Type0 h_mk_external_function x_3998 =
     1510  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3998 in
    15111511  h_mk_external_function ef_id0 ef_sig0
    15121512
     
    15751575    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15761576let rec fundef_rect_Type4 h_Internal h_External = function
    1577 | Internal x_4265 -> h_Internal x_4265
    1578 | External x_4266 -> h_External x_4266
     1577| Internal x_4018 -> h_Internal x_4018
     1578| External x_4019 -> h_External x_4019
    15791579
    15801580(** val fundef_rect_Type5 :
    15811581    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15821582let rec fundef_rect_Type5 h_Internal h_External = function
    1583 | Internal x_4270 -> h_Internal x_4270
    1584 | External x_4271 -> h_External x_4271
     1583| Internal x_4023 -> h_Internal x_4023
     1584| External x_4024 -> h_External x_4024
    15851585
    15861586(** val fundef_rect_Type3 :
    15871587    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15881588let rec fundef_rect_Type3 h_Internal h_External = function
    1589 | Internal x_4275 -> h_Internal x_4275
    1590 | External x_4276 -> h_External x_4276
     1589| Internal x_4028 -> h_Internal x_4028
     1590| External x_4029 -> h_External x_4029
    15911591
    15921592(** val fundef_rect_Type2 :
    15931593    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15941594let rec fundef_rect_Type2 h_Internal h_External = function
    1595 | Internal x_4280 -> h_Internal x_4280
    1596 | External x_4281 -> h_External x_4281
     1595| Internal x_4033 -> h_Internal x_4033
     1596| External x_4034 -> h_External x_4034
    15971597
    15981598(** val fundef_rect_Type1 :
    15991599    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16001600let rec fundef_rect_Type1 h_Internal h_External = function
    1601 | Internal x_4285 -> h_Internal x_4285
    1602 | External x_4286 -> h_External x_4286
     1601| Internal x_4038 -> h_Internal x_4038
     1602| External x_4039 -> h_External x_4039
    16031603
    16041604(** val fundef_rect_Type0 :
    16051605    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16061606let rec fundef_rect_Type0 h_Internal h_External = function
    1607 | Internal x_4290 -> h_Internal x_4290
    1608 | External x_4291 -> h_External x_4291
     1607| Internal x_4043 -> h_Internal x_4043
     1608| External x_4044 -> h_External x_4044
    16091609
    16101610(** val fundef_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.