X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=323c8985edae63b82aac8b090a8258eaaa08d767;hb=1c950d8cfe400f6b68eee7a67c555549db3a4d36;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..323c8985e 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -153,14 +153,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 +172,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 +209,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 +234,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 +287,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 +610,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 ();
@@ -701,6 +738,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 =