Changeset 967 for src/RTLabs


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

Update RTLabs pretty printer and examples.

Location:
src/RTLabs
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsMatitaPrinter.ml

    r898 r967  
    7070  | AST.Cmp_le -> "Cle"
    7171
    72 let print_cst = function
    73   | AST.Cst_int i -> Printf.sprintf "Ointconst (repr %d)" i
     72let print_constant ty = function
     73  | AST.Cst_int i ->
     74      Printf.sprintf "Ointconst I%d (repr ? %d)"
     75        (match ty with AST.Sig_int (sz, _) -> 8*sz | _ -> 32)
     76        i
    7477  | AST.Cst_float f -> Printf.sprintf "Ofloatconst %f" f
    75   | AST.Cst_addrsymbol id -> Printf.sprintf "Oaddrsymbol id_%s (repr 0)" id
     78  | AST.Cst_addrsymbol id -> Printf.sprintf "Oaddrsymbol id_%s 0" id
    7679  (*| AST.Cst_stackoffset off -> Printf.sprintf "Oaddrstack (repr %d)" off*)
    77   | AST.Cst_stack -> Printf.sprintf "Oaddrstack (repr 0)"
    78   | AST.Cst_offset off -> Printf.sprintf "Ointconst (repr %d)" (Driver.CminorMemory.concrete_offset off)
    79   | AST.Cst_sizeof sz -> Printf.sprintf "Ointconst (repr %d)" (Driver.CminorMemory.concrete_size sz)
     80  | AST.Cst_stack -> Printf.sprintf "Oaddrstack 0"
     81  | AST.Cst_offset off ->
     82      Printf.sprintf "Ointconst I%d (repr ? %d)"
     83        (match ty with AST.Sig_int (sz, _) -> 8*sz | _ -> 32)
     84        (Driver.CminorMemory.concrete_offset off)
     85  | AST.Cst_sizeof sz ->
     86      Printf.sprintf "Ointconst I%d (repr ? %d)"
     87        (match ty with AST.Sig_int (sz, _) -> 8*sz | _ -> 32)
     88        (Driver.CminorMemory.concrete_size sz)
    8089
    8190let print_op1 = function
    82   | AST.Op_cast((_,AST.Unsigned),1) -> "Ocast8unsigned"
    83   | AST.Op_cast((_,AST.Signed),1) -> "Ocast8signed"
    84   | AST.Op_cast((_,AST.Unsigned),2) -> "Ocast16unsigned"
    85   | AST.Op_cast((_,AST.Signed),2) -> "Ocast16signed"
    86   | AST.Op_cast((_,AST.Unsigned),4) -> "Oid"
    87   | AST.Op_cast((_,AST.Signed),4) -> "Oid"
     91  | AST.Op_cast((_,sg),sz) -> Printf.sprintf "(Ocastint %s I%d)" (print_signedness sg) (8*sz)
    8892  | AST.Op_negint -> "Onegint"
    8993  | AST.Op_notbool -> "Onotbool"
     
    9397  | AST.Op_intofptr -> "Ointofptr"
    9498
    95 let print_op2 = function
     99let print_op2 ty = function
    96100  | AST.Op_add -> "Oadd"
    97101  | AST.Op_sub -> "Osub"
     
    111115  | AST.Op_addp -> "Oaddp"
    112116  | AST.Op_subp -> "Osubpi"
    113   | AST.Op_subpp -> "Osubpp"
     117  | AST.Op_subpp ->
     118      Printf.sprintf "(Osubpp I%d)"
     119        (match ty with AST.Sig_int (sz, _) -> 8*sz | _ -> 32)
    114120  | AST.Op_cmpp cmp -> "(Ocmpp " ^ (print_cmp cmp) ^ ")"
    115121
     
    128134
    129135
    130 let print_statement = function
     136let print_statement lookup_type = function
    131137  | RTLabs.St_skip lbl -> "make_St_skip " ^ lbl
    132138  | RTLabs.St_cost (cost_lbl, lbl) ->
     
    135141      Printf.sprintf "make_St_const %s (%s) %s"
    136142        (Register.print dests)
    137         (print_cst cst)
     143        (print_constant (lookup_type dests) cst)
    138144        lbl
    139145  | RTLabs.St_op1 (op1, dests, srcs, lbl) ->
     
    145151  | RTLabs.St_op2 (op2, dests, srcs1, srcs2, lbl) ->
    146152      Printf.sprintf "make_St_op2 %s %s %s %s %s"
    147         (print_op2 op2)
     153        (print_op2 (lookup_type dests) op2)
    148154        (Register.print dests)
    149155        (Register.print srcs1)
     
    218224  snd (Label.Map.fold f c (0,""))
    219225
    220 let print_graph n c =
     226let print_graph n lookup_type c =
    221227  let f lbl stmt s =
    222228    Printf.sprintf "%s(pair ?? %s (%s))%s\n%s"
    223229      (n_spaces n)
    224230      lbl
    225       (print_statement stmt)
     231      (print_statement lookup_type stmt)
    226232      (if s = "" then "\n]" else ";")
    227233      s in
     
    229235
    230236let print_internal_decl n f def =
     237  let env = def.RTLabs.f_params @ def.RTLabs.f_locals in
     238  let lookup_type r =
     239    let _,ty = List.find (fun (r',_) -> r = r') env in ty
     240  in
    231241  Printf.sprintf
    232242    "%sdefinition id_%s := ident_of_nat %d.\n%s%s\n\n%sdefinition pre_%s := mk_pre_internal_function\n%s%s\n%s%s\n%s%s\n%s%d\n%s%s\n%s%s\n%s%s."
     
    247257    (Driver.RTLabsMemory.concrete_size def.RTLabs.f_stacksize)
    248258    (n_spaces (n+2))
    249     (print_graph (n+2) def.RTLabs.f_graph)
     259    (print_graph (n+2) lookup_type def.RTLabs.f_graph)
    250260    (n_spaces (n+2))
    251261    def.RTLabs.f_entry
  • 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.