From 4cdf45f08cd95641a094312ddc558320b874fa16 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 May 2006 08:29:31 +0000 Subject: [PATCH] utf8_macros moved to syntax_extensions. quoting for inline profiling added --- components/METAS/meta.helm-content_pres.src | 2 +- ...os.src => meta.helm-syntax_extensions.src} | 2 +- components/Makefile | 6 +-- components/acic_content/cicNotationPp.ml | 9 +++- components/binaries/saturate/Makefile | 2 + components/content_pres/Makefile | 2 +- components/grafite_parser/Makefile | 2 +- .../.depend | 0 .../Makefile | 12 ++++- .../README.syntax | 0 .../data/dictionary-tex.xml | 0 .../data/entities-table.xml | 0 .../data/extra-entities.xml | 0 .../make_table.ml | 0 .../pa_unicode_macro.ml | 0 .../syntax_extensions/profiling_macros.ml | 50 +++++++++++++++++++ .../test.ml | 0 .../utf8Macro.ml | 0 .../utf8Macro.mli | 0 .../utf8MacroTable.ml | 0 components/tactics/.depend | 39 ++++++++------- components/tactics/Makefile | 12 +++++ 22 files changed, 110 insertions(+), 28 deletions(-) rename components/METAS/{meta.helm-utf8_macros.src => meta.helm-syntax_extensions.src} (90%) rename components/{utf8_macros => syntax_extensions}/.depend (100%) rename components/{utf8_macros => syntax_extensions}/Makefile (75%) rename components/{utf8_macros => syntax_extensions}/README.syntax (100%) rename components/{utf8_macros => syntax_extensions}/data/dictionary-tex.xml (100%) rename components/{utf8_macros => syntax_extensions}/data/entities-table.xml (100%) rename components/{utf8_macros => syntax_extensions}/data/extra-entities.xml (100%) rename components/{utf8_macros => syntax_extensions}/make_table.ml (100%) rename components/{utf8_macros => syntax_extensions}/pa_unicode_macro.ml (100%) create mode 100644 components/syntax_extensions/profiling_macros.ml rename components/{utf8_macros => syntax_extensions}/test.ml (100%) rename components/{utf8_macros => syntax_extensions}/utf8Macro.ml (100%) rename components/{utf8_macros => syntax_extensions}/utf8Macro.mli (100%) rename components/{utf8_macros => syntax_extensions}/utf8MacroTable.ml (100%) diff --git a/components/METAS/meta.helm-content_pres.src b/components/METAS/meta.helm-content_pres.src index cd3d36854..1706818e2 100644 --- a/components/METAS/meta.helm-content_pres.src +++ b/components/METAS/meta.helm-content_pres.src @@ -1,4 +1,4 @@ -requires="helm-acic_content helm-utf8_macros camlp4.gramlib ulex" +requires="helm-acic_content helm-syntax_extensions camlp4.gramlib ulex" version="0.0.1" archive(byte)="content_pres.cma" archive(native)="content_pres.cmxa" diff --git a/components/METAS/meta.helm-utf8_macros.src b/components/METAS/meta.helm-syntax_extensions.src similarity index 90% rename from components/METAS/meta.helm-utf8_macros.src rename to components/METAS/meta.helm-syntax_extensions.src index c2da77649..5791bc2af 100644 --- a/components/METAS/meta.helm-utf8_macros.src +++ b/components/METAS/meta.helm-syntax_extensions.src @@ -3,5 +3,5 @@ version="0.0.1" archive(byte)="utf8_macros.cma" archive(native)="utf8_macros.cmxa" requires(syntax,preprocessor)="camlp4" -archive(syntax,preprocessor)="pa_extend.cmo pa_unicode_macro.cma" +archive(syntax,preprocessor)="pa_extend.cmo pa_unicode_macro.cma profiling_macros.cma" linkopts="" diff --git a/components/Makefile b/components/Makefile index 6b5e68325..948ba8f36 100644 --- a/components/Makefile +++ b/components/Makefile @@ -11,7 +11,7 @@ MODULES = \ hgdome \ registry \ hmysql \ - utf8_macros \ + syntax_extensions \ thread \ xmldiff \ urimanager \ @@ -49,8 +49,8 @@ else world: all endif syntax-extensions: - $(H)$(MAKE) -C utf8_macros depend - $(H)$(MAKE) -C utf8_macros pa_unicode_macro.cma + $(H)$(MAKE) -C syntax_extensions depend + $(H)$(MAKE) -C syntax_extensions depend: syntax-extensions $(MODULES:%=rec@depend@%) depend.opt: syntax-extensions $(MODULES:%=rec@depend.opt@%) install: $(MODULES:%=rec@install@%) diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml index ee389022c..590de7c54 100644 --- a/components/acic_content/cicNotationPp.ml +++ b/components/acic_content/cicNotationPp.ml @@ -171,9 +171,14 @@ and pp_pattern ((head, href, vars), term) = and pp_patterns patterns = sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns)) -and pp_capture_variable = function +and pp_capture_variable = + let clean s = + let s = String.sub s 1 (String.length s - 1) in + String.sub s 0 (String.length s - 1) + in + function | term, None -> pp_term term - | term, Some typ -> "(" ^ pp_term term ^ ": " ^ pp_term typ ^ ")" + | term, Some typ -> "(" ^ clean (pp_term term) ^ ": " ^ pp_term typ ^ ")" and pp_box_spec (kind, spacing, indent) = let int_of_bool b = if b then 1 else 0 in diff --git a/components/binaries/saturate/Makefile b/components/binaries/saturate/Makefile index 40ff4c3a7..567e3b0d3 100644 --- a/components/binaries/saturate/Makefile +++ b/components/binaries/saturate/Makefile @@ -27,4 +27,6 @@ clean: $(H)rm -f *.cm[iox] *.a *.o $(H)rm -f saturate saturate.opt +depend: + include ../../../Makefile.defs diff --git a/components/content_pres/Makefile b/components/content_pres/Makefile index 5d43e18ab..980e8c25a 100644 --- a/components/content_pres/Makefile +++ b/components/content_pres/Makefile @@ -46,7 +46,7 @@ include ../Makefile.common # cross compatibility among ocaml 3.09 and ocaml 3.08, to be removed as # soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by # "_loc" occurrences -UTF8DIR := $(shell $(OCAMLFIND) query helm-utf8_macros) +UTF8DIR := $(shell $(OCAMLFIND) query helm-syntax_extensions) ULEXDIR := $(shell $(OCAMLFIND) query ulex) MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" cicNotationLexer.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) diff --git a/components/grafite_parser/Makefile b/components/grafite_parser/Makefile index 964b0a86a..06824b141 100644 --- a/components/grafite_parser/Makefile +++ b/components/grafite_parser/Makefile @@ -17,7 +17,7 @@ clean: clean_tests # cross compatibility among ocaml 3.09 and ocaml 3.08, to be removed as # soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by # "_loc" occurrences -UTF8DIR = $(shell $(OCAMLFIND) query helm-utf8_macros) +UTF8DIR = $(shell $(OCAMLFIND) query helm-syntax_extensions) ULEXDIR = $(shell $(OCAMLFIND) query ulex) MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" grafiteParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) diff --git a/components/utf8_macros/.depend b/components/syntax_extensions/.depend similarity index 100% rename from components/utf8_macros/.depend rename to components/syntax_extensions/.depend diff --git a/components/utf8_macros/Makefile b/components/syntax_extensions/Makefile similarity index 75% rename from components/utf8_macros/Makefile rename to components/syntax_extensions/Makefile index 39ef46210..92ed07776 100644 --- a/components/utf8_macros/Makefile +++ b/components/syntax_extensions/Makefile @@ -3,12 +3,12 @@ PREDICATES = MAKE_TABLE_PACKAGES = helm-xml # modules which have both a .ml and a .mli -INTERFACE_FILES = utf8Macro.mli +INTERFACE_FILES = utf8Macro.mli IMPLEMENTATION_FILES = utf8MacroTable.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = -all: utf8_macros.cma pa_unicode_macro.cma +all: utf8_macros.cma pa_unicode_macro.cma profiling_macros.cma make_table: make_table.ml @echo " OCAMLC $<" @@ -27,6 +27,14 @@ pa_unicode_macro.cma: utf8MacroTable.cmo utf8Macro.cmo pa_unicode_macro.cmo @echo " OCAMLC -a $@" $(H)@$(OCAMLFIND) ocamlc -a -o $@ $^ +profiling_macros.cmo: profiling_macros.ml + @echo " OCAMLC $<" + $(H)@$(OCAMLFIND) ocamlc -package camlp4 -pp "camlp4o -loc loc" -c $< +profiling_macros.cma:profiling_macros.cmo + @echo " OCAMLC -a $@" + $(H)@$(OCAMLFIND) ocamlc -a -o $@ $^ + + .PHONY: test test: test.ml $(OCAMLFIND) ocamlc -package helm-utf8_macros -syntax camlp4o $< -o $@ diff --git a/components/utf8_macros/README.syntax b/components/syntax_extensions/README.syntax similarity index 100% rename from components/utf8_macros/README.syntax rename to components/syntax_extensions/README.syntax diff --git a/components/utf8_macros/data/dictionary-tex.xml b/components/syntax_extensions/data/dictionary-tex.xml similarity index 100% rename from components/utf8_macros/data/dictionary-tex.xml rename to components/syntax_extensions/data/dictionary-tex.xml diff --git a/components/utf8_macros/data/entities-table.xml b/components/syntax_extensions/data/entities-table.xml similarity index 100% rename from components/utf8_macros/data/entities-table.xml rename to components/syntax_extensions/data/entities-table.xml diff --git a/components/utf8_macros/data/extra-entities.xml b/components/syntax_extensions/data/extra-entities.xml similarity index 100% rename from components/utf8_macros/data/extra-entities.xml rename to components/syntax_extensions/data/extra-entities.xml diff --git a/components/utf8_macros/make_table.ml b/components/syntax_extensions/make_table.ml similarity index 100% rename from components/utf8_macros/make_table.ml rename to components/syntax_extensions/make_table.ml diff --git a/components/utf8_macros/pa_unicode_macro.ml b/components/syntax_extensions/pa_unicode_macro.ml similarity index 100% rename from components/utf8_macros/pa_unicode_macro.ml rename to components/syntax_extensions/pa_unicode_macro.ml diff --git a/components/syntax_extensions/profiling_macros.ml b/components/syntax_extensions/profiling_macros.ml new file mode 100644 index 000000000..fe5926a43 --- /dev/null +++ b/components/syntax_extensions/profiling_macros.ml @@ -0,0 +1,50 @@ +let max_profilers = 20;; +let profiler_no = ref 0;; +let profiler_label2int = Hashtbl.create 3;; +let name = ref "";; + + +let banner _ pname = + name := pname; + "(Array.make "^string_of_int max_profilers^" (0,0.)), + (Array.make "^string_of_int max_profilers^" (0.))" +;; + +let profile_start _ label = + if !profiler_no > max_profilers then + raise (Invalid_argument "Too many profilers."); + if not (Hashtbl.mem profiler_label2int label) then + begin + Hashtbl.add profiler_label2int label !profiler_no; + incr profiler_no; + end; + let id = Hashtbl.find profiler_label2int label in + " ((snd "^ !name^").("^string_of_int id^") <- Unix.gettimeofday()) " +;; + +let profile_stop _ label = + if not (Hashtbl.mem profiler_label2int label) then + raise (Invalid_argument "Profiler 'stop' before 'begin'."); + let id = Hashtbl.find profiler_label2int label in + " ( + let interval = + Unix.gettimeofday () -. (snd "^ !name^").("^string_of_int id^") + in + let oldcount,oldval = (fst "^ !name^").("^string_of_int id^") in + (fst "^ !name^").("^string_of_int id^") <- (oldcount+1,interval +. oldval) + ) " +;; + +let profile_show _ _ = + (Hashtbl.fold + (fun k v acc -> + acc ^ + "let t = (fst "^ !name^").("^string_of_int v^") in "^ + "let acc = acc ^ Printf.sprintf \"%20s: %5d %8.4f\" \""^k^"\" (fst t) (snd t) in") + profiler_label2int "let acc = \"\" in ") ^ " acc " +;; + +Quotation.add "profiler" (Quotation.ExStr banner);; +Quotation.add "start" (Quotation.ExStr profile_start);; +Quotation.add "stop" (Quotation.ExStr profile_stop);; +Quotation.add "show" (Quotation.ExStr profile_show);; diff --git a/components/utf8_macros/test.ml b/components/syntax_extensions/test.ml similarity index 100% rename from components/utf8_macros/test.ml rename to components/syntax_extensions/test.ml diff --git a/components/utf8_macros/utf8Macro.ml b/components/syntax_extensions/utf8Macro.ml similarity index 100% rename from components/utf8_macros/utf8Macro.ml rename to components/syntax_extensions/utf8Macro.ml diff --git a/components/utf8_macros/utf8Macro.mli b/components/syntax_extensions/utf8Macro.mli similarity index 100% rename from components/utf8_macros/utf8Macro.mli rename to components/syntax_extensions/utf8Macro.mli diff --git a/components/utf8_macros/utf8MacroTable.ml b/components/syntax_extensions/utf8MacroTable.ml similarity index 100% rename from components/utf8_macros/utf8MacroTable.ml rename to components/syntax_extensions/utf8MacroTable.ml diff --git a/components/tactics/.depend b/components/tactics/.depend index 360128fce..e94cfa5ab 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -7,12 +7,13 @@ primitiveTactics.cmi: proofEngineTypes.cmi metadataQuery.cmi: proofEngineTypes.cmi paramodulation/equality.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi -paramodulation/inference.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \ - paramodulation/equality.cmi +paramodulation/inference.cmi: paramodulation/utils.cmi \ + paramodulation/subst.cmi proofEngineTypes.cmi paramodulation/equality.cmi paramodulation/equality_indexing.cmi: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/indexing.cmi: paramodulation/utils.cmi \ - paramodulation/equality_indexing.cmi paramodulation/equality.cmi + paramodulation/subst.cmi paramodulation/equality_indexing.cmi \ + paramodulation/equality.cmi paramodulation/saturation.cmi: proofEngineTypes.cmi variousTactics.cmi: proofEngineTypes.cmi autoTactic.cmi: proofEngineTypes.cmi @@ -67,28 +68,32 @@ paramodulation/equality.cmo: paramodulation/utils.cmi \ paramodulation/equality.cmx: paramodulation/utils.cmx \ paramodulation/subst.cmx proofEngineReduction.cmx \ paramodulation/equality.cmi -paramodulation/inference.cmo: paramodulation/utils.cmi proofEngineHelpers.cmi \ - metadataQuery.cmi paramodulation/equality.cmi \ - paramodulation/inference.cmi -paramodulation/inference.cmx: paramodulation/utils.cmx proofEngineHelpers.cmx \ - metadataQuery.cmx paramodulation/equality.cmx \ - paramodulation/inference.cmi +paramodulation/inference.cmo: paramodulation/utils.cmi \ + paramodulation/subst.cmi proofEngineHelpers.cmi metadataQuery.cmi \ + paramodulation/equality.cmi paramodulation/inference.cmi +paramodulation/inference.cmx: paramodulation/utils.cmx \ + paramodulation/subst.cmx proofEngineHelpers.cmx metadataQuery.cmx \ + paramodulation/equality.cmx paramodulation/inference.cmi paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/equality_indexing.cmi paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \ paramodulation/equality.cmx paramodulation/equality_indexing.cmi paramodulation/indexing.cmo: paramodulation/utils.cmi \ - paramodulation/inference.cmi paramodulation/equality_indexing.cmi \ - paramodulation/equality.cmi paramodulation/indexing.cmi + paramodulation/subst.cmi paramodulation/inference.cmi \ + paramodulation/equality_indexing.cmi paramodulation/equality.cmi \ + paramodulation/indexing.cmi paramodulation/indexing.cmx: paramodulation/utils.cmx \ - paramodulation/inference.cmx paramodulation/equality_indexing.cmx \ - paramodulation/equality.cmx paramodulation/indexing.cmi -paramodulation/saturation.cmo: paramodulation/utils.cmi reductionTactics.cmi \ - proofEngineTypes.cmi proofEngineReduction.cmi primitiveTactics.cmi \ + paramodulation/subst.cmx paramodulation/inference.cmx \ + paramodulation/equality_indexing.cmx paramodulation/equality.cmx \ + paramodulation/indexing.cmi +paramodulation/saturation.cmo: paramodulation/utils.cmi \ + paramodulation/subst.cmi reductionTactics.cmi proofEngineTypes.cmi \ + proofEngineReduction.cmi primitiveTactics.cmi \ paramodulation/inference.cmi paramodulation/indexing.cmi \ paramodulation/equality.cmi paramodulation/saturation.cmi -paramodulation/saturation.cmx: paramodulation/utils.cmx reductionTactics.cmx \ - proofEngineTypes.cmx proofEngineReduction.cmx primitiveTactics.cmx \ +paramodulation/saturation.cmx: paramodulation/utils.cmx \ + paramodulation/subst.cmx reductionTactics.cmx proofEngineTypes.cmx \ + proofEngineReduction.cmx primitiveTactics.cmx \ paramodulation/inference.cmx paramodulation/indexing.cmx \ paramodulation/equality.cmx paramodulation/saturation.cmi variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ diff --git a/components/tactics/Makefile b/components/tactics/Makefile index 1fe925282..5538c15a0 100644 --- a/components/tactics/Makefile +++ b/components/tactics/Makefile @@ -32,6 +32,18 @@ tactics.mli: $(H)echo "(* GENERATED FILE, DO NOT EDIT. STAMP:`date` *)" > $@ $(H)$(OCAMLC) -I paramodulation -i $(tactics_mli_deps) >> $@ +UTF8DIR = $(shell $(OCAMLFIND) query helm-syntax_extensions) +MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) pa_extend.cmo profiling_macros.cma -loc loc" +paramodulation/saturation.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) +paramodulation/saturation.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) +depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) +depend.opt: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) +# +# +paramodulation/saturation.cmo: OCAMLC = $(OCAMLC_P4) +paramodulation/saturation.cmx: OCAMLOPT = $(OCAMLOPT_P4) + + STATS_EXCLUDE = tactics.mli include ../../Makefile.defs -- 2.39.2