One-shot aliases were no longer generated because of a bug (i.e. all aliases

retrieved from the universe used to have instance=0). Fixed by parameterizing
once again all the functions with a ~fix_instance function to fix the instance.

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
index 853c38e4b762cb6114c8ccf77db8cddda098e0ef..8f8bba7d81e2ba69923ca1e92cab72109c988296 100644 (file)
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
@@ -649,13 +649,14 @@ let string_context_of_context =
 
 let disambiguate_term ~context ~metasenv ~subst ~expty 
   ?(initial_ugraph = CicUniv.oblivion_ugraph)
-  ~mk_implicit ~description_of_alias ~mk_choice
+  ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
   ~aliases ~universe ~lookup_in_library (text,prefix_len,term)
 =
   let mk_localization_tbl x = Cic.CicHash.create x in
    MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
     ~initial_ugraph ~aliases ~string_context_of_context
     ~universe ~lookup_in_library ~mk_implicit ~description_of_alias
+    ~fix_instance
     ~uri:None ~pp_thing:CicNotationPp.pp_term
     ~domain_of_thing:Disambiguate.domain_of_term
     ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
@@ -665,7 +666,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty
     ~freshen_thing:CicNotationUtil.freshen_term
     ~passes:(MultiPassDisambiguator.passes ())
 
-let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
+let disambiguate_obj ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
  ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
 =
   let mk_localization_tbl x = Cic.CicHash.create x in
@@ -673,7 +674,7 @@ let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
     ~aliases ~universe ~uri ~string_context_of_context
     ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
     ~domain_of_thing:Disambiguate.domain_of_obj
-    ~lookup_in_library ~mk_implicit ~description_of_alias
+    ~lookup_in_library ~mk_implicit ~description_of_alias ~fix_instance
     ~initial_ugraph:CicUniv.empty_ugraph
     ~interpretate_thing:(interpretate_obj ~mk_choice)
     ~refine_thing:refine_obj

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.mli b/helm/software/components/cic_disambiguation/cicDisambiguate.mli
index ecb5926820a16be025e14c0f34f80037c2a53d56..52919dfa1f7cebc3eb38d32de51d97af37a68c2a 100644 (file)
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.mli
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.mli
@@ -35,6 +35,7 @@ val disambiguate_term :
   ?initial_ugraph:CicUniv.universe_graph -> 
   mk_implicit:(bool -> 'alias) ->
   description_of_alias:('alias -> string) ->
+  fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
   mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
   aliases:'alias DisambiguateTypes.Environment.t ->
   universe:'alias list DisambiguateTypes.Environment.t option ->
@@ -54,6 +55,7 @@ val disambiguate_term :
 val disambiguate_obj :
   mk_implicit:(bool -> 'alias) ->
   description_of_alias:('alias -> string) ->
+  fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
   mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
   aliases:'alias DisambiguateTypes.Environment.t ->
   universe:'alias list DisambiguateTypes.Environment.t option ->

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index f3ba95765274fcd5788b1dad2112177fa9e49ba8..5ac709f9b82fc4e7b5e6dbe6f85fee64abc53570 100644 (file)
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -408,11 +408,16 @@ let domain_diff dom1 dom2 =
 
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
+type alias_spec =
+  | Ident_alias of string * string        (* identifier, uri *)
+  | Symbol_alias of string * int * string (* name, instance no, description *)
+  | Number_alias of int * string          (* instance no, description *)
+
 let disambiguate_thing 
   ~context ~metasenv ~subst ~use_coercions
   ~string_context_of_context
   ~initial_ugraph:base_univ ~expty
-  ~mk_implicit ~description_of_alias
+  ~mk_implicit ~description_of_alias ~fix_instance
   ~aliases ~universe ~lookup_in_library 
   ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
   ~mk_localization_tbl
@@ -439,12 +444,7 @@ let disambiguate_thing
             input_or_locate_uri item
       | Some e ->
           (try
-            let item =
-              match item with
-              | Symbol (symb, _) -> Symbol (symb, 0)
-              | item -> item
-            in
-            Environment.find item e
+            fix_instance item (Environment.find item e)
           with Not_found -> [])
    in
 (*

diff --git a/helm/software/components/disambiguation/disambiguate.mli b/helm/software/components/disambiguation/disambiguate.mli
index ffbdf884d17135de2a4ef128ce5ad9fd0fe13c94..cffb1df0aee5d716a93398ca479699ec43498f34 100644 (file)
--- a/helm/software/components/disambiguation/disambiguate.mli
+++ b/helm/software/components/disambiguation/disambiguate.mli
@@ -96,6 +96,7 @@ val disambiguate_thing:
   expty: 'refined_thing option ->
   mk_implicit:(bool -> 'alias) ->
   description_of_alias:('alias -> string) ->
+  fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
   aliases:'alias DisambiguateTypes.Environment.t ->
   universe:'alias list DisambiguateTypes.Environment.t option ->
   lookup_in_library:(

diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml
index 5767aa3e3f04f09564beb9aa1d70d64f846f9335..d3250c2fe144b911fb3f43778db785d57bec23f0 100644 (file)
--- a/helm/software/components/disambiguation/multiPassDisambiguator.ml
+++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml
@@ -141,19 +141,22 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
     | [] -> assert false
   in
    aux 1 [] passes
+;;
 
 let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
   ~string_context_of_context ~initial_ugraph ~expty ~mk_implicit
-  ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing
-  ~domain_of_thing ~interpretate_thing ~refine_thing ~mk_localization_tbl thing
+  ~description_of_alias ~fix_instance ~aliases ~universe ~lookup_in_library
+  ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
+  ~mk_localization_tbl thing
  =
   let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) =
     let thing = if fresh_instances then freshen_thing thing else thing in
      Disambiguate.disambiguate_thing
       ~context ~metasenv ~subst ~use_coercions ~string_context_of_context
-      ~initial_ugraph ~expty ~mk_implicit ~description_of_alias
+      ~initial_ugraph ~expty ~mk_implicit ~description_of_alias ~fix_instance
       ~aliases ~universe ~lookup_in_library 
       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
       ~mk_localization_tbl (txt,len,thing)
   in
-  disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
+  disambiguate_thing ~description_of_alias ~passes ~aliases
+   ~universe ~f thing

diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.mli b/helm/software/components/disambiguation/multiPassDisambiguator.mli
index a5b5def32df25efaa6eead61293d1970e95d2020..41b79c9b025b2ea73761cf5937f62be39e841396 100644 (file)
--- a/helm/software/components/disambiguation/multiPassDisambiguator.mli
+++ b/helm/software/components/disambiguation/multiPassDisambiguator.mli
@@ -50,6 +50,7 @@ val disambiguate_thing:
   expty: 'refined_thing option ->
   mk_implicit:(bool -> 'alias) ->
   description_of_alias:('alias -> string) ->
+  fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
   aliases:'alias DisambiguateTypes.Environment.t ->
   universe:'alias list
     DisambiguateTypes.Environment.t option ->

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index b53d6ea3fb6db595178073874e3adc79b89a2416..6aee803f42578cf16cb04a5187856470c2f3c48a 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -175,6 +175,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 +204,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 +224,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 +246,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)
@@ -734,7 +752,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) 
@@ -781,7 +799,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

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index f221a2b05a57a31596ab767c2a8438f1d40a919c..7ebca20d763f41043577fd1ed953f38fd987c10e 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -614,7 +614,7 @@ let interpretate_obj
 ;;
 
 let disambiguate_term ~context ~metasenv ~subst ~expty
-   ~mk_implicit ~description_of_alias ~mk_choice
+   ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
    ~aliases ~universe ~rdb ~lookup_in_library 
    (text,prefix_len,term) 
  =
@@ -623,7 +623,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty
     MultiPassDisambiguator.disambiguate_thing
      ~freshen_thing:CicNotationUtil.freshen_term
      ~context ~metasenv ~initial_ugraph:() ~aliases
-     ~mk_implicit ~description_of_alias
+     ~mk_implicit ~description_of_alias ~fix_instance
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
      ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
      ~passes:(MultiPassDisambiguator.passes ())
@@ -636,7 +636,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty
 ;;
 
 let disambiguate_obj 
-   ~mk_implicit ~description_of_alias ~mk_choice
+   ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
    ~aliases ~universe ~rdb ~lookup_in_library ~uri
    (text,prefix_len,obj) 
  =
@@ -645,7 +645,7 @@ let disambiguate_obj
     MultiPassDisambiguator.disambiguate_thing
      ~freshen_thing:CicNotationUtil.freshen_obj
      ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
-     ~mk_implicit ~description_of_alias
+     ~mk_implicit ~description_of_alias ~fix_instance
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
      ~universe 
      ~uri:(Some uri)

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli
index a9f15244cd3bc880e481bf0420885c843193c735..d28708e3a533565276449683e61bc6be95ad308c 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli
@@ -20,6 +20,7 @@ val disambiguate_term :
   expty:NCic.term option ->
   mk_implicit: (bool -> 'alias) ->
   description_of_alias:('alias -> string) ->
+  fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
   mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
   aliases:'alias DisambiguateTypes.Environment.t ->
   universe:'alias list DisambiguateTypes.Environment.t option ->
@@ -37,20 +38,23 @@ val disambiguate_term :
   bool
   
 val disambiguate_obj :
-    mk_implicit:(bool -> 'a) ->
-    description_of_alias:('a -> string) ->
-    mk_choice:('a -> NCic.term DisambiguateTypes.codomain_item) ->
-    aliases:'a DisambiguateTypes.Environment.t ->
-    universe:'a list DisambiguateTypes.Environment.t option ->
-    rdb:#NRstatus.status ->
-    lookup_in_library:(DisambiguateTypes.interactive_user_uri_choice_type ->
-                       DisambiguateTypes.input_or_locate_uri_type ->
-                       DisambiguateTypes.Environment.key -> 'a list) ->
-    uri:NUri.uri ->
-    string * int * CicNotationPt.term CicNotationPt.obj ->
-    ((DisambiguateTypes.Environment.key * 'a) list * NCic.metasenv *
-     NCic.substitution * NCic.obj)
-    list * bool
+  mk_implicit:(bool -> 'alias) ->
+  description_of_alias:('alias -> string) ->
+  fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
+  mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
+  aliases:'alias DisambiguateTypes.Environment.t ->
+  universe:'alias list DisambiguateTypes.Environment.t option ->
+  rdb:#NRstatus.status ->
+  lookup_in_library:(
+    DisambiguateTypes.interactive_user_uri_choice_type ->
+    DisambiguateTypes.input_or_locate_uri_type ->
+    DisambiguateTypes.Environment.key ->
+     'alias list) ->
+  uri:NUri.uri ->
+  string * int * CicNotationPt.term CicNotationPt.obj ->
+  ((DisambiguateTypes.Environment.key * 'alias) list * NCic.metasenv *
+   NCic.substitution * NCic.obj)
+  list * bool
 
 val disambiguate_path: CicNotationPt.term -> NCic.term