coercions are there, but not heavily tested

[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..9950b4eb747ded55b256995bd108313d2a9da7ba 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -571,7 +571,9 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
     | CicNotationPt.Inductive _ -> assert false
     | CicNotationPt.Theorem _ -> None in
   (*
-  (match obj with
+  (let time = Unix.gettimeofday () in
+   prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE";
+   (match obj with
       CicNotationPt.Theorem (_,_,ty,_) ->
        (try
          (match 
@@ -580,14 +582,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,8 +601,9 @@ 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) *)
        )
-    | _ -> ()
+    | _ -> ())
   ); 
+  let time = Unix.gettimeofday () in
   *)
   let (diff, metasenv, _, cic, _) =
     singleton "third"
@@ -610,6 +615,10 @@ 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);
+*)
   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
   lexicon_status, metasenv, cic