(* implement module's API *)
-let disambiguate_thing ~aliases
- ~(f:?fresh_instances:bool -> aliases:Disambiguate.aliases -> 'a -> 'b)
+let disambiguate_thing ~aliases ~universe
+ ~(f:?fresh_instances:bool ->
+ aliases:DisambiguateTypes.environment ->
+ universe:DisambiguateTypes.multiple_environment option ->
+ '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
+ 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, library, 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) =
+ let try_pass (fresh_instances, (_, aliases, universe), use_coercions) =
CoercDb.use_coercions := use_coercions;
- f ~fresh_instances ~aliases thing
+ 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
+ res
+ else if user_asked then
+ res (* one shot aliases *)
+ else
+ set_aliases aliases res
in
let rec aux =
function
- | [ pass ] -> try_pass pass
+ | [ pass ] -> set_aliases 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)
+ set_aliases hd (try_pass hd)
+ with Disambiguate.NoWellTypedInterpretation -> aux tl)
| [] -> assert false
in
let saved_use_coercions = !CoercDb.use_coercions in
CoercDb.use_coercions := saved_use_coercions;
raise exn
+let disambiguate_thing =
+ let profiler = CicUtil.profile "disambiguate_thing" in
+ fun ~aliases ~universe
+ ~(f:?fresh_instances:bool ->
+ aliases:DisambiguateTypes.environment ->
+ universe:DisambiguateTypes.multiple_environment option ->
+ 'a -> 'b)
+ ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b)
+ (thing: 'a)
+ -> profiler.CicUtil.profile
+ (disambiguate_thing ~aliases ~universe ~f ~set_aliases) thing
+
+let disambiguate_thing ~aliases ~universe
+ ~(f:?fresh_instances:bool ->
+ aliases:DisambiguateTypes.environment ->
+ universe:DisambiguateTypes.multiple_environment option ->
+ 'a -> 'b)
+ ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b)
+ (thing: 'a)
+=
+ Obj.magic disambiguate_thing ~aliases ~universe ~f ~set_aliases thing
+
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 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 ~aliases ~f ~set_aliases term
+ disambiguate_thing ~aliases ~universe ~f ~set_aliases term
-let disambiguate_obj ~dbd ~aliases ~uri obj =
+let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj =
+ assert (fresh_instances = None);
let f = Disambiguator.disambiguate_obj ~dbd ~uri in
- disambiguate_thing ~aliases ~f ~set_aliases obj
-
+ disambiguate_thing ~aliases ~universe ~f ~set_aliases obj