From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 24 Jul 2006 14:58:55 +0000 (+0000)
Subject: Disambiguation passes simplified.
X-Git-Tag: make_still_working~7012
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f48ba5edb4602e663ee746964ec88ff673642388;p=helm.git

Disambiguation passes simplified.
---

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
index 05c988ac1..76d44421c 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
@@ -92,11 +92,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);
@@ -117,9 +115,10 @@ let disambiguate_thing ~aliases ~universe
    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) ->
@@ -128,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 ->