Missing optimization implemented: before starting to analyze the disambiguation

[helm.git] / helm / software / components / cic_disambiguation / disambiguate.ml

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 243f7c8bfe22313aa71e0f2643d7c91b28518187..3f3d8235aa79730fbb850c8cb3fd93303e398097 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -32,7 +32,10 @@ open UriManager
 
 (* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
- int * (Token.flocation option * string Lazy.t) list
+ int *
+ ((Token.flocation list * string * string) list *
+  (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+  Token.flocation option * string Lazy.t) list
 exception PathNotWellFormed
 
   (** raised when an environment is not enough informative to decide *)
@@ -945,7 +948,8 @@ in refine_profiler.HExtlib.profile foo ()
             (match test_env aliases [] base_univ with
             | Ok (thing, metasenv),new_univ -> 
                [ aliases, diff, metasenv, thing, new_univ ], []
-            | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg])
+            | Ko (loc,msg),_
+            | Uncertain (loc,msg),_ -> [],[aliases,diff,loc,msg])
         | (locs,item) :: remaining_dom ->
             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
              (string_of_domain_item item)));
@@ -955,7 +959,8 @@ in refine_profiler.HExtlib.profile foo ()
               | Some choices -> choices in
             match choices with
                [] ->
-                [], [Some (List.hd locs),
+                [], [aliases, diff,
+                     Some (List.hd locs),
                      lazy ("No choices for " ^ string_of_domain_item item)]
              | [codomain_item] ->
                  (* just one choice. We perform a one-step look-up and
@@ -985,11 +990,11 @@ in refine_profiler.HExtlib.profile foo ()
                             remaining_dom new_univ)
                     | Uncertain (loc,msg),new_univ ->
                         (match remaining_dom with
-                        | [] -> [], [loc,msg]
+                        | [] -> [], [new_env,new_diff,loc,msg]
                         | _ ->
                            aux new_env new_diff lookup_in_todo_dom
                             remaining_dom new_univ)
-                    | Ko (loc,msg),_ -> [], [loc,msg])
+                    | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg])
              | _::_ ->
                let rec filter univ = function 
                 | [] -> [],[]
@@ -1000,25 +1005,50 @@ in refine_profiler.HExtlib.profile foo ()
                     (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 ], []
+                        | [] -> [new_env,new_diff,metasenv,thing,new_univ], []
                         | _ -> aux new_env new_diff None remaining_dom new_univ
                         ) @@ 
                           filter univ tl
                     | Uncertain (loc,msg),new_univ ->
                         (match remaining_dom with
-                        | [] -> [],[loc,msg]
+                        | [] -> [],[new_env,new_diff,loc,msg]
                         | _ -> aux new_env new_diff None remaining_dom new_univ
                         ) @@ 
                           filter univ tl
-                    | Ko (loc,msg),_ -> ([],[loc,msg]) @@ filter univ tl)
+                    | Ko (loc,msg),_ -> ([],[new_env,new_diff,loc,msg]) @@ filter univ tl)
                in
                 filter base_univ choices
       in
+      let aux' aliases diff lookup_in_todo_dom todo_dom base_univ =
+       match test_env aliases todo_dom base_univ with
+        | Ok _,_
+        | Uncertain _,_ ->
+           aux aliases diff lookup_in_todo_dom todo_dom base_univ
+        | Ko (loc,msg),_ -> ([],[aliases,diff,loc,msg]) in
       let base_univ = initial_ugraph in
       try
         let res =
-         match aux aliases [] None todo_dom base_univ with
-         | [],errors -> raise (NoWellTypedInterpretation (0,errors))
+         match aux' aliases [] None todo_dom base_univ with
+         | [],errors ->
+            let errors =
+             List.map
+              (fun (env,diff,loc,msg) ->
+                let env' =
+                 HExtlib.filter_map
+                   (fun (locs,domain_item) ->
+                     try
+                      let description =
+                       fst (Environment.find domain_item env)
+                      in
+                       Some (locs,descr_of_domain_item domain_item,description)
+                     with
+                      Not_found -> None)
+                   thing_dom
+                in
+                 env',diff,loc,msg
+              ) errors
+            in
+             raise (NoWellTypedInterpretation (0,errors))
          | [_,diff,metasenv,t,ugraph],_ ->
              debug_print (lazy "SINGLE INTERPRETATION");
              [diff,metasenv,t,ugraph], false