+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