source: src/Cminor/cminorMatitaPrinter.ml @ 776

Last change on this file since 776 was 776, checked in by campbell, 10 years ago

Fix up some minor null pointer issues in Clight.
Add corresponding Cminor example and fix up pretty printer a little.

File size: 10.2 KB
Line 
1open AST
2
3let next_id = ref 0
4let fresh () = let i = !next_id in next_id := i+1; i
5
6let print_type = function
7  | Sig_int -> "ASTint"
8  | Sig_float -> "ASTfloat"
9  | Sig_ptr -> "ASTptr Any"
10
11let print_ret_type = function
12  | Type_ret t -> print_type t
13  | Type_void -> "void"
14
15
16let print_data = function
17  | Data_reserve n -> Printf.sprintf "Init_space %d" n
18  | Data_int8 i -> Printf.sprintf "Init_int8 (repr %d)" i
19  | Data_int16 i -> Printf.sprintf "Init_int16 (repr %d)" i
20  | Data_int32 i -> Printf.sprintf "Init_int32 (repr %d)" i
21  | Data_float32 f -> Printf.sprintf "Init_float32 %f" f
22  | Data_float64 f -> Printf.sprintf "Init_float64 %f" f
23
24let print_var n (id, init) =
25  Printf.sprintf "(pair ?? (pair ?? (pair ?? id_%s [%s]) Any) it)"
26    id
27    (MiscPottier.string_of_list ";" print_data init)
28
29let print_vars n = MiscPottier.string_of_list ";\n" (print_var n) 
30
31let print_cmp = function
32  | AST.Cmp_eq -> "Ceq"
33  | AST.Cmp_ne -> "Cne"
34  | AST.Cmp_gt -> "Cgt"
35  | AST.Cmp_ge -> "Cge"
36  | AST.Cmp_lt -> "Clt"
37  | AST.Cmp_le -> "Cle"
38
39let print_constant = function
40  | AST.Cst_int i -> Printf.sprintf "Ointconst (repr %d)" i
41  | AST.Cst_float f -> Printf.sprintf "Ofloatconst %f" f
42  | AST.Cst_addrsymbol id -> Printf.sprintf "Oaddrsymbol id_%s (repr 0)" id
43  | AST.Cst_stackoffset off -> Printf.sprintf "Oaddrstack (repr %d)" off
44
45let print_op1 = function
46  | AST.Op_cast8unsigned -> "Ocast8unsigned"
47  | AST.Op_cast8signed -> "Ocast8signed"
48  | AST.Op_cast16unsigned -> "Ocast16unsigned"
49  | AST.Op_cast16signed -> "Ocast16signed"
50  | AST.Op_negint -> "Onegint"
51  | AST.Op_notbool -> "Onotbool"
52  | 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"
60  | AST.Op_id -> "Oid"
61  | AST.Op_ptrofint -> "Optrofint"
62  | AST.Op_intofptr -> "Ointofptr"
63
64let print_op2 = function
65  | AST.Op_add -> "Oadd"
66  | AST.Op_sub -> "Osub"
67  | AST.Op_mul -> "Omul"
68  | AST.Op_div -> "Odiv"
69  | AST.Op_divu -> "Odivu"
70  | AST.Op_mod -> "Omod"
71  | AST.Op_modu -> "Omodu"
72  | AST.Op_and -> "Oand"
73  | AST.Op_or -> "Oor"
74  | AST.Op_xor -> "Oxor"
75  | AST.Op_shl -> "Oshl"
76  | AST.Op_shr -> "Oshr"
77  | AST.Op_shru -> "Oshru"
78  | AST.Op_addf -> "Oaddf"
79  | AST.Op_subf -> "Osubf"
80  | AST.Op_mulf -> "Omulf"
81  | AST.Op_divf -> "Odivf"
82  | AST.Op_cmp cmp -> "(Ocmp " ^ print_cmp cmp ^ ")"
83  | AST.Op_cmpu cmp -> "(Ocmpu " ^ (print_cmp cmp) ^ ")"
84  | AST.Op_cmpf cmp -> "(Ocmpf " ^ (print_cmp cmp) ^ ")"
85  | AST.Op_addp -> "Oaddp"
86  | AST.Op_subp -> "Osubpi" (* FIXME: there should be separate subpi and subpp ops*)
87  | AST.Op_cmpp cmp -> "(Ocmpp " ^ (print_cmp cmp) ^ ")"
88
89let rec define_expr_labels = function
90  | Cminor.Op1 (_, e) -> define_expr_labels e
91  | Cminor.Op2 (_, e1, e2) -> define_expr_labels e1 ^ define_expr_labels e2
92  | Cminor.Mem (_, e) -> define_expr_labels e
93  | Cminor.Cond (e1, e2, e3) ->
94      define_expr_labels e1 ^ define_expr_labels e2 ^ define_expr_labels e3 
95  | Cminor.Exp_cost (lab, e) ->
96      Printf.sprintf "definition C%s := costlabel_of_nat %d.\n%s"
97        lab (fresh ()) (define_expr_labels e)
98  | _ -> ""
99
100let print_quantity = function
101  | Memory.QInt 1 -> "Mint8unsigned"
102  | Memory.QInt 2 -> "Mint16unsigned"
103  | Memory.QInt 4 -> "Mint32"
104  | Memory.QPtr -> "Mpointer Any"
105
106let 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)
109  | Cminor.Op1 (op1, e) ->
110      Printf.sprintf "Op1 %s (%s)" (print_op1 op1) (print_expression p_id e)
111  | Cminor.Op2 (op2, e1, e2) ->
112      Printf.sprintf "Op2 %s (%s) (%s)"
113        (print_op2 op2)
114        (print_expression p_id e1)
115        (print_expression p_id e2)
116  | Cminor.Mem (q, e) ->
117      Printf.sprintf "Mem %s (%s)" (print_quantity q) (print_expression p_id e)
118  | Cminor.Cond (e1, e2, e3) ->
119      Printf.sprintf "Cond (%s) (%s) (%s)"
120        (print_expression p_id e1)
121        (print_expression p_id e2)
122        (print_expression p_id e3)
123  | Cminor.Exp_cost (lab, e) ->
124      Printf.sprintf "Ecost C%s (%s)" lab (print_expression p_id e)
125
126
127let rec print_args p_id = 
128  MiscPottier.string_of_list "; " (print_expression p_id)
129
130
131let n_spaces n = String.make n ' '
132
133
134let 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 ?")
139
140let print_locals p_id vars =
141  (MiscPottier.string_of_list "; " p_id vars)
142
143
144let print_table n =
145  let f (case, exit) =
146    Printf.sprintf "(pair ?? (repr %d) %d)" case exit
147  in
148  MiscPottier.string_of_list (";\n" ^ n_spaces n) f
149
150let rec define_labels = function
151  | Cminor.St_assign (_, e) -> define_expr_labels e
152  | Cminor.St_store (_, e1, e2) -> define_expr_labels e1 ^ define_expr_labels e2
153  | Cminor.St_call (_, _, args, _) -> String.concat "" (List.map define_expr_labels args)
154  | Cminor.St_tailcall (_, args, _) -> String.concat "" (List.map define_expr_labels args)
155  | Cminor.St_seq (s1, s2) -> define_labels s1 ^ define_labels s2
156  | Cminor.St_ifthenelse (e, s1, s2) -> define_expr_labels e ^ define_labels s1 ^ define_labels s2
157  | Cminor.St_loop s -> define_labels s
158  | Cminor.St_block s -> define_labels s
159  | Cminor.St_switch (e, _, _) -> define_expr_labels e
160  | Cminor.St_return (Some e) -> define_expr_labels e
161  | Cminor.St_label (l, s) ->
162      Printf.sprintf "definition L%s := ident_of_nat %d.\n%s"
163        l (fresh ()) (define_labels s)
164  | Cminor.St_cost (l, s) ->
165      Printf.sprintf "definition C%s := costlabel_of_nat %d.\n%s"
166        l (fresh ()) (define_labels s)
167  | _ -> ""
168
169let rec print_body p_id n = function
170  | Cminor.St_skip -> Printf.sprintf "%sSt_skip" (n_spaces n)
171  | Cminor.St_assign (id, e) ->
172      Printf.sprintf "%sSt_assign %s (%s)\n" (n_spaces n) (p_id id) (print_expression p_id e)
173  | Cminor.St_store (q, e1, e2) ->
174      Printf.sprintf "%sSt_store %s (%s) (%s)\n"
175        (n_spaces n)
176        (print_quantity q)
177        (print_expression p_id e1)
178        (print_expression p_id e2)
179  | Cminor.St_call (None, f, args, sg) ->
180      Printf.sprintf "%sSt_call (None ?) (%s) [%s] (%s)\n"
181        (n_spaces n)
182        (print_expression p_id f)
183        (print_args p_id args)
184        (print_sig sg)
185  | Cminor.St_call (Some id, f, args, sg) ->
186      Printf.sprintf "%sSt_call (Some ? %s) (%s) [%s] (%s)\n"
187        (n_spaces n)
188        (p_id id)
189        (print_expression p_id f)
190        (print_args p_id args)
191        (print_sig sg)
192  | Cminor.St_tailcall (f, args, sg) ->
193      Printf.sprintf "%sSt_tailcall (%s) [%s] (%s)\n"
194        (n_spaces n)
195        (print_expression p_id f)
196        (print_args p_id args)
197        (print_sig sg)
198  | Cminor.St_seq (s1, s2) ->
199      Printf.sprintf "%sSt_seq (\n%s%s) (\n%s%s)\n"
200        (n_spaces n)
201        (print_body p_id (n+2) s1)
202        (n_spaces n)
203        (print_body p_id n s2)
204        (n_spaces n)
205  | Cminor.St_ifthenelse (e, s1, s2) ->
206      Printf.sprintf "%sSt_ifthenelse (%s) (\n%s%s) (\n%s%s)\n"
207        (n_spaces n)
208        (print_expression p_id e)
209        (print_body p_id (n+2) s1)
210        (n_spaces n)
211        (print_body p_id (n+2) s2)
212        (n_spaces n)
213  | Cminor.St_loop s ->
214      Printf.sprintf "%sSt_loop (\n%s%s)\n"
215        (n_spaces n)
216        (print_body p_id (n+2) s)
217        (n_spaces n)
218  | Cminor.St_block s ->
219      Printf.sprintf "%sSt_block (\n%s%s)\n"
220        (n_spaces n)
221        (print_body p_id (n+2) s)
222        (n_spaces n)
223  | Cminor.St_exit i ->
224      Printf.sprintf "%sSt_exit %d\n" (n_spaces n) i
225  | Cminor.St_switch (e, tbl, dflt) ->
226      Printf.sprintf "%sSt_switch (%s) [\n%s%s] %d\n"
227        (n_spaces n)
228        (print_expression p_id e)
229        (n_spaces (n+2))
230        (print_table ( n+2) tbl)
231        dflt
232  | Cminor.St_return None -> Printf.sprintf "%sSt_return (None ?)\n" (n_spaces n)
233  | Cminor.St_return (Some e) ->
234      Printf.sprintf "%sSt_return (Some ? (%s))\n" (n_spaces n) (print_expression p_id e)
235  | Cminor.St_label (lbl, s) ->
236      Printf.sprintf "%sSt_label L%s (\n%s%s)\n" 
237        (n_spaces n)
238        lbl
239        (print_body p_id n s)
240        (n_spaces n)
241  | Cminor.St_goto lbl ->
242      Printf.sprintf "%sSt_goto L%s\n" (n_spaces n) lbl
243  | Cminor.St_cost (lbl, s) ->
244      Printf.sprintf "%sSt_cost C%s (\n%s%s)\n"
245        (n_spaces n) lbl (print_body p_id n s)
246        (n_spaces n)
247
248let print_ids fname vs =
249  List.fold_left (fun s v ->
250                  Printf.sprintf "%sdefinition id_%s_%s := ident_of_nat %d.\n"
251                                 s fname v (fresh ()))
252       "" vs
253
254let print_internal f_name f_def =
255  let fid = fresh () in
256  let p_id id = Printf.sprintf "id_%s_%s" f_name id in
257  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"
258    f_name
259    fid
260    (print_ids f_name (f_def.Cminor.f_vars @ f_def.Cminor.f_params))
261    (define_labels f_def.Cminor.f_body)
262    f_name
263    (print_sig f_def.Cminor.f_sig)
264    (print_locals p_id f_def.Cminor.f_params)
265    (print_locals p_id f_def.Cminor.f_vars)
266    (print_locals p_id f_def.Cminor.f_ptrs)
267    f_def.Cminor.f_stacksize
268    (print_body p_id 2 f_def.Cminor.f_body)
269
270
271let print_external f def =
272  Printf.sprintf "definition id_%s := ident_of_nat %d.\ndefinition f_%s := External internal_function (mk_external_function id_%s (%s)).\n"
273    f
274    (fresh ())
275    f
276    f
277    (print_sig def.AST.ef_sig)
278
279
280let print_funct (f_name, f_def) = match f_def with
281  | Cminor.F_int f_def -> print_internal f_name f_def
282  | Cminor.F_ext f_def -> print_external f_name f_def
283
284let print_functs = List.fold_left (fun s f -> s ^ (print_funct f)) ""
285
286
287let print_fun' n functs =
288  MiscPottier.string_of_list ";\n" (fun (f,def) ->
289    Printf.sprintf "%s(pair ?? id_%s f_%s)"
290      (n_spaces n) 
291      f
292      f)
293      functs
294
295let print_main n main =
296  Printf.sprintf "%s%s"
297    (n_spaces n)
298    (match main with Some f -> "id_" ^ f | None -> "ident_of_nat 0 (* None! *)")
299
300let define_var_id (id,_) =
301  Printf.sprintf "definition id_%s := ident_of_nat %d.\n" id (fresh ())
302
303let define_var_ids =
304  List.fold_left (fun s v -> s ^ (define_var_id v)) ""
305
306let print_program p =
307  Printf.sprintf "include \"Cminor/semantics.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n%s\n\ndefinition myprog : Cminor_program :=\nmk_program ?? [\n%s\n]%s\n[%s]\n.\n"
308    (define_var_ids p.Cminor.vars)
309    (print_functs p.Cminor.functs)
310    (print_fun' 2 p.Cminor.functs)
311    (print_main 2 p.Cminor.main)
312    (print_vars 2 p.Cminor.vars)
313
Note: See TracBrowser for help on using the repository browser.