X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=4ea3a95b3889cb6784cb77522e809e773039f836;hb=585469505faa97c21687128490828a1aabee94ee;hp=23ec1770edc387d5ea7f0fd0663264b1114564e5;hpb=4573f1fecaf83f4706f39702555d5319d132477b;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 23ec1770e..4ea3a95b3 100644
--- 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)))
 ;;
 
 
@@ -153,14 +160,14 @@ let lookup_in_library
 ;;
 
   (** @param term not meaningful when context is given *)
-let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv
+let disambiguate_term expty text prefix_len lexicon_status_ref context metasenv
 term =
   let lexicon_status = !lexicon_status_ref in
   let (diff, metasenv, subst, cic, _) =
     singleton "first"
       (CicDisambiguate.disambiguate_term
         ~aliases:lexicon_status.LexiconEngine.aliases
-        ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+        ~expty ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
         ~lookup_in_library
         ~mk_choice:cic_mk_choice
         ~mk_implicit
@@ -172,12 +179,32 @@ term =
   metasenv,(*subst,*) cic
 ;;
 
+let disambiguate_nterm expty lexicon_status context metasenv subst thing
+=
+  let diff, metasenv, subst, cic =
+    singleton "first"
+      (NCicDisambiguate.disambiguate_term
+        ~coercion_db:(NCicCoercion.db ())
+        ~aliases:lexicon_status.LexiconEngine.aliases
+        ~expty 
+        ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+        ~lookup_in_library
+        ~mk_choice:ncic_mk_choice
+        ~mk_implicit
+        ~description_of_alias:LexiconAst.description_of_alias
+        ~context ~metasenv ~subst thing)
+  in
+  let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+  metasenv, subst, lexicon_status, cic
+;;
+
+
   (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
    * rationale: lazy_term will be invoked in different context to obtain a term,
    * each invocation will disambiguate the term and can add aliases. Once all
    * disambiguations have been performed, the first returned function can be
    * used to obtain the resulting aliases *)
-let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term =
+let disambiguate_lazy_term expty text prefix_len lexicon_status_ref term =
   (fun context metasenv ugraph ->
     let lexicon_status = !lexicon_status_ref in
     let (diff, metasenv, _, cic, ugraph) =
@@ -189,8 +216,8 @@ let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term =
           ~description_of_alias:LexiconAst.description_of_alias
           ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
           ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
-          ~context ~metasenv ~subst:[] ?goal
-          (text,prefix_len,term)) in
+          ~context ~metasenv ~subst:[] 
+          (text,prefix_len,term) ~expty) in
     let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
     lexicon_status_ref := lexicon_status;
     cic, metasenv, ugraph)
@@ -214,6 +241,20 @@ let disambiguate_pattern
   (wanted, hyp_paths, goal_path)
 ;;
 
+type pattern = 
+  CicNotationPt.term Disambiguate.disambiguator_input option * 
+  (string * NCic.term) list * NCic.term option
+
+let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
+  let interp path = NCicDisambiguate.disambiguate_path path in
+  let goal_path = HExtlib.map_option interp goal_path in
+  let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
+  let wanted = 
+    match wanted with None -> None | Some x -> Some (text,prefix_len,x)
+  in
+   (wanted, hyp_paths, goal_path)
+;;
+
 let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
   | `Unfold (Some t) ->
       let t = 
@@ -253,7 +294,10 @@ let rec disambiguate_tactic
   lexicon_status_ref context metasenv goal (text,prefix_len,tactic) 
 =
   let disambiguate_term_hint = 
-    disambiguate_term goal text prefix_len lexicon_status_ref in
+    let _,_,expty = 
+      List.find (fun (x,_,_) -> Some x = goal) metasenv
+    in
+    disambiguate_term (Some expty) text prefix_len lexicon_status_ref in
   let disambiguate_term = 
     disambiguate_term None text prefix_len lexicon_status_ref in
   let disambiguate_pattern = 
@@ -573,7 +617,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
    in
      UriManager.uri_of_string (baseuri ^ "/" ^ name)
   in
- let try_new cic =
+ let _try_new cic =
   (NCicLibrary.clear_cache ();
    NCicEnvironment.invalidate ();
    OCic2NCic.clear ();
@@ -627,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
@@ -701,6 +745,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
   
 let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
   match cmd with
+   | GrafiteAst.NObj(loc,obj) -> lexicon_status, metasenv, GrafiteAst.NObj(loc,obj)
    | GrafiteAst.Index(loc,key,uri) ->
        let lexicon_status_ref = ref lexicon_status in 
        let disambiguate_term =
@@ -714,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 =
@@ -726,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 =
@@ -737,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) ->