X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguator.ml;h=8827e709b42328072edcb01591e9422ef73ba9e1;hb=68f3812e06c04ddd664e86dbfd3a1c32f96a22d1;hp=05c988ac16c98b349fed54a0a4c7268e3bcdb2de;hpb=5bc000d9a2e8e41db58d610f3221270add686888;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
index 05c988ac1..8827e709b 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
@@ -27,10 +27,17 @@
 
 open Printf
 
+let debug = false;;
+let debug_print s =
+ if debug then prerr_endline (Lazy.force s);;
+
 exception Ambiguous_input
 (* the integer is an offset to be added to each location *)
 exception DisambiguationError of
- int * (Token.flocation option * string Lazy.t) list list
+ int *
+ ((Stdpp.location list * string * string) list *
+  (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+  Stdpp.location option * string Lazy.t * bool) list list
   (** parameters are: option name, error message *)
 exception Unbound_identifier of string
 
@@ -39,7 +46,7 @@ type choose_uris_callback =
 
 type choose_interp_callback = 
   string -> int -> 
-    (Token.flocation list * string * string) list list -> int list
+    (Stdpp.location list * string * string) list list -> int list
 
 let mono_uris_callback ~id =
  if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
@@ -92,11 +99,9 @@ let disambiguate_thing ~aliases ~universe
   let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
   let passes = (* <fresh_instances?, aliases, coercions?> *)
    if !only_one_pass then
-    [ (false, mono_aliases, false) ]
+    [ (true, mono_aliases, false) ]
    else
-    [ (false, mono_aliases, false);
-      (false, multi_aliases, false);
-      (true, mono_aliases, false);
+    [ (true, mono_aliases, false);
       (true, multi_aliases, false);
       (true, mono_aliases, true);
       (true, multi_aliases, true);
@@ -110,16 +115,17 @@ let disambiguate_thing ~aliases ~universe
     f ~fresh_instances ~aliases ~universe thing
   in
   let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
-   if use_mono_aliases && not instances then
-    drop_aliases res
+   if use_mono_aliases then
+    drop_aliases ~minimize_instances:true res (* one shot aliases *)
    else if user_asked then
     drop_aliases ~minimize_instances:true res (* one shot aliases *)
    else
     drop_aliases_and_clear_diff res
   in
-  let rec aux errors =
-    function
-    | [ pass ] ->
+  let rec aux i errors passes =
+  debug_print (lazy ("Pass: " ^ string_of_int i));
+   match passes with
+      [ pass ] ->
         (try
           set_aliases pass (try_pass pass)
          with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
@@ -128,12 +134,12 @@ let disambiguate_thing ~aliases ~universe
         (try
           set_aliases hd (try_pass hd)
         with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
-         aux (errors @ [newerrors]) tl)
+         aux (i+1) (errors @ [newerrors]) tl)
     | [] -> assert false
   in
   let saved_insert_coercions = !CicRefine.insert_coercions in
   try
-    let res = aux [] passes in
+    let res = aux 1 [] passes in
     CicRefine.insert_coercions := saved_insert_coercions;
     res
   with exn ->