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