From b615d727f53aaa868f28dd3ba16c988d79e61bba Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Dec 2008 20:38:13 +0000 Subject: [PATCH] more pps --- .../grafite_parser/grafiteDisambiguate.ml | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index c1fd03af2..c5cfa3b29 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -590,12 +590,15 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = ugraph | _ -> CicUniv.empty_ugraph in + (* + prerr_endline "PRIMA COERCIONS"; let _,l = CicUniv.do_rank graph in List.iter (fun k -> prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int (CicUniv.get_rank k))) l; *) + let graph = List.fold_left (fun graph (_,_,l) -> @@ -607,6 +610,17 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = graph (CoercDb.to_list ()) in ignore(CicUniv.do_rank graph); + + +(* + prerr_endline "DOPO COERCIONS"; + let _,l = CicUniv.do_rank graph in + List.iter (fun k -> + prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int + (CicUniv.get_rank k))) l; +*) + + prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE"; let time = Unix.gettimeofday () in (try @@ -639,11 +653,13 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = ) in + (* try let time = Unix.gettimeofday () in *) + let (diff, metasenv, _, cic, _) = singleton "third" (CicDisambiguate.disambiguate_obj @@ -655,6 +671,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = ~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); @@ -662,9 +679,11 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = *) + let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in lexicon_status, metasenv, cic + (* with | Sys.Break as exn -> raise exn @@ -673,6 +692,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = raise exn *) + ;; let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)= -- 2.39.2