From 927b0dc91ca0369dd029c43ffe9258e17908fa38 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 Apr 2005 12:12:08 +0000 Subject: [PATCH] added parsing time benchmark universes generation counter is now properly reset added orrible hack to make the parser generate proper universes containig the uri --- helm/ocaml/cic_proof_checking/cicEnvironment.ml | 16 ++++++++++++---- helm/ocaml/cic_proof_checking/cicEnvironment.mli | 3 +++ 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index be0be0add..08166d564 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -476,6 +476,8 @@ let dump_to_channel = Cache.dump_to_channel;; let restore_from_channel = Cache.restore_from_channel;; let empty = Cache.empty;; +let total_parsing_time = ref 0.0 + let get_object_to_add uri = let filename = Http_getter.getxml' uri in let bodyfilename = @@ -506,12 +508,18 @@ let get_object_to_add uri = | None -> () end in - (* this brakes something : - * let _ = CicUniv.restart_numbering () in - *) + (* restarts the numbering of named universes (the ones inside the cic) *) + let _ = CicUniv.restart_numbering () in + (* HACK ORRIBILE: fa in modo che il parser metta degli universi fresh non + * anonimi *) + let _ = CicParser3.set_uri uri in let obj = try - CicParser.obj_of_xml filename bodyfilename + let time = Unix.gettimeofday() in + let rc = CicParser.obj_of_xml filename bodyfilename in + total_parsing_time := + !total_parsing_time +. ((Unix.gettimeofday()) -. time ); + rc with exn -> cleanup (); (match exn with diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index ce6a7f225..6108467b5 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -126,4 +126,7 @@ val list_uri: unit -> UriManager.uri list (** @return true for objects available in the library *) val in_library: UriManager.uri -> bool + (** total parsing time, only to benchmark the parser *) +val total_parsing_time: float ref + (* EOF *) -- 2.39.2