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
(* 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