From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 5 Dec 2008 11:29:39 +0000 (+0000)
Subject: still commented, but benchmarks the new/old disambigution process
X-Git-Tag: make_still_working~4455
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6d80ab08869042fc89f54ab781a27045023acd6f;p=helm.git

still commented, but benchmarks the new/old disambigution process
---

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index b02732543..fbbbf6e02 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -571,7 +571,9 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
     | CicNotationPt.Inductive _ -> assert false
     | CicNotationPt.Theorem _ -> None in
   (*
-  (match obj with
+  (let time = Unix.gettimeofday () in
+   prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE";
+   (match obj with
       CicNotationPt.Theorem (_,_,ty,_) ->
        (try
          (match 
@@ -586,8 +588,9 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
            (text,prefix_len,ty)
          with
          | [_,metasenv,subst,ty],_ ->
-          prerr_endline ("NUOVA DISAMBIGUAZIONE OK!!!!!!!!!  " ^
-           NCicPp.ppterm ~metasenv ~subst ~context:[] ty)
+          let time = Unix.gettimeofday () -. time in
+          prerr_endline ("NUOVA DISAMBIGUAZIONE OK: "^ string_of_float time);
+          prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context:[] ty)
          | _ ->
           prerr_endline ("NUOVA DISAMBIGUAZIONE AMBIGUO!!!!!!!!!  "))
        with 
@@ -597,8 +600,9 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
           (List.map (fun _,_,x,_ -> snd (Lazy.force x)) (List.flatten s)))
 (*        | exn -> prerr_endline (Printexc.to_string exn) *)
        )
-    | _ -> ()
+    | _ -> ())
   ); 
+  let time = Unix.gettimeofday () in
   *)
   let (diff, metasenv, _, cic, _) =
     singleton "third"
@@ -610,6 +614,10 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
         ~aliases:lexicon_status.LexiconEngine.aliases
         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri 
         (text,prefix_len,obj)) in
+(*
+  let time = Unix.gettimeofday () -. time in
+  prerr_endline ("VECCHIA DISAMBIGUAZIONE: " ^ string_of_float time);
+*)
   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
   lexicon_status, metasenv, cic