diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2015-06-23 18:02:30 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2015-06-23 18:04:11 +0200 |
commit | 5f7adad4af7d526aed3a97f8b24b2d9811f9fea7 (patch) | |
tree | d64fd513d3233715ad4d9c14b6e65672e60e1030 /kernel/cbytegen.ml | |
parent | b28bafb1d2003558c916c75d36784f94e9aa1684 (diff) |
Add a Set Dump Bytecode command for debugging purposes.
Prints the VM bytecode produced by compilation of a constant or a call to
vm_compute.
Diffstat (limited to 'kernel/cbytegen.ml')
-rw-r--r-- | kernel/cbytegen.ml | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 07fab06a4..ac46dc583 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -772,16 +772,18 @@ let compile fail_on_error env c = try let init_code = compile_constr reloc c 0 [Kstop] in let fv = List.rev (!(reloc.in_env).fv_rev) in -(* draw_instr init_code; - draw_instr !fun_code; - Format.print_string "fv = "; - List.iter (fun v -> - match v with - | FVnamed id -> Format.print_string ((Id.to_string id)^"; ") - | FVrel i -> Format.print_string ((string_of_int i)^"; ")) fv; Format - .print_string "\n"; - Format.print_flush(); *) - Some (init_code,!fun_code, Array.of_list fv) + let pp_v v = + match v with + | FVnamed id -> Pp.str (Id.to_string id) + | FVrel i -> Pp.str (string_of_int i) + in + let open Pp in + if !Flags.dump_bytecode then + (dump_bytecode init_code; + dump_bytecode !fun_code; + Pp.msg_debug (Pp.str "fv = " ++ + Pp.prlist_with_sep (fun () -> Pp.str "; ") pp_v fv ++ Pp.fnl ())); + Some (init_code,!fun_code, Array.of_list fv) with TooLargeInductive tname -> let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in (Pp.(fn |