X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaDisambiguator.ml;h=24a8355237b7d1e4a7b81d4b58068a01537bc22d;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=fcbcdea1442cce3be7be508881038f0599ebbce6;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index fcbcdea14..24a835523 100644
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -28,11 +28,19 @@ open Printf
 open MatitaTypes
 
 exception Ambiguous_input
+exception DisambiguationError of string Lazy.t list list
+
+type choose_uris_callback =
+  id:string -> UriManager.uri list -> UriManager.uri list
 
-type choose_uris_callback = id:string -> string list -> string 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,5 +69,106 @@ module Disambiguator = Disambiguate.Make (Callbacks)
 
 (* implement module's API *)
 
-let disambiguate_term = Disambiguator.disambiguate_term
+let disambiguate_thing ~aliases ~universe
+  ~(f:?fresh_instances:bool ->
+      aliases:DisambiguateTypes.environment ->
+      universe:DisambiguateTypes.multiple_environment option ->
+      'a -> 'b)
+  ~(drop_aliases: 'b -> 'b)
+  ~(drop_aliases_and_clear_diff: 'b -> 'b)
+  (thing: 'a)
+=
+  assert (universe <> None);
+  let library = false, DisambiguateTypes.Environment.empty, None in
+  let multi_aliases=false, DisambiguateTypes.Environment.empty, universe in
+  let mono_aliases = true, aliases, None 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, universe), use_coercions) =
+    CoercDb.use_coercions := use_coercions;
+    f ~fresh_instances ~aliases ~universe thing
+  in
+  let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
+   if use_mono_aliases && not instances then
+    drop_aliases res
+   else if user_asked then
+    drop_aliases res (* one shot aliases *)
+   else
+    drop_aliases_and_clear_diff res
+  in
+  let rec aux errors =
+    function
+    | [ pass ] ->
+        (try
+          set_aliases pass (try_pass pass)
+         with Disambiguate.NoWellTypedInterpretation newerrors ->
+          raise (DisambiguationError (errors @ [newerrors])))
+    | hd :: tl ->
+        (try
+          set_aliases hd (try_pass hd)
+        with Disambiguate.NoWellTypedInterpretation newerrors ->
+         aux (errors @ [newerrors]) 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
+
+type disambiguator_thing =
+ { do_it :
+    'a 'b.
+    aliases:DisambiguateTypes.environment ->
+    universe:DisambiguateTypes.multiple_environment option ->
+    f:(?fresh_instances:bool ->
+       aliases:DisambiguateTypes.environment ->
+       universe:DisambiguateTypes.multiple_environment option ->
+       'a -> 'b * bool) ->
+    drop_aliases:('b * bool -> 'b * bool) ->
+    drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
+ }
+
+let disambiguate_thing =
+ let profiler = HExtlib.profile "disambiguate_thing" in
+  { do_it =
+     fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
+     -> profiler.HExtlib.profile
+         (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
+           ~drop_aliases_and_clear_diff) thing
+  }
+
+let drop_aliases (choices, user_asked) =
+  (List.map (fun (d, a, b, c) -> d, a, b, c) choices),
+  user_asked
+
+let drop_aliases_and_clear_diff (choices, user_asked) =
+  (List.map (fun (_, a, b, c) -> [], a, b, c) choices),
+  user_asked
+
+let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph
+  ~aliases ~universe term
+ =
+  assert (fresh_instances = None);
+  let f =
+    Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph
+  in
+  disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
+   ~drop_aliases_and_clear_diff term
 
+let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj =
+  assert (fresh_instances = None);
+  let f = Disambiguator.disambiguate_obj ~dbd ~uri in
+  disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
+   ~drop_aliases_and_clear_diff obj