From 6d80ab08869042fc89f54ab781a27045023acd6f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 5 Dec 2008 11:29:39 +0000 Subject: [PATCH] still commented, but benchmarks the new/old disambigution process --- .../grafite_parser/grafiteDisambiguate.ml | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) 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 -- 2.39.2