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