Changeset 898 for src/Cminor


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

Update pretty printers and examples.

Location:
src/Cminor
Files:
2 added
3 deleted
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/cminorMatitaPrinter.ml

    r816 r898  
    44let fresh () = let i = !next_id in next_id := i+1; i
    55
     6let print_signedness = function
     7  | Signed -> "Signed"
     8  | Unsigned -> "Unsigned"
     9
    610let print_type = function
    7   | Sig_int -> "ASTint"
    8   | Sig_float -> "ASTfloat"
     11  | Sig_int (sz, sg) -> Printf.sprintf "ASTint I%d %s" (sz*8) (print_signedness sg)
     12  | Sig_float (sz, _) -> Printf.sprintf "ASTfloat F%d" (sz*8)
     13  | Sig_offset -> "ASTint I32 Unsigned"
    914  | Sig_ptr -> "ASTptr Any"
    1015
    1116let print_ret_type = function
    12   | Type_ret t -> print_type t
    13   | Type_void -> "void"
     17  | Type_ret t -> Printf.sprintf "Some ? (%s)" (print_type t)
     18  | Type_void -> "None ?"
    1419
    1520
    1621let print_data = function
    17   | Data_reserve n -> Printf.sprintf "Init_space %d" n
     22  (*| Data_reserve n -> Printf.sprintf "Init_space %d" n*)
    1823  | Data_int8 i -> Printf.sprintf "Init_int8 (repr %d)" i
    1924  | Data_int16 i -> Printf.sprintf "Init_int16 (repr %d)" i
     
    2227  | Data_float64 f -> Printf.sprintf "Init_float64 %f" f
    2328
    24 let print_var n (id, init) =
     29let print_var n (id, sz, init) =
    2530  Printf.sprintf "(pair ?? (pair ?? (pair ?? id_%s [%s]) Any) it)"
    2631    id
    27     (MiscPottier.string_of_list ";" print_data init)
     32    (match init with
     33     | None -> Printf.sprintf "Init_space %d" (Driver.CminorMemory.concrete_size sz)
     34     | Some init ->
     35         (MiscPottier.string_of_list ";" print_data init))
    2836
    2937let print_vars n = MiscPottier.string_of_list ";\n" (print_var n)
     
    4149  | AST.Cst_float f -> Printf.sprintf "Ofloatconst %f" f
    4250  | AST.Cst_addrsymbol id -> Printf.sprintf "Oaddrsymbol id_%s (repr 0)" id
    43   | AST.Cst_stackoffset off -> Printf.sprintf "Oaddrstack (repr %d)" off
     51  (*| AST.Cst_stackoffset off -> Printf.sprintf "Oaddrstack (repr %d)" off*)
     52  | AST.Cst_stack -> Printf.sprintf "Oaddrstack (repr 0)"
     53  | AST.Cst_offset off -> Printf.sprintf "Ointconst (repr %d)" (Driver.CminorMemory.concrete_offset off)
     54  | AST.Cst_sizeof sz -> Printf.sprintf "Ointconst (repr %d)" (Driver.CminorMemory.concrete_size sz)
    4455
    4556let print_op1 = function
    46   | AST.Op_cast8unsigned -> "Ocast8unsigned"
    47   | AST.Op_cast8signed -> "Ocast8signed"
    48   | AST.Op_cast16unsigned -> "Ocast16unsigned"
    49   | AST.Op_cast16signed -> "Ocast16signed"
     57  | AST.Op_cast((1,Unsigned),_) -> "Ocast8unsigned"
     58  | AST.Op_cast((1,Signed),_) -> "Ocast8signed"
     59  | AST.Op_cast((2,Unsigned),_) -> "Ocast16unsigned"
     60  | AST.Op_cast((2,Signed),_) -> "Ocast16signed"
     61  | AST.Op_cast((4,_),_) -> "Oid"
    5062  | AST.Op_negint -> "Onegint"
    5163  | AST.Op_notbool -> "Onotbool"
    5264  | AST.Op_notint -> "Onotint"
    53   | AST.Op_negf -> "Onegf"
    54   | AST.Op_absf -> "Oabsf"
    55   | AST.Op_singleoffloat -> "Osingleoffloat"
    56   | AST.Op_intoffloat -> "Ointoffloat"
    57   | AST.Op_intuoffloat -> "Ointuoffloat"
    58   | AST.Op_floatofint -> "Ofloatofint"
    59   | AST.Op_floatofintu -> "Ofloatofintu"
    6065  | AST.Op_id -> "Oid"
    61   | AST.Op_ptrofint -> "Optrofint"
     66  | AST.Op_ptrofint -> "(Optrofint Any)"
    6267  | AST.Op_intofptr -> "Ointofptr"
    6368
     
    7681  | AST.Op_shr -> "Oshr"
    7782  | AST.Op_shru -> "Oshru"
    78   | AST.Op_addf -> "Oaddf"
    79   | AST.Op_subf -> "Osubf"
    80   | AST.Op_mulf -> "Omulf"
    81   | AST.Op_divf -> "Odivf"
    8283  | AST.Op_cmp cmp -> "(Ocmp " ^ print_cmp cmp ^ ")"
    8384  | AST.Op_cmpu cmp -> "(Ocmpu " ^ (print_cmp cmp) ^ ")"
    84   | AST.Op_cmpf cmp -> "(Ocmpf " ^ (print_cmp cmp) ^ ")"
    8585  | AST.Op_addp -> "Oaddp"
    86   | AST.Op_subp -> "Osubpi" (* FIXME: there should be separate subpi and subpp ops*)
     86  | AST.Op_subp -> "Osubpi"
     87  | AST.Op_subpp -> "Osubpp"
    8788  | AST.Op_cmpp cmp -> "(Ocmpp " ^ (print_cmp cmp) ^ ")"
    8889
    8990let rec define_expr_labels = function
     91| Cminor.Expr (e,ty) -> match e with
    9092  | Cminor.Op1 (_, e) -> define_expr_labels e
    9193  | Cminor.Op2 (_, e1, e2) -> define_expr_labels e1 ^ define_expr_labels e2
     
    99101
    100102let print_quantity = function
    101   | Memory.QInt 1 -> "Mint8unsigned"
    102   | Memory.QInt 2 -> "Mint16unsigned"
    103   | Memory.QInt 4 -> "Mint32"
    104   | Memory.QPtr -> "Mpointer Any"
     103  | AST.QInt 1 -> "Mint8unsigned"
     104  | AST.QInt 2 -> "Mint16unsigned"
     105  | AST.QInt 4 -> "Mint32"
     106  | AST.QOffset -> "Mint32"
     107  | AST.QPtr -> "Mpointer Any"
     108
     109let typeof = function Cminor.Expr (_,ty) -> ty
    105110
    106111let rec print_expression p_id = function
    107   | Cminor.Id id -> "Id " ^ (p_id id)
    108   | Cminor.Cst cst -> Printf.sprintf "Cst (%s)" (print_constant cst)
     112| Cminor.Expr (e,ty) -> match e with
     113  | Cminor.Id id -> Printf.sprintf "Id (%s) %s" (print_type ty) (p_id id)
     114  | Cminor.Cst cst -> Printf.sprintf "Cst (%s) (%s)" (print_type ty) (print_constant cst)
    109115  | Cminor.Op1 (op1, e) ->
    110       Printf.sprintf "Op1 %s (%s)" (print_op1 op1) (print_expression p_id e)
     116      Printf.sprintf "Op1 (%s) (%s) %s (%s)"
     117        (print_type (typeof e)) (print_type ty)
     118        (print_op1 op1) (print_expression p_id e)
    111119  | Cminor.Op2 (op2, e1, e2) ->
    112       Printf.sprintf "Op2 %s (%s) (%s)"
     120      Printf.sprintf "Op2 (%s) (%s) (%s) %s (%s) (%s)"
     121        (print_type (typeof e1)) (print_type (typeof e2)) (print_type ty)
    113122        (print_op2 op2)
    114123        (print_expression p_id e1)
    115124        (print_expression p_id e2)
    116125  | Cminor.Mem (q, e) ->
    117       Printf.sprintf "Mem %s (%s)" (print_quantity q) (print_expression p_id e)
     126      Printf.sprintf "Mem (%s) Any %s (%s)"
     127        (print_type ty) (print_quantity q) (print_expression p_id e)
    118128  | Cminor.Cond (e1, e2, e3) ->
    119       Printf.sprintf "Cond (%s) (%s) (%s)"
     129      let sz,sg = match typeof e1 with Sig_int (sz, sg) -> sz,sg in
     130      Printf.sprintf "Cond I%d %s (%s) (%s) (%s) (%s)"
     131        (sz*8) (print_signedness sg)
     132        (print_type ty)
    120133        (print_expression p_id e1)
    121134        (print_expression p_id e2)
    122135        (print_expression p_id e3)
    123136  | Cminor.Exp_cost (lab, e) ->
    124       Printf.sprintf "Ecost C%s (%s)" lab (print_expression p_id e)
    125 
     137      Printf.sprintf "Ecost (%s) C%s (%s)" (print_type ty) lab (print_expression p_id e)
     138
     139let print_arg p_id e =
     140  Printf.sprintf "dp ?? (%s) (%s)" (print_type (typeof e)) (print_expression p_id e)
    126141
    127142let rec print_args p_id =
    128   MiscPottier.string_of_list "; " (print_expression p_id)
     143  MiscPottier.string_of_list "; " (print_arg p_id)
    129144
    130145
     
    132147
    133148
    134 let print_sig s =
    135   Printf.sprintf "mk_signature [%s] (%s)"
    136     (MiscPottier.string_of_list "; " print_type s.AST.args)
    137     (match s.AST.res with AST.Type_ret t -> "Some ? " ^ print_type t
    138                         | AST.Type_void  -> "None ?")
     149let print_local p_id (id,ty) =
     150  Printf.sprintf "pair ?? %s (%s)" (p_id id) (print_type ty)
    139151
    140152let print_locals p_id vars =
    141   (MiscPottier.string_of_list "; " p_id vars)
     153  (MiscPottier.string_of_list "; " (print_local p_id) vars)
    142154
    143155
     
    170182  | Cminor.St_skip -> Printf.sprintf "%sSt_skip" (n_spaces n)
    171183  | Cminor.St_assign (id, e) ->
    172       Printf.sprintf "%sSt_assign %s (%s)\n" (n_spaces n) (p_id id) (print_expression p_id e)
     184      Printf.sprintf "%sSt_assign (%s) %s (%s)\n"
     185        (n_spaces n) (print_type (typeof e))
     186        (p_id id) (print_expression p_id e)
    173187  | Cminor.St_store (q, e1, e2) ->
    174       Printf.sprintf "%sSt_store %s (%s) (%s)\n"
    175         (n_spaces n)
     188      Printf.sprintf "%sSt_store (%s) Any %s (%s) (%s)\n"
     189        (n_spaces n)
     190        (print_type (typeof e2))
    176191        (print_quantity q)
    177192        (print_expression p_id e1)
    178193        (print_expression p_id e2)
     194(* XXX cheat horribly *)
     195  | Cminor.St_call (None, Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f),_), args, sg) ->
     196      Printf.sprintf "%sSt_call (None ?) (Cst ? (Oaddrsymbol id_%s (repr 0))) [%s]\n"
     197        (n_spaces n)
     198        f
     199        (print_args p_id args)
     200  | Cminor.St_call (Some id, Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f),_), args, sg) ->
     201      Printf.sprintf "%sSt_call (Some ? %s) (Cst ? (Oaddrsymbol id_%s (repr 0))) [%s]\n"
     202        (n_spaces n)
     203        (p_id id)
     204        f
     205        (print_args p_id args)
     206  | Cminor.St_tailcall (Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f),_), args, sg) ->
     207      Printf.sprintf "%sSt_tailcall (Cst ? (Oaddrsymbol id_%s (repr 0))) [%s]\n"
     208        (n_spaces n)
     209        f
     210        (print_args p_id args)
     211(* XXX regular versions, but the region will be screwed up *)
    179212  | Cminor.St_call (None, f, args, sg) ->
    180213      Printf.sprintf "%sSt_call (None ?) (%s) [%s]\n"
     
    201234        (n_spaces n)
    202235  | Cminor.St_ifthenelse (e, s1, s2) ->
    203       Printf.sprintf "%sSt_ifthenelse (%s) (\n%s%s) (\n%s%s)\n"
    204         (n_spaces n)
     236      let sz,sg = match typeof e with Sig_int (sz, sg) -> sz,sg in
     237      Printf.sprintf "%sSt_ifthenelse I%d %s (%s) (\n%s%s) (\n%s%s)\n"
     238        (n_spaces n)
     239        (sz*8) (print_signedness sg)
    205240        (print_expression p_id e)
    206241        (print_body p_id (n+2) s1)
     
    221256      Printf.sprintf "%sSt_exit %d\n" (n_spaces n) i
    222257  | Cminor.St_switch (e, tbl, dflt) ->
    223       Printf.sprintf "%sSt_switch (%s) [\n%s%s] %d\n"
    224         (n_spaces n)
     258      let sz,sg = match typeof e with Sig_int (sz, sg) -> sz,sg in
     259      Printf.sprintf "%sSt_switch I%d %s (%s) [\n%s%s] %d\n"
     260        (n_spaces n)
     261        (sz*8) (print_signedness sg)
    225262        (print_expression p_id e)
    226263        (n_spaces (n+2))
     
    229266  | Cminor.St_return None -> Printf.sprintf "%sSt_return (None ?)\n" (n_spaces n)
    230267  | Cminor.St_return (Some e) ->
    231       Printf.sprintf "%sSt_return (Some ? (%s))\n" (n_spaces n) (print_expression p_id e)
     268      Printf.sprintf "%sSt_return (Some ? (%s))\n" (n_spaces n) (print_arg p_id e)
    232269  | Cminor.St_label (lbl, s) ->
    233270      Printf.sprintf "%sSt_label L%s (\n%s%s)\n"
     
    244281
    245282let print_ids fname vs =
    246   List.fold_left (fun s v ->
     283  List.fold_left (fun s (v,_) ->
    247284                  Printf.sprintf "%sdefinition id_%s_%s := ident_of_nat %d.\n"
    248285                                 s fname v (fresh ()))
     
    252289  let fid = fresh () in
    253290  let p_id id = Printf.sprintf "id_%s_%s" f_name id in
    254   Printf.sprintf "definition id_%s := ident_of_nat %d.\n%s%sdefinition f_%s := Internal ? (mk_internal_function\n  (%s)\n  [%s]\n  [%s]\n  [%s]\n  %d (\n%s\n)).\n\n"
     291  Printf.sprintf "definition id_%s := ident_of_nat %d.\n%s%sdefinition f_%s := Internal ? (mk_internal_function\n  (%s)\n  [%s]\n  [%s]\n  %d (\n%s\n)).\n\n"
    255292    f_name
    256293    fid
     
    258295    (define_labels f_def.Cminor.f_body)
    259296    f_name
    260     (print_sig f_def.Cminor.f_sig)
     297    (print_ret_type f_def.Cminor.f_return)
    261298    (print_locals p_id f_def.Cminor.f_params)
    262299    (print_locals p_id f_def.Cminor.f_vars)
    263     (print_locals p_id f_def.Cminor.f_ptrs)
    264     f_def.Cminor.f_stacksize
     300    (Driver.CminorMemory.concrete_size f_def.Cminor.f_stacksize)
    265301    (print_body p_id 2 f_def.Cminor.f_body)
     302
     303let print_sig s =
     304  Printf.sprintf "mk_signature [%s] (%s)"
     305    (MiscPottier.string_of_list "; " print_type s.AST.args)
     306    (match s.AST.res with AST.Type_ret t -> "Some ? " ^ print_type t
     307                        | AST.Type_void  -> "None ?")
     308
    266309
    267310
     
    295338    (match main with Some f -> "id_" ^ f | None -> "ident_of_nat 0 (* None! *)")
    296339
    297 let define_var_id (id,_) =
     340let define_var_id (id,_,_) =
    298341  Printf.sprintf "definition id_%s := ident_of_nat %d.\n" id (fresh ())
    299342
Note: See TracChangeset for help on using the changeset viewer.