Quick&dirty implementation of neqd:

[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 323c8985edae63b82aac8b090a8258eaaa08d767..4ea3a95b3889cb6784cb77522e809e773039f836 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -89,8 +89,15 @@ let ncic_mk_choice = function
   | LexiconAst.Ident_alias (name, uri) -> 
      uri, `Sym_interp 
       (fun l->assert(l = []);
-      let uri = UriManager.uri_of_string uri in
-       fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+        if String.sub uri 5 9 = "ng_matita" then
+         let nuri =
+          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)))
 ;;
 
 
@@ -664,7 +671,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
        (try
          (match 
           NCicDisambiguate.disambiguate_obj
-           ~lookup_in_library:lookup_in_library
+           ~lookup_in_library
            ~description_of_alias:LexiconAst.description_of_alias
            ~mk_choice:ncic_mk_choice
            ~mk_implicit
@@ -752,6 +759,10 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
        in
        let metasenv,key = disambiguate_term_option metasenv key in
        !lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri)
+   | GrafiteAst.Select (loc,uri) -> 
+        lexicon_status, metasenv, GrafiteAst.Select(loc,uri)
+   | GrafiteAst.Pump(loc,i) -> 
+        lexicon_status, metasenv, GrafiteAst.Pump(loc,i)
    | GrafiteAst.PreferCoercion (loc,t) -> 
        let lexicon_status_ref = ref lexicon_status in 
        let disambiguate_term =
@@ -764,6 +775,11 @@ 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.Inverter (loc,n,indty,params) ->
+       let lexicon_status_ref = ref lexicon_status in
+       let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in
+      let metasenv,indty = disambiguate_term metasenv indty in
+      !lexicon_status_ref, metasenv, GrafiteAst.Inverter (loc,n,indty,params)
    | GrafiteAst.UnificationHint (loc, t, n) ->
        let lexicon_status_ref = ref lexicon_status in 
        let disambiguate_term =
@@ -775,6 +791,7 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
    | GrafiteAst.Include _
    | GrafiteAst.Print _
    | GrafiteAst.Qed _
+   | GrafiteAst.NQed _
    | GrafiteAst.Set _ as cmd ->
        lexicon_status,metasenv,cmd
    | GrafiteAst.Obj (loc,obj) ->