open MatitaTypes
exception Ambiguous_input
+(* the integer is an offset to be added to each location *)
+exception DisambiguationError of
+ int * (Token.flocation option * string Lazy.t) list list
type choose_uris_callback =
id:string -> UriManager.uri list -> UriManager.uri list
=
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 multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
+ let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
let passes = (* <fresh_instances?, aliases, coercions?> *)
[ (false, mono_aliases, false);
(false, multi_aliases, false);
else
drop_aliases_and_clear_diff res
in
- let rec aux =
+ let rec aux errors =
function
- | [ pass ] -> set_aliases pass (try_pass pass)
+ | [ pass ] ->
+ (try
+ set_aliases pass (try_pass pass)
+ with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
+ raise (DisambiguationError (offset, errors @ [newerrors])))
| hd :: tl ->
(try
set_aliases hd (try_pass hd)
- with Disambiguate.NoWellTypedInterpretation -> aux tl)
+ with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
+ aux (errors @ [newerrors]) tl)
| [] -> assert false
in
let saved_use_coercions = !CoercDb.use_coercions in
try
- let res = aux passes in
+ let res = aux [] passes in
CoercDb.use_coercions := saved_use_coercions;
res
with exn ->
}
let disambiguate_thing =
- let profiler = CicUtil.profile "disambiguate_thing" in
+ let profiler = HExtlib.profile "disambiguate_thing" in
{ do_it =
fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
- -> profiler.CicUtil.profile
+ -> profiler.HExtlib.profile
(disambiguate_thing ~aliases ~universe ~f ~drop_aliases
~drop_aliases_and_clear_diff) thing
}