Changeset 967 for src/RTLabs/test


Ignore:
Timestamp:
Jun 15, 2011, 4:15:57 PM (8 years ago)
Author:
campbell
Message:

Update RTLabs pretty printer and examples.

Location:
src/RTLabs/test
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/test/search.RTLabs.ma

    r898 r967  
    7474    0
    7575    [
    76     (pair ?? search9 (make_St_const 10 (Ointconst (repr 1)) search8));
     76    (pair ?? search9 (make_St_const 10 (Ointconst I8 (repr ? 1)) search8));
    7777    (pair ?? search8 (make_St_op2 Oadd 9 4 10 search7));
    78     (pair ?? search7 (make_St_op1 Ocast8unsigned 5 9 search5));
     78    (pair ?? search7 (make_St_op1 (Ocastint Unsigned I8) 5 9 search5));
    7979    (pair ?? search6 (make_St_cost C_cost1 search5));
    8080    (pair ?? search50 (make_St_cost C_cost8 search49));
    8181    (pair ?? search5 (make_St_skip search44));
    82     (pair ?? search49 (make_St_const 35 (Ointconst (repr 0)) search48));
    83     (pair ?? search48 (make_St_op1 Ocast8signed 5 35 search47));
    84     (pair ?? search47 (make_St_const 34 (Ointconst (repr 1)) search46));
     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));
    8585    (pair ?? search46 (make_St_op2 Osub 33 1 34 search45));
    86     (pair ?? search45 (make_St_op1 Ocast8unsigned 3 33 search5));
     86    (pair ?? search45 (make_St_op1 (Ocastint Unsigned I8) 3 33 search5));
    8787    (pair ?? search44 (make_St_op2 (Ocmpu Cge) 32 3 5 search43));
    8888    (pair ?? search43 (make_St_op1 Onotbool 31 32 search42));
     
    9191    (pair ?? search40 (make_St_op2 Oadd 29 3 5 search39));
    9292    (pair ?? search4 (make_St_cost C_cost7 search3));
    93     (pair ?? search39 (make_St_const 30 (Ointconst (repr 2)) search38));
     93    (pair ?? search39 (make_St_const 30 (Ointconst I8 (repr ? 2)) search38));
    9494    (pair ?? search38 (make_St_op2 Odivu 28 29 30 search37));
    95     (pair ?? search37 (make_St_op1 Ocast8unsigned 4 28 search36));
    96     (pair ?? search36 (make_St_const 27 (Ointconst (repr 1)) search35));
     95    (pair ?? search37 (make_St_op1 (Ocastint Unsigned I8) 4 28 search36));
     96    (pair ?? search36 (make_St_const 27 (Ointconst I8 (repr ? 1)) search35));
    9797    (pair ?? search35 (make_St_op2 Omul 26 4 27 search34));
    9898    (pair ?? search34 (make_St_op2 Oaddp 25 0 26 search33));
     
    101101    (pair ?? search31 (make_St_cond 23 search30 search28));
    102102    (pair ?? search30 (make_St_cost C_cost4 search29));
    103     (pair ?? search3 (make_St_const 8 (Ointconst (repr 1)) search2));
     103    (pair ?? search3 (make_St_const 8 (Ointconst I8 (repr ? 1)) search2));
    104104    (pair ?? search29 (make_St_op1 Oid 6 4 search0));
    105105    (pair ?? search28 (make_St_cost C_cost5 search27));
    106     (pair ?? search27 (make_St_const 22 (Ointconst (repr 1)) search26));
     106    (pair ?? search27 (make_St_const 22 (Ointconst I8 (repr ? 1)) search26));
    107107    (pair ?? search26 (make_St_op2 Omul 21 4 22 search25));
    108108    (pair ?? search25 (make_St_op2 Oaddp 20 0 21 search24));
     
    111111    (pair ?? search22 (make_St_cond 18 search21 search17));
    112112    (pair ?? search21 (make_St_cost C_cost2 search20));
    113     (pair ?? search20 (make_St_const 17 (Ointconst (repr 1)) search19));
     113    (pair ?? search20 (make_St_const 17 (Ointconst I8 (repr ? 1)) search19));
    114114    (pair ?? search2 (make_St_op1 Onegint 7 8 search1));
    115115    (pair ?? search19 (make_St_op2 Osub 16 4 17 search18));
    116     (pair ?? search18 (make_St_op1 Ocast8unsigned 3 16 search16));
     116    (pair ?? search18 (make_St_op1 (Ocastint Unsigned I8) 3 16 search16));
    117117    (pair ?? search17 (make_St_cost C_cost3 search16));
    118     (pair ?? search16 (make_St_const 15 (Ointconst (repr 1)) search15));
     118    (pair ?? search16 (make_St_const 15 (Ointconst I8 (repr ? 1)) search15));
    119119    (pair ?? search15 (make_St_op2 Omul 14 4 15 search14));
    120120    (pair ?? search14 (make_St_op2 Oaddp 13 0 14 search13));
     
    123123    (pair ?? search11 (make_St_cond 11 search10 search6));
    124124    (pair ?? search10 (make_St_cost C_cost0 search9));
    125     (pair ?? search1 (make_St_op1 Ocast8signed 6 7 search0));
     125    (pair ?? search1 (make_St_op1 (Ocastint Signed I8) 6 7 search0));
    126126    (pair ?? search0 (make_St_return))
    127127]
     
    200200    []
    201201    [(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))]
    202     8
     202    5
    203203    [
    204     (pair ?? main9 (make_St_const 9 (Ointconst (repr 0)) main8));
     204    (pair ?? main9 (make_St_const 9 (Ointconst I32 (repr ? 0)) main8));
    205205    (pair ?? main8 (make_St_op2 Oaddp 3 8 9 main7));
    206     (pair ?? main7 (make_St_const 7 (Ointconst (repr 5)) main6));
     206    (pair ?? main7 (make_St_const 7 (Ointconst I8 (repr ? 5)) main6));
    207207    (pair ?? main61 (make_St_cost C_cost9 main60));
    208     (pair ?? main60 (make_St_const 53 (Oaddrstack (repr 0)) main59));
    209     (pair ?? main6 (make_St_op1 Ocast8signed 4 7 main5));
    210     (pair ?? main59 (make_St_const 54 (Ointconst (repr 0)) main58));
     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));
    211211    (pair ?? main58 (make_St_op2 Oaddp 49 53 54 main57));
    212     (pair ?? main57 (make_St_const 51 (Ointconst (repr 0)) main56));
    213     (pair ?? main56 (make_St_const 52 (Ointconst (repr 1)) main55));
     212    (pair ?? main57 (make_St_const 51 (Ointconst I8 (repr ? 0)) main56));
     213    (pair ?? main56 (make_St_const 52 (Ointconst I8 (repr ? 1)) main55));
    214214    (pair ?? main55 (make_St_op2 Omul 50 51 52 main54));
    215215    (pair ?? main54 (make_St_op2 Oaddp 46 49 50 main53));
    216     (pair ?? main53 (make_St_const 48 (Ointconst (repr 0)) main52));
    217     (pair ?? main52 (make_St_op1 Ocast8signed 47 48 main51));
     216    (pair ?? main53 (make_St_const 48 (Ointconst I8 (repr ? 0)) main52));
     217    (pair ?? main52 (make_St_op1 (Ocastint Signed I8) 47 48 main51));
    218218    (pair ?? main51 (make_St_store Mint8unsigned 46 47 main50));
    219     (pair ?? main50 (make_St_const 44 (Oaddrstack (repr 0)) main49));
    220     (pair ?? main5 (make_St_const 6 (Ointconst (repr 57)) main4));
    221     (pair ?? main49 (make_St_const 45 (Ointconst (repr 0)) main48));
     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));
    222222    (pair ?? main48 (make_St_op2 Oaddp 40 44 45 main47));
    223     (pair ?? main47 (make_St_const 42 (Ointconst (repr 1)) main46));
    224     (pair ?? main46 (make_St_const 43 (Ointconst (repr 1)) main45));
     223    (pair ?? main47 (make_St_const 42 (Ointconst I8 (repr ? 1)) main46));
     224    (pair ?? main46 (make_St_const 43 (Ointconst I8 (repr ? 1)) main45));
    225225    (pair ?? main45 (make_St_op2 Omul 41 42 43 main44));
    226226    (pair ?? main44 (make_St_op2 Oaddp 37 40 41 main43));
    227     (pair ?? main43 (make_St_const 39 (Ointconst (repr 18)) main42));
    228     (pair ?? main42 (make_St_op1 Ocast8signed 38 39 main41));
     227    (pair ?? main43 (make_St_const 39 (Ointconst I8 (repr ? 18)) main42));
     228    (pair ?? main42 (make_St_op1 (Ocastint Signed I8) 38 39 main41));
    229229    (pair ?? main41 (make_St_store Mint8unsigned 37 38 main40));
    230     (pair ?? main40 (make_St_const 35 (Oaddrstack (repr 0)) main39));
    231     (pair ?? main4 (make_St_op1 Ocast8signed 5 6 main3));
    232     (pair ?? main39 (make_St_const 36 (Ointconst (repr 0)) main38));
     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));
    233233    (pair ?? main38 (make_St_op2 Oaddp 31 35 36 main37));
    234     (pair ?? main37 (make_St_const 33 (Ointconst (repr 2)) main36));
    235     (pair ?? main36 (make_St_const 34 (Ointconst (repr 1)) main35));
     234    (pair ?? main37 (make_St_const 33 (Ointconst I8 (repr ? 2)) main36));
     235    (pair ?? main36 (make_St_const 34 (Ointconst I8 (repr ? 1)) main35));
    236236    (pair ?? main35 (make_St_op2 Omul 32 33 34 main34));
    237237    (pair ?? main34 (make_St_op2 Oaddp 28 31 32 main33));
    238     (pair ?? main33 (make_St_const 30 (Ointconst (repr 23)) main32));
    239     (pair ?? main32 (make_St_op1 Ocast8signed 29 30 main31));
     238    (pair ?? main33 (make_St_const 30 (Ointconst I8 (repr ? 23)) main32));
     239    (pair ?? main32 (make_St_op1 (Ocastint Signed I8) 29 30 main31));
    240240    (pair ?? main31 (make_St_store Mint8unsigned 28 29 main30));
    241     (pair ?? main30 (make_St_const 26 (Oaddrstack (repr 0)) main29));
     241    (pair ?? main30 (make_St_const 26 (Oaddrstack 0) main29));
    242242    (pair ?? main3 (make_St_call_id id_search [3; 4; 5] (Some ? 1) main2));
    243     (pair ?? main29 (make_St_const 27 (Ointconst (repr 0)) main28));
     243    (pair ?? main29 (make_St_const 27 (Ointconst I32 (repr ? 0)) main28));
    244244    (pair ?? main28 (make_St_op2 Oaddp 22 26 27 main27));
    245     (pair ?? main27 (make_St_const 24 (Ointconst (repr 3)) main26));
    246     (pair ?? main26 (make_St_const 25 (Ointconst (repr 1)) main25));
     245    (pair ?? main27 (make_St_const 24 (Ointconst I8 (repr ? 3)) main26));
     246    (pair ?? main26 (make_St_const 25 (Ointconst I8 (repr ? 1)) main25));
    247247    (pair ?? main25 (make_St_op2 Omul 23 24 25 main24));
    248248    (pair ?? main24 (make_St_op2 Oaddp 19 22 23 main23));
    249     (pair ?? main23 (make_St_const 21 (Ointconst (repr 57)) main22));
    250     (pair ?? main22 (make_St_op1 Ocast8signed 20 21 main21));
     249    (pair ?? main23 (make_St_const 21 (Ointconst I8 (repr ? 57)) main22));
     250    (pair ?? main22 (make_St_op1 (Ocastint Signed I8) 20 21 main21));
    251251    (pair ?? main21 (make_St_store Mint8unsigned 19 20 main20));
    252     (pair ?? main20 (make_St_const 17 (Oaddrstack (repr 0)) main19));
     252    (pair ?? main20 (make_St_const 17 (Oaddrstack 0) main19));
    253253    (pair ?? main2 (make_St_op1 Oid 0 1 main1));
    254     (pair ?? main19 (make_St_const 18 (Ointconst (repr 0)) main18));
     254    (pair ?? main19 (make_St_const 18 (Ointconst I32 (repr ? 0)) main18));
    255255    (pair ?? main18 (make_St_op2 Oaddp 13 17 18 main17));
    256     (pair ?? main17 (make_St_const 15 (Ointconst (repr 4)) main16));
    257     (pair ?? main16 (make_St_const 16 (Ointconst (repr 1)) main15));
     256    (pair ?? main17 (make_St_const 15 (Ointconst I8 (repr ? 4)) main16));
     257    (pair ?? main16 (make_St_const 16 (Ointconst I8 (repr ? 1)) main15));
    258258    (pair ?? main15 (make_St_op2 Omul 14 15 16 main14));
    259259    (pair ?? main14 (make_St_op2 Oaddp 10 13 14 main13));
    260     (pair ?? main13 (make_St_const 12 (Ointconst (repr 120)) main12));
    261     (pair ?? main12 (make_St_op1 Ocast8signed 11 12 main11));
     260    (pair ?? main13 (make_St_const 12 (Ointconst I8 (repr ? 120)) main12));
     261    (pair ?? main12 (make_St_op1 (Ocastint Signed I8) 11 12 main11));
    262262    (pair ?? main11 (make_St_store Mint8unsigned 10 11 main10));
    263     (pair ?? main10 (make_St_const 8 (Oaddrstack (repr 0)) main9));
    264     (pair ?? main1 (make_St_op1 Ocast8unsigned 2 0 main0));
     263    (pair ?? main10 (make_St_const 8 (Oaddrstack 0) main9));
     264    (pair ?? main1 (make_St_op1 (Ocastint Unsigned I32) 2 0 main0));
    265265    (pair ?? main0 (make_St_return))
    266266]
     
    284284).
    285285
    286    example exec: finishes_with (repr 3) ? (do p ← prog; do r ← exec_up_to RTLabs_fullexec p 1000 [ ]; OK ? r).
     286   example exec: finishes_with (repr I32 3) ? (do p ← prog; do r ← exec_up_to RTLabs_fullexec p 1000 [ ]; OK ? r).
    287287   normalize  (* you can examine the result here *)
    288288   @refl qed.
  • src/RTLabs/test/sum.RTLabs.ma

    r898 r967  
    8181    (pair ?? main8 (make_St_load Mint8unsigned 6 5 main7));
    8282    (pair ?? main7 (make_St_op2 Oadd 4 1 5 main6));
    83     (pair ?? main6 (make_St_op1 Ocast8unsigned 1 4 main5));
    84     (pair ?? main59 (make_St_const 43 (Oaddrsymbol id_src (repr 0)) main58));
    85     (pair ?? main58 (make_St_const 45 (Ointconst (repr 0)) main57));
    86     (pair ?? main57 (make_St_const 46 (Ointconst (repr 0)) main56));
     83    (pair ?? main6 (make_St_op1 (Ocastint Unsigned I8) 1 4 main5));
     84    (pair ?? main59 (make_St_const 43 (Oaddrsymbol id_src 0) main58));
     85    (pair ?? main58 (make_St_const 45 (Ointconst I32 (repr ? 0)) main57));
     86    (pair ?? main57 (make_St_const 46 (Ointconst I32 (repr ? 0)) main56));
    8787    (pair ?? main56 (make_St_op2 Oadd 44 45 46 main55));
    8888    (pair ?? main55 (make_St_op2 Oaddp 41 43 44 main54));
    89     (pair ?? main54 (make_St_const 42 (Ointconst (repr 28)) main53));
     89    (pair ?? main54 (make_St_const 42 (Ointconst I8 (repr ? 28)) main53));
    9090    (pair ?? main53 (make_St_store Mint8unsigned 41 42 main52));
    91     (pair ?? main52 (make_St_const 37 (Oaddrsymbol id_src (repr 0)) main51));
    92     (pair ?? main51 (make_St_const 39 (Ointconst (repr 0)) main50));
    93     (pair ?? main50 (make_St_const 40 (Ointconst (repr 1)) main49));
    94     (pair ?? main5 (make_St_const 3 (Ointconst (repr 1)) main4));
     91    (pair ?? main52 (make_St_const 37 (Oaddrsymbol id_src 0) main51));
     92    (pair ?? main51 (make_St_const 39 (Ointconst I32 (repr ? 0)) main50));
     93    (pair ?? main50 (make_St_const 40 (Ointconst I32 (repr ? 1)) main49));
     94    (pair ?? main5 (make_St_const 3 (Ointconst I32 (repr ? 1)) main4));
    9595    (pair ?? main49 (make_St_op2 Oadd 38 39 40 main48));
    9696    (pair ?? main48 (make_St_op2 Oaddp 35 37 38 main47));
    97     (pair ?? main47 (make_St_const 36 (Ointconst (repr 17)) main46));
     97    (pair ?? main47 (make_St_const 36 (Ointconst I8 (repr ? 17)) main46));
    9898    (pair ?? main46 (make_St_store Mint8unsigned 35 36 main45));
    99     (pair ?? main45 (make_St_const 31 (Oaddrsymbol id_src (repr 0)) main44));
    100     (pair ?? main44 (make_St_const 33 (Ointconst (repr 0)) main43));
    101     (pair ?? main43 (make_St_const 34 (Ointconst (repr 2)) main42));
     99    (pair ?? main45 (make_St_const 31 (Oaddrsymbol id_src 0) main44));
     100    (pair ?? main44 (make_St_const 33 (Ointconst I32 (repr ? 0)) main43));
     101    (pair ?? main43 (make_St_const 34 (Ointconst I32 (repr ? 2)) main42));
    102102    (pair ?? main42 (make_St_op2 Oadd 32 33 34 main41));
    103103    (pair ?? main41 (make_St_op2 Oaddp 29 31 32 main40));
    104     (pair ?? main40 (make_St_const 30 (Ointconst (repr 17)) main39));
     104    (pair ?? main40 (make_St_const 30 (Ointconst I8 (repr ? 17)) main39));
    105105    (pair ?? main4 (make_St_op2 Oadd 0 0 3 main3));
    106106    (pair ?? main39 (make_St_store Mint8unsigned 29 30 main38));
    107     (pair ?? main38 (make_St_const 25 (Oaddrsymbol id_src (repr 0)) main37));
    108     (pair ?? main37 (make_St_const 27 (Ointconst (repr 0)) main36));
    109     (pair ?? main36 (make_St_const 28 (Ointconst (repr 3)) main35));
     107    (pair ?? main38 (make_St_const 25 (Oaddrsymbol id_src 0) main37));
     108    (pair ?? main37 (make_St_const 27 (Ointconst I32 (repr ? 0)) main36));
     109    (pair ?? main36 (make_St_const 28 (Ointconst I32 (repr ? 3)) main35));
    110110    (pair ?? main35 (make_St_op2 Oadd 26 27 28 main34));
    111111    (pair ?? main34 (make_St_op2 Oaddp 23 25 26 main33));
    112     (pair ?? main33 (make_St_const 24 (Ointconst (repr 8)) main32));
     112    (pair ?? main33 (make_St_const 24 (Ointconst I8 (repr ? 8)) main32));
    113113    (pair ?? main32 (make_St_store Mint8unsigned 23 24 main31));
    114     (pair ?? main31 (make_St_const 19 (Oaddrsymbol id_src (repr 0)) main30));
    115     (pair ?? main30 (make_St_const 21 (Ointconst (repr 0)) main29));
     114    (pair ?? main31 (make_St_const 19 (Oaddrsymbol id_src 0) main30));
     115    (pair ?? main30 (make_St_const 21 (Ointconst I32 (repr ? 0)) main29));
    116116    (pair ?? main3 (make_St_skip main19));
    117     (pair ?? main29 (make_St_const 22 (Ointconst (repr 4)) main28));
     117    (pair ?? main29 (make_St_const 22 (Ointconst I32 (repr ? 4)) main28));
    118118    (pair ?? main28 (make_St_op2 Oadd 20 21 22 main27));
    119119    (pair ?? main27 (make_St_op2 Oaddp 17 19 20 main26));
    120     (pair ?? main26 (make_St_const 18 (Ointconst (repr 4)) main25));
     120    (pair ?? main26 (make_St_const 18 (Ointconst I8 (repr ? 4)) main25));
    121121    (pair ?? main25 (make_St_store Mint8unsigned 17 18 main24));
    122122    (pair ?? main24 (make_St_cost C_cost2 main23));
    123     (pair ?? main23 (make_St_const 16 (Ointconst (repr 0)) main22));
    124     (pair ?? main22 (make_St_op1 Ocast8signed 1 16 main21));
    125     (pair ?? main21 (make_St_const 15 (Ointconst (repr 0)) main20));
    126     (pair ?? main20 (make_St_op1 Oid 0 15 main3));
     123    (pair ?? main23 (make_St_const 16 (Ointconst I8 (repr ? 0)) main22));
     124    (pair ?? main22 (make_St_op1 (Ocastint Signed I8) 1 16 main21));
     125    (pair ?? main21 (make_St_const 15 (Ointconst I8 (repr ? 0)) main20));
     126    (pair ?? main20 (make_St_op1 (Ocastint Signed I32) 0 15 main3));
    127127    (pair ?? main2 (make_St_cost C_cost1 main1));
    128     (pair ?? main19 (make_St_op1 Oid 12 0 main18));
    129     (pair ?? main18 (make_St_const 14 (Ointconst (repr 8)) main17));
    130     (pair ?? main17 (make_St_op1 Oid 13 14 main16));
     128    (pair ?? main19 (make_St_op1 (Ocastint Signed I32) 12 0 main18));
     129    (pair ?? main18 (make_St_const 14 (Ointconst I8 (repr ? 5)) main17));
     130    (pair ?? main17 (make_St_op1 (Ocastint Unsigned I32) 13 14 main16));
    131131    (pair ?? main16 (make_St_op2 (Ocmpu Clt) 11 12 13 main15));
    132132    (pair ?? main15 (make_St_op1 Onotbool 10 11 main14));
    133133    (pair ?? main14 (make_St_cond 10 main2 main13));
    134134    (pair ?? main13 (make_St_cost C_cost0 main12));
    135     (pair ?? main12 (make_St_const 7 (Oaddrsymbol id_src (repr 0)) main11));
    136     (pair ?? main11 (make_St_const 9 (Ointconst (repr 1)) main10));
     135    (pair ?? main12 (make_St_const 7 (Oaddrsymbol id_src 0) main11));
     136    (pair ?? main11 (make_St_const 9 (Ointconst I32 (repr ? 1)) main10));
    137137    (pair ?? main10 (make_St_op2 Omul 8 0 9 main9));
    138     (pair ?? main1 (make_St_op1 Oid 2 1 main0));
     138    (pair ?? main1 (make_St_op1 (Ocastint Unsigned I32) 2 1 main0));
    139139    (pair ?? main0 (make_St_return))
    140140]
     
    153153  id_main
    154154  (*globals:*)
    155   [pair ?? (pair ?? (pair ?? id_src [Init_space 8 ]) Any) it]
     155  [pair ?? (pair ?? (pair ?? id_src [Init_space 5 ]) Any) it]
    156156).
     157
     158example exec: finishes_with (repr I32 74) ? (do myprog ← prog; exec_up_to RTLabs_fullexec myprog 1000 [ ]).
     159normalize  (* you can examine the result here *)
     160@refl
     161qed.
     162
Note: See TracChangeset for help on using the changeset viewer.