source: src/RTLabs/RTLabsMatitaPrinter.ml @ 2307

Last change on this file since 2307 was 1633, checked in by campbell, 8 years ago

Update Cminor pretty printer and examples.

File size: 9.7 KB
Line 
1
2let next_id = ref 0
3let fresh () = let i = !next_id in next_id := i+1; i
4
5let n_spaces n = String.make n ' '
6
7let print_signedness = function
8  | AST.Signed -> "Signed"
9  | AST.Unsigned -> "Unsigned"
10
11let print_sig_type = function
12  | AST.Sig_int (sz, sg) -> Printf.sprintf "ASTint I%d %s" (sz*8) (print_signedness sg)
13  | AST.Sig_float (sz, _) -> Printf.sprintf "ASTfloat F%d" (sz*8)
14  | AST.Sig_offset -> "ASTint I32 Unsigned"
15  | AST.Sig_ptr -> "ASTptr Any"
16
17let print_global (x, size) =
18  Printf.sprintf "pair ?? (pair ?? id_%s Any) %d" x
19    (Driver.RTLabsMemory.concrete_size size)
20
21let print_globals n globs =
22  Printf.sprintf "%s(*globals:*)\n%s[%s]"
23    (n_spaces n)
24    (n_spaces n)
25    (MiscPottier.string_of_list (";\n"^n_spaces n) print_global globs)
26
27let print_label l = "lbl_" ^ l
28
29let rec print_args args =
30  Printf.sprintf "[[%s]]" (MiscPottier.string_of_list "; " Register.print args)
31
32let print_regty (r,ty) =
33  Printf.sprintf "(pair ?? %s (%s))" (Register.print r) (print_sig_type ty)
34
35let print_result = function
36| None -> "(None ?)"
37| Some rty -> "(Some ? " ^ print_regty rty ^ ")"
38
39let print_params rl =
40  Printf.sprintf "[%s]" (MiscPottier.string_of_list "; " Register.print rl)
41
42let print_locals rl =
43  Printf.sprintf "[%s]" (MiscPottier.string_of_list "; " print_regty rl)
44
45let print_quantity = function
46  | AST.QInt 1 -> "Mint8unsigned"
47  | AST.QInt 2 -> "Mint16unsigned"
48  | AST.QInt 4 -> "Mint32"
49  | AST.QOffset -> "Mint32"
50  | AST.QPtr -> "Mpointer Any"
51(*
52let print_memory_q = function
53  | Memory.MQ_int8signed    -> "Mint8signed"
54  | Memory.MQ_int8unsigned  -> "Mint8unsigned"
55  | Memory.MQ_int16signed   -> "Mint16signed"
56  | Memory.MQ_int16unsigned -> "Mint16unsigned"
57  | Memory.MQ_int32         -> "Mint32"
58  | Memory.MQ_float32       -> "Mfloat32"
59  | Memory.MQ_float64       -> "Mfloat64"
60  | Memory.MQ_pointer       -> "Mpointer Any"
61  | Memory.MQ_chunk         -> "MXXX"
62*)
63
64
65let print_cmp = function
66  | AST.Cmp_eq -> "Ceq"
67  | AST.Cmp_ne -> "Cne"
68  | AST.Cmp_gt -> "Cgt"
69  | AST.Cmp_ge -> "Cge"
70  | AST.Cmp_lt -> "Clt"
71  | AST.Cmp_le -> "Cle"
72
73let print_constant ty = function
74  | AST.Cst_int i ->
75      Printf.sprintf "Ointconst I%d (repr ? %d)"
76        (match ty with AST.Sig_int (sz, _) -> 8*sz | _ -> 32)
77        i
78  | AST.Cst_float f -> Printf.sprintf "Ofloatconst %f" f
79  | AST.Cst_addrsymbol id -> Printf.sprintf "Oaddrsymbol id_%s 0" id
80  (*| AST.Cst_stackoffset off -> Printf.sprintf "Oaddrstack (repr %d)" off*)
81  | AST.Cst_stack -> Printf.sprintf "Oaddrstack 0"
82  | AST.Cst_offset off ->
83      Printf.sprintf "Ointconst I%d (repr ? %d)"
84        (match ty with AST.Sig_int (sz, _) -> 8*sz | _ -> 32)
85        (Driver.CminorMemory.concrete_offset off)
86  | AST.Cst_sizeof sz ->
87      Printf.sprintf "Ointconst I%d (repr ? %d)"
88        (match ty with AST.Sig_int (sz, _) -> 8*sz | _ -> 32)
89        (Driver.CminorMemory.concrete_size sz)
90
91let print_op1 = function
92  | AST.Op_cast((_,sg),sz) -> Printf.sprintf "(Ocastint %s I%d)" (print_signedness sg) (8*sz)
93  | AST.Op_negint -> "Onegint"
94  | AST.Op_notbool -> "Onotbool"
95  | AST.Op_notint -> "Onotint"
96  | AST.Op_id -> "Oid"
97  | AST.Op_ptrofint -> "Optrofint"
98  | AST.Op_intofptr -> "Ointofptr"
99
100let print_op2 ty = function
101  | AST.Op_add -> "Oadd"
102  | AST.Op_sub -> "Osub"
103  | AST.Op_mul -> "Omul"
104  | AST.Op_div -> "Odiv"
105  | AST.Op_divu -> "Odivu"
106  | AST.Op_mod -> "Omod"
107  | AST.Op_modu -> "Omodu"
108  | AST.Op_and -> "Oand"
109  | AST.Op_or -> "Oor"
110  | AST.Op_xor -> "Oxor"
111  | AST.Op_shl -> "Oshl"
112  | AST.Op_shr -> "Oshr"
113  | AST.Op_shru -> "Oshru"
114  | AST.Op_cmp cmp -> "(Ocmp " ^ print_cmp cmp ^ ")"
115  | AST.Op_cmpu cmp -> "(Ocmpu " ^ (print_cmp cmp) ^ ")"
116  | AST.Op_addp -> "Oaddp"
117  | AST.Op_subp -> "Osubpi"
118  | AST.Op_subpp ->
119      Printf.sprintf "(Osubpp I%d)"
120        (match ty with AST.Sig_int (sz, _) -> 8*sz | _ -> 32)
121  | AST.Op_cmpp cmp -> "(Ocmpp " ^ (print_cmp cmp) ^ ")"
122
123
124
125let print_sig s =
126  Printf.sprintf "mk_signature [%s] (%s)"
127    (MiscPottier.string_of_list "; " print_sig_type s.AST.args)
128    (match s.AST.res with AST.Type_ret t -> "Some ? " ^ print_sig_type t
129                        | AST.Type_void  -> "None ?")
130
131let rec print_table = function
132  | [] -> ""
133  | [lbl] -> print_label lbl
134  | lbl :: tbl -> (print_label lbl) ^ "; " ^ (print_table tbl)
135
136
137let print_statement lookup_type = function
138  | RTLabs.St_skip lbl
139  | RTLabs.St_ind_0 (_, lbl)
140  | RTLabs.St_ind_inc (_, lbl)
141     -> "make_St_skip " ^ (print_label lbl)
142  | RTLabs.St_cost (cost_lbl, lbl) ->
143      Printf.sprintf "make_St_cost C%s %s"
144        cost_lbl.CostLabel.name (print_label lbl)
145  | RTLabs.St_cst (dests, cst, lbl) ->
146      Printf.sprintf "make_St_const %s (%s) %s"
147        (Register.print dests)
148        (print_constant (lookup_type dests) cst)
149        (print_label lbl)
150  | RTLabs.St_op1 (op1, dests, srcs, lbl) ->
151      Printf.sprintf "make_St_op1 %s %s %s %s"
152        (print_op1 op1)
153        (Register.print dests)
154        (Register.print srcs)
155        (print_label lbl)
156  | RTLabs.St_op2 (op2, dests, srcs1, srcs2, lbl) ->
157      Printf.sprintf "make_St_op2 %s %s %s %s %s"
158        (print_op2 (lookup_type dests) op2)
159        (Register.print dests)
160        (Register.print srcs1)
161        (Register.print srcs2)
162        (print_label lbl)
163  | RTLabs.St_load (chunk, addr, dests, lbl) ->
164      Printf.sprintf "make_St_load %s %s %s %s"
165        (print_quantity chunk)
166        (Register.print addr)
167        (Register.print dests)
168        (print_label lbl)
169  | RTLabs.St_store (chunk, addr, srcs, lbl) ->
170      Printf.sprintf "make_St_store %s %s %s %s"
171        (print_quantity chunk)
172        (Register.print addr)
173        (Register.print srcs)
174        (print_label lbl)
175  | RTLabs.St_call_id (f, args, res, sg, lbl) ->
176      Printf.sprintf "make_St_call_id id_%s %s (%s) %s"
177        f
178        (print_params args)
179        (match res with None -> "None ?" | Some res -> "Some ? " ^ Register.print res)
180        (print_label lbl)
181  | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
182      Printf.sprintf "make_St_call_ptr %s %s (%s) %s"
183        (Register.print f)
184        (print_params args)
185        (match res with None -> "None ?" | Some res -> "Some ? " ^ (Register.print res))
186        (print_label lbl)
187  | RTLabs.St_tailcall_id (f, args, sg) ->
188      Printf.sprintf "make_St_tailcall_id id_%s %s"
189        f
190        (print_params args)
191  | RTLabs.St_tailcall_ptr (f, args, sg) ->
192      Printf.sprintf "make_St_tailcall_ptr %s %s"
193        (Register.print f)
194        (print_params args)
195  | RTLabs.St_cond (srcs, lbl_true, lbl_false) ->
196      Printf.sprintf "make_St_cond %s %s %s"
197        (Register.print srcs)
198        (print_label lbl_true)
199        (print_label lbl_false)
200  | RTLabs.St_jumptable (rs, tbl) ->
201      Printf.sprintf "make_St_jumptable %s [%s]"
202        (Register.print rs)
203        (print_table tbl)
204  | RTLabs.St_return -> "make_St_return"
205
206let print_cost_labels n c =
207  let f _ stmt (i,s) =
208    match stmt with
209    | RTLabs.St_cost (lbl, _) ->
210        i+1,
211        Printf.sprintf "%sdefinition C%s := costlabel_of_nat %d.\n%s"
212          (n_spaces n)
213          lbl
214          i
215          s
216    | _ -> i,s
217  in
218  snd (Label.Map.fold f c (0,""))
219
220let print_labels n c =
221  let f lbl _ (i,s) =
222    i+1,
223    Printf.sprintf "%sdefinition %s := %d.\n%s"
224      (n_spaces n)
225      (print_label lbl)
226      i
227      s
228  in
229  snd (Label.Map.fold f c (0,""))
230
231let print_graph n lookup_type c =
232  let f lbl stmt s =
233    Printf.sprintf "%s(pair ?? %s (%s))%s\n%s"
234      (n_spaces n)
235      (print_label lbl)
236      (print_statement lookup_type stmt)
237      (if s = "" then "\n]" else ";")
238      s in
239  "[\n" ^ Label.Map.fold f c ""
240
241let print_internal_decl n f def =
242  let env = def.RTLabs.f_params @ def.RTLabs.f_locals in
243  let lookup_type r =
244    let _,ty = List.find (fun (r',_) -> r = r') env in ty
245  in
246  Printf.sprintf
247    "%sdefinition id_%s := ident_of_nat %d.\n%s%s\n\n%sdefinition pre_%s := mk_pre_internal_function\n%s%s\n%s%s\n%s%s\n%s%d\n%s%s\n%s%s\n%s%s."
248    (n_spaces n)
249    f
250    (fresh ())
251    (print_labels n def.RTLabs.f_graph)
252    (print_cost_labels n def.RTLabs.f_graph)
253    (n_spaces n)
254    f
255    (n_spaces (n+2))
256    (print_result def.RTLabs.f_result)
257    (n_spaces (n+2))
258    (print_locals def.RTLabs.f_params)
259    (n_spaces (n+2))
260    (print_locals def.RTLabs.f_locals)
261    (n_spaces (n+2))
262    (Driver.RTLabsMemory.concrete_size def.RTLabs.f_stacksize)
263    (n_spaces (n+2))
264    (print_graph (n+2) lookup_type def.RTLabs.f_graph)
265    (n_spaces (n+2))
266    (print_label def.RTLabs.f_entry)
267    (n_spaces (n+2))
268    (print_label def.RTLabs.f_exit)
269
270
271
272let print_external_decl n f def =
273  Printf.sprintf "%sdefinition id_%s := ident_of_nat %d.\n%sdefinition f_%s := External (mk_external_function id_%s (%s)).\n"
274    (n_spaces n)
275    f
276    (fresh ())
277    (n_spaces n)
278    f
279    f
280    (print_sig def.AST.ef_sig)
281
282
283let print_fun_decl n (f, def) = match def with
284  | RTLabs.F_int def -> print_internal_decl n f def
285  | RTLabs.F_ext def -> print_external_decl n f def
286
287let print_fun_decls n =
288  List.fold_left (fun s f -> s ^ (print_fun_decl n f) ^ "\n\n") ""
289
290let print_fun n functs =
291  List.fold_left (fun s (f,_) ->
292    Printf.sprintf "%sdo f_%s \\larr make_internal_function pre_%s;\n%s"
293      (n_spaces n) 
294      f
295      f
296      s) "" functs
297
298let print_fun' n functs =
299  List.fold_left (fun s (f,def) ->
300    Printf.sprintf "%s(pair ?? id_%s f_%s)::\n%s"
301      (n_spaces n) 
302      f
303      f
304      s) "(nil ?)" functs
305
306let print_main n main =
307  Printf.sprintf "%s%s"
308    (n_spaces n)
309    (match main with Some f -> "id_" ^ f | None -> "ident_of_nat 0 (* None! *)")
310
311let define_var_id (id,_) =
312  Printf.sprintf "definition id_%s := ident_of_nat %d.\n" id (fresh ())
313
314let define_var_ids =
315  List.fold_left (fun s v -> s ^ (define_var_id v)) ""
316
317let print_program p =
318  Printf.sprintf "include \"RTLabs/import.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n\n%s\n\ndefinition prog : res RTLabs_program :=\n%s\nOK ? (mk_program ??\n%s\n(%s)\n%s\n).\n"
319    (define_var_ids p.RTLabs.vars)
320    (print_fun_decls 2 p.RTLabs.functs)
321    (print_fun 2 p.RTLabs.functs)
322    (print_globals 2 p.RTLabs.vars)
323    (print_fun' 2 p.RTLabs.functs)
324    (print_main 2 p.RTLabs.main)
Note: See TracBrowser for help on using the repository browser.