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

    r2649 r2717  
    3535open Identifiers
    3636
     37open Exp
     38
    3739open Arithmetic
    3840
     
    6769open AST
    6870
     71open BitVectorTrie
     72
    6973open CostLabel
    7074
     
    96100
    97101open Registers
    98 
    99 open BitVectorTrie
    100102
    101103open Graphs
     
    137139    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    138140let rec statement_rect_Type4 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    139 | St_skip x_11448 -> h_St_skip x_11448
    140 | St_cost (x_11450, x_11449) -> h_St_cost x_11450 x_11449
    141 | St_const (t, x_11453, x_11452, x_11451) ->
    142   h_St_const t x_11453 x_11452 x_11451
    143 | St_op1 (t', t, x_11457, x_11456, x_11455, x_11454) ->
    144   h_St_op1 t' t x_11457 x_11456 x_11455 x_11454
    145 | St_op2 (t', t1, t2, x_11462, x_11461, x_11460, x_11459, x_11458) ->
    146   h_St_op2 t' t1 t2 x_11462 x_11461 x_11460 x_11459 x_11458
    147 | St_load (x_11466, x_11465, x_11464, x_11463) ->
    148   h_St_load x_11466 x_11465 x_11464 x_11463
    149 | St_store (x_11470, x_11469, x_11468, x_11467) ->
    150   h_St_store x_11470 x_11469 x_11468 x_11467
    151 | St_call_id (x_11474, x_11473, x_11472, x_11471) ->
    152   h_St_call_id x_11474 x_11473 x_11472 x_11471
    153 | St_call_ptr (x_11478, x_11477, x_11476, x_11475) ->
    154   h_St_call_ptr x_11478 x_11477 x_11476 x_11475
    155 | St_cond (x_11481, x_11480, x_11479) -> h_St_cond x_11481 x_11480 x_11479
     141| St_skip x_14738 -> h_St_skip x_14738
     142| St_cost (x_14740, x_14739) -> h_St_cost x_14740 x_14739
     143| St_const (t, x_14743, x_14742, x_14741) ->
     144  h_St_const t x_14743 x_14742 x_14741
     145| St_op1 (t', t, x_14747, x_14746, x_14745, x_14744) ->
     146  h_St_op1 t' t x_14747 x_14746 x_14745 x_14744
     147| St_op2 (t', t1, t2, x_14752, x_14751, x_14750, x_14749, x_14748) ->
     148  h_St_op2 t' t1 t2 x_14752 x_14751 x_14750 x_14749 x_14748
     149| St_load (x_14756, x_14755, x_14754, x_14753) ->
     150  h_St_load x_14756 x_14755 x_14754 x_14753
     151| St_store (x_14760, x_14759, x_14758, x_14757) ->
     152  h_St_store x_14760 x_14759 x_14758 x_14757
     153| St_call_id (x_14764, x_14763, x_14762, x_14761) ->
     154  h_St_call_id x_14764 x_14763 x_14762 x_14761
     155| St_call_ptr (x_14768, x_14767, x_14766, x_14765) ->
     156  h_St_call_ptr x_14768 x_14767 x_14766 x_14765
     157| St_cond (x_14771, x_14770, x_14769) -> h_St_cond x_14771 x_14770 x_14769
    156158| St_return -> h_St_return
    157159
     
    172174    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    173175let rec statement_rect_Type5 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    174 | St_skip x_11494 -> h_St_skip x_11494
    175 | St_cost (x_11496, x_11495) -> h_St_cost x_11496 x_11495
    176 | St_const (t, x_11499, x_11498, x_11497) ->
    177   h_St_const t x_11499 x_11498 x_11497
    178 | St_op1 (t', t, x_11503, x_11502, x_11501, x_11500) ->
    179   h_St_op1 t' t x_11503 x_11502 x_11501 x_11500
    180 | St_op2 (t', t1, t2, x_11508, x_11507, x_11506, x_11505, x_11504) ->
    181   h_St_op2 t' t1 t2 x_11508 x_11507 x_11506 x_11505 x_11504
    182 | St_load (x_11512, x_11511, x_11510, x_11509) ->
    183   h_St_load x_11512 x_11511 x_11510 x_11509
    184 | St_store (x_11516, x_11515, x_11514, x_11513) ->
    185   h_St_store x_11516 x_11515 x_11514 x_11513
    186 | St_call_id (x_11520, x_11519, x_11518, x_11517) ->
    187   h_St_call_id x_11520 x_11519 x_11518 x_11517
    188 | St_call_ptr (x_11524, x_11523, x_11522, x_11521) ->
    189   h_St_call_ptr x_11524 x_11523 x_11522 x_11521
    190 | St_cond (x_11527, x_11526, x_11525) -> h_St_cond x_11527 x_11526 x_11525
     176| St_skip x_14784 -> h_St_skip x_14784
     177| St_cost (x_14786, x_14785) -> h_St_cost x_14786 x_14785
     178| St_const (t, x_14789, x_14788, x_14787) ->
     179  h_St_const t x_14789 x_14788 x_14787
     180| St_op1 (t', t, x_14793, x_14792, x_14791, x_14790) ->
     181  h_St_op1 t' t x_14793 x_14792 x_14791 x_14790
     182| St_op2 (t', t1, t2, x_14798, x_14797, x_14796, x_14795, x_14794) ->
     183  h_St_op2 t' t1 t2 x_14798 x_14797 x_14796 x_14795 x_14794
     184| St_load (x_14802, x_14801, x_14800, x_14799) ->
     185  h_St_load x_14802 x_14801 x_14800 x_14799
     186| St_store (x_14806, x_14805, x_14804, x_14803) ->
     187  h_St_store x_14806 x_14805 x_14804 x_14803
     188| St_call_id (x_14810, x_14809, x_14808, x_14807) ->
     189  h_St_call_id x_14810 x_14809 x_14808 x_14807
     190| St_call_ptr (x_14814, x_14813, x_14812, x_14811) ->
     191  h_St_call_ptr x_14814 x_14813 x_14812 x_14811
     192| St_cond (x_14817, x_14816, x_14815) -> h_St_cond x_14817 x_14816 x_14815
    191193| St_return -> h_St_return
    192194
     
    207209    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    208210let rec statement_rect_Type3 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    209 | St_skip x_11540 -> h_St_skip x_11540
    210 | St_cost (x_11542, x_11541) -> h_St_cost x_11542 x_11541
    211 | St_const (t, x_11545, x_11544, x_11543) ->
    212   h_St_const t x_11545 x_11544 x_11543
    213 | St_op1 (t', t, x_11549, x_11548, x_11547, x_11546) ->
    214   h_St_op1 t' t x_11549 x_11548 x_11547 x_11546
    215 | St_op2 (t', t1, t2, x_11554, x_11553, x_11552, x_11551, x_11550) ->
    216   h_St_op2 t' t1 t2 x_11554 x_11553 x_11552 x_11551 x_11550
    217 | St_load (x_11558, x_11557, x_11556, x_11555) ->
    218   h_St_load x_11558 x_11557 x_11556 x_11555
    219 | St_store (x_11562, x_11561, x_11560, x_11559) ->
    220   h_St_store x_11562 x_11561 x_11560 x_11559
    221 | St_call_id (x_11566, x_11565, x_11564, x_11563) ->
    222   h_St_call_id x_11566 x_11565 x_11564 x_11563
    223 | St_call_ptr (x_11570, x_11569, x_11568, x_11567) ->
    224   h_St_call_ptr x_11570 x_11569 x_11568 x_11567
    225 | St_cond (x_11573, x_11572, x_11571) -> h_St_cond x_11573 x_11572 x_11571
     211| St_skip x_14830 -> h_St_skip x_14830
     212| St_cost (x_14832, x_14831) -> h_St_cost x_14832 x_14831
     213| St_const (t, x_14835, x_14834, x_14833) ->
     214  h_St_const t x_14835 x_14834 x_14833
     215| St_op1 (t', t, x_14839, x_14838, x_14837, x_14836) ->
     216  h_St_op1 t' t x_14839 x_14838 x_14837 x_14836
     217| St_op2 (t', t1, t2, x_14844, x_14843, x_14842, x_14841, x_14840) ->
     218  h_St_op2 t' t1 t2 x_14844 x_14843 x_14842 x_14841 x_14840
     219| St_load (x_14848, x_14847, x_14846, x_14845) ->
     220  h_St_load x_14848 x_14847 x_14846 x_14845
     221| St_store (x_14852, x_14851, x_14850, x_14849) ->
     222  h_St_store x_14852 x_14851 x_14850 x_14849
     223| St_call_id (x_14856, x_14855, x_14854, x_14853) ->
     224  h_St_call_id x_14856 x_14855 x_14854 x_14853
     225| St_call_ptr (x_14860, x_14859, x_14858, x_14857) ->
     226  h_St_call_ptr x_14860 x_14859 x_14858 x_14857
     227| St_cond (x_14863, x_14862, x_14861) -> h_St_cond x_14863 x_14862 x_14861
    226228| St_return -> h_St_return
    227229
     
    242244    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    243245let rec statement_rect_Type2 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    244 | St_skip x_11586 -> h_St_skip x_11586
    245 | St_cost (x_11588, x_11587) -> h_St_cost x_11588 x_11587
    246 | St_const (t, x_11591, x_11590, x_11589) ->
    247   h_St_const t x_11591 x_11590 x_11589
    248 | St_op1 (t', t, x_11595, x_11594, x_11593, x_11592) ->
    249   h_St_op1 t' t x_11595 x_11594 x_11593 x_11592
    250 | St_op2 (t', t1, t2, x_11600, x_11599, x_11598, x_11597, x_11596) ->
    251   h_St_op2 t' t1 t2 x_11600 x_11599 x_11598 x_11597 x_11596
    252 | St_load (x_11604, x_11603, x_11602, x_11601) ->
    253   h_St_load x_11604 x_11603 x_11602 x_11601
    254 | St_store (x_11608, x_11607, x_11606, x_11605) ->
    255   h_St_store x_11608 x_11607 x_11606 x_11605
    256 | St_call_id (x_11612, x_11611, x_11610, x_11609) ->
    257   h_St_call_id x_11612 x_11611 x_11610 x_11609
    258 | St_call_ptr (x_11616, x_11615, x_11614, x_11613) ->
    259   h_St_call_ptr x_11616 x_11615 x_11614 x_11613
    260 | St_cond (x_11619, x_11618, x_11617) -> h_St_cond x_11619 x_11618 x_11617
     246| St_skip x_14876 -> h_St_skip x_14876
     247| St_cost (x_14878, x_14877) -> h_St_cost x_14878 x_14877
     248| St_const (t, x_14881, x_14880, x_14879) ->
     249  h_St_const t x_14881 x_14880 x_14879
     250| St_op1 (t', t, x_14885, x_14884, x_14883, x_14882) ->
     251  h_St_op1 t' t x_14885 x_14884 x_14883 x_14882
     252| St_op2 (t', t1, t2, x_14890, x_14889, x_14888, x_14887, x_14886) ->
     253  h_St_op2 t' t1 t2 x_14890 x_14889 x_14888 x_14887 x_14886
     254| St_load (x_14894, x_14893, x_14892, x_14891) ->
     255  h_St_load x_14894 x_14893 x_14892 x_14891
     256| St_store (x_14898, x_14897, x_14896, x_14895) ->
     257  h_St_store x_14898 x_14897 x_14896 x_14895
     258| St_call_id (x_14902, x_14901, x_14900, x_14899) ->
     259  h_St_call_id x_14902 x_14901 x_14900 x_14899
     260| St_call_ptr (x_14906, x_14905, x_14904, x_14903) ->
     261  h_St_call_ptr x_14906 x_14905 x_14904 x_14903
     262| St_cond (x_14909, x_14908, x_14907) -> h_St_cond x_14909 x_14908 x_14907
    261263| St_return -> h_St_return
    262264
     
    277279    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    278280let rec statement_rect_Type1 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    279 | St_skip x_11632 -> h_St_skip x_11632
    280 | St_cost (x_11634, x_11633) -> h_St_cost x_11634 x_11633
    281 | St_const (t, x_11637, x_11636, x_11635) ->
    282   h_St_const t x_11637 x_11636 x_11635
    283 | St_op1 (t', t, x_11641, x_11640, x_11639, x_11638) ->
    284   h_St_op1 t' t x_11641 x_11640 x_11639 x_11638
    285 | St_op2 (t', t1, t2, x_11646, x_11645, x_11644, x_11643, x_11642) ->
    286   h_St_op2 t' t1 t2 x_11646 x_11645 x_11644 x_11643 x_11642
    287 | St_load (x_11650, x_11649, x_11648, x_11647) ->
    288   h_St_load x_11650 x_11649 x_11648 x_11647
    289 | St_store (x_11654, x_11653, x_11652, x_11651) ->
    290   h_St_store x_11654 x_11653 x_11652 x_11651
    291 | St_call_id (x_11658, x_11657, x_11656, x_11655) ->
    292   h_St_call_id x_11658 x_11657 x_11656 x_11655
    293 | St_call_ptr (x_11662, x_11661, x_11660, x_11659) ->
    294   h_St_call_ptr x_11662 x_11661 x_11660 x_11659
    295 | St_cond (x_11665, x_11664, x_11663) -> h_St_cond x_11665 x_11664 x_11663
     281| St_skip x_14922 -> h_St_skip x_14922
     282| St_cost (x_14924, x_14923) -> h_St_cost x_14924 x_14923
     283| St_const (t, x_14927, x_14926, x_14925) ->
     284  h_St_const t x_14927 x_14926 x_14925
     285| St_op1 (t', t, x_14931, x_14930, x_14929, x_14928) ->
     286  h_St_op1 t' t x_14931 x_14930 x_14929 x_14928
     287| St_op2 (t', t1, t2, x_14936, x_14935, x_14934, x_14933, x_14932) ->
     288  h_St_op2 t' t1 t2 x_14936 x_14935 x_14934 x_14933 x_14932
     289| St_load (x_14940, x_14939, x_14938, x_14937) ->
     290  h_St_load x_14940 x_14939 x_14938 x_14937
     291| St_store (x_14944, x_14943, x_14942, x_14941) ->
     292  h_St_store x_14944 x_14943 x_14942 x_14941
     293| St_call_id (x_14948, x_14947, x_14946, x_14945) ->
     294  h_St_call_id x_14948 x_14947 x_14946 x_14945
     295| St_call_ptr (x_14952, x_14951, x_14950, x_14949) ->
     296  h_St_call_ptr x_14952 x_14951 x_14950 x_14949
     297| St_cond (x_14955, x_14954, x_14953) -> h_St_cond x_14955 x_14954 x_14953
    296298| St_return -> h_St_return
    297299
     
    312314    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    313315let rec statement_rect_Type0 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    314 | St_skip x_11678 -> h_St_skip x_11678
    315 | St_cost (x_11680, x_11679) -> h_St_cost x_11680 x_11679
    316 | St_const (t, x_11683, x_11682, x_11681) ->
    317   h_St_const t x_11683 x_11682 x_11681
    318 | St_op1 (t', t, x_11687, x_11686, x_11685, x_11684) ->
    319   h_St_op1 t' t x_11687 x_11686 x_11685 x_11684
    320 | St_op2 (t', t1, t2, x_11692, x_11691, x_11690, x_11689, x_11688) ->
    321   h_St_op2 t' t1 t2 x_11692 x_11691 x_11690 x_11689 x_11688
    322 | St_load (x_11696, x_11695, x_11694, x_11693) ->
    323   h_St_load x_11696 x_11695 x_11694 x_11693
    324 | St_store (x_11700, x_11699, x_11698, x_11697) ->
    325   h_St_store x_11700 x_11699 x_11698 x_11697
    326 | St_call_id (x_11704, x_11703, x_11702, x_11701) ->
    327   h_St_call_id x_11704 x_11703 x_11702 x_11701
    328 | St_call_ptr (x_11708, x_11707, x_11706, x_11705) ->
    329   h_St_call_ptr x_11708 x_11707 x_11706 x_11705
    330 | St_cond (x_11711, x_11710, x_11709) -> h_St_cond x_11711 x_11710 x_11709
     316| St_skip x_14968 -> h_St_skip x_14968
     317| St_cost (x_14970, x_14969) -> h_St_cost x_14970 x_14969
     318| St_const (t, x_14973, x_14972, x_14971) ->
     319  h_St_const t x_14973 x_14972 x_14971
     320| St_op1 (t', t, x_14977, x_14976, x_14975, x_14974) ->
     321  h_St_op1 t' t x_14977 x_14976 x_14975 x_14974
     322| St_op2 (t', t1, t2, x_14982, x_14981, x_14980, x_14979, x_14978) ->
     323  h_St_op2 t' t1 t2 x_14982 x_14981 x_14980 x_14979 x_14978
     324| St_load (x_14986, x_14985, x_14984, x_14983) ->
     325  h_St_load x_14986 x_14985 x_14984 x_14983
     326| St_store (x_14990, x_14989, x_14988, x_14987) ->
     327  h_St_store x_14990 x_14989 x_14988 x_14987
     328| St_call_id (x_14994, x_14993, x_14992, x_14991) ->
     329  h_St_call_id x_14994 x_14993 x_14992 x_14991
     330| St_call_ptr (x_14998, x_14997, x_14996, x_14995) ->
     331  h_St_call_ptr x_14998 x_14997 x_14996 x_14995
     332| St_cond (x_15001, x_15000, x_14999) -> h_St_cond x_15001 x_15000 x_14999
    331333| St_return -> h_St_return
    332334
     
    464466    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    465467    internal_function -> 'a1 **)
    466 let rec internal_function_rect_Type4 h_mk_internal_function x_12001 =
     468let rec internal_function_rect_Type4 h_mk_internal_function x_15291 =
    467469  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    468470    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    469     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_12001
     471    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15291
    470472  in
    471473  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    479481    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    480482    internal_function -> 'a1 **)
    481 let rec internal_function_rect_Type5 h_mk_internal_function x_12003 =
     483let rec internal_function_rect_Type5 h_mk_internal_function x_15293 =
    482484  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    483485    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    484     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_12003
     486    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15293
    485487  in
    486488  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    494496    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    495497    internal_function -> 'a1 **)
    496 let rec internal_function_rect_Type3 h_mk_internal_function x_12005 =
     498let rec internal_function_rect_Type3 h_mk_internal_function x_15295 =
    497499  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    498500    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    499     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_12005
     501    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15295
    500502  in
    501503  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    509511    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    510512    internal_function -> 'a1 **)
    511 let rec internal_function_rect_Type2 h_mk_internal_function x_12007 =
     513let rec internal_function_rect_Type2 h_mk_internal_function x_15297 =
    512514  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    513515    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    514     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_12007
     516    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15297
    515517  in
    516518  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    524526    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    525527    internal_function -> 'a1 **)
    526 let rec internal_function_rect_Type1 h_mk_internal_function x_12009 =
     528let rec internal_function_rect_Type1 h_mk_internal_function x_15299 =
    527529  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    528530    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    529     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_12009
     531    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15299
    530532  in
    531533  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    539541    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    540542    internal_function -> 'a1 **)
    541 let rec internal_function_rect_Type0 h_mk_internal_function x_12011 =
     543let rec internal_function_rect_Type0 h_mk_internal_function x_15301 =
    542544  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    543545    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    544     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_12011
     546    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15301
    545547  in
    546548  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
Note: See TracChangeset for help on using the changeset viewer.