From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 9 Dec 2008 18:30:47 +0000 (+0000)
Subject: new disambiguatio attached with the right universe graph
X-Git-Tag: make_still_working~4423
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=09aa78d84b199053e089052890455f5fcd411f50;p=helm.git

new disambiguatio attached with the right universe graph
---

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 9950b4eb7..bcbcf9c93 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -570,11 +570,51 @@ 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 (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 time = Unix.gettimeofday () in
    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 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);
        (try
          (match 
           NCicDisambiguate.disambiguate_term
@@ -603,21 +643,6 @@ 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