X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=c5cfa3b290fbae393fd589095258e1789b5dabc2;hb=5be81fce195f2b45ec57c5422d35e4c03827891d;hp=bb7508bd9737aa2bff62ad1275d569aa74dac546;hpb=2050f08c3db678506f6e356cd6f0eb6ac72e7cf1;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index bb7508bd9..c5cfa3b29 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -570,20 +570,7 @@ 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 try_new cic =
   (NCicLibrary.clear_cache ();
    NCicEnvironment.invalidate ();
    OCic2NCic.clear ();
@@ -603,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) ->
@@ -620,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
@@ -649,10 +650,50 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
 (*        | exn -> prerr_endline (Printexc.to_string exn) *)
        )
     | _ -> ())
-  ); 
-  
+  )
+ in 
+
+
+(*
+ try
+  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);
+  try_new cic;
+*)
+
+
+
   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
   lexicon_status, metasenv, cic
+
+
+(*
+ with 
+ | Sys.Break as exn -> raise exn
+ | exn ->
+   try_new (Cic.InductiveDefinition ([],[],0,[])); 
+   raise exn
+*)
+
+
+;;
   
 let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
   match cmd with
@@ -675,6 +716,12 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
 	 disambiguate_term None text prefix_len lexicon_status_ref [] in
       let metasenv,t = disambiguate_term metasenv t in
       !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
+   | GrafiteAst.UnificationHint (loc, t) ->
+       let lexicon_status_ref = ref lexicon_status in 
+       let disambiguate_term =
+	 disambiguate_term None text prefix_len lexicon_status_ref [] in
+      let metasenv,t = disambiguate_term metasenv t in
+      !lexicon_status_ref, metasenv, GrafiteAst.UnificationHint (loc,t)
    | GrafiteAst.Default _
    | GrafiteAst.Drop _
    | GrafiteAst.Include _