added unification hint

[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 b02732543b0c541504cd1d82778b5cad43fa8a1a..c1fd03af2225403f5fd3d5204f8a1525cdd34f88 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -570,9 +570,45 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
          | None -> raise BaseUriNotSetYet)
     | CicNotationPt.Inductive _ -> assert false
     | CicNotationPt.Theorem _ -> None in
-  (*
-  (match obj with
+ let try_new cic =
+  (NCicLibrary.clear_cache ();
+   NCicEnvironment.invalidate ();
+   OCic2NCic.clear ();
+   (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);
+   prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE";
+   let time = Unix.gettimeofday () in
        (try
          (match 
           NCicDisambiguate.disambiguate_term
@@ -580,14 +616,16 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
            ~description_of_alias:LexiconAst.description_of_alias
            ~mk_choice:ncic_mk_choice
            ~mk_implicit
+           ~coercion_db:(NCicCoercion.db ())
            ~context:[] ~metasenv:[] ~subst:[]
-        ~aliases:lexicon_status.LexiconEngine.aliases
-        ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) 
+           ~aliases:lexicon_status.LexiconEngine.aliases
+           ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) 
            (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,9 +635,15 @@ 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) *)
        )
-    | _ -> ()
-  ); 
-  *)
+    | _ -> ())
+  )
+ in 
+
+(*
+ try
+  let time = Unix.gettimeofday () in 
+*)
+
   let (diff, metasenv, _, cic, _) =
     singleton "third"
       (CicDisambiguate.disambiguate_obj 
@@ -610,8 +654,26 @@ 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);
+  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
@@ -634,6 +696,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 _