source: src/Cminor/cminorMatitaPrinter.ml @ 898

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

Update pretty printers and examples.

File size: 12.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_signedness = function
7  | Signed -> "Signed"
8  | Unsigned -> "Unsigned"
9
10let print_type = function
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"
14  | Sig_ptr -> "ASTptr Any"
15
16let print_ret_type = function
17  | Type_ret t -> Printf.sprintf "Some ? (%s)" (print_type t)
18  | Type_void -> "None ?"
19
20
21let print_data = function
22  (*| Data_reserve n -> Printf.sprintf "Init_space %d" n*)
23  | Data_int8 i -> Printf.sprintf "Init_int8 (repr %d)" i
24  | Data_int16 i -> Printf.sprintf "Init_int16 (repr %d)" i
25  | Data_int32 i -> Printf.sprintf "Init_int32 (repr %d)" i
26  | Data_float32 f -> Printf.sprintf "Init_float32 %f" f
27  | Data_float64 f -> Printf.sprintf "Init_float64 %f" f
28
29let print_var n (id, sz, init) =
30  Printf.sprintf "(pair ?? (pair ?? (pair ?? id_%s [%s]) Any) it)"
31    id
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))
36
37let print_vars n = MiscPottier.string_of_list ";\n" (print_var n) 
38
39let print_cmp = function
40  | AST.Cmp_eq -> "Ceq"
41  | AST.Cmp_ne -> "Cne"
42  | AST.Cmp_gt -> "Cgt"
43  | AST.Cmp_ge -> "Cge"
44  | AST.Cmp_lt -> "Clt"
45  | AST.Cmp_le -> "Cle"
46
47let print_constant = function
48  | AST.Cst_int i -> Printf.sprintf "Ointconst (repr %d)" i
49  | AST.Cst_float f -> Printf.sprintf "Ofloatconst %f" f
50  | AST.Cst_addrsymbol id -> Printf.sprintf "Oaddrsymbol id_%s (repr 0)" id
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)
55
56let print_op1 = function
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"
62  | AST.Op_negint -> "Onegint"
63  | AST.Op_notbool -> "Onotbool"
64  | AST.Op_notint -> "Onotint"
65  | AST.Op_id -> "Oid"
66  | AST.Op_ptrofint -> "(Optrofint Any)"
67  | AST.Op_intofptr -> "Ointofptr"
68
69let print_op2 = function
70  | AST.Op_add -> "Oadd"
71  | AST.Op_sub -> "Osub"
72  | AST.Op_mul -> "Omul"
73  | AST.Op_div -> "Odiv"
74  | AST.Op_divu -> "Odivu"
75  | AST.Op_mod -> "Omod"
76  | AST.Op_modu -> "Omodu"
77  | AST.Op_and -> "Oand"
78  | AST.Op_or -> "Oor"
79  | AST.Op_xor -> "Oxor"
80  | AST.Op_shl -> "Oshl"
81  | AST.Op_shr -> "Oshr"
82  | AST.Op_shru -> "Oshru"
83  | AST.Op_cmp cmp -> "(Ocmp " ^ print_cmp cmp ^ ")"
84  | AST.Op_cmpu cmp -> "(Ocmpu " ^ (print_cmp cmp) ^ ")"
85  | AST.Op_addp -> "Oaddp"
86  | AST.Op_subp -> "Osubpi"
87  | AST.Op_subpp -> "Osubpp"
88  | AST.Op_cmpp cmp -> "(Ocmpp " ^ (print_cmp cmp) ^ ")"
89
90let rec define_expr_labels = function
91| Cminor.Expr (e,ty) -> match e with
92  | Cminor.Op1 (_, e) -> define_expr_labels e
93  | Cminor.Op2 (_, e1, e2) -> define_expr_labels e1 ^ define_expr_labels e2
94  | Cminor.Mem (_, e) -> define_expr_labels e
95  | Cminor.Cond (e1, e2, e3) ->
96      define_expr_labels e1 ^ define_expr_labels e2 ^ define_expr_labels e3 
97  | Cminor.Exp_cost (lab, e) ->
98      Printf.sprintf "definition C%s := costlabel_of_nat %d.\n%s"
99        lab (fresh ()) (define_expr_labels e)
100  | _ -> ""
101
102let print_quantity = function
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
110
111let rec print_expression p_id = function
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)
115  | Cminor.Op1 (op1, 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)
119  | Cminor.Op2 (op2, e1, e2) ->
120      Printf.sprintf "Op2 (%s) (%s) (%s) %s (%s) (%s)"
121        (print_type (typeof e1)) (print_type (typeof e2)) (print_type ty)
122        (print_op2 op2)
123        (print_expression p_id e1)
124        (print_expression p_id e2)
125  | Cminor.Mem (q, e) ->
126      Printf.sprintf "Mem (%s) Any %s (%s)"
127        (print_type ty) (print_quantity q) (print_expression p_id e)
128  | Cminor.Cond (e1, e2, e3) ->
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)
133        (print_expression p_id e1)
134        (print_expression p_id e2)
135        (print_expression p_id e3)
136  | Cminor.Exp_cost (lab, e) ->
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)
141
142let rec print_args p_id = 
143  MiscPottier.string_of_list "; " (print_arg p_id)
144
145
146let n_spaces n = String.make n ' '
147
148
149let print_local p_id (id,ty) =
150  Printf.sprintf "pair ?? %s (%s)" (p_id id) (print_type ty)
151
152let print_locals p_id vars =
153  (MiscPottier.string_of_list "; " (print_local p_id) vars)
154
155
156let print_table n =
157  let f (case, exit) =
158    Printf.sprintf "(pair ?? (repr %d) %d)" case exit
159  in
160  MiscPottier.string_of_list (";\n" ^ n_spaces n) f
161
162let rec define_labels = function
163  | Cminor.St_assign (_, e) -> define_expr_labels e
164  | Cminor.St_store (_, e1, e2) -> define_expr_labels e1 ^ define_expr_labels e2
165  | Cminor.St_call (_, _, args, _) -> String.concat "" (List.map define_expr_labels args)
166  | Cminor.St_tailcall (_, args, _) -> String.concat "" (List.map define_expr_labels args)
167  | Cminor.St_seq (s1, s2) -> define_labels s1 ^ define_labels s2
168  | Cminor.St_ifthenelse (e, s1, s2) -> define_expr_labels e ^ define_labels s1 ^ define_labels s2
169  | Cminor.St_loop s -> define_labels s
170  | Cminor.St_block s -> define_labels s
171  | Cminor.St_switch (e, _, _) -> define_expr_labels e
172  | Cminor.St_return (Some e) -> define_expr_labels e
173  | Cminor.St_label (l, s) ->
174      Printf.sprintf "definition L%s := ident_of_nat %d.\n%s"
175        l (fresh ()) (define_labels s)
176  | Cminor.St_cost (l, s) ->
177      Printf.sprintf "definition C%s := costlabel_of_nat %d.\n%s"
178        l (fresh ()) (define_labels s)
179  | _ -> ""
180
181let rec print_body p_id n = function
182  | Cminor.St_skip -> Printf.sprintf "%sSt_skip" (n_spaces n)
183  | Cminor.St_assign (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)
187  | Cminor.St_store (q, e1, e2) ->
188      Printf.sprintf "%sSt_store (%s) Any %s (%s) (%s)\n"
189        (n_spaces n)
190        (print_type (typeof e2))
191        (print_quantity q)
192        (print_expression p_id e1)
193        (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 *)
212  | Cminor.St_call (None, f, args, sg) ->
213      Printf.sprintf "%sSt_call (None ?) (%s) [%s]\n"
214        (n_spaces n)
215        (print_expression p_id f)
216        (print_args p_id args)
217  | Cminor.St_call (Some id, f, args, sg) ->
218      Printf.sprintf "%sSt_call (Some ? %s) (%s) [%s]\n"
219        (n_spaces n)
220        (p_id id)
221        (print_expression p_id f)
222        (print_args p_id args)
223  | Cminor.St_tailcall (f, args, sg) ->
224      Printf.sprintf "%sSt_tailcall (%s) [%s]\n"
225        (n_spaces n)
226        (print_expression p_id f)
227        (print_args p_id args)
228  | Cminor.St_seq (s1, s2) ->
229      Printf.sprintf "%sSt_seq (\n%s%s) (\n%s%s)\n"
230        (n_spaces n)
231        (print_body p_id (n+2) s1)
232        (n_spaces n)
233        (print_body p_id n s2)
234        (n_spaces n)
235  | Cminor.St_ifthenelse (e, s1, s2) ->
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)
240        (print_expression p_id e)
241        (print_body p_id (n+2) s1)
242        (n_spaces n)
243        (print_body p_id (n+2) s2)
244        (n_spaces n)
245  | Cminor.St_loop s ->
246      Printf.sprintf "%sSt_loop (\n%s%s)\n"
247        (n_spaces n)
248        (print_body p_id (n+2) s)
249        (n_spaces n)
250  | Cminor.St_block s ->
251      Printf.sprintf "%sSt_block (\n%s%s)\n"
252        (n_spaces n)
253        (print_body p_id (n+2) s)
254        (n_spaces n)
255  | Cminor.St_exit i ->
256      Printf.sprintf "%sSt_exit %d\n" (n_spaces n) i
257  | Cminor.St_switch (e, tbl, dflt) ->
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)
262        (print_expression p_id e)
263        (n_spaces (n+2))
264        (print_table ( n+2) tbl)
265        dflt
266  | Cminor.St_return None -> Printf.sprintf "%sSt_return (None ?)\n" (n_spaces n)
267  | Cminor.St_return (Some e) ->
268      Printf.sprintf "%sSt_return (Some ? (%s))\n" (n_spaces n) (print_arg p_id e)
269  | Cminor.St_label (lbl, s) ->
270      Printf.sprintf "%sSt_label L%s (\n%s%s)\n" 
271        (n_spaces n)
272        lbl
273        (print_body p_id n s)
274        (n_spaces n)
275  | Cminor.St_goto lbl ->
276      Printf.sprintf "%sSt_goto L%s\n" (n_spaces n) lbl
277  | Cminor.St_cost (lbl, s) ->
278      Printf.sprintf "%sSt_cost C%s (\n%s%s)\n"
279        (n_spaces n) lbl (print_body p_id n s)
280        (n_spaces n)
281
282let print_ids fname vs =
283  List.fold_left (fun s (v,_) ->
284                  Printf.sprintf "%sdefinition id_%s_%s := ident_of_nat %d.\n"
285                                 s fname v (fresh ()))
286       "" vs
287
288let print_internal f_name f_def =
289  let fid = fresh () in
290  let p_id id = Printf.sprintf "id_%s_%s" f_name id in
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"
292    f_name
293    fid
294    (print_ids f_name (f_def.Cminor.f_vars @ f_def.Cminor.f_params))
295    (define_labels f_def.Cminor.f_body)
296    f_name
297    (print_ret_type f_def.Cminor.f_return)
298    (print_locals p_id f_def.Cminor.f_params)
299    (print_locals p_id f_def.Cminor.f_vars)
300    (Driver.CminorMemory.concrete_size f_def.Cminor.f_stacksize)
301    (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
309
310
311let print_external f def =
312  Printf.sprintf "definition id_%s := ident_of_nat %d.\ndefinition f_%s := External internal_function (mk_external_function id_%s (%s)).\n"
313    f
314    (fresh ())
315    f
316    f
317    (print_sig def.AST.ef_sig)
318
319
320let print_funct (f_name, f_def) = match f_def with
321  | Cminor.F_int f_def -> print_internal f_name f_def
322  | Cminor.F_ext f_def -> print_external f_name f_def
323
324let print_functs = List.fold_left (fun s f -> s ^ (print_funct f)) ""
325
326
327let print_fun' n functs =
328  MiscPottier.string_of_list ";\n" (fun (f,def) ->
329    Printf.sprintf "%s(pair ?? id_%s f_%s)"
330      (n_spaces n) 
331      f
332      f)
333      functs
334
335let print_main n main =
336  Printf.sprintf "%s%s"
337    (n_spaces n)
338    (match main with Some f -> "id_" ^ f | None -> "ident_of_nat 0 (* None! *)")
339
340let define_var_id (id,_,_) =
341  Printf.sprintf "definition id_%s := ident_of_nat %d.\n" id (fresh ())
342
343let define_var_ids =
344  List.fold_left (fun s v -> s ^ (define_var_id v)) ""
345
346let print_program p =
347  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"
348    (define_var_ids p.Cminor.vars)
349    (print_functs p.Cminor.functs)
350    (print_fun' 2 p.Cminor.functs)
351    (print_main 2 p.Cminor.main)
352    (print_vars 2 p.Cminor.vars)
353
Note: See TracBrowser for help on using the repository browser.