Ignore:
Timestamp:
Jan 4, 2012, 7:19:09 PM (8 years ago)
Author:
campbell
Message:

Update Cminor pretty printer and examples.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/cminorMatitaPrinter.ml

    r1226 r1633  
    1313  | Sig_offset -> "ASTint I32 Unsigned"
    1414  | Sig_ptr -> "ASTptr Any"
     15
     16let print_type_return = function
     17  | Type_ret t -> (print_type t)
     18  | Type_void -> "?" (* shouldn't happen *)
    1519
    1620let print_ret_type = function
     
    2832
    2933let print_var n (id, sz, init) =
    30   Printf.sprintf "(pair ?? (pair ?? id_%s Any) [%s])"
     34  Printf.sprintf "(mk_Prod ?? (mk_Prod ?? id_%s Any) [%s])"
    3135    id
    3236    (match init with
     
    6367        (Driver.CminorMemory.concrete_size sz)
    6468
     69(* Matita will figure out the missing information from the types produced
     70   by the caller *)
    6571let print_op1 = function
    66   | AST.Op_cast((_,sg),sz) -> Printf.sprintf "(Ocastint %s I%d)" (print_signedness sg) (8*sz)
    67   | AST.Op_negint -> "Onegint"
    68   | AST.Op_notbool -> "Onotbool"
    69   | AST.Op_notint -> "Onotint"
    70   | AST.Op_id -> "Oid"
    71   | AST.Op_ptrofint -> "(Optrofint Any)"
    72   | AST.Op_intofptr -> "(Ointofptr ?)"
     72  | AST.Op_cast _ -> "(Ocastint ????)"
     73  | AST.Op_negint -> "(Onegint ??)"
     74  | AST.Op_notbool -> "(Onotbool ??? I)"
     75  | AST.Op_notint -> "(Onotint ??)"
     76  | AST.Op_id -> "(Oid ?)"
     77  | AST.Op_ptrofint -> "(Optrofint ?? Any)"
     78  | AST.Op_intofptr -> "(Ointofptr ???)"
    7379
    7480let print_op2 ty = function
     
    104110  | Cminor.Exp_cost (lab, e) ->
    105111      Printf.sprintf "definition C%s := costlabel_of_nat %d.\n%s"
    106         lab (fresh ()) (define_expr_labels e)
     112        lab.CostLabel.name (fresh ()) (define_expr_labels e)
    107113  | _ -> ""
    108114
     
    142148        (print_expression p_id e3)
    143149  | Cminor.Exp_cost (lab, e) ->
    144       Printf.sprintf "Ecost (%s) C%s (%s)" (print_type ty) lab (print_expression p_id e)
     150      Printf.sprintf "Ecost (%s) C%s (%s)" (print_type ty) lab.CostLabel.name (print_expression p_id e)
    145151
    146152let print_arg p_id e =
    147   Printf.sprintf "dp ?? (%s) (%s)" (print_type (typeof e)) (print_expression p_id e)
     153  Printf.sprintf "mk_DPair ?? (%s) (%s)" (print_type (typeof e)) (print_expression p_id e)
    148154
    149155let rec print_args p_id =
     
    155161
    156162let print_local p_id (id,ty) =
    157   Printf.sprintf "pair ?? %s (%s)" (p_id id) (print_type ty)
     163  Printf.sprintf "mk_Prod ?? %s (%s)" (p_id id) (print_type ty)
    158164
    159165let print_locals p_id vars =
     
    163169let print_table n =
    164170  let f (case, exit) =
    165     Printf.sprintf "(pair ?? (repr ? %d) %d)" case exit
     171    Printf.sprintf "(mk_Prod ?? (repr ? %d) %d)" case exit
    166172  in
    167173  MiscPottier.string_of_list (";\n" ^ n_spaces n) f
     
    174180  | Cminor.St_seq (s1, s2) -> define_labels s1 ^ define_labels s2
    175181  | Cminor.St_ifthenelse (e, s1, s2) -> define_expr_labels e ^ define_labels s1 ^ define_labels s2
    176   | Cminor.St_loop s -> define_labels s
    177   | Cminor.St_block s -> define_labels s
    178182  | Cminor.St_switch (e, _, _) -> define_expr_labels e
    179183  | Cminor.St_return (Some e) -> define_expr_labels e
    180184  | Cminor.St_label (l, s) ->
    181       Printf.sprintf "definition L%s := ident_of_nat %d.\n%s"
     185      Printf.sprintf "definition L%s := label_of_nat %d.\n%s"
    182186        l (fresh ()) (define_labels s)
    183187  | Cminor.St_cost (l, s) ->
    184188      Printf.sprintf "definition C%s := costlabel_of_nat %d.\n%s"
    185         l (fresh ()) (define_labels s)
     189        l.CostLabel.name (fresh ()) (define_labels s)
     190  | Cminor.St_ind_0 (_, s) -> define_labels s
     191  | Cminor.St_ind_inc (_, s) -> define_labels s
    186192  | _ -> ""
    187193
     
    206212        (print_args p_id args)
    207213  | Cminor.St_call (Some id, Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f),_), args, sg) ->
    208       Printf.sprintf "%sSt_call (Some ? %s) (Cst ? (Oaddrsymbol id_%s 0)) [%s]\n"
     214      Printf.sprintf "%sSt_call (Some ? (mk_Prod ?? %s (%s))) (Cst ? (Oaddrsymbol id_%s 0)) [%s]\n"
    209215        (n_spaces n)
    210216        (p_id id)
     217        (print_type_return sg.AST.res)
    211218        f
    212219        (print_args p_id args)
     
    250257        (print_body p_id (n+2) s2)
    251258        (n_spaces n)
    252   | Cminor.St_loop s ->
    253       Printf.sprintf "%sSt_loop (\n%s%s)\n"
    254         (n_spaces n)
    255         (print_body p_id (n+2) s)
    256         (n_spaces n)
    257   | Cminor.St_block s ->
    258       Printf.sprintf "%sSt_block (\n%s%s)\n"
    259         (n_spaces n)
    260         (print_body p_id (n+2) s)
    261         (n_spaces n)
    262   | Cminor.St_exit i ->
    263       Printf.sprintf "%sSt_exit %d\n" (n_spaces n) i
    264   | Cminor.St_switch (e, tbl, dflt) ->
     259  | Cminor.St_switch (e, tbl, dflt) -> assert false
     260(*
    265261      let sz,sg = match typeof e with Sig_int (sz, sg) -> sz,sg in
    266262      Printf.sprintf "%sSt_switch I%d %s (%s) [\n%s%s] %d\n"
     
    270266        (n_spaces (n+2))
    271267        (print_table ( n+2) tbl)
    272         dflt
     268        dflt*)
    273269  | Cminor.St_return None -> Printf.sprintf "%sSt_return (None ?)\n" (n_spaces n)
    274270  | Cminor.St_return (Some e) ->
     
    284280  | Cminor.St_cost (lbl, s) ->
    285281      Printf.sprintf "%sSt_cost C%s (\n%s%s)\n"
    286         (n_spaces n) lbl (print_body p_id n s)
     282        (n_spaces n) lbl.CostLabel.name (print_body p_id n s)
    287283        (n_spaces n)
     284  | Cminor.St_ind_0 (_, s) -> print_body p_id n s
     285  | Cminor.St_ind_inc (_, s) -> print_body p_id n s
    288286
    289287let print_ids fname vs =
     
    296294  let fid = fresh () in
    297295  let p_id id = Printf.sprintf "id_%s_%s" f_name id in
    298   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"
     296  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) %s).\n\n"
    299297    f_name
    300298    fid
     
    305303    (print_locals p_id f_def.Cminor.f_params)
    306304    (print_locals p_id f_def.Cminor.f_vars)
     305    "(match daemon in False with [ ])"  (* ewww *)
    307306    (Driver.CminorMemory.concrete_size f_def.Cminor.f_stacksize)
    308307    (print_body p_id 2 f_def.Cminor.f_body)
     308    "(match daemon in False with [ ])"  (* ewww *)
    309309
    310310let print_sig s =
    311311  Printf.sprintf "mk_signature [%s] (%s)"
    312312    (MiscPottier.string_of_list "; " print_type s.AST.args)
    313     (match s.AST.res with AST.Type_ret t -> "Some ? " ^ print_type t
     313    (match s.AST.res with AST.Type_ret t -> "Some ? (" ^ print_type t ^ ")"
    314314                        | AST.Type_void  -> "None ?")
    315315
     
    334334let print_fun' n functs =
    335335  MiscPottier.string_of_list ";\n" (fun (f,def) ->
    336     Printf.sprintf "%s(pair ?? id_%s f_%s)"
     336    Printf.sprintf "%s(mk_Prod ?? id_%s f_%s)"
    337337      (n_spaces n)
    338338      f
     
    352352
    353353let print_program p =
    354   Printf.sprintf "include \"Cminor/semantics.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n%s\n\ndefinition myprog : Cminor_program :=\nmk_program ?? [%s] [\n%s\n]%s\n.\n"
     354  Printf.sprintf "include \"Cminor/semantics.ma\".\ninclude \"common/Animation.ma\".\n\ndefinition label_of_nat : nat -> identifier Label := identifier_of_nat ?.\n\n%s\n\n%s\n\ndefinition myprog : Cminor_program :=\nmk_program ?? [%s] [\n%s\n]%s\n.\n"
    355355    (define_var_ids p.Cminor.vars)
    356356    (print_functs p.Cminor.functs)
Note: See TracChangeset for help on using the changeset viewer.