+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