Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (7 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/rTLabs_syntax.ml

    r2730 r2743  
    139139    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    140140let 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
    141 | St_skip x_1809 -> h_St_skip x_1809
    142 | St_cost (x_1811, x_1810) -> h_St_cost x_1811 x_1810
    143 | St_const (t, x_1814, x_1813, x_1812) -> h_St_const t x_1814 x_1813 x_1812
    144 | St_op1 (t', t, x_1818, x_1817, x_1816, x_1815) ->
    145   h_St_op1 t' t x_1818 x_1817 x_1816 x_1815
    146 | St_op2 (t', t1, t2, x_1823, x_1822, x_1821, x_1820, x_1819) ->
    147   h_St_op2 t' t1 t2 x_1823 x_1822 x_1821 x_1820 x_1819
    148 | St_load (x_1827, x_1826, x_1825, x_1824) ->
    149   h_St_load x_1827 x_1826 x_1825 x_1824
    150 | St_store (x_1831, x_1830, x_1829, x_1828) ->
    151   h_St_store x_1831 x_1830 x_1829 x_1828
    152 | St_call_id (x_1835, x_1834, x_1833, x_1832) ->
    153   h_St_call_id x_1835 x_1834 x_1833 x_1832
    154 | St_call_ptr (x_1839, x_1838, x_1837, x_1836) ->
    155   h_St_call_ptr x_1839 x_1838 x_1837 x_1836
    156 | St_cond (x_1842, x_1841, x_1840) -> h_St_cond x_1842 x_1841 x_1840
     141| St_skip x_14764 -> h_St_skip x_14764
     142| St_cost (x_14766, x_14765) -> h_St_cost x_14766 x_14765
     143| St_const (t, x_14769, x_14768, x_14767) ->
     144  h_St_const t x_14769 x_14768 x_14767
     145| St_op1 (t', t, x_14773, x_14772, x_14771, x_14770) ->
     146  h_St_op1 t' t x_14773 x_14772 x_14771 x_14770
     147| St_op2 (t', t1, t2, x_14778, x_14777, x_14776, x_14775, x_14774) ->
     148  h_St_op2 t' t1 t2 x_14778 x_14777 x_14776 x_14775 x_14774
     149| St_load (x_14782, x_14781, x_14780, x_14779) ->
     150  h_St_load x_14782 x_14781 x_14780 x_14779
     151| St_store (x_14786, x_14785, x_14784, x_14783) ->
     152  h_St_store x_14786 x_14785 x_14784 x_14783
     153| St_call_id (x_14790, x_14789, x_14788, x_14787) ->
     154  h_St_call_id x_14790 x_14789 x_14788 x_14787
     155| St_call_ptr (x_14794, x_14793, x_14792, x_14791) ->
     156  h_St_call_ptr x_14794 x_14793 x_14792 x_14791
     157| St_cond (x_14797, x_14796, x_14795) -> h_St_cond x_14797 x_14796 x_14795
    157158| St_return -> h_St_return
    158159
     
    173174    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    174175let 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
    175 | St_skip x_1855 -> h_St_skip x_1855
    176 | St_cost (x_1857, x_1856) -> h_St_cost x_1857 x_1856
    177 | St_const (t, x_1860, x_1859, x_1858) -> h_St_const t x_1860 x_1859 x_1858
    178 | St_op1 (t', t, x_1864, x_1863, x_1862, x_1861) ->
    179   h_St_op1 t' t x_1864 x_1863 x_1862 x_1861
    180 | St_op2 (t', t1, t2, x_1869, x_1868, x_1867, x_1866, x_1865) ->
    181   h_St_op2 t' t1 t2 x_1869 x_1868 x_1867 x_1866 x_1865
    182 | St_load (x_1873, x_1872, x_1871, x_1870) ->
    183   h_St_load x_1873 x_1872 x_1871 x_1870
    184 | St_store (x_1877, x_1876, x_1875, x_1874) ->
    185   h_St_store x_1877 x_1876 x_1875 x_1874
    186 | St_call_id (x_1881, x_1880, x_1879, x_1878) ->
    187   h_St_call_id x_1881 x_1880 x_1879 x_1878
    188 | St_call_ptr (x_1885, x_1884, x_1883, x_1882) ->
    189   h_St_call_ptr x_1885 x_1884 x_1883 x_1882
    190 | St_cond (x_1888, x_1887, x_1886) -> h_St_cond x_1888 x_1887 x_1886
     176| St_skip x_14810 -> h_St_skip x_14810
     177| St_cost (x_14812, x_14811) -> h_St_cost x_14812 x_14811
     178| St_const (t, x_14815, x_14814, x_14813) ->
     179  h_St_const t x_14815 x_14814 x_14813
     180| St_op1 (t', t, x_14819, x_14818, x_14817, x_14816) ->
     181  h_St_op1 t' t x_14819 x_14818 x_14817 x_14816
     182| St_op2 (t', t1, t2, x_14824, x_14823, x_14822, x_14821, x_14820) ->
     183  h_St_op2 t' t1 t2 x_14824 x_14823 x_14822 x_14821 x_14820
     184| St_load (x_14828, x_14827, x_14826, x_14825) ->
     185  h_St_load x_14828 x_14827 x_14826 x_14825
     186| St_store (x_14832, x_14831, x_14830, x_14829) ->
     187  h_St_store x_14832 x_14831 x_14830 x_14829
     188| St_call_id (x_14836, x_14835, x_14834, x_14833) ->
     189  h_St_call_id x_14836 x_14835 x_14834 x_14833
     190| St_call_ptr (x_14840, x_14839, x_14838, x_14837) ->
     191  h_St_call_ptr x_14840 x_14839 x_14838 x_14837
     192| St_cond (x_14843, x_14842, x_14841) -> h_St_cond x_14843 x_14842 x_14841
    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_1901 -> h_St_skip x_1901
    210 | St_cost (x_1903, x_1902) -> h_St_cost x_1903 x_1902
    211 | St_const (t, x_1906, x_1905, x_1904) -> h_St_const t x_1906 x_1905 x_1904
    212 | St_op1 (t', t, x_1910, x_1909, x_1908, x_1907) ->
    213   h_St_op1 t' t x_1910 x_1909 x_1908 x_1907
    214 | St_op2 (t', t1, t2, x_1915, x_1914, x_1913, x_1912, x_1911) ->
    215   h_St_op2 t' t1 t2 x_1915 x_1914 x_1913 x_1912 x_1911
    216 | St_load (x_1919, x_1918, x_1917, x_1916) ->
    217   h_St_load x_1919 x_1918 x_1917 x_1916
    218 | St_store (x_1923, x_1922, x_1921, x_1920) ->
    219   h_St_store x_1923 x_1922 x_1921 x_1920
    220 | St_call_id (x_1927, x_1926, x_1925, x_1924) ->
    221   h_St_call_id x_1927 x_1926 x_1925 x_1924
    222 | St_call_ptr (x_1931, x_1930, x_1929, x_1928) ->
    223   h_St_call_ptr x_1931 x_1930 x_1929 x_1928
    224 | St_cond (x_1934, x_1933, x_1932) -> h_St_cond x_1934 x_1933 x_1932
     211| St_skip x_14856 -> h_St_skip x_14856
     212| St_cost (x_14858, x_14857) -> h_St_cost x_14858 x_14857
     213| St_const (t, x_14861, x_14860, x_14859) ->
     214  h_St_const t x_14861 x_14860 x_14859
     215| St_op1 (t', t, x_14865, x_14864, x_14863, x_14862) ->
     216  h_St_op1 t' t x_14865 x_14864 x_14863 x_14862
     217| St_op2 (t', t1, t2, x_14870, x_14869, x_14868, x_14867, x_14866) ->
     218  h_St_op2 t' t1 t2 x_14870 x_14869 x_14868 x_14867 x_14866
     219| St_load (x_14874, x_14873, x_14872, x_14871) ->
     220  h_St_load x_14874 x_14873 x_14872 x_14871
     221| St_store (x_14878, x_14877, x_14876, x_14875) ->
     222  h_St_store x_14878 x_14877 x_14876 x_14875
     223| St_call_id (x_14882, x_14881, x_14880, x_14879) ->
     224  h_St_call_id x_14882 x_14881 x_14880 x_14879
     225| St_call_ptr (x_14886, x_14885, x_14884, x_14883) ->
     226  h_St_call_ptr x_14886 x_14885 x_14884 x_14883
     227| St_cond (x_14889, x_14888, x_14887) -> h_St_cond x_14889 x_14888 x_14887
    225228| St_return -> h_St_return
    226229
     
    241244    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    242245let 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
    243 | St_skip x_1947 -> h_St_skip x_1947
    244 | St_cost (x_1949, x_1948) -> h_St_cost x_1949 x_1948
    245 | St_const (t, x_1952, x_1951, x_1950) -> h_St_const t x_1952 x_1951 x_1950
    246 | St_op1 (t', t, x_1956, x_1955, x_1954, x_1953) ->
    247   h_St_op1 t' t x_1956 x_1955 x_1954 x_1953
    248 | St_op2 (t', t1, t2, x_1961, x_1960, x_1959, x_1958, x_1957) ->
    249   h_St_op2 t' t1 t2 x_1961 x_1960 x_1959 x_1958 x_1957
    250 | St_load (x_1965, x_1964, x_1963, x_1962) ->
    251   h_St_load x_1965 x_1964 x_1963 x_1962
    252 | St_store (x_1969, x_1968, x_1967, x_1966) ->
    253   h_St_store x_1969 x_1968 x_1967 x_1966
    254 | St_call_id (x_1973, x_1972, x_1971, x_1970) ->
    255   h_St_call_id x_1973 x_1972 x_1971 x_1970
    256 | St_call_ptr (x_1977, x_1976, x_1975, x_1974) ->
    257   h_St_call_ptr x_1977 x_1976 x_1975 x_1974
    258 | St_cond (x_1980, x_1979, x_1978) -> h_St_cond x_1980 x_1979 x_1978
     246| St_skip x_14902 -> h_St_skip x_14902
     247| St_cost (x_14904, x_14903) -> h_St_cost x_14904 x_14903
     248| St_const (t, x_14907, x_14906, x_14905) ->
     249  h_St_const t x_14907 x_14906 x_14905
     250| St_op1 (t', t, x_14911, x_14910, x_14909, x_14908) ->
     251  h_St_op1 t' t x_14911 x_14910 x_14909 x_14908
     252| St_op2 (t', t1, t2, x_14916, x_14915, x_14914, x_14913, x_14912) ->
     253  h_St_op2 t' t1 t2 x_14916 x_14915 x_14914 x_14913 x_14912
     254| St_load (x_14920, x_14919, x_14918, x_14917) ->
     255  h_St_load x_14920 x_14919 x_14918 x_14917
     256| St_store (x_14924, x_14923, x_14922, x_14921) ->
     257  h_St_store x_14924 x_14923 x_14922 x_14921
     258| St_call_id (x_14928, x_14927, x_14926, x_14925) ->
     259  h_St_call_id x_14928 x_14927 x_14926 x_14925
     260| St_call_ptr (x_14932, x_14931, x_14930, x_14929) ->
     261  h_St_call_ptr x_14932 x_14931 x_14930 x_14929
     262| St_cond (x_14935, x_14934, x_14933) -> h_St_cond x_14935 x_14934 x_14933
    259263| St_return -> h_St_return
    260264
     
    275279    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    276280let 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
    277 | St_skip x_1993 -> h_St_skip x_1993
    278 | St_cost (x_1995, x_1994) -> h_St_cost x_1995 x_1994
    279 | St_const (t, x_1998, x_1997, x_1996) -> h_St_const t x_1998 x_1997 x_1996
    280 | St_op1 (t', t, x_2002, x_2001, x_2000, x_1999) ->
    281   h_St_op1 t' t x_2002 x_2001 x_2000 x_1999
    282 | St_op2 (t', t1, t2, x_2007, x_2006, x_2005, x_2004, x_2003) ->
    283   h_St_op2 t' t1 t2 x_2007 x_2006 x_2005 x_2004 x_2003
    284 | St_load (x_2011, x_2010, x_2009, x_2008) ->
    285   h_St_load x_2011 x_2010 x_2009 x_2008
    286 | St_store (x_2015, x_2014, x_2013, x_2012) ->
    287   h_St_store x_2015 x_2014 x_2013 x_2012
    288 | St_call_id (x_2019, x_2018, x_2017, x_2016) ->
    289   h_St_call_id x_2019 x_2018 x_2017 x_2016
    290 | St_call_ptr (x_2023, x_2022, x_2021, x_2020) ->
    291   h_St_call_ptr x_2023 x_2022 x_2021 x_2020
    292 | St_cond (x_2026, x_2025, x_2024) -> h_St_cond x_2026 x_2025 x_2024
     281| St_skip x_14948 -> h_St_skip x_14948
     282| St_cost (x_14950, x_14949) -> h_St_cost x_14950 x_14949
     283| St_const (t, x_14953, x_14952, x_14951) ->
     284  h_St_const t x_14953 x_14952 x_14951
     285| St_op1 (t', t, x_14957, x_14956, x_14955, x_14954) ->
     286  h_St_op1 t' t x_14957 x_14956 x_14955 x_14954
     287| St_op2 (t', t1, t2, x_14962, x_14961, x_14960, x_14959, x_14958) ->
     288  h_St_op2 t' t1 t2 x_14962 x_14961 x_14960 x_14959 x_14958
     289| St_load (x_14966, x_14965, x_14964, x_14963) ->
     290  h_St_load x_14966 x_14965 x_14964 x_14963
     291| St_store (x_14970, x_14969, x_14968, x_14967) ->
     292  h_St_store x_14970 x_14969 x_14968 x_14967
     293| St_call_id (x_14974, x_14973, x_14972, x_14971) ->
     294  h_St_call_id x_14974 x_14973 x_14972 x_14971
     295| St_call_ptr (x_14978, x_14977, x_14976, x_14975) ->
     296  h_St_call_ptr x_14978 x_14977 x_14976 x_14975
     297| St_cond (x_14981, x_14980, x_14979) -> h_St_cond x_14981 x_14980 x_14979
    293298| St_return -> h_St_return
    294299
     
    309314    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    310315let 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
    311 | St_skip x_2039 -> h_St_skip x_2039
    312 | St_cost (x_2041, x_2040) -> h_St_cost x_2041 x_2040
    313 | St_const (t, x_2044, x_2043, x_2042) -> h_St_const t x_2044 x_2043 x_2042
    314 | St_op1 (t', t, x_2048, x_2047, x_2046, x_2045) ->
    315   h_St_op1 t' t x_2048 x_2047 x_2046 x_2045
    316 | St_op2 (t', t1, t2, x_2053, x_2052, x_2051, x_2050, x_2049) ->
    317   h_St_op2 t' t1 t2 x_2053 x_2052 x_2051 x_2050 x_2049
    318 | St_load (x_2057, x_2056, x_2055, x_2054) ->
    319   h_St_load x_2057 x_2056 x_2055 x_2054
    320 | St_store (x_2061, x_2060, x_2059, x_2058) ->
    321   h_St_store x_2061 x_2060 x_2059 x_2058
    322 | St_call_id (x_2065, x_2064, x_2063, x_2062) ->
    323   h_St_call_id x_2065 x_2064 x_2063 x_2062
    324 | St_call_ptr (x_2069, x_2068, x_2067, x_2066) ->
    325   h_St_call_ptr x_2069 x_2068 x_2067 x_2066
    326 | St_cond (x_2072, x_2071, x_2070) -> h_St_cond x_2072 x_2071 x_2070
     316| St_skip x_14994 -> h_St_skip x_14994
     317| St_cost (x_14996, x_14995) -> h_St_cost x_14996 x_14995
     318| St_const (t, x_14999, x_14998, x_14997) ->
     319  h_St_const t x_14999 x_14998 x_14997
     320| St_op1 (t', t, x_15003, x_15002, x_15001, x_15000) ->
     321  h_St_op1 t' t x_15003 x_15002 x_15001 x_15000
     322| St_op2 (t', t1, t2, x_15008, x_15007, x_15006, x_15005, x_15004) ->
     323  h_St_op2 t' t1 t2 x_15008 x_15007 x_15006 x_15005 x_15004
     324| St_load (x_15012, x_15011, x_15010, x_15009) ->
     325  h_St_load x_15012 x_15011 x_15010 x_15009
     326| St_store (x_15016, x_15015, x_15014, x_15013) ->
     327  h_St_store x_15016 x_15015 x_15014 x_15013
     328| St_call_id (x_15020, x_15019, x_15018, x_15017) ->
     329  h_St_call_id x_15020 x_15019 x_15018 x_15017
     330| St_call_ptr (x_15024, x_15023, x_15022, x_15021) ->
     331  h_St_call_ptr x_15024 x_15023 x_15022 x_15021
     332| St_cond (x_15027, x_15026, x_15025) -> h_St_cond x_15027 x_15026 x_15025
    327333| St_return -> h_St_return
    328334
     
    460466    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    461467    internal_function -> 'a1 **)
    462 let rec internal_function_rect_Type4 h_mk_internal_function x_2362 =
     468let rec internal_function_rect_Type4 h_mk_internal_function x_15317 =
    463469  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    464470    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    465     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_2362
     471    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15317
    466472  in
    467473  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    475481    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    476482    internal_function -> 'a1 **)
    477 let rec internal_function_rect_Type5 h_mk_internal_function x_2364 =
     483let rec internal_function_rect_Type5 h_mk_internal_function x_15319 =
    478484  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    479485    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    480     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_2364
     486    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15319
    481487  in
    482488  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    490496    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    491497    internal_function -> 'a1 **)
    492 let rec internal_function_rect_Type3 h_mk_internal_function x_2366 =
     498let rec internal_function_rect_Type3 h_mk_internal_function x_15321 =
    493499  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    494500    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    495     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_2366
     501    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15321
    496502  in
    497503  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    505511    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    506512    internal_function -> 'a1 **)
    507 let rec internal_function_rect_Type2 h_mk_internal_function x_2368 =
     513let rec internal_function_rect_Type2 h_mk_internal_function x_15323 =
    508514  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    509515    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    510     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_2368
     516    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15323
    511517  in
    512518  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    520526    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    521527    internal_function -> 'a1 **)
    522 let rec internal_function_rect_Type1 h_mk_internal_function x_2370 =
     528let rec internal_function_rect_Type1 h_mk_internal_function x_15325 =
    523529  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    524530    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    525     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_2370
     531    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15325
    526532  in
    527533  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    535541    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    536542    internal_function -> 'a1 **)
    537 let rec internal_function_rect_Type0 h_mk_internal_function x_2372 =
     543let rec internal_function_rect_Type0 h_mk_internal_function x_15327 =
    538544  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    539545    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    540     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_2372
     546    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15327
    541547  in
    542548  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
Note: See TracChangeset for help on using the changeset viewer.