dep.opt regenerated

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 9950b4eb747ded55b256995bd108313d2a9da7ba..28551550d8a21d7abb54af5a4f3664b4a1a74e0e 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -570,11 +570,58 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
          | None -> raise BaseUriNotSetYet)
     | CicNotationPt.Inductive _ -> assert false
     | CicNotationPt.Theorem _ -> None in
-  (*
-  (let time = Unix.gettimeofday () in
+  let time = Unix.gettimeofday () in 
+  let (diff, metasenv, _, cic, _) =
+    singleton "third"
+      (CicDisambiguate.disambiguate_obj 
+        ~lookup_in_library 
+        ~mk_choice:cic_mk_choice
+        ~mk_implicit
+        ~description_of_alias:LexiconAst.description_of_alias
+        ~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);
+  (NCicLibrary.clear_cache ();
+   NCicEnvironment.invalidate ();
+   OCic2NCic.clear ();
    prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE";
    (match obj with
       CicNotationPt.Theorem (_,_,ty,_) ->
+   let graph = 
+     match cic with
+     | Cic.CurrentProof (_,metasenv, _, ty,_,_) ->
+         let _, ugraph = 
+           CicTypeChecker.type_of_aux' metasenv [] ty CicUniv.empty_ugraph
+         in
+           ugraph
+     | Cic.Constant (_,_, ty,_,_) ->
+         let _, ugraph = 
+                 CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph
+         in
+           ugraph
+     | _ -> CicUniv.empty_ugraph
+   in
+(*
+   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) ->
+           List.fold_left
+             (fun graph (uri,_,_) ->
+                let _,g = CicTypeChecker.typecheck uri in
+                CicUniv.merge_ugraphs ~base_ugraph:graph ~increment:(g,uri))
+             graph l)
+       graph (CoercDb.to_list ())
+   in
+   ignore(CicUniv.do_rank graph);
+   let time = Unix.gettimeofday () in
        (try
          (match 
           NCicDisambiguate.disambiguate_term
@@ -603,22 +650,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
        )
     | _ -> ())
   ); 
-  let time = Unix.gettimeofday () in
-  *)
-  let (diff, metasenv, _, cic, _) =
-    singleton "third"
-      (CicDisambiguate.disambiguate_obj 
-        ~lookup_in_library 
-        ~mk_choice:cic_mk_choice
-        ~mk_implicit
-        ~description_of_alias:LexiconAst.description_of_alias
-        ~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