X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaDisambiguator.ml;h=22819536fe31b02ea993b8cf3dcc6185c549b5d2;hb=8530992b72238902faae5e8bff74550fd8d7264a;hp=fe9cdca761785a081c3ae18e84addbe68bd27ae9;hpb=49430a1d657ec9521619ea35fe911b598f055df9;p=helm.git

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index fe9cdca76..22819536f 100644
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -68,14 +68,19 @@ module Disambiguator = Disambiguate.Make (Callbacks)
 
 (* implement module's API *)
 
-let disambiguate_thing ~aliases
-  ~(f:?fresh_instances:bool -> aliases:Disambiguate.aliases -> 'a -> 'b)
-  ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b)
+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_and_clear_diff: 'b -> 'b)
   (thing: 'a)
 =
-  let library = true, DisambiguateTypes.empty_environment in
-  let multi_aliases = true, aliases in
-  let mono_aliases = false, aliases in
+  assert (universe <> None);
+  let library = false, DisambiguateTypes.Environment.empty, None in
+  let multi_aliases=false, DisambiguateTypes.Environment.empty, universe in
+  let mono_aliases = true, aliases, None in
   let passes =  (* <fresh_instances?, aliases, coercions?> *)
     [ (false, mono_aliases, false);
       (false, multi_aliases, false);
@@ -86,17 +91,17 @@ let disambiguate_thing ~aliases
       (true, library, true);
     ]
   in
-  let try_pass (fresh_instances, aliases, use_coercions) =
+  let try_pass (fresh_instances, (_, aliases, universe), use_coercions) =
     CoercDb.use_coercions := use_coercions;
-    f ~fresh_instances ~aliases thing
+    f ~fresh_instances ~aliases ~universe thing
   in
-  let set_aliases (_,(use_multi_aliases,_),_) (_, user_asked as res) =
-   if not use_multi_aliases then
-    res
+  let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
+   if use_mono_aliases && not instances then
+    drop_aliases res
    else if user_asked then
-    res (* one shot aliases *)
+    drop_aliases res (* one shot aliases *)
    else
-    set_aliases aliases res
+    drop_aliases_and_clear_diff res
   in
   let rec aux =
     function
@@ -116,17 +121,48 @@ let disambiguate_thing ~aliases
     CoercDb.use_coercions := saved_use_coercions;
     raise exn
 
-let set_aliases aliases (choices, user_asked) =
-  (List.map (fun (_, a, b, c) -> aliases, a, b, c) choices),
+type disambiguator_thing =
+ { do_it :
+    'a 'b.
+    aliases:DisambiguateTypes.environment ->
+    universe:DisambiguateTypes.multiple_environment option ->
+    f:(?fresh_instances:bool ->
+       aliases:DisambiguateTypes.environment ->
+       universe:DisambiguateTypes.multiple_environment option ->
+       'a -> 'b * bool) ->
+    drop_aliases:('b * bool -> 'b * bool) ->
+    drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
+ }
+
+let disambiguate_thing =
+ let profiler = HExtlib.profile "disambiguate_thing" in
+  { do_it =
+     fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
+     -> profiler.HExtlib.profile
+         (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
+           ~drop_aliases_and_clear_diff) thing
+  }
+
+let drop_aliases (choices, user_asked) =
+  (List.map (fun (d, a, b, c) -> d, a, b, c) choices),
+  user_asked
+
+let drop_aliases_and_clear_diff (choices, user_asked) =
+  (List.map (fun (_, a, b, c) -> [], a, b, c) choices),
   user_asked
 
-let disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph ~aliases term =
+let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph
+  ~aliases ~universe term
+ =
+  assert (fresh_instances = None);
   let f =
     Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph
   in
-  disambiguate_thing ~aliases ~f ~set_aliases term
+  disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
+   ~drop_aliases_and_clear_diff term
 
-let disambiguate_obj ~dbd ~aliases ~uri obj =
+let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj =
+  assert (fresh_instances = None);
   let f = Disambiguator.disambiguate_obj ~dbd ~uri in
-  disambiguate_thing ~aliases ~f ~set_aliases obj
-
+  disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
+   ~drop_aliases_and_clear_diff obj