From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 5 Dec 2006 17:11:23 +0000 (+0000)
Subject: experimental classification of disambiguation error, so that supposedly non significa... 
X-Git-Tag: 0.4.95@7852~749
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=45ac0bf0fb6c58e03646588d4f81cf5125058e67;p=helm.git

experimental classification of disambiguation error, so that supposedly non significant errors can be hidden to the user
ATM an error is non significant if obtained interpretating a symbol that can be interpreted in an error-free way
---

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index f3600b7cb..d334c72fe 100644
--- 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))
diff --git a/components/cic_disambiguation/disambiguate.mli b/components/cic_disambiguation/disambiguate.mli
index 4a8f90b00..021fe1c9d 100644
--- a/components/cic_disambiguation/disambiguate.mli
+++ b/components/cic_disambiguation/disambiguate.mli
@@ -26,11 +26,18 @@
 (** {2 Disambiguation interface} *)
 
 (* the integer is an offset to be added to each location *)
+(* list of located error messages, each list is a tuple:
+  * - environment in string form
+  * - environment patch
+  * - location
+  * - error message
+  * - significancy of the error message, if false the error is likely to be
+  *   useless for the final user ... *)
 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
 
 val interpretate_path :
diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 65371bc67..9eb1e53fa 100644
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -157,7 +157,7 @@ let disambiguate_tactic
                     metasenv,(GrafiteAst.Type (uri, tyno) :: types)
                 | _ ->
                   raise (GrafiteDisambiguator.DisambiguationError
-                   (0,[[[],[],None,lazy "Decompose works only on inductive types"]])))
+                   (0,[[[],[],None,lazy "Decompose works only on inductive types",true]])))
         in
         let metasenv,types =
          List.fold_left disambiguate (metasenv,[]) types
diff --git a/components/grafite_parser/grafiteDisambiguator.ml b/components/grafite_parser/grafiteDisambiguator.ml
index 2c38dd8a9..4f812ff2f 100644
--- a/components/grafite_parser/grafiteDisambiguator.ml
+++ b/components/grafite_parser/grafiteDisambiguator.ml
@@ -33,7 +33,7 @@ exception DisambiguationError of
  int *
  ((Token.flocation list * string * string) list *
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-  Token.flocation option * string Lazy.t) list list
+  Token.flocation option * string Lazy.t * bool) list list
   (** parameters are: option name, error message *)
 exception Unbound_identifier of string
 
diff --git a/components/grafite_parser/grafiteDisambiguator.mli b/components/grafite_parser/grafiteDisambiguator.mli
index 1b63690d7..f37991f93 100644
--- a/components/grafite_parser/grafiteDisambiguator.mli
+++ b/components/grafite_parser/grafiteDisambiguator.mli
@@ -31,7 +31,7 @@ exception DisambiguationError of
  int *
  ((Token.flocation list * string * string) list *
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-  Token.flocation option * string Lazy.t) list list
+  Token.flocation option * string Lazy.t * bool) list list
   (** parameters are: option name, error message *)
 
 (** initially false; for debugging only (???) *)
diff --git a/matita/matitaExcPp.ml b/matita/matitaExcPp.ml
index a314556bd..8ed272454 100644
--- a/matita/matitaExcPp.ml
+++ b/matita/matitaExcPp.ml
@@ -71,7 +71,7 @@ let rec to_string =
        | phase::tl ->
           let msg =
            String.concat "\n\n\n"
-            (List.map (fun (_,_,floc,msg) ->
+            (List.map (fun (_,_,floc,msg,significant) ->
               let loc_descr =
                match floc with
                   None -> ""
@@ -79,7 +79,8 @@ let rec to_string =
                    let (x, y) = HExtlib.loc_of_floc floc in
                     sprintf " at %d-%d" (x+offset) (y+offset)
               in
-               "*Error" ^ loc_descr ^ ": " ^ Lazy.force msg) phase)
+               "*" ^ (if not significant then "(Ignorable) " else "")
+               ^ "Error" ^ loc_descr ^ ": " ^ Lazy.force msg) phase)
           in
            if msg = prev_msg then
             aux (n+1) (msg,phases@[n]) tl
@@ -88,7 +89,7 @@ let rec to_string =
              (aux (n+1) (msg,[n]) tl) in
      let loc =
       match errorll with
-         ((_,_,Some floc,_)::_)::_ ->
+         ((_,_,Some floc,_,_)::_)::_ ->
           let (x, y) = HExtlib.loc_of_floc floc in
           let x = x + offset in
           let y = y + offset in
diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index ff00ce27b..bd434ed74 100644
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -157,7 +157,7 @@ class interpErrorModel =
               (let loc_row = tree_store#append () in
                 begin
                  match lll with
-                    [passes,envs_and_diffs,_] ->
+                    [passes,envs_and_diffs,_,_] ->
                       tree_store#set ~row:loc_row ~column:id_col
                        ("Error location " ^ string_of_int (!idx1+1) ^
                         ", error message " ^ string_of_int (!idx1+1) ^ ".1" ^
@@ -175,7 +175,7 @@ class interpErrorModel =
                 Some loc_row) in
             let idx2 = ref ~-1 in
              List.iter
-              (fun passes,envs_and_diffs,_ ->
+              (fun passes,envs_and_diffs,_,_ ->
                 incr idx2;
                 let msg_row =
                  if List.length lll = 1 then
@@ -235,10 +235,14 @@ class interpErrorModel =
 let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll
 = 
   let errorll' =
+   let remove_non_significant =
+     List.filter (fun (_env,_diff,_loc,_msg,significant) -> significant) in
    if all_passes then errorll else
     (* We remove passes 1,2 and 5,6 *)
-    []::[]::
-     List.tl (List.tl (List.rev (List.tl (List.tl (List.rev errorll))))) in
+     []::[]
+     ::(remove_non_significant (List.nth errorll 2))
+     ::(remove_non_significant (List.nth errorll 3))
+     ::[]::[] in
   let choices =
    let pass = ref 0 in
    List.flatten
@@ -246,15 +250,15 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
       (fun l ->
         incr pass;
         List.map
-         (fun (env,diff,offset,msg) ->
-           offset, [[!pass], [[!pass], env, diff], msg]) l
+         (fun (env,diff,offset,msg,significant) ->
+           offset, [[!pass], [[!pass], env, diff], msg, significant]) l
       ) errorll') in
   (* Here we are doing a stable sort and list_uniq returns the latter
      "equal" element. I.e. we are showing the error corresponding to the
      most advanced disambiguation pass *)
   let choices =
    let choices_compare (o1,_) (o2,_) = compare o1 o2 in
-   let choices_compare_by_passes (p1,_,_) (p2,_,_) =
+   let choices_compare_by_passes (p1,_,_,_) (p2,_,_,_) =
     compare p1 p2 in
    let rec uniq =
     function
@@ -277,14 +281,15 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
            List.sort choices_compare_by_passes
             (uniq_by_env (List.stable_sort choices_compare_by_env errors))
          in
-         let choices_compare_by_msg (_,_,m1) (_,_,m2) =
+         let choices_compare_by_msg (_,_,m1,_) (_,_,m2,_) =
           compare (Lazy.force m1) (Lazy.force m2) in
          let rec uniq_by_msg =
           function
              [] -> []
            | h::[] -> [h]
-           | (p1,i1,m1)::(p2,i2,m2)::tl when Lazy.force m1 = Lazy.force m2 ->
-               uniq_by_msg ((p1@p2,merge_by_env (i1@i2),m2) :: tl) 
+           | (p1,i1,m1,s1)::(p2,i2,m2,s2)::tl
+             when Lazy.force m1 = Lazy.force m2 && s1 = s2 ->
+               uniq_by_msg ((p1@p2,merge_by_env (i1@i2),m2,s2) :: tl)
            | h1::tl -> h1 :: uniq_by_msg tl
          in
           List.sort choices_compare_by_msg
@@ -299,11 +304,11 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
   in
    match choices with
       [] -> assert false
-    | [loffset,[_,envs_and_diffs,msg]] ->
+    | [loffset,[_,envs_and_diffs,msg,significant]] ->
         let _,env,diff = List.hd envs_and_diffs in
          notify_exn
           (GrafiteDisambiguator.DisambiguationError
-            (offset,[[env,diff,loffset,msg]]));
+            (offset,[[env,diff,loffset,msg,significant]]));
     | _::_ ->
        let dialog = new disambiguationErrors () in
        dialog#check_widgets ();
@@ -321,10 +326,12 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
            | Some tp -> tp in
           let idx1,idx2,idx3 = model#get_interp_no tree_path in
           let loffset,lll = List.nth choices idx1 in
-          let _,envs_and_diffs,msg =
+          let _,envs_and_diffs,msg,significant =
            match idx2 with
               Some idx2 -> List.nth lll idx2
-            | None -> [],[],lazy "Multiple error messages. Please select one." in
+            | None ->
+                [],[],lazy "Multiple error messages. Please select one.",true
+          in
           let _,env,diff =
            match idx3 with
               Some idx3 -> List.nth envs_and_diffs idx3
@@ -336,7 +343,7 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
              ~stop:source_buffer#end_iter;
            notify_exn
             (GrafiteDisambiguator.DisambiguationError
-              (offset,[[env,diff,loffset,msg]]))
+              (offset,[[env,diff,loffset,msg,significant]]))
            ));
        let return _ =
          dialog#disambiguationErrors#destroy ();
@@ -355,7 +362,7 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
            match idx2,idx3 with
               Some idx2, Some idx3 ->
                let _,lll = List.nth choices idx1 in
-               let _,envs_and_diffs,_ = List.nth lll idx2 in
+               let _,envs_and_diffs,_,_ = List.nth lll idx2 in
                let _,_,diff = List.nth envs_and_diffs idx3 in
                 diff
             | _,_ -> assert false