Experimental enhancements to the ndestruct tactic. By using the syntax

[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 6b5dfca61b829235b852cdc4e7f0a44cd6d52501..7ce0407e85d58e24a481f023b024a0eb49159368 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -81,12 +81,18 @@ let ncic_mk_choice = function
         ~term_of_nref:(fun nref -> NCic.Const nref)
        name dsc
   | LexiconAst.Number_alias (_, dsc) -> 
-       let desc,f = DisambiguateChoices.lookup_num_by_dsc dsc in
-       desc, `Num_interp
+     (try
+       let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
+        desc, `Num_interp
+         (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
+      with
+       DisambiguateChoices.Choice_not_found _ ->
+        let desc,f = DisambiguateChoices.lookup_num_by_dsc dsc in
+        desc, `Num_interp
          (fun num -> 
             fst (OCic2NCic.convert_term 
               (UriManager.uri_of_string "cic:/xxx/x.con") 
-              (match f with `Num_interp f -> f num | _ -> assert false)))
+              (match f with `Num_interp f -> f num | _ -> assert false))))
   | LexiconAst.Ident_alias (name, uri) -> 
      uri, `Sym_interp 
       (fun l->assert(l = []);
@@ -175,6 +181,24 @@ let nlookup_in_library
   | _ -> lookup_in_library interactive_user_uri_choice input_or_locate_uri item 
 ;;
 
+let fix_instance item l =
+ match item with
+    DisambiguateTypes.Symbol (_,n) ->
+     List.map
+      (function
+          LexiconAst.Symbol_alias (s,_,d) -> LexiconAst.Symbol_alias (s,n,d)
+        | _ -> assert false
+      ) l
+  | DisambiguateTypes.Num n ->
+     List.map
+      (function
+          LexiconAst.Number_alias (_,d) -> LexiconAst.Number_alias (n,d)
+        | _ -> assert false
+      ) l
+  | DisambiguateTypes.Id _ -> l
+;;
+
+
   (** @param term not meaningful when context is given *)
 let disambiguate_term expty text prefix_len lexicon_status_ref context metasenv
 term =
@@ -186,7 +210,7 @@ term =
         ~expty ~universe:(Some lexicon_status#lstatus.LexiconEngine.multi_aliases)
         ~lookup_in_library
         ~mk_choice:cic_mk_choice
-        ~mk_implicit
+        ~mk_implicit ~fix_instance
         ~description_of_alias:LexiconAst.description_of_alias
         ~context ~metasenv ~subst:[] (text,prefix_len,term))
   in
@@ -206,7 +230,7 @@ let disambiguate_nterm expty estatus context metasenv subst thing
         ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
         ~lookup_in_library:nlookup_in_library
         ~mk_choice:ncic_mk_choice
-        ~mk_implicit
+        ~mk_implicit ~fix_instance
         ~description_of_alias:LexiconAst.description_of_alias
         ~context ~metasenv ~subst thing)
   in
@@ -228,7 +252,7 @@ let disambiguate_lazy_term expty text prefix_len lexicon_status_ref term =
         (CicDisambiguate.disambiguate_term 
           ~lookup_in_library
           ~mk_choice:cic_mk_choice
-          ~mk_implicit
+          ~mk_implicit ~fix_instance
           ~description_of_alias:LexiconAst.description_of_alias
           ~initial_ugraph:ugraph ~aliases:lexicon_status#lstatus.LexiconEngine.aliases
           ~universe:(Some lexicon_status#lstatus.LexiconEngine.multi_aliases)
@@ -283,15 +307,18 @@ let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
 ;;
 
 let disambiguate_auto_params 
-  disambiguate_term metasenv context (terms, params) 
+  disambiguate_term metasenv context (oterms, params) 
 =
-    let metasenv, terms = 
-      List.fold_right 
-       (fun t (metasenv, terms) ->
-         let metasenv,t = disambiguate_term context metasenv t in
-         metasenv,t::terms) terms (metasenv, [])
-    in
-    metasenv, (terms, params)
+  match oterms with 
+    | None -> metasenv, (None, params)
+    | Some terms ->
+       let metasenv, terms = 
+         List.fold_right 
+           (fun t (metasenv, terms) ->
+               let metasenv,t = disambiguate_term context metasenv t in
+                metasenv,t::terms) terms (metasenv, [])
+       in
+         metasenv, (Some terms, params)
 ;;
 
 let disambiguate_just disambiguate_term context metasenv =
@@ -628,7 +655,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
      match obj with
      | CicNotationPt.Inductive (_,(name,_,_,_)::_)
      | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
-     | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con"
+     | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
      | CicNotationPt.Inductive _ -> assert false
    in
      UriManager.uri_of_string (baseuri ^ "/" ^ name)
@@ -734,7 +761,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
       (CicDisambiguate.disambiguate_obj 
         ~lookup_in_library 
         ~mk_choice:cic_mk_choice
-        ~mk_implicit
+        ~mk_implicit ~fix_instance
         ~description_of_alias:LexiconAst.description_of_alias
         ~aliases:estatus#lstatus.LexiconEngine.aliases
         ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) 
@@ -770,7 +797,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
      match obj with
      | CicNotationPt.Inductive (_,(name,_,_,_)::_)
      | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
-     | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con"
+     | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
      | CicNotationPt.Inductive _ -> assert false
    in
      UriManager.uri_of_string (baseuri ^ "/" ^ name)
@@ -781,7 +808,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
       ~lookup_in_library:nlookup_in_library
       ~description_of_alias:LexiconAst.description_of_alias
       ~mk_choice:ncic_mk_choice
-      ~mk_implicit
+      ~mk_implicit ~fix_instance
       ~uri:(OCic2NCic.nuri_of_ouri uri)
       ~rdb:estatus
       ~aliases:estatus#lstatus.LexiconEngine.aliases