Ignore:
Timestamp:
Apr 12, 2011, 12:32:33 PM (9 years ago)
Author:
campbell
Message:

Track some of the changes to the prototype in RTLabs.

Just one register in each place now, f_ptrs is present but not checked.
The changes to memory quantities have been glossed over for now.
A new difference from the prototype: return registers are optional.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsMatitaPrinter.ml

    r737 r750  
    1313
    1414
    15 let print_reg_list rl =
    16   Printf.sprintf "(dp ?? %d [[%s]])" (List.length rl) (MiscPottier.string_of_list " ; " Register.print rl)
    17 
    1815let rec print_args args =
    19   Printf.sprintf "[[%s]]" (MiscPottier.string_of_list "; " print_reg_list args)
    20 
    21 let print_result rl = print_reg_list rl
     16  Printf.sprintf "[[%s]]" (MiscPottier.string_of_list "; " Register.print args)
     17
     18let print_result rl = Register.print rl
    2219
    2320let print_params rl =
    24   Printf.sprintf "[%s]" (MiscPottier.string_of_list "; " print_reg_list rl)
     21  Printf.sprintf "[%s]" (MiscPottier.string_of_list "; " Register.print rl)
    2522
    2623let print_locals rl =
    27   Printf.sprintf "[%s]" (MiscPottier.string_of_list "; " print_reg_list rl)
    28 
    29 
     24  Printf.sprintf "[%s]" (MiscPottier.string_of_list "; " Register.print rl)
     25
     26let print_quantity = function
     27  | Memory.QInt 1 -> "Mint8unsigned"
     28  | Memory.QInt 2 -> "Mint16unsigned"
     29  | Memory.QInt 4 -> "Mint32"
     30  | Memory.QPtr -> "Mpointer Any"
     31(*
    3032let print_memory_q = function
    3133  | Memory.MQ_int8signed    -> "Mint8signed"
     
    3840  | Memory.MQ_pointer       -> "Mpointer Any"
    3941  | Memory.MQ_chunk         -> "MXXX"
    40 
     42*)
    4143
    4244
     
    131133  | RTLabs.St_cst (dests, cst, lbl) ->
    132134      Printf.sprintf "make_St_const %s (%s) %s"
    133         (print_reg_list dests)
     135        (Register.print dests)
    134136        (print_cst cst)
    135137        lbl
     
    137139      Printf.sprintf "make_St_op1 %s %s %s %s"
    138140        (print_op1 op1)
    139         (print_reg_list dests)
    140         (print_reg_list srcs)
     141        (Register.print dests)
     142        (Register.print srcs)
    141143        lbl
    142144  | RTLabs.St_op2 (op2, dests, srcs1, srcs2, lbl) ->
    143145      Printf.sprintf "make_St_op2 %s %s %s %s %s"
    144146        (print_op2 op2)
    145         (print_reg_list dests)
    146         (print_reg_list srcs1)
    147         (print_reg_list srcs2)
     147        (Register.print dests)
     148        (Register.print srcs1)
     149        (Register.print srcs2)
    148150        lbl
    149151  | RTLabs.St_load (chunk, mode, args, dests, lbl) ->
    150152      Printf.sprintf "make_St_load %s (%s) %s %s %s"
    151         (print_memory_q chunk)
     153        (print_quantity chunk)
    152154        (print_addressing mode)
    153155        (print_args args)
    154         (print_reg_list dests)
     156        (Register.print dests)
    155157        lbl
    156158  | RTLabs.St_store (chunk, mode, args, srcs, lbl) ->
    157159      Printf.sprintf "make_St_store %s (%s) %s %s %s"
    158         (print_memory_q chunk)
     160        (print_quantity chunk)
    159161        (print_addressing mode)
    160162        (print_args args)
    161         (print_reg_list srcs)
     163        (Register.print srcs)
    162164        lbl
    163165  | RTLabs.St_call_id (f, args, res, sg, lbl) ->
    164       Printf.sprintf "make_St_call_id id_%s %s %s (%s) %s"
     166      Printf.sprintf "make_St_call_id id_%s %s (Some ? %s) (%s) %s"
    165167        f
    166168        (print_params args)
    167         (print_reg_list res)
     169        (Register.print res)
    168170        (print_sig sg)
    169171        lbl
    170172  | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
    171       Printf.sprintf "make_St_call_ptr %s %s %s (%s) %s"
    172         (print_reg_list f)
     173      Printf.sprintf "make_St_call_ptr %s %s (Some ? %s) (%s) %s"
     174        (Register.print f)
    173175        (print_params args)
    174         (print_reg_list res)
     176        (Register.print res)
    175177        (print_sig sg)
    176178        lbl
     
    182184  | RTLabs.St_tailcall_ptr (f, args, sg) ->
    183185      Printf.sprintf "make_St_tailcall_ptr %s %s (%s)"
    184         (print_reg_list f)
     186        (Register.print f)
    185187        (print_params args)
    186188        (print_sig sg)
     
    193195      Printf.sprintf "make_St_cond1 %s %s %s %s"
    194196        (print_op1 op1)
    195         (print_reg_list srcs)
     197        (Register.print srcs)
    196198        lbl_true
    197199        lbl_false
     
    199201      Printf.sprintf "make_St_cond2 %s %s %s %s %s"
    200202        (print_op2 op2)
    201         (print_reg_list srcs1)
    202         (print_reg_list srcs2)
     203        (Register.print srcs1)
     204        (Register.print srcs2)
    203205        lbl_true
    204206        lbl_false
    205207  | RTLabs.St_jumptable (rs, tbl) ->
    206208      Printf.sprintf "make_St_jumptable %s [%s]"
    207         (print_reg_list rs)
     209        (Register.print rs)
    208210        (print_table tbl)
    209   | RTLabs.St_return rs -> Printf.sprintf "make_St_return %s" (print_reg_list rs)
     211  | RTLabs.St_return rs -> Printf.sprintf "make_St_return %s" (Register.print rs)
    210212
    211213let print_cost_labels n c =
     
    246248let print_internal_decl n f def m =
    247249  Printf.sprintf
    248     "%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%s\n%s%d\n%s%s\n%s%s\n%s%s."
     250    "%sdefinition id_%s := ident_of_nat %d.\n%s%s\n\n%sdefinition pre_%s := mk_pre_internal_function\n%s(%s)\n%s(Some ? %s)\n%s%s\n%s%s\n%s%s\n%s%d\n%s%s\n%s%s\n%s%s."
    249251    (n_spaces n)
    250252    f
     
    262264    (n_spaces (n+2))
    263265    (print_locals def.RTLabs.f_locals)
     266    (n_spaces (n+2))
     267    (print_locals def.RTLabs.f_ptrs)
    264268    (n_spaces (n+2))
    265269    def.RTLabs.f_stacksize
Note: See TracChangeset for help on using the changeset viewer.