From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 14 Apr 2006 10:15:48 +0000 (+0000)
Subject: multi-instances aliases are compressed to single instances if possible
X-Git-Tag: 0.4.95@7852~1502
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=74aa40a50acaf5efdaacb3b6677e2b623b5f39ab;p=helm.git

multi-instances aliases are compressed to single instances if possible
---

diff --git a/components/grafite_parser/grafiteDisambiguator.ml b/components/grafite_parser/grafiteDisambiguator.ml
index abe8c1de1..2803c88f6 100644
--- a/components/grafite_parser/grafiteDisambiguator.ml
+++ b/components/grafite_parser/grafiteDisambiguator.ml
@@ -80,7 +80,7 @@ let disambiguate_thing ~aliases ~universe
       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)
 =
@@ -106,7 +106,7 @@ let disambiguate_thing ~aliases ~universe
    if use_mono_aliases && not instances then
     drop_aliases res
    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
@@ -142,7 +142,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 +155,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) =