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 DisambiguationError of
int *
(* 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
+ 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