experimental classification of disambiguation error, so that supposedly non significa...

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

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index f3600b7cbc34602ba9e8a433ae853aaf66f4d3b8..d334c72fe9c5c24dd757d7d15eec21030c30addd 100644 (file)
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -35,7 +35,7 @@ exception NoWellTypedInterpretation of
  int *
  ((Token.flocation list * string * string) list *
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-  Token.flocation option * string Lazy.t) list
+  Token.flocation option * string Lazy.t * bool) list
 exception PathNotWellFormed
 
   (** raised when an environment is not enough informative to decide *)
@@ -952,7 +952,7 @@ in refine_profiler.HExtlib.profile foo ()
             | Ok (thing, metasenv),new_univ -> 
                [ aliases, diff, metasenv, thing, new_univ ], []
             | Ko (loc,msg),_
-            | Uncertain (loc,msg),_ -> [],[aliases,diff,loc,msg])
+            | Uncertain (loc,msg),_ -> [],[aliases,diff,loc,msg,true])
         | (locs,item) :: remaining_dom ->
             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
              (string_of_domain_item item)));
@@ -964,7 +964,8 @@ in refine_profiler.HExtlib.profile foo ()
                [] ->
                 [], [aliases, diff,
                      Some (List.hd locs),
-                     lazy ("No choices for " ^ string_of_domain_item item)]
+                     lazy ("No choices for " ^ string_of_domain_item item),
+                     true]
              | [codomain_item] ->
                  (* just one choice. We perform a one-step look-up and
                     if the next set of choices is also a singleton we
@@ -993,41 +994,70 @@ in refine_profiler.HExtlib.profile foo ()
                             remaining_dom new_univ)
                     | Uncertain (loc,msg),new_univ ->
                         (match remaining_dom with
-                        | [] -> [], [new_env,new_diff,loc,msg]
+                        | [] -> [], [new_env,new_diff,loc,msg,true]
                         | _ ->
                            aux new_env new_diff lookup_in_todo_dom
                             remaining_dom new_univ)
-                    | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg])
+                    | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
              | _::_ ->
+                 let mark_not_significant (successes, failures) =
+                   successes,
+                   List.map
+                    (fun (env, diff, loc, msg, _b) ->
+                      env, diff, loc, msg, false)
+                    failures in
+                 let classify_errors outcome =
+                   if List.exists (function `Ok _ -> true | _ -> false) outcome
+                   then
+                     List.fold_right
+                      (fun res acc ->
+                        match res with
+                        | `Ok res -> res @@ acc
+                        | `Ko res -> mark_not_significant res @@ acc)
+                      outcome ([],[])
+                   else
+                     List.fold_right
+                      (fun res acc ->
+                        match res with
+                        | `Ok res | `Ko res -> res @@ acc)
+                      outcome ([],[]) 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 None remaining_dom new_univ
-                        ) @@ 
-                          filter univ tl
+                        let res = 
+                          (match remaining_dom with
+                          | [] -> [new_env,new_diff,metasenv,thing,new_univ], []
+                          | _ ->
+                              aux new_env new_diff None remaining_dom new_univ
+                          ) 
+                        in
+                        `Ok res :: filter univ tl
                     | Uncertain (loc,msg),new_univ ->
-                        (match remaining_dom with
-                        | [] -> [],[new_env,new_diff,loc,msg]
-                        | _ -> aux new_env new_diff None remaining_dom new_univ
-                        ) @@ 
-                          filter univ tl
-                    | Ko (loc,msg),_ -> ([],[new_env,new_diff,loc,msg]) @@ filter univ tl)
+                        let res =
+                          (match remaining_dom with
+                          | [] -> [],[new_env,new_diff,loc,msg,true]
+                          | _ ->
+                              aux new_env new_diff None remaining_dom new_univ
+                          )
+                        in
+                        `Ok res :: filter univ tl
+                    | Ko (loc,msg),_ ->
+                        let res = [],[new_env,new_diff,loc,msg,true] in
+                        `Ko res :: filter univ tl)
                in
-                filter base_univ choices
+               classify_errors (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
+        | Ko (loc,msg),_ -> ([],[aliases,diff,loc,msg,true]) in
       let base_univ = initial_ugraph in
       try
         let res =
@@ -1035,7 +1065,7 @@ in refine_profiler.HExtlib.profile foo ()
          | [],errors ->
             let errors =
              List.map
-              (fun (env,diff,loc,msg) ->
+              (fun (env,diff,loc,msg,significant) ->
                 let env' =
                  HExtlib.filter_map
                    (fun (locs,domain_item) ->
@@ -1048,7 +1078,7 @@ in refine_profiler.HExtlib.profile foo ()
                       Not_found -> None)
                    thing_dom
                 in
-                 env',diff,loc,msg
+                 env',diff,loc,msg,significant
               ) errors
             in
              raise (NoWellTypedInterpretation (0,errors))