Added support for multiple disambiguation passes.

[helm.git] / helm / matita / matitaDisambiguator.ml

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index d2c11890fa7cf7ae4d61c88063124727f98bbd75..db69cb71dfdd0eedf5050d3f03278e4106c24084 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -29,7 +29,9 @@ 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 =
@@ -37,6 +39,7 @@ let mono_uris_callback ~id =
   function l -> l
  else
   raise Ambiguous_input
+
 let mono_interp_callback _ = raise Ambiguous_input
 
 let _choose_uris_callback = ref mono_uris_callback
@@ -65,6 +68,58 @@ 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 = false, 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, library, 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 rec aux =
+    function
+    | [ pass ] -> try_pass pass
+    | hd :: tl ->
+        (try
+          try_pass hd
+        with Disambiguate.NoWellTypedInterpretation ->
+          let (_, user_asked) as res = aux tl in
+          if user_asked then res else set_aliases aliases res)
+    | [] -> 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