Further speed-up in the disambiguation algorithm.

The case |choices| = 1 is handled in a special way:
 if |choices| = 1 also for the next ambiguous symbol, then the
  current refinement step is skipped

NOTE: this suggests that pre-setting all the interpretations with cardinality 1
(as it used to be) could greatly speed up things in certain cases

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 05a15691eb3d478e7e8a0e986babac1adb7640db..51c124a9b5d83824d0f5ba128460d2bc0ef49e6c 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -706,10 +706,12 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
       let thing_dom = domain_of_thing ~context:disambiguate_context thing in
       debug_print (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"
         (string_of_domain thing_dom)));
+(*
       debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
         (DisambiguatePp.pp_environment aliases)));
       debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s"
         (match universe with None -> "None" | Some _ -> "Some _")));
+*)
       let current_dom =
         Environment.fold (fun item _ dom -> item :: dom) aliases []
       in
@@ -790,9 +792,10 @@ in refine_profiler.HExtlib.profile foo ()
         | Invalid_choice -> Ko, ugraph
       in
       (* (4) build all possible interpretations *)
-      let rec aux aliases diff todo_dom base_univ =
+      let rec aux aliases diff lookup_in_todo_dom todo_dom base_univ =
         match todo_dom with
         | [] ->
+            assert (lookup_in_todo_dom = None);
             (match test_env aliases [] base_univ with
             | Ok (thing, metasenv),new_univ -> 
                [ aliases, diff, metasenv, thing, new_univ ]
@@ -800,32 +803,72 @@ in refine_profiler.HExtlib.profile foo ()
         | item :: remaining_dom ->
             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
              (string_of_domain_item item)));
-            let choices = lookup_choices item in
-            let rec filter univ = function 
-              | [] -> []
-              | codomain_item :: tl ->
-                  debug_print (lazy (sprintf "%s CHOSEN" (fst codomain_item))) ;
-                  let new_env = Environment.add item codomain_item aliases in
-                  let new_diff = (item,codomain_item)::diff in
-                  (match test_env new_env remaining_dom univ with
-                  | Ok (thing, metasenv),new_univ ->
-                      (match remaining_dom with
-                      | [] -> [ new_env, new_diff, metasenv, thing, new_univ ]
-                      | _ -> aux new_env new_diff remaining_dom new_univ )@ 
-                        filter univ tl
-                  | Uncertain,new_univ ->
-                      (match remaining_dom with
-                      | [] -> []
-                      | _ -> aux new_env new_diff remaining_dom new_univ )@ 
-                        filter univ tl
-                  | Ko,_ -> filter univ tl)
-            in
-            filter base_univ choices 
+            let choices =
+             match lookup_in_todo_dom with
+                None -> lookup_choices item
+              | Some choices -> choices in
+            match choices with
+               [] -> []
+             | [codomain_item] ->
+                 (* just one choice. We perform a one-step look-up and
+                    if the next set of choices is also a singleton we
+                    skip this refinement step *)
+                 debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
+                 let new_env = Environment.add item codomain_item aliases in
+                 let new_diff = (item,codomain_item)::diff in
+                 let lookup_in_todo_dom,next_choice_is_single =
+                  match remaining_dom with
+                     [] -> None,false
+                   | he::_ ->
+                      let choices = lookup_choices he in
+                       Some choices,List.length choices = 1
+                 in
+                  if next_choice_is_single then
+                   aux new_env new_diff lookup_in_todo_dom remaining_dom
+                    base_univ
+                  else
+                    (match test_env new_env remaining_dom base_univ with
+                    | Ok (thing, metasenv),new_univ ->
+                        (match remaining_dom with
+                        | [] -> [ new_env, new_diff, metasenv, thing, new_univ ]
+                        | _ ->
+                           aux new_env new_diff lookup_in_todo_dom
+                            remaining_dom new_univ)
+                    | Uncertain,new_univ ->
+                        (match remaining_dom with
+                        | [] -> []
+                        | _ ->
+                           aux new_env new_diff lookup_in_todo_dom
+                            remaining_dom new_univ)
+                    | Ko,_ -> [])
+             | _::_ ->
+               let rec filter univ = function 
+                | [] -> []
+                | codomain_item :: tl ->
+                    debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
+                    let new_env = Environment.add item codomain_item aliases in
+                    let new_diff = (item,codomain_item)::diff in
+                    (match test_env new_env remaining_dom univ with
+                    | Ok (thing, metasenv),new_univ ->
+                        (match remaining_dom with
+                        | [] -> [ new_env, new_diff, metasenv, thing, new_univ ]
+                        | _ -> aux new_env new_diff None remaining_dom new_univ
+                        ) @ 
+                          filter univ tl
+                    | Uncertain,new_univ ->
+                        (match remaining_dom with
+                        | [] -> []
+                        | _ -> aux new_env new_diff None remaining_dom new_univ
+                        ) @ 
+                          filter univ tl
+                    | Ko,_ -> filter univ tl)
+               in
+                filter base_univ choices
       in
       let base_univ = initial_ugraph in
       try
         let res =
-         match aux aliases [] todo_dom base_univ with
+         match aux aliases [] None todo_dom base_univ with
          | [] -> raise NoWellTypedInterpretation
          | [_,diff,metasenv,t,ugraph] ->
              debug_print (lazy "SINGLE INTERPRETATION");