- Grammar for all obj commands ported to NG (let recs and inductives still need

[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 4ea3a95b3889cb6784cb77522e809e773039f836..b5c08fba696b979333991ed9f1d661688d9c6fc3 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -89,15 +89,32 @@ let ncic_mk_choice = function
   | LexiconAst.Ident_alias (name, uri) -> 
      uri, `Sym_interp 
       (fun l->assert(l = []);
-        if String.sub uri 5 9 = "ng_matita" then
-         let nuri =
+        let nuri = NUri.uri_of_string uri in
+        try
+         let _,height,_,_,_ = NCicEnvironment.get_checked_obj nuri in
+          NCic.Const
+           (NReference.reference_of_spec nuri (NReference.Def height))
+        with
+         NCicEnvironment.ObjectNotFound _ ->
+(*
+(*
+        if String.sub uri (String.length uri - 3) 3 = "def" then
+*)
+         let nuri = NUri.uri_of_string uri in(*
           NUri.uri_of_string (String.sub uri 0 (String.length uri -3) ^ "def")
          in
+*)
           NCic.Const
            (NReference.reference_of_spec nuri (NReference.Def 0))
+)
+*)
+(*
         else
+*)
          let uri = UriManager.uri_of_string uri in
           fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+(*
+*)
 ;;
 
 
@@ -740,7 +757,36 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
  | exn ->
 (*    try_new None; *)
    raise exn
+;;
 
+let disambiguate_nobj lexicon_status ?baseuri (text,prefix_len,obj) =
+  let uri =
+   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 diff, _, _, cic =
+   singleton "third"
+    (NCicDisambiguate.disambiguate_obj
+      ~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 ())
+      ~aliases:lexicon_status.LexiconEngine.aliases
+      ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) 
+      (text,prefix_len,obj)) in
+  let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+  lexicon_status, cic
 ;;
   
 let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=