source: src/RTLabs/RTLabsMatitaPrinter.ml @ 765

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

Remove superfluous register in RTLabs return statements.

Also fix up RTLabs prototype pretty printer's handling of global variables.

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