source: src/RTLabs/RTLabsMatitaPrinter.ml @ 750

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

Track some of the changes to the prototype in RTLabs.

Just one register in each place now, f_ptrs is present but not checked.
The changes to memory quantities have been glossed over for now.
A new difference from the prototype: return registers are optional.

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