Changeset 2743 for extracted/csem.ml


Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (8 years ago)
Author:
sacerdot
Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/csem.ml

    r2730 r2743  
    780780let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    781781| Kstop -> h_Kstop
    782 | Kseq (x_6713, x_6712) ->
    783   h_Kseq x_6713 x_6712
     782| Kseq (x_8648, x_8647) ->
     783  h_Kseq x_8648 x_8647
    784784    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    785       h_Kswitch h_Kcall x_6712)
    786 | Kwhile (x_6716, x_6715, x_6714) ->
    787   h_Kwhile x_6716 x_6715 x_6714
     785      h_Kswitch h_Kcall x_8647)
     786| Kwhile (x_8651, x_8650, x_8649) ->
     787  h_Kwhile x_8651 x_8650 x_8649
    788788    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    789       h_Kswitch h_Kcall x_6714)
    790 | Kdowhile (x_6719, x_6718, x_6717) ->
    791   h_Kdowhile x_6719 x_6718 x_6717
     789      h_Kswitch h_Kcall x_8649)
     790| Kdowhile (x_8654, x_8653, x_8652) ->
     791  h_Kdowhile x_8654 x_8653 x_8652
    792792    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    793       h_Kswitch h_Kcall x_6717)
    794 | Kfor2 (x_6723, x_6722, x_6721, x_6720) ->
    795   h_Kfor2 x_6723 x_6722 x_6721 x_6720
     793      h_Kswitch h_Kcall x_8652)
     794| Kfor2 (x_8658, x_8657, x_8656, x_8655) ->
     795  h_Kfor2 x_8658 x_8657 x_8656 x_8655
    796796    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    797       h_Kswitch h_Kcall x_6720)
    798 | Kfor3 (x_6727, x_6726, x_6725, x_6724) ->
    799   h_Kfor3 x_6727 x_6726 x_6725 x_6724
     797      h_Kswitch h_Kcall x_8655)
     798| Kfor3 (x_8662, x_8661, x_8660, x_8659) ->
     799  h_Kfor3 x_8662 x_8661 x_8660 x_8659
    800800    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    801       h_Kswitch h_Kcall x_6724)
    802 | Kswitch x_6728 ->
    803   h_Kswitch x_6728
     801      h_Kswitch h_Kcall x_8659)
     802| Kswitch x_8663 ->
     803  h_Kswitch x_8663
    804804    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    805       h_Kswitch h_Kcall x_6728)
    806 | Kcall (x_6732, x_6731, x_6730, x_6729) ->
    807   h_Kcall x_6732 x_6731 x_6730 x_6729
     805      h_Kswitch h_Kcall x_8663)
     806| Kcall (x_8667, x_8666, x_8665, x_8664) ->
     807  h_Kcall x_8667 x_8666 x_8665 x_8664
    808808    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    809       h_Kswitch h_Kcall x_6729)
     809      h_Kswitch h_Kcall x_8664)
    810810
    811811(** val cont_rect_Type3 :
     
    820820let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    821821| Kstop -> h_Kstop
    822 | Kseq (x_6773, x_6772) ->
    823   h_Kseq x_6773 x_6772
     822| Kseq (x_8708, x_8707) ->
     823  h_Kseq x_8708 x_8707
    824824    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    825       h_Kswitch h_Kcall x_6772)
    826 | Kwhile (x_6776, x_6775, x_6774) ->
    827   h_Kwhile x_6776 x_6775 x_6774
     825      h_Kswitch h_Kcall x_8707)
     826| Kwhile (x_8711, x_8710, x_8709) ->
     827  h_Kwhile x_8711 x_8710 x_8709
    828828    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    829       h_Kswitch h_Kcall x_6774)
    830 | Kdowhile (x_6779, x_6778, x_6777) ->
    831   h_Kdowhile x_6779 x_6778 x_6777
     829      h_Kswitch h_Kcall x_8709)
     830| Kdowhile (x_8714, x_8713, x_8712) ->
     831  h_Kdowhile x_8714 x_8713 x_8712
    832832    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    833       h_Kswitch h_Kcall x_6777)
    834 | Kfor2 (x_6783, x_6782, x_6781, x_6780) ->
    835   h_Kfor2 x_6783 x_6782 x_6781 x_6780
     833      h_Kswitch h_Kcall x_8712)
     834| Kfor2 (x_8718, x_8717, x_8716, x_8715) ->
     835  h_Kfor2 x_8718 x_8717 x_8716 x_8715
    836836    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    837       h_Kswitch h_Kcall x_6780)
    838 | Kfor3 (x_6787, x_6786, x_6785, x_6784) ->
    839   h_Kfor3 x_6787 x_6786 x_6785 x_6784
     837      h_Kswitch h_Kcall x_8715)
     838| Kfor3 (x_8722, x_8721, x_8720, x_8719) ->
     839  h_Kfor3 x_8722 x_8721 x_8720 x_8719
    840840    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    841       h_Kswitch h_Kcall x_6784)
    842 | Kswitch x_6788 ->
    843   h_Kswitch x_6788
     841      h_Kswitch h_Kcall x_8719)
     842| Kswitch x_8723 ->
     843  h_Kswitch x_8723
    844844    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    845       h_Kswitch h_Kcall x_6788)
    846 | Kcall (x_6792, x_6791, x_6790, x_6789) ->
    847   h_Kcall x_6792 x_6791 x_6790 x_6789
     845      h_Kswitch h_Kcall x_8723)
     846| Kcall (x_8727, x_8726, x_8725, x_8724) ->
     847  h_Kcall x_8727 x_8726 x_8725 x_8724
    848848    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    849       h_Kswitch h_Kcall x_6789)
     849      h_Kswitch h_Kcall x_8724)
    850850
    851851(** val cont_rect_Type2 :
     
    860860let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    861861| Kstop -> h_Kstop
    862 | Kseq (x_6803, x_6802) ->
    863   h_Kseq x_6803 x_6802
     862| Kseq (x_8738, x_8737) ->
     863  h_Kseq x_8738 x_8737
    864864    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    865       h_Kswitch h_Kcall x_6802)
    866 | Kwhile (x_6806, x_6805, x_6804) ->
    867   h_Kwhile x_6806 x_6805 x_6804
     865      h_Kswitch h_Kcall x_8737)
     866| Kwhile (x_8741, x_8740, x_8739) ->
     867  h_Kwhile x_8741 x_8740 x_8739
    868868    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    869       h_Kswitch h_Kcall x_6804)
    870 | Kdowhile (x_6809, x_6808, x_6807) ->
    871   h_Kdowhile x_6809 x_6808 x_6807
     869      h_Kswitch h_Kcall x_8739)
     870| Kdowhile (x_8744, x_8743, x_8742) ->
     871  h_Kdowhile x_8744 x_8743 x_8742
    872872    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    873       h_Kswitch h_Kcall x_6807)
    874 | Kfor2 (x_6813, x_6812, x_6811, x_6810) ->
    875   h_Kfor2 x_6813 x_6812 x_6811 x_6810
     873      h_Kswitch h_Kcall x_8742)
     874| Kfor2 (x_8748, x_8747, x_8746, x_8745) ->
     875  h_Kfor2 x_8748 x_8747 x_8746 x_8745
    876876    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    877       h_Kswitch h_Kcall x_6810)
    878 | Kfor3 (x_6817, x_6816, x_6815, x_6814) ->
    879   h_Kfor3 x_6817 x_6816 x_6815 x_6814
     877      h_Kswitch h_Kcall x_8745)
     878| Kfor3 (x_8752, x_8751, x_8750, x_8749) ->
     879  h_Kfor3 x_8752 x_8751 x_8750 x_8749
    880880    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    881       h_Kswitch h_Kcall x_6814)
    882 | Kswitch x_6818 ->
    883   h_Kswitch x_6818
     881      h_Kswitch h_Kcall x_8749)
     882| Kswitch x_8753 ->
     883  h_Kswitch x_8753
    884884    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    885       h_Kswitch h_Kcall x_6818)
    886 | Kcall (x_6822, x_6821, x_6820, x_6819) ->
    887   h_Kcall x_6822 x_6821 x_6820 x_6819
     885      h_Kswitch h_Kcall x_8753)
     886| Kcall (x_8757, x_8756, x_8755, x_8754) ->
     887  h_Kcall x_8757 x_8756 x_8755 x_8754
    888888    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    889       h_Kswitch h_Kcall x_6819)
     889      h_Kswitch h_Kcall x_8754)
    890890
    891891(** val cont_rect_Type1 :
     
    900900let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    901901| Kstop -> h_Kstop
    902 | Kseq (x_6833, x_6832) ->
    903   h_Kseq x_6833 x_6832
     902| Kseq (x_8768, x_8767) ->
     903  h_Kseq x_8768 x_8767
    904904    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    905       h_Kswitch h_Kcall x_6832)
    906 | Kwhile (x_6836, x_6835, x_6834) ->
    907   h_Kwhile x_6836 x_6835 x_6834
     905      h_Kswitch h_Kcall x_8767)
     906| Kwhile (x_8771, x_8770, x_8769) ->
     907  h_Kwhile x_8771 x_8770 x_8769
    908908    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    909       h_Kswitch h_Kcall x_6834)
    910 | Kdowhile (x_6839, x_6838, x_6837) ->
    911   h_Kdowhile x_6839 x_6838 x_6837
     909      h_Kswitch h_Kcall x_8769)
     910| Kdowhile (x_8774, x_8773, x_8772) ->
     911  h_Kdowhile x_8774 x_8773 x_8772
    912912    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    913       h_Kswitch h_Kcall x_6837)
    914 | Kfor2 (x_6843, x_6842, x_6841, x_6840) ->
    915   h_Kfor2 x_6843 x_6842 x_6841 x_6840
     913      h_Kswitch h_Kcall x_8772)
     914| Kfor2 (x_8778, x_8777, x_8776, x_8775) ->
     915  h_Kfor2 x_8778 x_8777 x_8776 x_8775
    916916    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    917       h_Kswitch h_Kcall x_6840)
    918 | Kfor3 (x_6847, x_6846, x_6845, x_6844) ->
    919   h_Kfor3 x_6847 x_6846 x_6845 x_6844
     917      h_Kswitch h_Kcall x_8775)
     918| Kfor3 (x_8782, x_8781, x_8780, x_8779) ->
     919  h_Kfor3 x_8782 x_8781 x_8780 x_8779
    920920    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    921       h_Kswitch h_Kcall x_6844)
    922 | Kswitch x_6848 ->
    923   h_Kswitch x_6848
     921      h_Kswitch h_Kcall x_8779)
     922| Kswitch x_8783 ->
     923  h_Kswitch x_8783
    924924    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    925       h_Kswitch h_Kcall x_6848)
    926 | Kcall (x_6852, x_6851, x_6850, x_6849) ->
    927   h_Kcall x_6852 x_6851 x_6850 x_6849
     925      h_Kswitch h_Kcall x_8783)
     926| Kcall (x_8787, x_8786, x_8785, x_8784) ->
     927  h_Kcall x_8787 x_8786 x_8785 x_8784
    928928    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    929       h_Kswitch h_Kcall x_6849)
     929      h_Kswitch h_Kcall x_8784)
    930930
    931931(** val cont_rect_Type0 :
     
    940940let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    941941| Kstop -> h_Kstop
    942 | Kseq (x_6863, x_6862) ->
    943   h_Kseq x_6863 x_6862
     942| Kseq (x_8798, x_8797) ->
     943  h_Kseq x_8798 x_8797
    944944    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    945       h_Kswitch h_Kcall x_6862)
    946 | Kwhile (x_6866, x_6865, x_6864) ->
    947   h_Kwhile x_6866 x_6865 x_6864
     945      h_Kswitch h_Kcall x_8797)
     946| Kwhile (x_8801, x_8800, x_8799) ->
     947  h_Kwhile x_8801 x_8800 x_8799
    948948    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    949       h_Kswitch h_Kcall x_6864)
    950 | Kdowhile (x_6869, x_6868, x_6867) ->
    951   h_Kdowhile x_6869 x_6868 x_6867
     949      h_Kswitch h_Kcall x_8799)
     950| Kdowhile (x_8804, x_8803, x_8802) ->
     951  h_Kdowhile x_8804 x_8803 x_8802
    952952    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    953       h_Kswitch h_Kcall x_6867)
    954 | Kfor2 (x_6873, x_6872, x_6871, x_6870) ->
    955   h_Kfor2 x_6873 x_6872 x_6871 x_6870
     953      h_Kswitch h_Kcall x_8802)
     954| Kfor2 (x_8808, x_8807, x_8806, x_8805) ->
     955  h_Kfor2 x_8808 x_8807 x_8806 x_8805
    956956    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    957       h_Kswitch h_Kcall x_6870)
    958 | Kfor3 (x_6877, x_6876, x_6875, x_6874) ->
    959   h_Kfor3 x_6877 x_6876 x_6875 x_6874
     957      h_Kswitch h_Kcall x_8805)
     958| Kfor3 (x_8812, x_8811, x_8810, x_8809) ->
     959  h_Kfor3 x_8812 x_8811 x_8810 x_8809
    960960    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    961       h_Kswitch h_Kcall x_6874)
    962 | Kswitch x_6878 ->
    963   h_Kswitch x_6878
     961      h_Kswitch h_Kcall x_8809)
     962| Kswitch x_8813 ->
     963  h_Kswitch x_8813
    964964    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    965       h_Kswitch h_Kcall x_6878)
    966 | Kcall (x_6882, x_6881, x_6880, x_6879) ->
    967   h_Kcall x_6882 x_6881 x_6880 x_6879
     965      h_Kswitch h_Kcall x_8813)
     966| Kcall (x_8817, x_8816, x_8815, x_8814) ->
     967  h_Kcall x_8817 x_8816 x_8815 x_8814
    968968    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    969       h_Kswitch h_Kcall x_6879)
     969      h_Kswitch h_Kcall x_8814)
    970970
    971971(** val cont_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.