X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteDisambiguator.ml;h=181532462b7b370140297ee48a119e7510e30991;hb=4a612cd8684c60345c6f5a1f4f8fcc96fdc39685;hp=abe8c1de1f75373c33fbfdf018eaaf3984d4c785;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/grafite_parser/grafiteDisambiguator.ml b/components/grafite_parser/grafiteDisambiguator.ml
index abe8c1de1..181532462 100644
--- a/components/grafite_parser/grafiteDisambiguator.ml
+++ b/components/grafite_parser/grafiteDisambiguator.ml
@@ -37,7 +37,9 @@ exception Unbound_identifier of string
 type choose_uris_callback =
   id:string -> UriManager.uri list -> UriManager.uri list
 
-type choose_interp_callback = (string * string) list list -> int list
+type choose_interp_callback = 
+  string -> int -> 
+    (Token.flocation list * string * string) list list -> int list
 
 let mono_uris_callback ~id =
  if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
@@ -47,7 +49,7 @@ let mono_uris_callback ~id =
  else
   raise Ambiguous_input
 
-let mono_interp_callback _ = 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
@@ -63,24 +65,24 @@ module Callbacks =
     let interactive_interpretation_choice interp =
       !_choose_interp_callback interp
 
-    let input_or_locate_uri ~(title:string) ?id =
+    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 *)
-      let msg = match id with Some id -> id | _ -> "_" in
-      raise (Unbound_identifier msg)
   end
   
 module Disambiguator = Disambiguate.Make (Callbacks)
 
 (* implement module's API *)
 
+let only_one_pass = ref false;;
+
 let disambiguate_thing ~aliases ~universe
   ~(f:?fresh_instances:bool ->
       aliases:DisambiguateTypes.environment ->
       universe:DisambiguateTypes.multiple_environment option ->
       'a -> 'b)
-  ~(drop_aliases: 'b -> 'b)
+  ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b)
   ~(drop_aliases_and_clear_diff: 'b -> 'b)
   (thing: 'a)
 =
@@ -88,13 +90,16 @@ let disambiguate_thing ~aliases ~universe
   let library = false, DisambiguateTypes.Environment.empty, None in
   let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
   let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
-  let passes =  (* <fresh_instances?, aliases, coercions?> *)
-    [ (false, mono_aliases, false);
-      (false, multi_aliases, false);
-      (true, mono_aliases, false);
+  let passes = (* <fresh_instances?, aliases, coercions?> *)
+   if !only_one_pass then
+    [ (true, mono_aliases, false) ]
+   else
+    [ (true, mono_aliases, false);
       (true, multi_aliases, false);
       (true, mono_aliases, true);
       (true, multi_aliases, true);
+      (true, library, false); 
+        (* for demo to reduce the number of interpretations *)
       (true, library, true);
     ]
   in
@@ -103,16 +108,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 res (* one shot aliases *)
+    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 =
+(*prerr_endline ("Pass: " ^ string_of_int i);*)
+   match passes with
+      [ pass ] ->
         (try
           set_aliases pass (try_pass pass)
          with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
@@ -121,12 +127,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 ->
@@ -142,7 +148,7 @@ type disambiguator_thing =
        aliases:DisambiguateTypes.environment ->
        universe:DisambiguateTypes.multiple_environment option ->
        'a -> 'b * bool) ->
-    drop_aliases:('b * bool -> 'b * bool) ->
+    drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) ->
     drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
  }
 
@@ -155,8 +161,39 @@ let disambiguate_thing =
            ~drop_aliases_and_clear_diff) thing
   }
 
-let drop_aliases (choices, user_asked) =
-  (List.map (fun (d, a, b, c) -> d, a, b, c) choices),
+let drop_aliases ?(minimize_instances=false) (choices, user_asked) =
+ let module D = DisambiguateTypes in
+ let minimize d =
+  if not minimize_instances then
+   d
+  else
+   let rec aux =
+    function
+       [] -> []
+     | (D.Symbol (s,n),((descr,_) as ci)) as he::tl when n > 0 ->
+         if
+          List.for_all
+           (function
+               (D.Symbol (s2,_),(descr2,_)) -> s2 <> s || descr = descr2
+             | _ -> true
+           ) d
+         then
+          (D.Symbol (s,0),ci)::(aux tl)
+         else
+          he::(aux tl)
+     | (D.Num n,((descr,_) as ci)) as he::tl when n > 0 ->
+         if
+          List.for_all
+           (function (D.Num _,(descr2,_)) -> descr = descr2 | _ -> true) d
+         then
+          (D.Num 0,ci)::(aux tl)
+         else
+          he::(aux tl)
+      | he::tl -> he::(aux tl)
+   in
+    aux d
+ in
+  (List.map (fun (d, a, b, c) -> minimize d, a, b, c) choices),
   user_asked
 
 let drop_aliases_and_clear_diff (choices, user_asked) =