From a7c8e4f4ef4a5f0a15283cd3f0999f3fa24e581d Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 12 Sep 2019 17:03:14 +0200 Subject: Reworked json export. The json export prints formatted json, which takes a lot of additional time, however the result is only consumed by other tools and not meant for human reading. This commit implements several small changes in order to speedup the json export: * Removal of usage of the Format Module * Replacing `fprintf` calls by calls to function that print directly, such as `output_string`, etc. * Replacing list of all instruction names by a set of all instructions --- backend/JsonAST.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/JsonAST.mli') diff --git a/backend/JsonAST.mli b/backend/JsonAST.mli index 7afdce51..c32439e4 100644 --- a/backend/JsonAST.mli +++ b/backend/JsonAST.mli @@ -13,4 +13,4 @@ val pp_mnemonics : Format.formatter -> string list -> unit -val pp_ast : Format.formatter -> (Format.formatter -> Asm.code -> unit) -> (Asm.coq_function AST.fundef, 'a) AST.program -> string -> unit +val pp_ast : out_channel -> (out_channel -> Asm.code -> unit) -> (Asm.coq_function AST.fundef, 'a) AST.program -> string -> unit -- cgit