X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaDisambiguator.ml;h=b7de40ed966eb580740c5b506f4bb53103180b4e;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=e286fb5502a3714087fe925a2181d1ce75cda81b;hpb=a7b90d2494f7d580faa54ecd2835bd4649129763;p=helm.git

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index e286fb550..b7de40ed9 100644
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -29,10 +29,17 @@ open MatitaTypes
 
 exception Ambiguous_input
 
-type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list
+type choose_uris_callback =
+  id:string -> UriManager.uri list -> UriManager.uri list
+
 type choose_interp_callback = (string * string) list list -> int list
 
-let mono_uris_callback ~id = raise Ambiguous_input
+let mono_uris_callback ~id =
+ if Helm_registry.get_bool "matita.auto_disambiguation" then
+  function l -> l
+ else
+  raise Ambiguous_input
+
 let mono_interp_callback _ = raise Ambiguous_input
 
 let _choose_uris_callback = ref mono_uris_callback
@@ -61,6 +68,65 @@ module Disambiguator = Disambiguate.Make (Callbacks)
 
 (* implement module's API *)
 
-let disambiguate_term = Disambiguator.disambiguate_term
+let disambiguate_thing ~aliases
+  ~(f:?fresh_instances:bool -> aliases:Disambiguate.aliases -> 'a -> 'b)
+  ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b)
+  (thing: 'a)
+=
+  let library = true, DisambiguateTypes.empty_environment in
+  let multi_aliases = true, aliases in
+  let mono_aliases = false, aliases in
+  let passes =  (* <fresh_instances?, aliases, coercions?> *)
+    [ (false, mono_aliases, false);
+      (false, multi_aliases, false);
+      (true, mono_aliases, false);
+      (true, multi_aliases, false);
+      (true, mono_aliases, true);
+      (true, multi_aliases, true);
+      (true, library, true);
+    ]
+  in
+  let try_pass (fresh_instances, aliases, use_coercions) =
+    CoercDb.use_coercions := use_coercions;
+    f ~fresh_instances ~aliases thing
+  in
+  let set_aliases (instances,(use_multi_aliases,_),_) (_, user_asked as res) =
+   if not use_multi_aliases && not instances then
+    res
+   else if user_asked then
+    res (* one shot aliases *)
+   else
+    set_aliases aliases res
+  in
+  let rec aux =
+    function
+    | [ pass ] -> set_aliases pass (try_pass pass)
+    | hd :: tl ->
+        (try
+          set_aliases hd (try_pass hd)
+        with Disambiguate.NoWellTypedInterpretation -> aux tl)
+    | [] -> assert false
+  in
+  let saved_use_coercions = !CoercDb.use_coercions in
+  try
+    let res = aux passes in
+    CoercDb.use_coercions := saved_use_coercions;
+    res
+  with exn ->
+    CoercDb.use_coercions := saved_use_coercions;
+    raise exn
+
+let set_aliases aliases (choices, user_asked) =
+  (List.map (fun (_, a, b, c) -> aliases, a, b, c) choices),
+  user_asked
+
+let disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph ~aliases term =
+  let f =
+    Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph
+  in
+  disambiguate_thing ~aliases ~f ~set_aliases term
+
+let disambiguate_obj ~dbd ~aliases ~uri obj =
+  let f = Disambiguator.disambiguate_obj ~dbd ~uri in
+  disambiguate_thing ~aliases ~f ~set_aliases obj
 
-let disambiguate_obj = Disambiguator.disambiguate_obj