Ignore:
Timestamp:
Jun 8, 2011, 1:14:55 PM (9 years ago)
Author:
campbell
Message:

Update pretty printers and examples.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsMatitaPrinter.ml

    r816 r898  
    55let n_spaces n = String.make n ' '
    66
     7let print_signedness = function
     8  | AST.Signed -> "Signed"
     9  | AST.Unsigned -> "Unsigned"
     10
     11let print_sig_type = function
     12  | AST.Sig_int (sz, sg) -> Printf.sprintf "ASTint I%d %s" (sz*8) (print_signedness sg)
     13  | AST.Sig_float (sz, _) -> Printf.sprintf "ASTfloat F%d" (sz*8)
     14  | AST.Sig_offset -> "ASTint I32 Unsigned"
     15  | AST.Sig_ptr -> "ASTptr Any"
    716
    817let print_global (x, size) =
    9   Printf.sprintf "pair ?? (pair ?? (pair ?? id_%s [Init_space %d ]) Any) it" x size
     18  Printf.sprintf "pair ?? (pair ?? (pair ?? id_%s [Init_space %d ]) Any) it" x
     19    (Driver.RTLabsMemory.concrete_size size)
    1020
    1121let print_globals n globs =
     
    1929  Printf.sprintf "[[%s]]" (MiscPottier.string_of_list "; " Register.print args)
    2030
    21 let print_result rl = Register.print rl
     31let print_regty (r,ty) =
     32  Printf.sprintf "(pair ?? %s (%s))" (Register.print r) (print_sig_type ty)
     33
     34let print_result = function
     35| None -> "(None ?)"
     36| Some rty -> "(Some ? " ^ print_regty rty ^ ")"
    2237
    2338let print_params rl =
     
    2540
    2641let print_locals rl =
    27   Printf.sprintf "[%s]" (MiscPottier.string_of_list "; " Register.print rl)
     42  Printf.sprintf "[%s]" (MiscPottier.string_of_list "; " print_regty rl)
    2843
    2944let print_quantity = function
    30   | Memory.QInt 1 -> "Mint8unsigned"
    31   | Memory.QInt 2 -> "Mint16unsigned"
    32   | Memory.QInt 4 -> "Mint32"
    33   | Memory.QPtr -> "Mpointer Any"
     45  | AST.QInt 1 -> "Mint8unsigned"
     46  | AST.QInt 2 -> "Mint16unsigned"
     47  | AST.QInt 4 -> "Mint32"
     48  | AST.QOffset -> "Mint32"
     49  | AST.QPtr -> "Mpointer Any"
    3450(*
    3551let print_memory_q = function
     
    5874  | AST.Cst_float f -> Printf.sprintf "Ofloatconst %f" f
    5975  | AST.Cst_addrsymbol id -> Printf.sprintf "Oaddrsymbol id_%s (repr 0)" id
    60   | AST.Cst_stackoffset off -> Printf.sprintf "Oaddrstack (repr %d)" off
     76  (*| 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)
    6180
    6281let print_op1 = function
    63   | AST.Op_cast8unsigned -> "Ocast8unsigned"
    64   | AST.Op_cast8signed -> "Ocast8signed"
    65   | AST.Op_cast16unsigned -> "Ocast16unsigned"
    66   | AST.Op_cast16signed -> "Ocast16signed"
     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"
    6788  | AST.Op_negint -> "Onegint"
    6889  | AST.Op_notbool -> "Onotbool"
    6990  | AST.Op_notint -> "Onotint"
    70   | AST.Op_negf -> "Onegf"
    71   | AST.Op_absf -> "Oabsf"
    72   | AST.Op_singleoffloat -> "Osingleoffloat"
    73   | AST.Op_intoffloat -> "Ointoffloat"
    74   | AST.Op_intuoffloat -> "Ointuoffloat"
    75   | AST.Op_floatofint -> "Ofloatofint"
    76   | AST.Op_floatofintu -> "Ofloatofintu"
    7791  | AST.Op_id -> "Oid"
    7892  | AST.Op_ptrofint -> "Optrofint"
     
    93107  | AST.Op_shr -> "Oshr"
    94108  | AST.Op_shru -> "Oshru"
    95   | AST.Op_addf -> "Oaddf"
    96   | AST.Op_subf -> "Osubf"
    97   | AST.Op_mulf -> "Omulf"
    98   | AST.Op_divf -> "Odivf"
    99109  | AST.Op_cmp cmp -> "(Ocmp " ^ print_cmp cmp ^ ")"
    100110  | AST.Op_cmpu cmp -> "(Ocmpu " ^ (print_cmp cmp) ^ ")"
    101   | AST.Op_cmpf cmp -> "(Ocmpf " ^ (print_cmp cmp) ^ ")"
    102111  | AST.Op_addp -> "Oaddp"
    103   | AST.Op_subp -> "Osubp"
    104   | AST.Op_cmpp cmp -> (print_cmp cmp) ^ "Ocmpp"
    105 
    106 
    107 let print_addressing = function
    108   | RTLabs.Aindexed off -> Printf.sprintf "Aindexed (repr %d)" off
    109   | RTLabs.Aindexed2 -> "Aindexed2"
    110   | RTLabs.Aglobal (id, off) -> Printf.sprintf "Aglobal id_%s (repr %d)" id off
    111   | RTLabs.Abased (id, off) -> Printf.sprintf "Abased id_%s (repr %d)" id off
    112   | RTLabs.Ainstack off -> Printf.sprintf "Ainstack (repr %d)" off
    113 
    114 
    115 let print_sig_type = function
    116 | AST.Sig_int -> "ASTint"
    117 | AST.Sig_float -> "ASTfloat"
    118 | AST.Sig_ptr -> "ASTptr Any"
     112  | AST.Op_subp -> "Osubpi"
     113  | AST.Op_subpp -> "Osubpp"
     114  | AST.Op_cmpp cmp -> "(Ocmpp " ^ (print_cmp cmp) ^ ")"
     115
     116
    119117
    120118let print_sig s =
     
    152150        (Register.print srcs2)
    153151        lbl
    154   | RTLabs.St_load (chunk, mode, args, dests, lbl) ->
    155       Printf.sprintf "make_St_load %s (%s) %s %s %s"
     152  | RTLabs.St_load (chunk, addr, dests, lbl) ->
     153      Printf.sprintf "make_St_load %s %s %s %s"
    156154        (print_quantity chunk)
    157         (print_addressing mode)
    158         (print_args args)
     155        (Register.print addr)
    159156        (Register.print dests)
    160157        lbl
    161   | RTLabs.St_store (chunk, mode, args, srcs, lbl) ->
    162       Printf.sprintf "make_St_store %s (%s) %s %s %s"
     158  | RTLabs.St_store (chunk, addr, srcs, lbl) ->
     159      Printf.sprintf "make_St_store %s %s %s %s"
    163160        (print_quantity chunk)
    164         (print_addressing mode)
    165         (print_args args)
     161        (Register.print addr)
    166162        (Register.print srcs)
    167163        lbl
    168164  | RTLabs.St_call_id (f, args, res, sg, lbl) ->
    169       Printf.sprintf "make_St_call_id id_%s %s (Some ? %s) %s"
     165      Printf.sprintf "make_St_call_id id_%s %s (%s) %s"
    170166        f
    171167        (print_params args)
    172         (Register.print res)
     168        (match res with None -> "None ?" | Some res -> "Some ? " ^ Register.print res)
    173169        lbl
    174170  | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
    175       Printf.sprintf "make_St_call_ptr %s %s (Some ? %s) %s"
     171      Printf.sprintf "make_St_call_ptr %s %s (%s) %s"
    176172        (Register.print f)
    177173        (print_params args)
    178         (Register.print res)
     174        (match res with None -> "None ?" | Some res -> "Some ? " ^ (Register.print res))
    179175        lbl
    180176  | RTLabs.St_tailcall_id (f, args, sg) ->
     
    186182        (Register.print f)
    187183        (print_params args)
    188   | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
    189       Printf.sprintf "make_St_condcst (%s) %s %s"
    190         (print_cst cst)
    191         lbl_true
    192         lbl_false
    193   | RTLabs.St_cond1 (op1, srcs, lbl_true, lbl_false) ->
    194       Printf.sprintf "make_St_cond1 %s %s %s %s"
    195         (print_op1 op1)
     184  | RTLabs.St_cond (srcs, lbl_true, lbl_false) ->
     185      Printf.sprintf "make_St_cond %s %s %s"
    196186        (Register.print srcs)
    197         lbl_true
    198         lbl_false
    199   | RTLabs.St_cond2 (op2, srcs1, srcs2, lbl_true, lbl_false) ->
    200       Printf.sprintf "make_St_cond2 %s %s %s %s %s"
    201         (print_op2 op2)
    202         (Register.print srcs1)
    203         (Register.print srcs2)
    204187        lbl_true
    205188        lbl_false
     
    247230let print_internal_decl n f def =
    248231  Printf.sprintf
    249     "%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."
     232    "%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."
    250233    (n_spaces n)
    251234    f
     
    256239    f
    257240    (n_spaces (n+2))
    258     (print_sig def.RTLabs.f_sig)
    259     (n_spaces (n+2))
    260241    (print_result def.RTLabs.f_result)
    261242    (n_spaces (n+2))
    262     (print_params def.RTLabs.f_params)
     243    (print_locals def.RTLabs.f_params)
    263244    (n_spaces (n+2))
    264245    (print_locals def.RTLabs.f_locals)
    265246    (n_spaces (n+2))
    266     (print_locals def.RTLabs.f_ptrs)
    267     (n_spaces (n+2))
    268     def.RTLabs.f_stacksize
     247    (Driver.RTLabsMemory.concrete_size def.RTLabs.f_stacksize)
    269248    (n_spaces (n+2))
    270249    (print_graph (n+2) def.RTLabs.f_graph)
Note: See TracChangeset for help on using the changeset viewer.