new tactics are almost ready

[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 23ec1770edc387d5ea7f0fd0663264b1114564e5..027cde4a599d090787e1e2d86661577444df8e8f 100644 (file)
--- 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)
@@ -253,7 +273,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 +596,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 +724,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 =