Ignore:
Timestamp:
Aug 31, 2011, 12:15:39 PM (10 years ago)
Author:
campbell
Message:

Update pretty printers and examples.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/RTLabs/test/search.RTLabs.ma

    r967 r1157  
    55
    66
    7   definition id_search := ident_of_nat 0.
    8   definition search9 := 50.
    9   definition search8 := 49.
    10   definition search7 := 48.
    11   definition search6 := 47.
    12   definition search50 := 46.
    13   definition search5 := 45.
    14   definition search49 := 44.
    15   definition search48 := 43.
    16   definition search47 := 42.
    17   definition search46 := 41.
    18   definition search45 := 40.
    19   definition search44 := 39.
    20   definition search43 := 38.
    21   definition search42 := 37.
    22   definition search41 := 36.
    23   definition search40 := 35.
    24   definition search4 := 34.
    25   definition search39 := 33.
    26   definition search38 := 32.
    27   definition search37 := 31.
    28   definition search36 := 30.
    29   definition search35 := 29.
    30   definition search34 := 28.
    31   definition search33 := 27.
    32   definition search32 := 26.
    33   definition search31 := 25.
    34   definition search30 := 24.
    35   definition search3 := 23.
    36   definition search29 := 22.
    37   definition search28 := 21.
    38   definition search27 := 20.
    39   definition search26 := 19.
    40   definition search25 := 18.
    41   definition search24 := 17.
    42   definition search23 := 16.
    43   definition search22 := 15.
    44   definition search21 := 14.
    45   definition search20 := 13.
    46   definition search2 := 12.
    47   definition search19 := 11.
    48   definition search18 := 10.
    49   definition search17 := 9.
    50   definition search16 := 8.
    51   definition search15 := 7.
    52   definition search14 := 6.
    53   definition search13 := 5.
    54   definition search12 := 4.
    55   definition search11 := 3.
    56   definition search10 := 2.
    57   definition search1 := 1.
    58   definition search0 := 0.
    59   definition C_cost1 := costlabel_of_nat 8.
    60   definition C_cost8 := costlabel_of_nat 7.
    61   definition C_cost6 := costlabel_of_nat 6.
    62   definition C_cost7 := costlabel_of_nat 5.
    63   definition C_cost4 := costlabel_of_nat 4.
    64   definition C_cost5 := costlabel_of_nat 3.
    65   definition C_cost2 := costlabel_of_nat 2.
    66   definition C_cost3 := costlabel_of_nat 1.
    67   definition C_cost0 := costlabel_of_nat 0.
    68 
    69 
    70   definition pre_search := mk_pre_internal_function
    71     (Some ? (pair ?? 6 (ASTint I8 Unsigned)))
    72     [(pair ?? 0 (ASTptr Any)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I8 Unsigned))]
    73     [(pair ?? 3 (ASTint I8 Unsigned)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Unsigned)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTint I8 Signed)); (pair ?? 9 (ASTint I8 Unsigned)); (pair ?? 10 (ASTint I8 Unsigned)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Unsigned)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I8 Unsigned)); (pair ?? 15 (ASTint I8 Unsigned)); (pair ?? 16 (ASTint I8 Unsigned)); (pair ?? 17 (ASTint I8 Unsigned)); (pair ?? 18 (ASTint I8 Unsigned)); (pair ?? 19 (ASTint I8 Unsigned)); (pair ?? 20 (ASTptr Any)); (pair ?? 21 (ASTint I8 Unsigned)); (pair ?? 22 (ASTint I8 Unsigned)); (pair ?? 23 (ASTint I8 Unsigned)); (pair ?? 24 (ASTint I8 Unsigned)); (pair ?? 25 (ASTptr Any)); (pair ?? 26 (ASTint I8 Unsigned)); (pair ?? 27 (ASTint I8 Unsigned)); (pair ?? 28 (ASTint I8 Unsigned)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Unsigned)); (pair ?? 31 (ASTint I8 Unsigned)); (pair ?? 32 (ASTint I8 Unsigned)); (pair ?? 33 (ASTint I8 Unsigned)); (pair ?? 34 (ASTint I8 Unsigned)); (pair ?? 35 (ASTint I8 Signed))]
     7  definition id__div32u := ident_of_nat 0.
     8  definition lbl__div32u9 := 15.
     9  definition lbl__div32u8 := 14.
     10  definition lbl__div32u7 := 13.
     11  definition lbl__div32u6 := 12.
     12  definition lbl__div32u5 := 11.
     13  definition lbl__div32u4 := 10.
     14  definition lbl__div32u3 := 9.
     15  definition lbl__div32u2 := 8.
     16  definition lbl__div32u15 := 7.
     17  definition lbl__div32u14 := 6.
     18  definition lbl__div32u13 := 5.
     19  definition lbl__div32u12 := 4.
     20  definition lbl__div32u11 := 3.
     21  definition lbl__div32u10 := 2.
     22  definition lbl__div32u1 := 1.
     23  definition lbl__div32u0 := 0.
     24  definition C_cost0 := costlabel_of_nat 2.
     25  definition C_cost1 := costlabel_of_nat 1.
     26  definition C_cost2 := costlabel_of_nat 0.
     27
     28
     29  definition pre__div32u := mk_pre_internal_function
     30    (Some ? (pair ?? 4 (ASTint I32 Unsigned)))
     31    [(pair ?? 0 (ASTint I32 Unsigned)); (pair ?? 1 (ASTint I32 Unsigned))]
     32    [(pair ?? 2 (ASTint I32 Unsigned)); (pair ?? 3 (ASTint I32 Unsigned)); (pair ?? 4 (ASTint I32 Unsigned)); (pair ?? 5 (ASTint I32 Unsigned)); (pair ?? 6 (ASTint I32 Signed)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I32 Signed)); (pair ?? 9 (ASTint I8 Signed))]
    7433    0
    7534    [
    76     (pair ?? search9 (make_St_const 10 (Ointconst I8 (repr ? 1)) search8));
    77     (pair ?? search8 (make_St_op2 Oadd 9 4 10 search7));
    78     (pair ?? search7 (make_St_op1 (Ocastint Unsigned I8) 5 9 search5));
    79     (pair ?? search6 (make_St_cost C_cost1 search5));
    80     (pair ?? search50 (make_St_cost C_cost8 search49));
    81     (pair ?? search5 (make_St_skip search44));
    82     (pair ?? search49 (make_St_const 35 (Ointconst I8 (repr ? 0)) search48));
    83     (pair ?? search48 (make_St_op1 (Ocastint Signed I8) 5 35 search47));
    84     (pair ?? search47 (make_St_const 34 (Ointconst I8 (repr ? 1)) search46));
    85     (pair ?? search46 (make_St_op2 Osub 33 1 34 search45));
    86     (pair ?? search45 (make_St_op1 (Ocastint Unsigned I8) 3 33 search5));
    87     (pair ?? search44 (make_St_op2 (Ocmpu Cge) 32 3 5 search43));
    88     (pair ?? search43 (make_St_op1 Onotbool 31 32 search42));
    89     (pair ?? search42 (make_St_cond 31 search4 search41));
    90     (pair ?? search41 (make_St_cost C_cost6 search40));
    91     (pair ?? search40 (make_St_op2 Oadd 29 3 5 search39));
    92     (pair ?? search4 (make_St_cost C_cost7 search3));
    93     (pair ?? search39 (make_St_const 30 (Ointconst I8 (repr ? 2)) search38));
    94     (pair ?? search38 (make_St_op2 Odivu 28 29 30 search37));
    95     (pair ?? search37 (make_St_op1 (Ocastint Unsigned I8) 4 28 search36));
    96     (pair ?? search36 (make_St_const 27 (Ointconst I8 (repr ? 1)) search35));
    97     (pair ?? search35 (make_St_op2 Omul 26 4 27 search34));
    98     (pair ?? search34 (make_St_op2 Oaddp 25 0 26 search33));
    99     (pair ?? search33 (make_St_load Mint8unsigned 25 24 search32));
    100     (pair ?? search32 (make_St_op2 (Ocmpu Ceq) 23 24 2 search31));
    101     (pair ?? search31 (make_St_cond 23 search30 search28));
    102     (pair ?? search30 (make_St_cost C_cost4 search29));
    103     (pair ?? search3 (make_St_const 8 (Ointconst I8 (repr ? 1)) search2));
    104     (pair ?? search29 (make_St_op1 Oid 6 4 search0));
    105     (pair ?? search28 (make_St_cost C_cost5 search27));
    106     (pair ?? search27 (make_St_const 22 (Ointconst I8 (repr ? 1)) search26));
    107     (pair ?? search26 (make_St_op2 Omul 21 4 22 search25));
    108     (pair ?? search25 (make_St_op2 Oaddp 20 0 21 search24));
    109     (pair ?? search24 (make_St_load Mint8unsigned 20 19 search23));
    110     (pair ?? search23 (make_St_op2 (Ocmpu Cgt) 18 19 2 search22));
    111     (pair ?? search22 (make_St_cond 18 search21 search17));
    112     (pair ?? search21 (make_St_cost C_cost2 search20));
    113     (pair ?? search20 (make_St_const 17 (Ointconst I8 (repr ? 1)) search19));
    114     (pair ?? search2 (make_St_op1 Onegint 7 8 search1));
    115     (pair ?? search19 (make_St_op2 Osub 16 4 17 search18));
    116     (pair ?? search18 (make_St_op1 (Ocastint Unsigned I8) 3 16 search16));
    117     (pair ?? search17 (make_St_cost C_cost3 search16));
    118     (pair ?? search16 (make_St_const 15 (Ointconst I8 (repr ? 1)) search15));
    119     (pair ?? search15 (make_St_op2 Omul 14 4 15 search14));
    120     (pair ?? search14 (make_St_op2 Oaddp 13 0 14 search13));
    121     (pair ?? search13 (make_St_load Mint8unsigned 13 12 search12));
    122     (pair ?? search12 (make_St_op2 (Ocmpu Clt) 11 12 2 search11));
    123     (pair ?? search11 (make_St_cond 11 search10 search6));
    124     (pair ?? search10 (make_St_cost C_cost0 search9));
    125     (pair ?? search1 (make_St_op1 (Ocastint Signed I8) 6 7 search0));
    126     (pair ?? search0 (make_St_return))
     35    (pair ?? lbl__div32u9 (make_St_cond 7 lbl__div32u2 lbl__div32u8));
     36    (pair ?? lbl__div32u8 (make_St_cost C_cost0 lbl__div32u7));
     37    (pair ?? lbl__div32u7 (make_St_op2 Osub 3 3 1 lbl__div32u6));
     38    (pair ?? lbl__div32u6 (make_St_const 6 (Ointconst I32 (repr ? 1)) lbl__div32u5));
     39    (pair ?? lbl__div32u5 (make_St_op1 (Ocastint Signed I32) 5 6 lbl__div32u4));
     40    (pair ?? lbl__div32u4 (make_St_op2 Oadd 2 2 5 lbl__div32u3));
     41    (pair ?? lbl__div32u3 (make_St_skip lbl__div32u11));
     42    (pair ?? lbl__div32u2 (make_St_cost C_cost1 lbl__div32u1));
     43    (pair ?? lbl__div32u15 (make_St_cost C_cost2 lbl__div32u14));
     44    (pair ?? lbl__div32u14 (make_St_const 9 (Ointconst I8 (repr ? 0)) lbl__div32u13));
     45    (pair ?? lbl__div32u13 (make_St_op1 (Ocastint Signed I32) 2 9 lbl__div32u12));
     46    (pair ?? lbl__div32u12 (make_St_op1 Oid 3 0 lbl__div32u3));
     47    (pair ?? lbl__div32u11 (make_St_op2 (Ocmpu Cge) 8 3 1 lbl__div32u10));
     48    (pair ?? lbl__div32u10 (make_St_op1 Onotbool 7 8 lbl__div32u9));
     49    (pair ?? lbl__div32u1 (make_St_op1 Oid 4 2 lbl__div32u0));
     50    (pair ?? lbl__div32u0 (make_St_return))
    12751]
    12852
    129     search50
    130     search0.
    131 
    132   definition id_main := ident_of_nat 1.
    133   definition main9 := 61.
    134   definition main8 := 60.
    135   definition main7 := 59.
    136   definition main61 := 58.
    137   definition main60 := 57.
    138   definition main6 := 56.
    139   definition main59 := 55.
    140   definition main58 := 54.
    141   definition main57 := 53.
    142   definition main56 := 52.
    143   definition main55 := 51.
    144   definition main54 := 50.
    145   definition main53 := 49.
    146   definition main52 := 48.
    147   definition main51 := 47.
    148   definition main50 := 46.
    149   definition main5 := 45.
    150   definition main49 := 44.
    151   definition main48 := 43.
    152   definition main47 := 42.
    153   definition main46 := 41.
    154   definition main45 := 40.
    155   definition main44 := 39.
    156   definition main43 := 38.
    157   definition main42 := 37.
    158   definition main41 := 36.
    159   definition main40 := 35.
    160   definition main4 := 34.
    161   definition main39 := 33.
    162   definition main38 := 32.
    163   definition main37 := 31.
    164   definition main36 := 30.
    165   definition main35 := 29.
    166   definition main34 := 28.
    167   definition main33 := 27.
    168   definition main32 := 26.
    169   definition main31 := 25.
    170   definition main30 := 24.
    171   definition main3 := 23.
    172   definition main29 := 22.
    173   definition main28 := 21.
    174   definition main27 := 20.
    175   definition main26 := 19.
    176   definition main25 := 18.
    177   definition main24 := 17.
    178   definition main23 := 16.
    179   definition main22 := 15.
    180   definition main21 := 14.
    181   definition main20 := 13.
    182   definition main2 := 12.
    183   definition main19 := 11.
    184   definition main18 := 10.
    185   definition main17 := 9.
    186   definition main16 := 8.
    187   definition main15 := 7.
    188   definition main14 := 6.
    189   definition main13 := 5.
    190   definition main12 := 4.
    191   definition main11 := 3.
    192   definition main10 := 2.
    193   definition main1 := 1.
    194   definition main0 := 0.
    195   definition C_cost9 := costlabel_of_nat 0.
     53    lbl__div32u15
     54    lbl__div32u0.
     55
     56  definition id__div32s := ident_of_nat 1.
     57  definition lbl__div32s9 := 25.
     58  definition lbl__div32s8 := 24.
     59  definition lbl__div32s7 := 23.
     60  definition lbl__div32s6 := 22.
     61  definition lbl__div32s5 := 21.
     62  definition lbl__div32s4 := 20.
     63  definition lbl__div32s3 := 19.
     64  definition lbl__div32s25 := 18.
     65  definition lbl__div32s24 := 17.
     66  definition lbl__div32s23 := 16.
     67  definition lbl__div32s22 := 15.
     68  definition lbl__div32s21 := 14.
     69  definition lbl__div32s20 := 13.
     70  definition lbl__div32s2 := 12.
     71  definition lbl__div32s19 := 11.
     72  definition lbl__div32s18 := 10.
     73  definition lbl__div32s17 := 9.
     74  definition lbl__div32s16 := 8.
     75  definition lbl__div32s15 := 7.
     76  definition lbl__div32s14 := 6.
     77  definition lbl__div32s13 := 5.
     78  definition lbl__div32s12 := 4.
     79  definition lbl__div32s11 := 3.
     80  definition lbl__div32s10 := 2.
     81  definition lbl__div32s1 := 1.
     82  definition lbl__div32s0 := 0.
     83  definition C_cost3 := costlabel_of_nat 4.
     84  definition C_cost4 := costlabel_of_nat 3.
     85  definition C_cost7 := costlabel_of_nat 2.
     86  definition C_cost5 := costlabel_of_nat 1.
     87  definition C_cost6 := costlabel_of_nat 0.
     88
     89
     90  definition pre__div32s := mk_pre_internal_function
     91    (Some ? (pair ?? 7 (ASTint I32 Signed)))
     92    [(pair ?? 0 (ASTint I32 Signed)); (pair ?? 1 (ASTint I32 Signed))]
     93    [(pair ?? 2 (ASTint I32 Unsigned)); (pair ?? 3 (ASTint I32 Signed)); (pair ?? 4 (ASTint I32 Unsigned)); (pair ?? 5 (ASTint I32 Unsigned)); (pair ?? 6 (ASTint I32 Unsigned)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I32 Signed)); (pair ?? 9 (ASTint I32 Signed)); (pair ?? 10 (ASTint I32 Signed)); (pair ?? 11 (ASTint I32 Signed)); (pair ?? 12 (ASTint I32 Signed)); (pair ?? 13 (ASTint I32 Signed)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I8 Signed))]
     94    0
     95    [
     96    (pair ?? lbl__div32s9 (make_St_cost C_cost3 lbl__div32s8));
     97    (pair ?? lbl__div32s8 (make_St_op1 Onegint 9 1 lbl__div32s7));
     98    (pair ?? lbl__div32s7 (make_St_op1 (Ocastint Signed I32) 5 9 lbl__div32s6));
     99    (pair ?? lbl__div32s6 (make_St_op1 Onegint 3 3 lbl__div32s4));
     100    (pair ?? lbl__div32s5 (make_St_cost C_cost4 lbl__div32s4));
     101    (pair ?? lbl__div32s4 (make_St_call_id id__div32u [4; 5] (Some ? 6) lbl__div32s3));
     102    (pair ?? lbl__div32s3 (make_St_op1 Oid 2 6 lbl__div32s2));
     103    (pair ?? lbl__div32s25 (make_St_cost C_cost7 lbl__div32s24));
     104    (pair ?? lbl__div32s24 (make_St_op1 (Ocastint Signed I32) 4 0 lbl__div32s23));
     105    (pair ?? lbl__div32s23 (make_St_op1 (Ocastint Signed I32) 5 1 lbl__div32s22));
     106    (pair ?? lbl__div32s22 (make_St_const 15 (Ointconst I8 (repr ? 1)) lbl__div32s21));
     107    (pair ?? lbl__div32s21 (make_St_op1 (Ocastint Signed I32) 3 15 lbl__div32s20));
     108    (pair ?? lbl__div32s20 (make_St_const 14 (Ointconst I32 (repr ? 0)) lbl__div32s19));
     109    (pair ?? lbl__div32s2 (make_St_op1 (Ocastint Unsigned I32) 8 2 lbl__div32s1));
     110    (pair ?? lbl__div32s19 (make_St_op2 (Ocmp Clt) 13 0 14 lbl__div32s18));
     111    (pair ?? lbl__div32s18 (make_St_cond 13 lbl__div32s17 lbl__div32s13));
     112    (pair ?? lbl__div32s17 (make_St_cost C_cost5 lbl__div32s16));
     113    (pair ?? lbl__div32s16 (make_St_op1 Onegint 12 0 lbl__div32s15));
     114    (pair ?? lbl__div32s15 (make_St_op1 (Ocastint Signed I32) 4 12 lbl__div32s14));
     115    (pair ?? lbl__div32s14 (make_St_op1 Onegint 3 3 lbl__div32s12));
     116    (pair ?? lbl__div32s13 (make_St_cost C_cost6 lbl__div32s12));
     117    (pair ?? lbl__div32s12 (make_St_const 11 (Ointconst I32 (repr ? 0)) lbl__div32s11));
     118    (pair ?? lbl__div32s11 (make_St_op2 (Ocmp Clt) 10 1 11 lbl__div32s10));
     119    (pair ?? lbl__div32s10 (make_St_cond 10 lbl__div32s9 lbl__div32s5));
     120    (pair ?? lbl__div32s1 (make_St_op2 Omul 7 3 8 lbl__div32s0));
     121    (pair ?? lbl__div32s0 (make_St_return))
     122]
     123
     124    lbl__div32s25
     125    lbl__div32s0.
     126
     127  definition id_search := ident_of_nat 2.
     128  definition lbl_search9 := 65.
     129  definition lbl_search8 := 64.
     130  definition lbl_search7 := 63.
     131  definition lbl_search65 := 62.
     132  definition lbl_search64 := 61.
     133  definition lbl_search63 := 60.
     134  definition lbl_search62 := 59.
     135  definition lbl_search61 := 58.
     136  definition lbl_search60 := 57.
     137  definition lbl_search6 := 56.
     138  definition lbl_search59 := 55.
     139  definition lbl_search58 := 54.
     140  definition lbl_search57 := 53.
     141  definition lbl_search56 := 52.
     142  definition lbl_search55 := 51.
     143  definition lbl_search54 := 50.
     144  definition lbl_search53 := 49.
     145  definition lbl_search52 := 48.
     146  definition lbl_search51 := 47.
     147  definition lbl_search50 := 46.
     148  definition lbl_search5 := 45.
     149  definition lbl_search49 := 44.
     150  definition lbl_search48 := 43.
     151  definition lbl_search47 := 42.
     152  definition lbl_search46 := 41.
     153  definition lbl_search45 := 40.
     154  definition lbl_search44 := 39.
     155  definition lbl_search43 := 38.
     156  definition lbl_search42 := 37.
     157  definition lbl_search41 := 36.
     158  definition lbl_search40 := 35.
     159  definition lbl_search4 := 34.
     160  definition lbl_search39 := 33.
     161  definition lbl_search38 := 32.
     162  definition lbl_search37 := 31.
     163  definition lbl_search36 := 30.
     164  definition lbl_search35 := 29.
     165  definition lbl_search34 := 28.
     166  definition lbl_search33 := 27.
     167  definition lbl_search32 := 26.
     168  definition lbl_search31 := 25.
     169  definition lbl_search30 := 24.
     170  definition lbl_search3 := 23.
     171  definition lbl_search29 := 22.
     172  definition lbl_search28 := 21.
     173  definition lbl_search27 := 20.
     174  definition lbl_search26 := 19.
     175  definition lbl_search25 := 18.
     176  definition lbl_search24 := 17.
     177  definition lbl_search23 := 16.
     178  definition lbl_search22 := 15.
     179  definition lbl_search21 := 14.
     180  definition lbl_search20 := 13.
     181  definition lbl_search2 := 12.
     182  definition lbl_search19 := 11.
     183  definition lbl_search18 := 10.
     184  definition lbl_search17 := 9.
     185  definition lbl_search16 := 8.
     186  definition lbl_search15 := 7.
     187  definition lbl_search14 := 6.
     188  definition lbl_search13 := 5.
     189  definition lbl_search12 := 4.
     190  definition lbl_search11 := 3.
     191  definition lbl_search10 := 2.
     192  definition lbl_search1 := 1.
     193  definition lbl_search0 := 0.
     194  definition C_cost16 := costlabel_of_nat 8.
     195  definition C_cost9 := costlabel_of_nat 7.
     196  definition C_cost14 := costlabel_of_nat 6.
     197  definition C_cost15 := costlabel_of_nat 5.
     198  definition C_cost12 := costlabel_of_nat 4.
     199  definition C_cost13 := costlabel_of_nat 3.
     200  definition C_cost10 := costlabel_of_nat 2.
     201  definition C_cost11 := costlabel_of_nat 1.
     202  definition C_cost8 := costlabel_of_nat 0.
     203
     204
     205  definition pre_search := mk_pre_internal_function
     206    (Some ? (pair ?? 8 (ASTint I8 Unsigned)))
     207    [(pair ?? 0 (ASTptr Any)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I8 Unsigned))]
     208    [(pair ?? 3 (ASTint I32 Signed)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Unsigned)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I8 Unsigned)); (pair ?? 9 (ASTint I32 Signed)); (pair ?? 10 (ASTint I32 Signed)); (pair ?? 11 (ASTint I32 Signed)); (pair ?? 12 (ASTint I32 Signed)); (pair ?? 13 (ASTint I32 Signed)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I32 Signed)); (pair ?? 16 (ASTint I32 Signed)); (pair ?? 17 (ASTint I8 Unsigned)); (pair ?? 18 (ASTptr Any)); (pair ?? 19 (ASTint I8 Unsigned)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I32 Signed)); (pair ?? 22 (ASTint I32 Signed)); (pair ?? 23 (ASTint I32 Signed)); (pair ?? 24 (ASTint I32 Signed)); (pair ?? 25 (ASTint I32 Signed)); (pair ?? 26 (ASTint I32 Signed)); (pair ?? 27 (ASTint I8 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Unsigned)); (pair ?? 31 (ASTint I32 Signed)); (pair ?? 32 (ASTint I32 Signed)); (pair ?? 33 (ASTint I32 Signed)); (pair ?? 34 (ASTint I8 Unsigned)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I8 Unsigned)); (pair ?? 37 (ASTint I8 Unsigned)); (pair ?? 38 (ASTint I32 Signed)); (pair ?? 39 (ASTint I32 Signed)); (pair ?? 40 (ASTint I8 Signed)); (pair ?? 41 (ASTint I32 Signed)); (pair ?? 42 (ASTint I32 Signed)); (pair ?? 43 (ASTint I32 Signed)); (pair ?? 44 (ASTint I32 Signed)); (pair ?? 45 (ASTint I32 Signed)); (pair ?? 46 (ASTint I32 Signed)); (pair ?? 47 (ASTint I32 Signed)); (pair ?? 48 (ASTint I32 Signed)); (pair ?? 49 (ASTint I32 Signed)); (pair ?? 50 (ASTint I8 Signed))]
     209    0
     210    [
     211    (pair ?? lbl_search9 (make_St_const 13 (Ointconst I32 (repr ? 1)) lbl_search8));
     212    (pair ?? lbl_search8 (make_St_op2 Oadd 11 12 13 lbl_search7));
     213    (pair ?? lbl_search7 (make_St_op1 (Ocastint Signed I8) 6 11 lbl_search5));
     214    (pair ?? lbl_search65 (make_St_cost C_cost16 lbl_search64));
     215    (pair ?? lbl_search64 (make_St_const 50 (Ointconst I8 (repr ? 0)) lbl_search63));
     216    (pair ?? lbl_search63 (make_St_op1 (Ocastint Signed I8) 6 50 lbl_search62));
     217    (pair ?? lbl_search62 (make_St_op1 (Ocastint Unsigned I32) 48 1 lbl_search61));
     218    (pair ?? lbl_search61 (make_St_const 49 (Ointconst I32 (repr ? 1)) lbl_search60));
     219    (pair ?? lbl_search60 (make_St_op2 Osub 47 48 49 lbl_search59));
     220    (pair ?? lbl_search6 (make_St_cost C_cost9 lbl_search5));
     221    (pair ?? lbl_search59 (make_St_op1 (Ocastint Signed I8) 4 47 lbl_search5));
     222    (pair ?? lbl_search58 (make_St_op1 (Ocastint Unsigned I32) 45 4 lbl_search57));
     223    (pair ?? lbl_search57 (make_St_op1 (Ocastint Unsigned I32) 46 6 lbl_search56));
     224    (pair ?? lbl_search56 (make_St_op2 (Ocmp Cge) 44 45 46 lbl_search55));
     225    (pair ?? lbl_search55 (make_St_op1 Onotbool 43 44 lbl_search54));
     226    (pair ?? lbl_search54 (make_St_cond 43 lbl_search4 lbl_search53));
     227    (pair ?? lbl_search53 (make_St_cost C_cost14 lbl_search52));
     228    (pair ?? lbl_search52 (make_St_op1 (Ocastint Unsigned I32) 41 4 lbl_search51));
     229    (pair ?? lbl_search51 (make_St_op1 (Ocastint Unsigned I32) 42 6 lbl_search50));
     230    (pair ?? lbl_search50 (make_St_op2 Oadd 38 41 42 lbl_search49));
     231    (pair ?? lbl_search5 (make_St_skip lbl_search58));
     232    (pair ?? lbl_search49 (make_St_const 40 (Ointconst I8 (repr ? 2)) lbl_search48));
     233    (pair ?? lbl_search48 (make_St_op1 (Ocastint Signed I32) 39 40 lbl_search47));
     234    (pair ?? lbl_search47 (make_St_call_id id__div32s [38; 39] (Some ? 7) lbl_search46));
     235    (pair ?? lbl_search46 (make_St_op1 Oid 3 7 lbl_search45));
     236    (pair ?? lbl_search45 (make_St_op1 (Ocastint Signed I8) 5 3 lbl_search44));
     237    (pair ?? lbl_search44 (make_St_const 37 (Ointconst I8 (repr ? 1)) lbl_search43));
     238    (pair ?? lbl_search43 (make_St_op2 Omul 36 5 37 lbl_search42));
     239    (pair ?? lbl_search42 (make_St_op2 Oaddp 35 0 36 lbl_search41));
     240    (pair ?? lbl_search41 (make_St_load Mint8unsigned 35 34 lbl_search40));
     241    (pair ?? lbl_search40 (make_St_op1 (Ocastint Unsigned I32) 32 34 lbl_search39));
     242    (pair ?? lbl_search4 (make_St_cost C_cost15 lbl_search3));
     243    (pair ?? lbl_search39 (make_St_op1 (Ocastint Unsigned I32) 33 2 lbl_search38));
     244    (pair ?? lbl_search38 (make_St_op2 (Ocmp Ceq) 31 32 33 lbl_search37));
     245    (pair ?? lbl_search37 (make_St_cond 31 lbl_search36 lbl_search34));
     246    (pair ?? lbl_search36 (make_St_cost C_cost12 lbl_search35));
     247    (pair ?? lbl_search35 (make_St_op1 Oid 8 5 lbl_search0));
     248    (pair ?? lbl_search34 (make_St_cost C_cost13 lbl_search33));
     249    (pair ?? lbl_search33 (make_St_const 30 (Ointconst I8 (repr ? 1)) lbl_search32));
     250    (pair ?? lbl_search32 (make_St_op2 Omul 29 5 30 lbl_search31));
     251    (pair ?? lbl_search31 (make_St_op2 Oaddp 28 0 29 lbl_search30));
     252    (pair ?? lbl_search30 (make_St_load Mint8unsigned 28 27 lbl_search29));
     253    (pair ?? lbl_search3 (make_St_const 10 (Ointconst I32 (repr ? 1)) lbl_search2));
     254    (pair ?? lbl_search29 (make_St_op1 (Ocastint Unsigned I32) 25 27 lbl_search28));
     255    (pair ?? lbl_search28 (make_St_op1 (Ocastint Unsigned I32) 26 2 lbl_search27));
     256    (pair ?? lbl_search27 (make_St_op2 (Ocmp Cgt) 24 25 26 lbl_search26));
     257    (pair ?? lbl_search26 (make_St_cond 24 lbl_search25 lbl_search20));
     258    (pair ?? lbl_search25 (make_St_cost C_cost10 lbl_search24));
     259    (pair ?? lbl_search24 (make_St_op1 (Ocastint Unsigned I32) 22 5 lbl_search23));
     260    (pair ?? lbl_search23 (make_St_const 23 (Ointconst I32 (repr ? 1)) lbl_search22));
     261    (pair ?? lbl_search22 (make_St_op2 Osub 21 22 23 lbl_search21));
     262    (pair ?? lbl_search21 (make_St_op1 (Ocastint Signed I8) 4 21 lbl_search19));
     263    (pair ?? lbl_search20 (make_St_cost C_cost11 lbl_search19));
     264    (pair ?? lbl_search2 (make_St_op1 Onegint 9 10 lbl_search1));
     265    (pair ?? lbl_search19 (make_St_const 20 (Ointconst I8 (repr ? 1)) lbl_search18));
     266    (pair ?? lbl_search18 (make_St_op2 Omul 19 5 20 lbl_search17));
     267    (pair ?? lbl_search17 (make_St_op2 Oaddp 18 0 19 lbl_search16));
     268    (pair ?? lbl_search16 (make_St_load Mint8unsigned 18 17 lbl_search15));
     269    (pair ?? lbl_search15 (make_St_op1 (Ocastint Unsigned I32) 15 17 lbl_search14));
     270    (pair ?? lbl_search14 (make_St_op1 (Ocastint Unsigned I32) 16 2 lbl_search13));
     271    (pair ?? lbl_search13 (make_St_op2 (Ocmp Clt) 14 15 16 lbl_search12));
     272    (pair ?? lbl_search12 (make_St_cond 14 lbl_search11 lbl_search6));
     273    (pair ?? lbl_search11 (make_St_cost C_cost8 lbl_search10));
     274    (pair ?? lbl_search10 (make_St_op1 (Ocastint Unsigned I32) 12 5 lbl_search9));
     275    (pair ?? lbl_search1 (make_St_op1 (Ocastint Signed I8) 8 9 lbl_search0));
     276    (pair ?? lbl_search0 (make_St_return))
     277]
     278
     279    lbl_search65
     280    lbl_search0.
     281
     282  definition id_main := ident_of_nat 3.
     283  definition lbl_main9 := 61.
     284  definition lbl_main8 := 60.
     285  definition lbl_main7 := 59.
     286  definition lbl_main61 := 58.
     287  definition lbl_main60 := 57.
     288  definition lbl_main6 := 56.
     289  definition lbl_main59 := 55.
     290  definition lbl_main58 := 54.
     291  definition lbl_main57 := 53.
     292  definition lbl_main56 := 52.
     293  definition lbl_main55 := 51.
     294  definition lbl_main54 := 50.
     295  definition lbl_main53 := 49.
     296  definition lbl_main52 := 48.
     297  definition lbl_main51 := 47.
     298  definition lbl_main50 := 46.
     299  definition lbl_main5 := 45.
     300  definition lbl_main49 := 44.
     301  definition lbl_main48 := 43.
     302  definition lbl_main47 := 42.
     303  definition lbl_main46 := 41.
     304  definition lbl_main45 := 40.
     305  definition lbl_main44 := 39.
     306  definition lbl_main43 := 38.
     307  definition lbl_main42 := 37.
     308  definition lbl_main41 := 36.
     309  definition lbl_main40 := 35.
     310  definition lbl_main4 := 34.
     311  definition lbl_main39 := 33.
     312  definition lbl_main38 := 32.
     313  definition lbl_main37 := 31.
     314  definition lbl_main36 := 30.
     315  definition lbl_main35 := 29.
     316  definition lbl_main34 := 28.
     317  definition lbl_main33 := 27.
     318  definition lbl_main32 := 26.
     319  definition lbl_main31 := 25.
     320  definition lbl_main30 := 24.
     321  definition lbl_main3 := 23.
     322  definition lbl_main29 := 22.
     323  definition lbl_main28 := 21.
     324  definition lbl_main27 := 20.
     325  definition lbl_main26 := 19.
     326  definition lbl_main25 := 18.
     327  definition lbl_main24 := 17.
     328  definition lbl_main23 := 16.
     329  definition lbl_main22 := 15.
     330  definition lbl_main21 := 14.
     331  definition lbl_main20 := 13.
     332  definition lbl_main2 := 12.
     333  definition lbl_main19 := 11.
     334  definition lbl_main18 := 10.
     335  definition lbl_main17 := 9.
     336  definition lbl_main16 := 8.
     337  definition lbl_main15 := 7.
     338  definition lbl_main14 := 6.
     339  definition lbl_main13 := 5.
     340  definition lbl_main12 := 4.
     341  definition lbl_main11 := 3.
     342  definition lbl_main10 := 2.
     343  definition lbl_main1 := 1.
     344  definition lbl_main0 := 0.
     345  definition C_cost17 := costlabel_of_nat 0.
    196346
    197347
    … …  
    199349    (Some ? (pair ?? 2 (ASTint I32 Signed)))
    200350    []
    201     [(pair ?? 0 (ASTint I8 Unsigned)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I32 Signed)); (pair ?? 3 (ASTptr Any)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Signed)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTptr Any)); (pair ?? 9 (ASTint I32 Unsigned)); (pair ?? 10 (ASTptr Any)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Signed)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I8 Signed)); (pair ?? 15 (ASTint I8 Signed)); (pair ?? 16 (ASTint I8 Signed)); (pair ?? 17 (ASTptr Any)); (pair ?? 18 (ASTint I32 Unsigned)); (pair ?? 19 (ASTptr Any)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I8 Signed)); (pair ?? 22 (ASTptr Any)); (pair ?? 23 (ASTint I8 Signed)); (pair ?? 24 (ASTint I8 Signed)); (pair ?? 25 (ASTint I8 Signed)); (pair ?? 26 (ASTptr Any)); (pair ?? 27 (ASTint I32 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Signed)); (pair ?? 31 (ASTptr Any)); (pair ?? 32 (ASTint I8 Signed)); (pair ?? 33 (ASTint I8 Signed)); (pair ?? 34 (ASTint I8 Signed)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I32 Unsigned)); (pair ?? 37 (ASTptr Any)); (pair ?? 38 (ASTint I8 Unsigned)); (pair ?? 39 (ASTint I8 Signed)); (pair ?? 40 (ASTptr Any)); (pair ?? 41 (ASTint I8 Signed)); (pair ?? 42 (ASTint I8 Signed)); (pair ?? 43 (ASTint I8 Signed)); (pair ?? 44 (ASTptr Any)); (pair ?? 45 (ASTint I32 Unsigned)); (pair ?? 46 (ASTptr Any)); (pair ?? 47 (ASTint I8 Unsigned)); (pair ?? 48 (ASTint I8 Signed)); (pair ?? 49 (ASTptr Any)); (pair ?? 50 (ASTint I8 Signed)); (pair ?? 51 (ASTint I8 Signed)); (pair ?? 52 (ASTint I8 Signed)); (pair ?? 53 (ASTptr Any)); (pair ?? 54 (ASTint I32 Unsigned))]
     351    [(pair ?? 0 (ASTint I8 Unsigned)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I32 Signed)); (pair ?? 3 (ASTptr Any)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Signed)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTptr Any)); (pair ?? 9 (ASTint I32 Unsigned)); (pair ?? 10 (ASTptr Any)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Signed)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I32 Signed)); (pair ?? 16 (ASTint I32 Signed)); (pair ?? 17 (ASTptr Any)); (pair ?? 18 (ASTint I32 Unsigned)); (pair ?? 19 (ASTptr Any)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I8 Signed)); (pair ?? 22 (ASTptr Any)); (pair ?? 23 (ASTint I32 Signed)); (pair ?? 24 (ASTint I32 Signed)); (pair ?? 25 (ASTint I32 Signed)); (pair ?? 26 (ASTptr Any)); (pair ?? 27 (ASTint I32 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Signed)); (pair ?? 31 (ASTptr Any)); (pair ?? 32 (ASTint I32 Signed)); (pair ?? 33 (ASTint I32 Signed)); (pair ?? 34 (ASTint I32 Signed)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I32 Unsigned)); (pair ?? 37 (ASTptr Any)); (pair ?? 38 (ASTint I8 Unsigned)); (pair ?? 39 (ASTint I8 Signed)); (pair ?? 40 (ASTptr Any)); (pair ?? 41 (ASTint I32 Signed)); (pair ?? 42 (ASTint I32 Signed)); (pair ?? 43 (ASTint I32 Signed)); (pair ?? 44 (ASTptr Any)); (pair ?? 45 (ASTint I32 Unsigned)); (pair ?? 46 (ASTptr Any)); (pair ?? 47 (ASTint I8 Unsigned)); (pair ?? 48 (ASTint I8 Signed)); (pair ?? 49 (ASTptr Any)); (pair ?? 50 (ASTint I32 Signed)); (pair ?? 51 (ASTint I32 Signed)); (pair ?? 52 (ASTint I32 Signed)); (pair ?? 53 (ASTptr Any)); (pair ?? 54 (ASTint I32 Unsigned))]
    202352    5
    203353    [
    204     (pair ?? main9 (make_St_const 9 (Ointconst I32 (repr ? 0)) main8));
    205     (pair ?? main8 (make_St_op2 Oaddp 3 8 9 main7));
    206     (pair ?? main7 (make_St_const 7 (Ointconst I8 (repr ? 5)) main6));
    207     (pair ?? main61 (make_St_cost C_cost9 main60));
    208     (pair ?? main60 (make_St_const 53 (Oaddrstack 0) main59));
    209     (pair ?? main6 (make_St_op1 (Ocastint Signed I8) 4 7 main5));
    210     (pair ?? main59 (make_St_const 54 (Ointconst I32 (repr ? 0)) main58));
    211     (pair ?? main58 (make_St_op2 Oaddp 49 53 54 main57));
    212     (pair ?? main57 (make_St_const 51 (Ointconst I8 (repr ? 0)) main56));
    213     (pair ?? main56 (make_St_const 52 (Ointconst I8 (repr ? 1)) main55));
    214     (pair ?? main55 (make_St_op2 Omul 50 51 52 main54));
    215     (pair ?? main54 (make_St_op2 Oaddp 46 49 50 main53));
    216     (pair ?? main53 (make_St_const 48 (Ointconst I8 (repr ? 0)) main52));
    217     (pair ?? main52 (make_St_op1 (Ocastint Signed I8) 47 48 main51));
    218     (pair ?? main51 (make_St_store Mint8unsigned 46 47 main50));
    219     (pair ?? main50 (make_St_const 44 (Oaddrstack 0) main49));
    220     (pair ?? main5 (make_St_const 6 (Ointconst I8 (repr ? 57)) main4));
    221     (pair ?? main49 (make_St_const 45 (Ointconst I32 (repr ? 0)) main48));
    222     (pair ?? main48 (make_St_op2 Oaddp 40 44 45 main47));
    223     (pair ?? main47 (make_St_const 42 (Ointconst I8 (repr ? 1)) main46));
    224     (pair ?? main46 (make_St_const 43 (Ointconst I8 (repr ? 1)) main45));
    225     (pair ?? main45 (make_St_op2 Omul 41 42 43 main44));
    226     (pair ?? main44 (make_St_op2 Oaddp 37 40 41 main43));
    227     (pair ?? main43 (make_St_const 39 (Ointconst I8 (repr ? 18)) main42));
    228     (pair ?? main42 (make_St_op1 (Ocastint Signed I8) 38 39 main41));
    229     (pair ?? main41 (make_St_store Mint8unsigned 37 38 main40));
    230     (pair ?? main40 (make_St_const 35 (Oaddrstack 0) main39));
    231     (pair ?? main4 (make_St_op1 (Ocastint Signed I8) 5 6 main3));
    232     (pair ?? main39 (make_St_const 36 (Ointconst I32 (repr ? 0)) main38));
    233     (pair ?? main38 (make_St_op2 Oaddp 31 35 36 main37));
    234     (pair ?? main37 (make_St_const 33 (Ointconst I8 (repr ? 2)) main36));
    235     (pair ?? main36 (make_St_const 34 (Ointconst I8 (repr ? 1)) main35));
    236     (pair ?? main35 (make_St_op2 Omul 32 33 34 main34));
    237     (pair ?? main34 (make_St_op2 Oaddp 28 31 32 main33));
    238     (pair ?? main33 (make_St_const 30 (Ointconst I8 (repr ? 23)) main32));
    239     (pair ?? main32 (make_St_op1 (Ocastint Signed I8) 29 30 main31));
    240     (pair ?? main31 (make_St_store Mint8unsigned 28 29 main30));
    241     (pair ?? main30 (make_St_const 26 (Oaddrstack 0) main29));
    242     (pair ?? main3 (make_St_call_id id_search [3; 4; 5] (Some ? 1) main2));
    243     (pair ?? main29 (make_St_const 27 (Ointconst I32 (repr ? 0)) main28));
    244     (pair ?? main28 (make_St_op2 Oaddp 22 26 27 main27));
    245     (pair ?? main27 (make_St_const 24 (Ointconst I8 (repr ? 3)) main26));
    246     (pair ?? main26 (make_St_const 25 (Ointconst I8 (repr ? 1)) main25));
    247     (pair ?? main25 (make_St_op2 Omul 23 24 25 main24));
    248     (pair ?? main24 (make_St_op2 Oaddp 19 22 23 main23));
    249     (pair ?? main23 (make_St_const 21 (Ointconst I8 (repr ? 57)) main22));
    250     (pair ?? main22 (make_St_op1 (Ocastint Signed I8) 20 21 main21));
    251     (pair ?? main21 (make_St_store Mint8unsigned 19 20 main20));
    252     (pair ?? main20 (make_St_const 17 (Oaddrstack 0) main19));
    253     (pair ?? main2 (make_St_op1 Oid 0 1 main1));
    254     (pair ?? main19 (make_St_const 18 (Ointconst I32 (repr ? 0)) main18));
    255     (pair ?? main18 (make_St_op2 Oaddp 13 17 18 main17));
    256     (pair ?? main17 (make_St_const 15 (Ointconst I8 (repr ? 4)) main16));
    257     (pair ?? main16 (make_St_const 16 (Ointconst I8 (repr ? 1)) main15));
    258     (pair ?? main15 (make_St_op2 Omul 14 15 16 main14));
    259     (pair ?? main14 (make_St_op2 Oaddp 10 13 14 main13));
    260     (pair ?? main13 (make_St_const 12 (Ointconst I8 (repr ? 120)) main12));
    261     (pair ?? main12 (make_St_op1 (Ocastint Signed I8) 11 12 main11));
    262     (pair ?? main11 (make_St_store Mint8unsigned 10 11 main10));
    263     (pair ?? main10 (make_St_const 8 (Oaddrstack 0) main9));
    264     (pair ?? main1 (make_St_op1 (Ocastint Unsigned I32) 2 0 main0));
    265     (pair ?? main0 (make_St_return))
     354    (pair ?? lbl_main9 (make_St_const 9 (Ointconst I32 (repr ? 0)) lbl_main8));
     355    (pair ?? lbl_main8 (make_St_op2 Oaddp 3 8 9 lbl_main7));
     356    (pair ?? lbl_main7 (make_St_const 7 (Ointconst I8 (repr ? 5)) lbl_main6));
     357    (pair ?? lbl_main61 (make_St_cost C_cost17 lbl_main60));
     358    (pair ?? lbl_main60 (make_St_const 53 (Oaddrstack 0) lbl_main59));
     359    (pair ?? lbl_main6 (make_St_op1 (Ocastint Signed I8) 4 7 lbl_main5));
     360    (pair ?? lbl_main59 (make_St_const 54 (Ointconst I32 (repr ? 0)) lbl_main58));
     361    (pair ?? lbl_main58 (make_St_op2 Oaddp 49 53 54 lbl_main57));
     362    (pair ?? lbl_main57 (make_St_const 51 (Ointconst I32 (repr ? 0)) lbl_main56));
     363    (pair ?? lbl_main56 (make_St_const 52 (Ointconst I32 (repr ? 1)) lbl_main55));
     364    (pair ?? lbl_main55 (make_St_op2 Omul 50 51 52 lbl_main54));
     365    (pair ?? lbl_main54 (make_St_op2 Oaddp 46 49 50 lbl_main53));
     366    (pair ?? lbl_main53 (make_St_const 48 (Ointconst I8 (repr ? 0)) lbl_main52));
     367    (pair ?? lbl_main52 (make_St_op1 (Ocastint Signed I8) 47 48 lbl_main51));
     368    (pair ?? lbl_main51 (make_St_store Mint8unsigned 46 47 lbl_main50));
     369    (pair ?? lbl_main50 (make_St_const 44 (Oaddrstack 0) lbl_main49));
     370    (pair ?? lbl_main5 (make_St_const 6 (Ointconst I8 (repr ? 57)) lbl_main4));
     371    (pair ?? lbl_main49 (make_St_const 45 (Ointconst I32 (repr ? 0)) lbl_main48));
     372    (pair ?? lbl_main48 (make_St_op2 Oaddp 40 44 45 lbl_main47));
     373    (pair ?? lbl_main47 (make_St_const 42 (Ointconst I32 (repr ? 1)) lbl_main46));
     374    (pair ?? lbl_main46 (make_St_const 43 (Ointconst I32 (repr ? 1)) lbl_main45));
     375    (pair ?? lbl_main45 (make_St_op2 Omul 41 42 43 lbl_main44));
     376    (pair ?? lbl_main44 (make_St_op2 Oaddp 37 40 41 lbl_main43));
     377    (pair ?? lbl_main43 (make_St_const 39 (Ointconst I8 (repr ? 18)) lbl_main42));
     378    (pair ?? lbl_main42 (make_St_op1 (Ocastint Signed I8) 38 39 lbl_main41));
     379    (pair ?? lbl_main41 (make_St_store Mint8unsigned 37 38 lbl_main40));
     380    (pair ?? lbl_main40 (make_St_const 35 (Oaddrstack 0) lbl_main39));
     381    (pair ?? lbl_main4 (make_St_op1 (Ocastint Signed I8) 5 6 lbl_main3));
     382    (pair ?? lbl_main39 (make_St_const 36 (Ointconst I32 (repr ? 0)) lbl_main38));
     383    (pair ?? lbl_main38 (make_St_op2 Oaddp 31 35 36 lbl_main37));
     384    (pair ?? lbl_main37 (make_St_const 33 (Ointconst I32 (repr ? 2)) lbl_main36));
     385    (pair ?? lbl_main36 (make_St_const 34 (Ointconst I32 (repr ? 1)) lbl_main35));
     386    (pair ?? lbl_main35 (make_St_op2 Omul 32 33 34 lbl_main34));
     387    (pair ?? lbl_main34 (make_St_op2 Oaddp 28 31 32 lbl_main33));
     388    (pair ?? lbl_main33 (make_St_const 30 (Ointconst I8 (repr ? 23)) lbl_main32));
     389    (pair ?? lbl_main32 (make_St_op1 (Ocastint Signed I8) 29 30 lbl_main31));
     390    (pair ?? lbl_main31 (make_St_store Mint8unsigned 28 29 lbl_main30));
     391    (pair ?? lbl_main30 (make_St_const 26 (Oaddrstack 0) lbl_main29));
     392    (pair ?? lbl_main3 (make_St_call_id id_search [3; 4; 5] (Some ? 1) lbl_main2));
     393    (pair ?? lbl_main29 (make_St_const 27 (Ointconst I32 (repr ? 0)) lbl_main28));
     394    (pair ?? lbl_main28 (make_St_op2 Oaddp 22 26 27 lbl_main27));
     395    (pair ?? lbl_main27 (make_St_const 24 (Ointconst I32 (repr ? 3)) lbl_main26));
     396    (pair ?? lbl_main26 (make_St_const 25 (Ointconst I32 (repr ? 1)) lbl_main25));
     397    (pair ?? lbl_main25 (make_St_op2 Omul 23 24 25 lbl_main24));
     398    (pair ?? lbl_main24 (make_St_op2 Oaddp 19 22 23 lbl_main23));
     399    (pair ?? lbl_main23 (make_St_const 21 (Ointconst I8 (repr ? 57)) lbl_main22));
     400    (pair ?? lbl_main22 (make_St_op1 (Ocastint Signed I8) 20 21 lbl_main21));
     401    (pair ?? lbl_main21 (make_St_store Mint8unsigned 19 20 lbl_main20));
     402    (pair ?? lbl_main20 (make_St_const 17 (Oaddrstack 0) lbl_main19));
     403    (pair ?? lbl_main2 (make_St_op1 Oid 0 1 lbl_main1));
     404    (pair ?? lbl_main19 (make_St_const 18 (Ointconst I32 (repr ? 0)) lbl_main18));
     405    (pair ?? lbl_main18 (make_St_op2 Oaddp 13 17 18 lbl_main17));
     406    (pair ?? lbl_main17 (make_St_const 15 (Ointconst I32 (repr ? 4)) lbl_main16));
     407    (pair ?? lbl_main16 (make_St_const 16 (Ointconst I32 (repr ? 1)) lbl_main15));
     408    (pair ?? lbl_main15 (make_St_op2 Omul 14 15 16 lbl_main14));
     409    (pair ?? lbl_main14 (make_St_op2 Oaddp 10 13 14 lbl_main13));
     410    (pair ?? lbl_main13 (make_St_const 12 (Ointconst I8 (repr ? 120)) lbl_main12));
     411    (pair ?? lbl_main12 (make_St_op1 (Ocastint Signed I8) 11 12 lbl_main11));
     412    (pair ?? lbl_main11 (make_St_store Mint8unsigned 10 11 lbl_main10));
     413    (pair ?? lbl_main10 (make_St_const 8 (Oaddrstack 0) lbl_main9));
     414    (pair ?? lbl_main1 (make_St_op1 (Ocastint Unsigned I32) 2 0 lbl_main0));
     415    (pair ?? lbl_main0 (make_St_return))
    266416]
    267417
    268     main61
    269     main0.
     418    lbl_main61
     419    lbl_main0.
    270420
    271421
    … …  
    274424  do f_main \larr make_internal_function pre_main;
    275425  do f_search \larr make_internal_function pre_search;
     426  do f__div32s \larr make_internal_function pre__div32s;
     427  do f__div32u \larr make_internal_function pre__div32u;
    276428
    277429OK ? (mk_program ??
    278430(  (pair ?? id_main f_main)::
    279431  (pair ?? id_search f_search)::
     432  (pair ?? id__div32s f__div32s)::
     433  (pair ?? id__div32u f__div32u)::
    280434(nil ?))
    281435  id_main
    … …  
    287441   normalize  (* you can examine the result here *)
    288442   @refl qed.
    289 
Note: See TracChangeset for help on using the changeset viewer.