]
;;
+(* XXX is this useful anymore? *)
let drop_aliases ?(minimize_instances=false) ~description_of_alias
(choices, user_asked)
=
let rec aux =
function
[] -> []
- | (D.Symbol (s,n),ci1) as he::tl when n > 0 ->
+(* now it's ALWAYS None
+ | (D.Symbol (s,n),ci1) as he::tl when n <> None ->
if
List.for_all
(function
| _ -> true
) d
then
- (D.Symbol (s,0),ci1)::(aux tl)
+ (D.Symbol (s,None),ci1)::(aux tl)
else
he::(aux tl)
- | (D.Num n,ci1) as he::tl when n > 0 ->
+ | (D.Num n,ci1) as he::tl when n <> None ->
if
List.for_all
(function (D.Num _,ci2) -> compare ci1 ci2 | _ -> true) d
then
- (D.Num 0,ci1)::(aux tl)
+ (D.Num None,ci1)::(aux tl)
else
- he::(aux tl)
+ he::(aux tl) *)
| he::tl -> he::(aux tl)
in
aux d
in
- (List.map (fun (d, a, b, c, e) -> minimize d, a, b, c, e) choices),
+ (List.map (fun (t, d, a, b, c, e) -> t, minimize d, a, b, c, e) choices),
user_asked
let drop_aliases_and_clear_diff (choices, user_asked) =
- (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
+ (List.map (fun (t,_, a, b, c, d) -> t,[], a, b, c, d) choices),
user_asked
-let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
+(*let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~visit ~f thing
=
- 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, Some DisambiguateTypes.Environment.empty in
+ let library = false, DisambiguateTypes.InterprEnv.empty,
+ DisambiguateTypes.Environment.empty in
+ let multi_aliases = false, DisambiguateTypes.InterprEnv.empty, universe in
+ let mono_aliases = true, aliases, DisambiguateTypes.Environment.empty in
let passes =
List.map
(function (fresh_instances,env,use_coercions) ->
else if user_asked then
drop_aliases ~minimize_instances:true ~description_of_alias res (* one shot aliases *)
else
- drop_aliases_and_clear_diff res
+ drop_aliases_and_clear_diff res
in
let rec aux i errors passes =
debug_print (lazy ("Pass: " ^ string_of_int i));
| [] -> assert false
in
aux 1 [] passes
-;;
+;;*)
let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
~string_context_of_context ~initial_ugraph ~expty ~mk_implicit
~description_of_alias ~fix_instance ~aliases ~universe ~lookup_in_library
- ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
+ ~uri ~pp_thing ~pp_term ~domain_of_thing ~interpretate_thing ~refine_thing ~visit
~mk_localization_tbl thing
=
- let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) =
+(*
+ let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) =
let thing = if fresh_instances then freshen_thing thing else thing in
Disambiguate.disambiguate_thing
~context ~metasenv ~subst ~use_coercions ~string_context_of_context
~initial_ugraph ~expty ~mk_implicit ~description_of_alias ~fix_instance
~aliases ~universe ~lookup_in_library
- ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
- ~mk_localization_tbl (txt,len,thing)
+ ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~visit
+ ~mk_localization_tbl ~pp_term (txt,len,thing)
in
disambiguate_thing ~description_of_alias ~passes ~aliases
- ~universe ~f thing
+ ~universe ~visit ~f thing
+ *)
+ match
+ Disambiguate.disambiguate_thing
+ ~context ~metasenv ~subst ~use_coercions:true ~string_context_of_context
+ ~initial_ugraph ~expty ~mk_implicit ~description_of_alias ~fix_instance
+ ~aliases ~universe ~lookup_in_library
+ ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~visit
+ ~mk_localization_tbl ~pp_term thing
+ with
+ | Disambiguate.Disamb_success res -> res
+ | Disambiguate.Disamb_failure (herrors, serrors) ->
+ (* temporary *)
+ let offset = 0 in
+ raise (DisambiguationError (offset, newerrors))