From f48ba5edb4602e663ee746964ec88ff673642388 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 24 Jul 2006 14:58:55 +0000 Subject: [PATCH] Disambiguation passes simplified. --- .../grafite_parser/grafiteDisambiguator.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) 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 = (* *) 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 -> -- 2.39.2