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

Update RTLabs pretty printer and examples.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.