open Printf
-let debug = false;;
+let debug = ref false;;
let debug_print s =
- if debug then prerr_endline (Lazy.force s);;
+ if !debug then prerr_endline (Lazy.force s) else ();;
-exception Ambiguous_input
-(* the integer is an offset to be added to each location *)
exception DisambiguationError of
int *
((Stdpp.location list * string * string) list *
(Stdpp.location * string) Lazy.t * bool) list list
(** parameters are: option name, error message *)
-let mono_uris_callback ~selection_mode ?ok
- ?(enable_button_for_non_vars = true) ~title ~msg ~id =
- if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
- "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
-let _choose_interp_callback = ref mono_interp_callback
-let set_choose_uris_callback f = _choose_uris_callback := f
-let set_choose_interp_callback f = _choose_interp_callback := f
-
-module Callbacks =
- struct
- let interactive_user_uri_choice = !_choose_uris_callback
-
- let interactive_interpretation_choice interp =
- !_choose_interp_callback interp
-
- let input_or_locate_uri ~(title:string) ?id () = None
- (* Zack: I try to avoid using this callback. I therefore assume that
- * the presence of an identifier that can't be resolved via "locate"
- * query is a syntax error *)
- end
-
-module Disambiguator = Disambiguate.Make (Callbacks)
-
(* implement module's API *)
let only_one_pass = ref false;;
+let use_library = ref false;;
let passes () = (* <fresh_instances?, aliases, coercions?> *)
if !only_one_pass then
[ (true, `Mono, false) ]
+ else if !use_library then
+ [ (true, `Library, false);
+ (* for demo to reduce the number of interpretations *)
+ (true, `Library, true);
+ ]
+ else if !debug then
+ [ (true, `Multi, true); ]
else
[ (true, `Mono, false);
(true, `Multi, false);
(true, `Mono, true);
(true, `Multi, true);
- (true, `Library, false);
- (* for demo to reduce the number of interpretations *)
- (true, `Library, true);
]
;;
-let drop_aliases ?(minimize_instances=false) (choices, user_asked) =
+let drop_aliases ?(minimize_instances=false) ~description_of_alias
+ (choices, user_asked)
+=
let module D = DisambiguateTypes in
+ let compare ci1 ci2 = description_of_alias ci1 = description_of_alias ci2 in
let minimize d =
if not minimize_instances then
d
let rec aux =
function
[] -> []
- | (D.Symbol (s,n),((descr,_) as ci)) as he::tl when n > 0 ->
+ | (D.Symbol (s,n),ci1) as he::tl when n > 0 ->
if
List.for_all
(function
- (D.Symbol (s2,_),(descr2,_)) -> s2 <> s || descr = descr2
+ (D.Symbol (s2,_),ci2) -> s2 <> s || compare ci1 ci2
| _ -> true
) d
then
- (D.Symbol (s,0),ci)::(aux tl)
+ (D.Symbol (s,0),ci1)::(aux tl)
else
he::(aux tl)
- | (D.Num n,((descr,_) as ci)) as he::tl when n > 0 ->
+ | (D.Num n,ci1) as he::tl when n > 0 ->
if
List.for_all
- (function (D.Num _,(descr2,_)) -> descr = descr2 | _ -> true) d
+ (function (D.Num _,ci2) -> compare ci1 ci2 | _ -> true) d
then
- (D.Num 0,ci)::(aux tl)
+ (D.Num 0,ci1)::(aux tl)
else
he::(aux tl)
| he::tl -> he::(aux tl)
(List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
user_asked
-let disambiguate_thing ~passes ~aliases ~universe ~f thing =
+let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
+=
assert (universe <> None);
let library = false, DisambiguateTypes.Environment.empty, None in
let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
in
let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
if use_mono_aliases then
- drop_aliases ~minimize_instances:true res (* one shot aliases *)
+ drop_aliases ~minimize_instances:true ~description_of_alias res (* one shot aliases *)
else if user_asked then
- drop_aliases ~minimize_instances:true res (* one shot aliases *)
+ drop_aliases ~minimize_instances:true ~description_of_alias res (* one shot aliases *)
else
drop_aliases_and_clear_diff res
in
| [] -> assert false
in
aux 1 [] passes
+;;
let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
- ~mk_implicit ~string_context_of_context ~initial_ugraph ~hint ~aliases
- ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing
- ~interpretate_thing ~refine_thing ~localization_tbl thing
+ ~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 thing
=
let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) =
- let thing = if fresh_instances then freshen_thing thing else thing
- in
- Disambiguator.disambiguate_thing
- ~context ~metasenv ~subst ~use_coercions
- ~mk_implicit ~string_context_of_context
- ~initial_ugraph ~hint
+ 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
- ~localization_tbl (txt,len,thing)
+ ~mk_localization_tbl (txt,len,thing)
in
- disambiguate_thing ~passes ~aliases ~universe ~f thing
+ disambiguate_thing ~description_of_alias ~passes ~aliases
+ ~universe ~f thing
projects / helm.git / blobdiff