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

Update pretty printers and examples.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsMatitaPrinter.ml

    r967 r1157  
    1616
    1717let print_global (x, size) =
    18   Printf.sprintf "pair ?? (pair ?? (pair ?? id_%s [Init_space %d ]) Any) it" x
     18  Printf.sprintf "pair ?? (pair ?? id_%s Any) %d" x
    1919    (Driver.RTLabsMemory.concrete_size size)
    2020
     
    2525    (MiscPottier.string_of_list (";\n"^n_spaces n) print_global globs)
    2626
     27let print_label l = "lbl_" ^ l
    2728
    2829let rec print_args args =
     
    130131let rec print_table = function
    131132  | [] -> ""
    132   | [lbl] -> lbl
    133   | lbl :: tbl -> lbl ^ "; " ^ (print_table tbl)
     133  | [lbl] -> print_label lbl
     134  | lbl :: tbl -> (print_label lbl) ^ "; " ^ (print_table tbl)
    134135
    135136
    136137let print_statement lookup_type = function
    137   | RTLabs.St_skip lbl -> "make_St_skip " ^ lbl
     138  | RTLabs.St_skip lbl -> "make_St_skip " ^ (print_label lbl)
    138139  | RTLabs.St_cost (cost_lbl, lbl) ->
    139       Printf.sprintf "make_St_cost C%s %s" cost_lbl lbl
     140      Printf.sprintf "make_St_cost C%s %s" cost_lbl (print_label lbl)
    140141  | RTLabs.St_cst (dests, cst, lbl) ->
    141142      Printf.sprintf "make_St_const %s (%s) %s"
    142143        (Register.print dests)
    143144        (print_constant (lookup_type dests) cst)
    144         lbl
     145        (print_label lbl)
    145146  | RTLabs.St_op1 (op1, dests, srcs, lbl) ->
    146147      Printf.sprintf "make_St_op1 %s %s %s %s"
     
    148149        (Register.print dests)
    149150        (Register.print srcs)
    150         lbl
     151        (print_label lbl)
    151152  | RTLabs.St_op2 (op2, dests, srcs1, srcs2, lbl) ->
    152153      Printf.sprintf "make_St_op2 %s %s %s %s %s"
     
    155156        (Register.print srcs1)
    156157        (Register.print srcs2)
    157         lbl
     158        (print_label lbl)
    158159  | RTLabs.St_load (chunk, addr, dests, lbl) ->
    159160      Printf.sprintf "make_St_load %s %s %s %s"
     
    161162        (Register.print addr)
    162163        (Register.print dests)
    163         lbl
     164        (print_label lbl)
    164165  | RTLabs.St_store (chunk, addr, srcs, lbl) ->
    165166      Printf.sprintf "make_St_store %s %s %s %s"
     
    167168        (Register.print addr)
    168169        (Register.print srcs)
    169         lbl
     170        (print_label lbl)
    170171  | RTLabs.St_call_id (f, args, res, sg, lbl) ->
    171172      Printf.sprintf "make_St_call_id id_%s %s (%s) %s"
     
    173174        (print_params args)
    174175        (match res with None -> "None ?" | Some res -> "Some ? " ^ Register.print res)
    175         lbl
     176        (print_label lbl)
    176177  | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
    177178      Printf.sprintf "make_St_call_ptr %s %s (%s) %s"
     
    179180        (print_params args)
    180181        (match res with None -> "None ?" | Some res -> "Some ? " ^ (Register.print res))
    181         lbl
     182        (print_label lbl)
    182183  | RTLabs.St_tailcall_id (f, args, sg) ->
    183184      Printf.sprintf "make_St_tailcall_id id_%s %s"
     
    191192      Printf.sprintf "make_St_cond %s %s %s"
    192193        (Register.print srcs)
    193         lbl_true
    194         lbl_false
     194        (print_label lbl_true)
     195        (print_label lbl_false)
    195196  | RTLabs.St_jumptable (rs, tbl) ->
    196197      Printf.sprintf "make_St_jumptable %s [%s]"
     
    218219    Printf.sprintf "%sdefinition %s := %d.\n%s"
    219220      (n_spaces n)
    220       lbl
     221      (print_label lbl)
    221222      i
    222223      s
     
    228229    Printf.sprintf "%s(pair ?? %s (%s))%s\n%s"
    229230      (n_spaces n)
    230       lbl
     231      (print_label lbl)
    231232      (print_statement lookup_type stmt)
    232233      (if s = "" then "\n]" else ";")
     
    259260    (print_graph (n+2) lookup_type def.RTLabs.f_graph)
    260261    (n_spaces (n+2))
    261     def.RTLabs.f_entry
    262     (n_spaces (n+2))
    263     def.RTLabs.f_exit
     262    (print_label def.RTLabs.f_entry)
     263    (n_spaces (n+2))
     264    (print_label def.RTLabs.f_exit)
    264265
    265266
Note: See TracChangeset for help on using the changeset viewer.