1

我编写了一个解析器程序（用 OCaml 编写），它接受一个输入是一个 xsd，然后将它生成到 Coq 文件。但是在终端中生成需要很长时间（~：0m.0152s）。我想知道一些建议以使 praser 运行得更快？例如，使程序变慢的原因是什么？这是我第一次遇到这个运行时间问题。所以我非常感谢任何关于它的建议/经验？

非常感谢你

编辑：我可以尝试通过主文件来解释：

open Libxml;; (*it is the library for xml file*)
open Error;; (* it is for the error message*)

let main () =     
  let xml = parse_xml stdin in
  let xsds = Xsd_of_xml.xsd_of_xml xml in (* It is a parsing from xml to xsds *)
  let b = Buffer.create 10000 in

  Coq_of_xsd.genr_coq b xsds; (* It is a parsing from xsds to Coq type *)
  Buffer.output_buffer stdout b;;

let _ = run main;;

我这样写Makefile.xsd2coq：

MAIN := xsd2coq

FILES := util error libxml xsd scc xsd_of_xml coqxsd_matrix coqxsd_print coq_of_xsd

FRAGILE_FILES := xsd coqxsd_matrix coqxsd_print coq_of_xsd

LIBS := xml-light/xml-light

INCLUDES := -I xml-light

coq_of_xsd.cmo coq_of_xsd.cmx libxml.cmo libxml.cmx: WARNINGS = -warn-error Aezk

include Makefile.ocaml

在一个主要的：Makefile

xsd2coq: FORCE
    $(MAKE) -f Makefile.xsd2coq depend
    $(MAKE) -f Makefile.xsd2coq
4

1 回答 1

2

当我测试我的解析器组合器时，我使用的是. 我已经看到 70% 的时间都花在了块分配上。也许探查器输出将帮助您找到类似的问题。

于 2013-10-21T10:26:09.573 回答