]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/disambiguation/multiPassDisambiguator.ml
patches for hints & unification:
[helm.git] / helm / software / components / disambiguation / multiPassDisambiguator.ml
index 07bbdeba29d68e389590bd3b72650ac1bbe63d2f..b1cf9aed0ec55f13e3317489b8e9f63e044d1ffe 100644 (file)
@@ -27,9 +27,9 @@
 
 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 *
@@ -41,18 +41,23 @@ exception DisambiguationError of
 (* 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);
   ]
 ;;
 
@@ -138,20 +143,22 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
     | [] -> 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