1

入力を xsd とするパーサープログラム (OCaml で作成) を作成し、それを 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 に答える