.ma inclusions corrected/minimized

[helm.git] / helm / matita / matitaDisambiguator.ml

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index db69cb71dfdd0eedf5050d3f03278e4106c24084..5a7fe0b9f45ff925fcb0ca28947f3900597c49b0 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -68,36 +68,47 @@ module Disambiguator = Disambiguate.Make (Callbacks)
 
 (* implement module's API *)
 
-let disambiguate_thing ~aliases
-  ~(f:?fresh_instances:bool -> aliases:Disambiguate.aliases -> 'a -> 'b)
+let disambiguate_thing ~aliases ~universe
+  ~(f:?fresh_instances:bool ->
+      aliases:DisambiguateTypes.environment ->
+      universe:DisambiguateTypes.multiple_environment option ->
+      'a -> 'b)
   ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b)
   (thing: 'a)
 =
-  let library = false, 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);
-      (true, library, false);
+      (true, mono_aliases, false);
+      (true, multi_aliases, false);
       (true, mono_aliases, true);
       (true, multi_aliases, true);
       (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 (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
+   if use_mono_aliases && not instances then
+    res
+   else if user_asked then
+    res (* one shot aliases *)
+   else
+    set_aliases aliases res
   in
   let rec aux =
     function
-    | [ pass ] -> try_pass pass
+    | [ pass ] -> set_aliases pass (try_pass pass)
     | hd :: tl ->
         (try
-          try_pass hd
-        with Disambiguate.NoWellTypedInterpretation ->
-          let (_, user_asked) as res = aux tl in
-          if user_asked then res else set_aliases aliases res)
+          set_aliases hd (try_pass hd)
+        with Disambiguate.NoWellTypedInterpretation -> aux tl)
     | [] -> assert false
   in
   let saved_use_coercions = !CoercDb.use_coercions in
@@ -113,13 +124,17 @@ let set_aliases aliases (choices, user_asked) =
   (List.map (fun (_, a, b, c) -> aliases, 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 ~aliases ~universe ~f ~set_aliases 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 ~aliases ~universe ~f ~set_aliases obj