source: src/Cminor/cminorMatitaPrinter.ml @ 2260

Last change on this file since 2260 was 1633, checked in by campbell, 9 years ago

Update Cminor pretty printer and examples.

File size: 12.6 KB
RevLine 
[751]1open AST
2
3let next_id = ref 0
4let fresh () = let i = !next_id in next_id := i+1; i
5
[898]6let print_signedness = function
7  | Signed -> "Signed"
8  | Unsigned -> "Unsigned"
9
[751]10let print_type = function
[898]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"
[751]14  | Sig_ptr -> "ASTptr Any"
15
[1633]16let print_type_return = function
17  | Type_ret t -> (print_type t)
18  | Type_void -> "?" (* shouldn't happen *)
19
[751]20let print_ret_type = function
[898]21  | Type_ret t -> Printf.sprintf "Some ? (%s)" (print_type t)
22  | Type_void -> "None ?"
[751]23
24
25let print_data = function
[898]26  (*| Data_reserve n -> Printf.sprintf "Init_space %d" n*)
[966]27  | Data_int8 i -> Printf.sprintf "Init_int8 (repr I8 %d)" i
28  | Data_int16 i -> Printf.sprintf "Init_int16 (repr I16 %d)" i
29  | Data_int32 i -> Printf.sprintf "Init_int32 (repr I32 %d)" i
[751]30  | Data_float32 f -> Printf.sprintf "Init_float32 %f" f
31  | Data_float64 f -> Printf.sprintf "Init_float64 %f" f
32
[898]33let print_var n (id, sz, init) =
[1633]34  Printf.sprintf "(mk_Prod ?? (mk_Prod ?? id_%s Any) [%s])"
[751]35    id
[898]36    (match init with
37     | None -> Printf.sprintf "Init_space %d" (Driver.CminorMemory.concrete_size sz)
38     | Some init ->
39         (MiscPottier.string_of_list ";" print_data init))
[751]40
41let print_vars n = MiscPottier.string_of_list ";\n" (print_var n) 
42
43let print_cmp = function
44  | AST.Cmp_eq -> "Ceq"
45  | AST.Cmp_ne -> "Cne"
46  | AST.Cmp_gt -> "Cgt"
47  | AST.Cmp_ge -> "Cge"
48  | AST.Cmp_lt -> "Clt"
49  | AST.Cmp_le -> "Cle"
50
[966]51let print_constant ty = function
52  | AST.Cst_int i ->
53      Printf.sprintf "Ointconst I%d (repr ? %d)"
54        (match ty with Sig_int (sz, _) -> 8*sz | _ -> 32)
55        i
[751]56  | AST.Cst_float f -> Printf.sprintf "Ofloatconst %f" f
[966]57  | AST.Cst_addrsymbol id -> Printf.sprintf "Oaddrsymbol id_%s 0" id
[898]58  (*| AST.Cst_stackoffset off -> Printf.sprintf "Oaddrstack (repr %d)" off*)
[966]59  | AST.Cst_stack -> Printf.sprintf "Oaddrstack 0"
60  | AST.Cst_offset off ->
61      Printf.sprintf "Ointconst I%d (repr ? %d)"
62        (match ty with Sig_int (sz, _) -> 8*sz | _ -> 32)
63        (Driver.CminorMemory.concrete_offset off)
64  | AST.Cst_sizeof sz ->
65      Printf.sprintf "Ointconst I%d (repr ? %d)"
66        (match ty with Sig_int (sz, _) -> 8*sz | _ -> 32)
67        (Driver.CminorMemory.concrete_size sz)
[751]68
[1633]69(* Matita will figure out the missing information from the types produced
70   by the caller *)
[751]71let print_op1 = function
[1633]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 ???)"
[751]79
[966]80let print_op2 ty = function
[751]81  | AST.Op_add -> "Oadd"
82  | AST.Op_sub -> "Osub"
83  | AST.Op_mul -> "Omul"
84  | AST.Op_div -> "Odiv"
85  | AST.Op_divu -> "Odivu"
86  | AST.Op_mod -> "Omod"
87  | AST.Op_modu -> "Omodu"
88  | AST.Op_and -> "Oand"
89  | AST.Op_or -> "Oor"
90  | AST.Op_xor -> "Oxor"
91  | AST.Op_shl -> "Oshl"
92  | AST.Op_shr -> "Oshr"
93  | AST.Op_shru -> "Oshru"
94  | AST.Op_cmp cmp -> "(Ocmp " ^ print_cmp cmp ^ ")"
95  | AST.Op_cmpu cmp -> "(Ocmpu " ^ (print_cmp cmp) ^ ")"
96  | AST.Op_addp -> "Oaddp"
[898]97  | AST.Op_subp -> "Osubpi"
[966]98  | AST.Op_subpp ->
99      Printf.sprintf "(Osubpp I%d)"
100        (match ty with Sig_int (sz, _) -> 8*sz | _ -> 32)
[776]101  | AST.Op_cmpp cmp -> "(Ocmpp " ^ (print_cmp cmp) ^ ")"
[751]102
103let rec define_expr_labels = function
[898]104| Cminor.Expr (e,ty) -> match e with
[751]105  | Cminor.Op1 (_, e) -> define_expr_labels e
106  | Cminor.Op2 (_, e1, e2) -> define_expr_labels e1 ^ define_expr_labels e2
107  | Cminor.Mem (_, e) -> define_expr_labels e
108  | Cminor.Cond (e1, e2, e3) ->
109      define_expr_labels e1 ^ define_expr_labels e2 ^ define_expr_labels e3 
110  | Cminor.Exp_cost (lab, e) ->
111      Printf.sprintf "definition C%s := costlabel_of_nat %d.\n%s"
[1633]112        lab.CostLabel.name (fresh ()) (define_expr_labels e)
[751]113  | _ -> ""
114
115let print_quantity = function
[898]116  | AST.QInt 1 -> "Mint8unsigned"
117  | AST.QInt 2 -> "Mint16unsigned"
118  | AST.QInt 4 -> "Mint32"
119  | AST.QOffset -> "Mint32"
120  | AST.QPtr -> "Mpointer Any"
[751]121
[898]122let typeof = function Cminor.Expr (_,ty) -> ty
123
[751]124let rec print_expression p_id = function
[898]125| Cminor.Expr (e,ty) -> match e with
126  | Cminor.Id id -> Printf.sprintf "Id (%s) %s" (print_type ty) (p_id id)
[966]127  | Cminor.Cst cst -> Printf.sprintf "Cst (%s) (%s)" (print_type ty) (print_constant ty cst)
[751]128  | Cminor.Op1 (op1, e) ->
[898]129      Printf.sprintf "Op1 (%s) (%s) %s (%s)"
130        (print_type (typeof e)) (print_type ty)
131        (print_op1 op1) (print_expression p_id e)
[751]132  | Cminor.Op2 (op2, e1, e2) ->
[898]133      Printf.sprintf "Op2 (%s) (%s) (%s) %s (%s) (%s)"
134        (print_type (typeof e1)) (print_type (typeof e2)) (print_type ty)
[966]135        (print_op2 ty op2)
[751]136        (print_expression p_id e1)
137        (print_expression p_id e2)
138  | Cminor.Mem (q, e) ->
[898]139      Printf.sprintf "Mem (%s) Any %s (%s)"
140        (print_type ty) (print_quantity q) (print_expression p_id e)
[751]141  | Cminor.Cond (e1, e2, e3) ->
[898]142      let sz,sg = match typeof e1 with Sig_int (sz, sg) -> sz,sg in
143      Printf.sprintf "Cond I%d %s (%s) (%s) (%s) (%s)"
144        (sz*8) (print_signedness sg)
145        (print_type ty)
[751]146        (print_expression p_id e1)
147        (print_expression p_id e2)
148        (print_expression p_id e3)
149  | Cminor.Exp_cost (lab, e) ->
[1633]150      Printf.sprintf "Ecost (%s) C%s (%s)" (print_type ty) lab.CostLabel.name (print_expression p_id e)
[751]151
[898]152let print_arg p_id e =
[1633]153  Printf.sprintf "mk_DPair ?? (%s) (%s)" (print_type (typeof e)) (print_expression p_id e)
[751]154
155let rec print_args p_id = 
[898]156  MiscPottier.string_of_list "; " (print_arg p_id)
[751]157
158
159let n_spaces n = String.make n ' '
160
161
[898]162let print_local p_id (id,ty) =
[1633]163  Printf.sprintf "mk_Prod ?? %s (%s)" (p_id id) (print_type ty)
[751]164
165let print_locals p_id vars =
[898]166  (MiscPottier.string_of_list "; " (print_local p_id) vars)
[751]167
168
169let print_table n =
170  let f (case, exit) =
[1633]171    Printf.sprintf "(mk_Prod ?? (repr ? %d) %d)" case exit
[751]172  in
173  MiscPottier.string_of_list (";\n" ^ n_spaces n) f
174
175let rec define_labels = function
176  | Cminor.St_assign (_, e) -> define_expr_labels e
177  | Cminor.St_store (_, e1, e2) -> define_expr_labels e1 ^ define_expr_labels e2
178  | Cminor.St_call (_, _, args, _) -> String.concat "" (List.map define_expr_labels args)
179  | Cminor.St_tailcall (_, args, _) -> String.concat "" (List.map define_expr_labels args)
180  | Cminor.St_seq (s1, s2) -> define_labels s1 ^ define_labels s2
181  | Cminor.St_ifthenelse (e, s1, s2) -> define_expr_labels e ^ define_labels s1 ^ define_labels s2
182  | Cminor.St_switch (e, _, _) -> define_expr_labels e
183  | Cminor.St_return (Some e) -> define_expr_labels e
184  | Cminor.St_label (l, s) ->
[1633]185      Printf.sprintf "definition L%s := label_of_nat %d.\n%s"
[751]186        l (fresh ()) (define_labels s)
187  | Cminor.St_cost (l, s) ->
188      Printf.sprintf "definition C%s := costlabel_of_nat %d.\n%s"
[1633]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
[751]192  | _ -> ""
193
194let rec print_body p_id n = function
195  | Cminor.St_skip -> Printf.sprintf "%sSt_skip" (n_spaces n)
196  | Cminor.St_assign (id, e) ->
[898]197      Printf.sprintf "%sSt_assign (%s) %s (%s)\n"
198        (n_spaces n) (print_type (typeof e))
199        (p_id id) (print_expression p_id e)
[751]200  | Cminor.St_store (q, e1, e2) ->
[898]201      Printf.sprintf "%sSt_store (%s) Any %s (%s) (%s)\n"
[751]202        (n_spaces n)
[898]203        (print_type (typeof e2))
[751]204        (print_quantity q)
205        (print_expression p_id e1)
206        (print_expression p_id e2)
[898]207(* XXX cheat horribly *)
208  | Cminor.St_call (None, Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f),_), args, sg) ->
[966]209      Printf.sprintf "%sSt_call (None ?) (Cst ? (Oaddrsymbol id_%s 0)) [%s]\n"
[898]210        (n_spaces n)
211        f
212        (print_args p_id args)
213  | Cminor.St_call (Some id, Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f),_), args, sg) ->
[1633]214      Printf.sprintf "%sSt_call (Some ? (mk_Prod ?? %s (%s))) (Cst ? (Oaddrsymbol id_%s 0)) [%s]\n"
[898]215        (n_spaces n)
216        (p_id id)
[1633]217        (print_type_return sg.AST.res)
[898]218        f
219        (print_args p_id args)
220  | Cminor.St_tailcall (Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f),_), args, sg) ->
[966]221      Printf.sprintf "%sSt_tailcall (Cst ? (Oaddrsymbol id_%s 0)) [%s]\n"
[898]222        (n_spaces n)
223        f
224        (print_args p_id args)
225(* XXX regular versions, but the region will be screwed up *)
[751]226  | Cminor.St_call (None, f, args, sg) ->
[816]227      Printf.sprintf "%sSt_call (None ?) (%s) [%s]\n"
[751]228        (n_spaces n)
229        (print_expression p_id f)
230        (print_args p_id args)
231  | Cminor.St_call (Some id, f, args, sg) ->
[816]232      Printf.sprintf "%sSt_call (Some ? %s) (%s) [%s]\n"
[751]233        (n_spaces n)
234        (p_id id)
235        (print_expression p_id f)
236        (print_args p_id args)
237  | Cminor.St_tailcall (f, args, sg) ->
[816]238      Printf.sprintf "%sSt_tailcall (%s) [%s]\n"
[751]239        (n_spaces n)
240        (print_expression p_id f)
241        (print_args p_id args)
242  | Cminor.St_seq (s1, s2) ->
243      Printf.sprintf "%sSt_seq (\n%s%s) (\n%s%s)\n"
244        (n_spaces n)
245        (print_body p_id (n+2) s1)
246        (n_spaces n)
247        (print_body p_id n s2)
248        (n_spaces n)
249  | Cminor.St_ifthenelse (e, s1, s2) ->
[898]250      let sz,sg = match typeof e with Sig_int (sz, sg) -> sz,sg in
251      Printf.sprintf "%sSt_ifthenelse I%d %s (%s) (\n%s%s) (\n%s%s)\n"
[751]252        (n_spaces n)
[898]253        (sz*8) (print_signedness sg)
[751]254        (print_expression p_id e)
255        (print_body p_id (n+2) s1)
256        (n_spaces n)
257        (print_body p_id (n+2) s2)
258        (n_spaces n)
[1633]259  | Cminor.St_switch (e, tbl, dflt) -> assert false
260(*
[898]261      let sz,sg = match typeof e with Sig_int (sz, sg) -> sz,sg in
262      Printf.sprintf "%sSt_switch I%d %s (%s) [\n%s%s] %d\n"
[751]263        (n_spaces n)
[898]264        (sz*8) (print_signedness sg)
[751]265        (print_expression p_id e)
266        (n_spaces (n+2))
267        (print_table ( n+2) tbl)
[1633]268        dflt*)
[751]269  | Cminor.St_return None -> Printf.sprintf "%sSt_return (None ?)\n" (n_spaces n)
270  | Cminor.St_return (Some e) ->
[898]271      Printf.sprintf "%sSt_return (Some ? (%s))\n" (n_spaces n) (print_arg p_id e)
[751]272  | Cminor.St_label (lbl, s) ->
273      Printf.sprintf "%sSt_label L%s (\n%s%s)\n" 
274        (n_spaces n)
275        lbl
276        (print_body p_id n s)
277        (n_spaces n)
278  | Cminor.St_goto lbl ->
279      Printf.sprintf "%sSt_goto L%s\n" (n_spaces n) lbl
280  | Cminor.St_cost (lbl, s) ->
281      Printf.sprintf "%sSt_cost C%s (\n%s%s)\n"
[1633]282        (n_spaces n) lbl.CostLabel.name (print_body p_id n s)
[751]283        (n_spaces n)
[1633]284  | Cminor.St_ind_0 (_, s) -> print_body p_id n s
285  | Cminor.St_ind_inc (_, s) -> print_body p_id n s
[751]286
287let print_ids fname vs =
[898]288  List.fold_left (fun s (v,_) ->
[751]289                  Printf.sprintf "%sdefinition id_%s_%s := ident_of_nat %d.\n"
290                                 s fname v (fresh ()))
291       "" vs
292
293let print_internal f_name f_def =
294  let fid = fresh () in
295  let p_id id = Printf.sprintf "id_%s_%s" f_name id in
[1633]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"
[751]297    f_name
298    fid
299    (print_ids f_name (f_def.Cminor.f_vars @ f_def.Cminor.f_params))
300    (define_labels f_def.Cminor.f_body)
301    f_name
[898]302    (print_ret_type f_def.Cminor.f_return)
[751]303    (print_locals p_id f_def.Cminor.f_params)
304    (print_locals p_id f_def.Cminor.f_vars)
[1633]305    "(match daemon in False with [ ])"  (* ewww *)
[898]306    (Driver.CminorMemory.concrete_size f_def.Cminor.f_stacksize)
[751]307    (print_body p_id 2 f_def.Cminor.f_body)
[1633]308    "(match daemon in False with [ ])"  (* ewww *)
[751]309
[898]310let print_sig s =
311  Printf.sprintf "mk_signature [%s] (%s)"
312    (MiscPottier.string_of_list "; " print_type s.AST.args)
[1633]313    (match s.AST.res with AST.Type_ret t -> "Some ? (" ^ print_type t ^ ")"
[898]314                        | AST.Type_void  -> "None ?")
[751]315
[898]316
317
[751]318let print_external f def =
319  Printf.sprintf "definition id_%s := ident_of_nat %d.\ndefinition f_%s := External internal_function (mk_external_function id_%s (%s)).\n"
320    f
321    (fresh ())
322    f
323    f
324    (print_sig def.AST.ef_sig)
325
326
327let print_funct (f_name, f_def) = match f_def with
328  | Cminor.F_int f_def -> print_internal f_name f_def
329  | Cminor.F_ext f_def -> print_external f_name f_def
330
331let print_functs = List.fold_left (fun s f -> s ^ (print_funct f)) ""
332
333
334let print_fun' n functs =
335  MiscPottier.string_of_list ";\n" (fun (f,def) ->
[1633]336    Printf.sprintf "%s(mk_Prod ?? id_%s f_%s)"
[751]337      (n_spaces n) 
338      f
339      f)
340      functs
341
342let print_main n main =
343  Printf.sprintf "%s%s"
344    (n_spaces n)
345    (match main with Some f -> "id_" ^ f | None -> "ident_of_nat 0 (* None! *)")
346
[898]347let define_var_id (id,_,_) =
[758]348  Printf.sprintf "definition id_%s := ident_of_nat %d.\n" id (fresh ())
349
350let define_var_ids =
351  List.fold_left (fun s v -> s ^ (define_var_id v)) ""
352
[751]353let print_program p =
[1633]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"
[758]355    (define_var_ids p.Cminor.vars)
[751]356    (print_functs p.Cminor.functs)
[1226]357    (print_vars 2 p.Cminor.vars)
[751]358    (print_fun' 2 p.Cminor.functs)
359    (print_main 2 p.Cminor.main)
360
Note: See TracBrowser for help on using the repository browser.