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/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
Note: See TracChangeset for help on using the changeset viewer.