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);
]
;;
| [] -> assert false
in
aux 1 [] passes
+;;
let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
- ~string_context_of_context ~initial_ugraph ~hint ~mk_implicit
- ~description_of_alias ~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
+ 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 ~hint ~mk_implicit ~description_of_alias
+ ~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 ~description_of_alias ~passes ~aliases ~universe ~f thing
+ disambiguate_thing ~description_of_alias ~passes ~aliases
+ ~universe ~f thing