Changeset 2717 for extracted/aST.ml


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

    r2649 r2717  
    1010
    1111open Types
     12
     13open Exp
    1214
    1315open Arithmetic
     
    416418    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    417419let rec typ_rect_Type4 h_ASTint h_ASTptr = function
    418 | ASTint (x_1373, x_1372) -> h_ASTint x_1373 x_1372
     420| ASTint (x_3480, x_3479) -> h_ASTint x_3480 x_3479
    419421| ASTptr -> h_ASTptr
    420422
     
    422424    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    423425let rec typ_rect_Type5 h_ASTint h_ASTptr = function
    424 | ASTint (x_1378, x_1377) -> h_ASTint x_1378 x_1377
     426| ASTint (x_3485, x_3484) -> h_ASTint x_3485 x_3484
    425427| ASTptr -> h_ASTptr
    426428
     
    428430    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    429431let rec typ_rect_Type3 h_ASTint h_ASTptr = function
    430 | ASTint (x_1383, x_1382) -> h_ASTint x_1383 x_1382
     432| ASTint (x_3490, x_3489) -> h_ASTint x_3490 x_3489
    431433| ASTptr -> h_ASTptr
    432434
     
    434436    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    435437let rec typ_rect_Type2 h_ASTint h_ASTptr = function
    436 | ASTint (x_1388, x_1387) -> h_ASTint x_1388 x_1387
     438| ASTint (x_3495, x_3494) -> h_ASTint x_3495 x_3494
    437439| ASTptr -> h_ASTptr
    438440
     
    440442    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    441443let rec typ_rect_Type1 h_ASTint h_ASTptr = function
    442 | ASTint (x_1393, x_1392) -> h_ASTint x_1393 x_1392
     444| ASTint (x_3500, x_3499) -> h_ASTint x_3500 x_3499
    443445| ASTptr -> h_ASTptr
    444446
     
    446448    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    447449let rec typ_rect_Type0 h_ASTint h_ASTptr = function
    448 | ASTint (x_1398, x_1397) -> h_ASTint x_1398 x_1397
     450| ASTint (x_3505, x_3504) -> h_ASTint x_3505 x_3504
    449451| ASTptr -> h_ASTptr
    450452
     
    875877(** val signature_rect_Type4 :
    876878    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    877 let rec signature_rect_Type4 h_mk_signature x_1433 =
    878   let { sig_args = sig_args0; sig_res = sig_res0 } = x_1433 in
     879let rec signature_rect_Type4 h_mk_signature x_3540 =
     880  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3540 in
    879881  h_mk_signature sig_args0 sig_res0
    880882
    881883(** val signature_rect_Type5 :
    882884    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    883 let rec signature_rect_Type5 h_mk_signature x_1435 =
    884   let { sig_args = sig_args0; sig_res = sig_res0 } = x_1435 in
     885let rec signature_rect_Type5 h_mk_signature x_3542 =
     886  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3542 in
    885887  h_mk_signature sig_args0 sig_res0
    886888
    887889(** val signature_rect_Type3 :
    888890    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    889 let rec signature_rect_Type3 h_mk_signature x_1437 =
    890   let { sig_args = sig_args0; sig_res = sig_res0 } = x_1437 in
     891let rec signature_rect_Type3 h_mk_signature x_3544 =
     892  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3544 in
    891893  h_mk_signature sig_args0 sig_res0
    892894
    893895(** val signature_rect_Type2 :
    894896    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    895 let rec signature_rect_Type2 h_mk_signature x_1439 =
    896   let { sig_args = sig_args0; sig_res = sig_res0 } = x_1439 in
     897let rec signature_rect_Type2 h_mk_signature x_3546 =
     898  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3546 in
    897899  h_mk_signature sig_args0 sig_res0
    898900
    899901(** val signature_rect_Type1 :
    900902    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    901 let rec signature_rect_Type1 h_mk_signature x_1441 =
    902   let { sig_args = sig_args0; sig_res = sig_res0 } = x_1441 in
     903let rec signature_rect_Type1 h_mk_signature x_3548 =
     904  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3548 in
    903905  h_mk_signature sig_args0 sig_res0
    904906
    905907(** val signature_rect_Type0 :
    906908    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    907 let rec signature_rect_Type0 h_mk_signature x_1443 =
    908   let { sig_args = sig_args0; sig_res = sig_res0 } = x_1443 in
     909let rec signature_rect_Type0 h_mk_signature x_3550 =
     910  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3550 in
    909911  h_mk_signature sig_args0 sig_res0
    910912
     
    982984    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    983985let rec init_data_rect_Type4 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    984 | Init_int8 x_1471 -> h_Init_int8 x_1471
    985 | Init_int16 x_1472 -> h_Init_int16 x_1472
    986 | Init_int32 x_1473 -> h_Init_int32 x_1473
    987 | Init_space x_1474 -> h_Init_space x_1474
     986| Init_int8 x_3578 -> h_Init_int8 x_3578
     987| Init_int16 x_3579 -> h_Init_int16 x_3579
     988| Init_int32 x_3580 -> h_Init_int32 x_3580
     989| Init_space x_3581 -> h_Init_space x_3581
    988990| Init_null -> h_Init_null
    989 | Init_addrof (x_1476, x_1475) -> h_Init_addrof x_1476 x_1475
     991| Init_addrof (x_3583, x_3582) -> h_Init_addrof x_3583 x_3582
    990992
    991993(** val init_data_rect_Type5 :
     
    993995    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    994996let rec init_data_rect_Type5 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    995 | Init_int8 x_1484 -> h_Init_int8 x_1484
    996 | Init_int16 x_1485 -> h_Init_int16 x_1485
    997 | Init_int32 x_1486 -> h_Init_int32 x_1486
    998 | Init_space x_1487 -> h_Init_space x_1487
     997| Init_int8 x_3591 -> h_Init_int8 x_3591
     998| Init_int16 x_3592 -> h_Init_int16 x_3592
     999| Init_int32 x_3593 -> h_Init_int32 x_3593
     1000| Init_space x_3594 -> h_Init_space x_3594
    9991001| Init_null -> h_Init_null
    1000 | Init_addrof (x_1489, x_1488) -> h_Init_addrof x_1489 x_1488
     1002| Init_addrof (x_3596, x_3595) -> h_Init_addrof x_3596 x_3595
    10011003
    10021004(** val init_data_rect_Type3 :
     
    10041006    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10051007let rec init_data_rect_Type3 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1006 | Init_int8 x_1497 -> h_Init_int8 x_1497
    1007 | Init_int16 x_1498 -> h_Init_int16 x_1498
    1008 | Init_int32 x_1499 -> h_Init_int32 x_1499
    1009 | Init_space x_1500 -> h_Init_space x_1500
     1008| Init_int8 x_3604 -> h_Init_int8 x_3604
     1009| Init_int16 x_3605 -> h_Init_int16 x_3605
     1010| Init_int32 x_3606 -> h_Init_int32 x_3606
     1011| Init_space x_3607 -> h_Init_space x_3607
    10101012| Init_null -> h_Init_null
    1011 | Init_addrof (x_1502, x_1501) -> h_Init_addrof x_1502 x_1501
     1013| Init_addrof (x_3609, x_3608) -> h_Init_addrof x_3609 x_3608
    10121014
    10131015(** val init_data_rect_Type2 :
     
    10151017    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10161018let rec init_data_rect_Type2 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1017 | Init_int8 x_1510 -> h_Init_int8 x_1510
    1018 | Init_int16 x_1511 -> h_Init_int16 x_1511
    1019 | Init_int32 x_1512 -> h_Init_int32 x_1512
    1020 | Init_space x_1513 -> h_Init_space x_1513
     1019| Init_int8 x_3617 -> h_Init_int8 x_3617
     1020| Init_int16 x_3618 -> h_Init_int16 x_3618
     1021| Init_int32 x_3619 -> h_Init_int32 x_3619
     1022| Init_space x_3620 -> h_Init_space x_3620
    10211023| Init_null -> h_Init_null
    1022 | Init_addrof (x_1515, x_1514) -> h_Init_addrof x_1515 x_1514
     1024| Init_addrof (x_3622, x_3621) -> h_Init_addrof x_3622 x_3621
    10231025
    10241026(** val init_data_rect_Type1 :
     
    10261028    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10271029let rec init_data_rect_Type1 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1028 | Init_int8 x_1523 -> h_Init_int8 x_1523
    1029 | Init_int16 x_1524 -> h_Init_int16 x_1524
    1030 | Init_int32 x_1525 -> h_Init_int32 x_1525
    1031 | Init_space x_1526 -> h_Init_space x_1526
     1030| Init_int8 x_3630 -> h_Init_int8 x_3630
     1031| Init_int16 x_3631 -> h_Init_int16 x_3631
     1032| Init_int32 x_3632 -> h_Init_int32 x_3632
     1033| Init_space x_3633 -> h_Init_space x_3633
    10321034| Init_null -> h_Init_null
    1033 | Init_addrof (x_1528, x_1527) -> h_Init_addrof x_1528 x_1527
     1035| Init_addrof (x_3635, x_3634) -> h_Init_addrof x_3635 x_3634
    10341036
    10351037(** val init_data_rect_Type0 :
     
    10371039    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10381040let rec init_data_rect_Type0 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1039 | Init_int8 x_1536 -> h_Init_int8 x_1536
    1040 | Init_int16 x_1537 -> h_Init_int16 x_1537
    1041 | Init_int32 x_1538 -> h_Init_int32 x_1538
    1042 | Init_space x_1539 -> h_Init_space x_1539
     1041| Init_int8 x_3643 -> h_Init_int8 x_3643
     1042| Init_int16 x_3644 -> h_Init_int16 x_3644
     1043| Init_int32 x_3645 -> h_Init_int32 x_3645
     1044| Init_space x_3646 -> h_Init_space x_3646
    10431045| Init_null -> h_Init_null
    1044 | Init_addrof (x_1541, x_1540) -> h_Init_addrof x_1541 x_1540
     1046| Init_addrof (x_3648, x_3647) -> h_Init_addrof x_3648 x_3647
    10451047
    10461048(** val init_data_inv_rect_Type4 :
     
    11091111    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11101112    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1111 let rec program_rect_Type4 h_mk_program x_1628 =
     1113let rec program_rect_Type4 h_mk_program x_3735 =
    11121114  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1113     prog_main0 } = x_1628
     1115    prog_main0 } = x_3735
    11141116  in
    11151117  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11181120    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11191121    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1120 let rec program_rect_Type5 h_mk_program x_1630 =
     1122let rec program_rect_Type5 h_mk_program x_3737 =
    11211123  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1122     prog_main0 } = x_1630
     1124    prog_main0 } = x_3737
    11231125  in
    11241126  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11271129    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11281130    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1129 let rec program_rect_Type3 h_mk_program x_1632 =
     1131let rec program_rect_Type3 h_mk_program x_3739 =
    11301132  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1131     prog_main0 } = x_1632
     1133    prog_main0 } = x_3739
    11321134  in
    11331135  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11361138    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11371139    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1138 let rec program_rect_Type2 h_mk_program x_1634 =
     1140let rec program_rect_Type2 h_mk_program x_3741 =
    11391141  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1140     prog_main0 } = x_1634
     1142    prog_main0 } = x_3741
    11411143  in
    11421144  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11451147    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11461148    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1147 let rec program_rect_Type1 h_mk_program x_1636 =
     1149let rec program_rect_Type1 h_mk_program x_3743 =
    11481150  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1149     prog_main0 } = x_1636
     1151    prog_main0 } = x_3743
    11501152  in
    11511153  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11541156    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11551157    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1156 let rec program_rect_Type0 h_mk_program x_1638 =
     1158let rec program_rect_Type0 h_mk_program x_3745 =
    11571159  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1158     prog_main0 } = x_1638
     1160    prog_main0 } = x_3745
    11591161  in
    11601162  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    14791481(** val external_function_rect_Type4 :
    14801482    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1481 let rec external_function_rect_Type4 h_mk_external_function x_1842 =
    1482   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_1842 in
     1483let rec external_function_rect_Type4 h_mk_external_function x_3949 =
     1484  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3949 in
    14831485  h_mk_external_function ef_id0 ef_sig0
    14841486
    14851487(** val external_function_rect_Type5 :
    14861488    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1487 let rec external_function_rect_Type5 h_mk_external_function x_1844 =
    1488   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_1844 in
     1489let rec external_function_rect_Type5 h_mk_external_function x_3951 =
     1490  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3951 in
    14891491  h_mk_external_function ef_id0 ef_sig0
    14901492
    14911493(** val external_function_rect_Type3 :
    14921494    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1493 let rec external_function_rect_Type3 h_mk_external_function x_1846 =
    1494   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_1846 in
     1495let rec external_function_rect_Type3 h_mk_external_function x_3953 =
     1496  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3953 in
    14951497  h_mk_external_function ef_id0 ef_sig0
    14961498
    14971499(** val external_function_rect_Type2 :
    14981500    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1499 let rec external_function_rect_Type2 h_mk_external_function x_1848 =
    1500   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_1848 in
     1501let rec external_function_rect_Type2 h_mk_external_function x_3955 =
     1502  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3955 in
    15011503  h_mk_external_function ef_id0 ef_sig0
    15021504
    15031505(** val external_function_rect_Type1 :
    15041506    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1505 let rec external_function_rect_Type1 h_mk_external_function x_1850 =
    1506   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_1850 in
     1507let rec external_function_rect_Type1 h_mk_external_function x_3957 =
     1508  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3957 in
    15071509  h_mk_external_function ef_id0 ef_sig0
    15081510
    15091511(** val external_function_rect_Type0 :
    15101512    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1511 let rec external_function_rect_Type0 h_mk_external_function x_1852 =
    1512   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_1852 in
     1513let rec external_function_rect_Type0 h_mk_external_function x_3959 =
     1514  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3959 in
    15131515  h_mk_external_function ef_id0 ef_sig0
    15141516
     
    15771579    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15781580let rec fundef_rect_Type4 h_Internal h_External = function
    1579 | Internal x_1872 -> h_Internal x_1872
    1580 | External x_1873 -> h_External x_1873
     1581| Internal x_3979 -> h_Internal x_3979
     1582| External x_3980 -> h_External x_3980
    15811583
    15821584(** val fundef_rect_Type5 :
    15831585    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15841586let rec fundef_rect_Type5 h_Internal h_External = function
    1585 | Internal x_1877 -> h_Internal x_1877
    1586 | External x_1878 -> h_External x_1878
     1587| Internal x_3984 -> h_Internal x_3984
     1588| External x_3985 -> h_External x_3985
    15871589
    15881590(** val fundef_rect_Type3 :
    15891591    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15901592let rec fundef_rect_Type3 h_Internal h_External = function
    1591 | Internal x_1882 -> h_Internal x_1882
    1592 | External x_1883 -> h_External x_1883
     1593| Internal x_3989 -> h_Internal x_3989
     1594| External x_3990 -> h_External x_3990
    15931595
    15941596(** val fundef_rect_Type2 :
    15951597    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15961598let rec fundef_rect_Type2 h_Internal h_External = function
    1597 | Internal x_1887 -> h_Internal x_1887
    1598 | External x_1888 -> h_External x_1888
     1599| Internal x_3994 -> h_Internal x_3994
     1600| External x_3995 -> h_External x_3995
    15991601
    16001602(** val fundef_rect_Type1 :
    16011603    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16021604let rec fundef_rect_Type1 h_Internal h_External = function
    1603 | Internal x_1892 -> h_Internal x_1892
    1604 | External x_1893 -> h_External x_1893
     1605| Internal x_3999 -> h_Internal x_3999
     1606| External x_4000 -> h_External x_4000
    16051607
    16061608(** val fundef_rect_Type0 :
    16071609    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16081610let rec fundef_rect_Type0 h_Internal h_External = function
    1609 | Internal x_1897 -> h_Internal x_1897
    1610 | External x_1898 -> h_External x_1898
     1611| Internal x_4004 -> h_Internal x_4004
     1612| External x_4005 -> h_External x_4005
    16111613
    16121614(** val fundef_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.