- fixed hint generation, more hints are generated

[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 9f63a5d8f6bd52a8a1d979d84d8ea957b47f6a93..32d666a384eaa69a04310f9f2dfa6ecadaa91593 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -561,21 +561,22 @@ let rec disambiguate_tactic
 
 let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
   let uri =
-   match obj with
-    | CicNotationPt.Inductive (_,(name,_,_,_)::_)
-    | CicNotationPt.Record (_,name,_,_) ->
-       (match baseuri with
-         | Some baseuri ->
-            Some (UriManager.uri_of_string (baseuri ^ "/" ^ name ^ ".ind"))
-         | None -> raise BaseUriNotSetYet)
-    | CicNotationPt.Inductive _ -> assert false
-    | CicNotationPt.Theorem _ -> None in
+   let baseuri = 
+     match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
+   in
+   let name = 
+     match obj with
+     | CicNotationPt.Inductive (_,(name,_,_,_)::_)
+     | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
+     | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con"
+     | CicNotationPt.Inductive _ -> assert false
+   in
+     UriManager.uri_of_string (baseuri ^ "/" ^ name)
+  in
  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,_,_) ->
@@ -625,39 +626,45 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
    let time = Unix.gettimeofday () in
        (try
          (match 
-          NCicDisambiguate.disambiguate_term
+          NCicDisambiguate.disambiguate_obj
            ~lookup_in_library:lookup_in_library
            ~description_of_alias:LexiconAst.description_of_alias
            ~mk_choice:ncic_mk_choice
            ~mk_implicit
+           ~uri:(OCic2NCic.nuri_of_ouri uri)
            ~coercion_db:(NCicCoercion.db ())
-           ~context:[] ~metasenv:[] ~subst:[]
            ~aliases:lexicon_status.LexiconEngine.aliases
            ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) 
-           (text,prefix_len,ty)
+           (text,prefix_len,obj)
          with
-         | [_,metasenv,subst,ty],_ ->
+         | [_,_,_,obj],_ ->
           let time = Unix.gettimeofday () -. time in
+(*           NCicTypeChecker.typecheck_obj obj; *)
           prerr_endline ("NUOVA DISAMBIGUAZIONE OK: "^ string_of_float time);
-          prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context:[] ty)
+(*
+          let obj = 
+            let u,i,m,_,o = obj in
+            u,i,m,[],o
+          in
+*)
+          prerr_endline (NCicPp.ppobj obj)
          | _ ->
           prerr_endline ("NUOVA DISAMBIGUAZIONE AMBIGUO!!!!!!!!!  "))
        with 
        | MultiPassDisambiguator.DisambiguationError (_,s) ->
-        prerr_endline ("ERRORE NUOVA DISAMBIGUAZIONE:\n" ^
+        prerr_endline ("ERRORE NUOVA DISAMBIGUAZIONE ("
+          ^UriManager.string_of_uri uri^
+          "):\n" ^
          String.concat "\n" 
           (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 time = Unix.gettimeofday () in  *)
 
 
   let (diff, metasenv, _, cic, _) =
@@ -668,30 +675,26 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
         ~mk_implicit
         ~description_of_alias:LexiconAst.description_of_alias
         ~aliases:lexicon_status.LexiconEngine.aliases
-        ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri 
+        ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) 
+        ~uri:(Some uri)
         (text,prefix_len,obj)) in
 
 
 (*
   let time = Unix.gettimeofday () -. time in
-  prerr_endline ("VECCHIA DISAMBIGUAZIONE: " ^ string_of_float time);
-  try_new cic;
+  prerr_endline ("VECCHIA DISAMBIGUAZIONE ("^
+    UriManager.string_of_uri uri ^"): " ^ 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
-*)
-
 
 ;;