From: Claudio Sacerdoti Coen Date: Mon, 26 Nov 2007 11:54:52 +0000 (+0000) Subject: Disambiguation error compaction is now performed in the same way by matita and X-Git-Tag: make_still_working~5779 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1df136280cced19d29b62451c8c03948070259d8;p=helm.git Disambiguation error compaction is now performed in the same way by matita and matitac. The difference is that matitac shows every error in every pass, marking spurious errors as spurious. --- diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml index 42777735c..03f0be3dc 100644 --- a/helm/software/matita/matitaExcPp.ml +++ b/helm/software/matita/matitaExcPp.ml @@ -27,6 +27,90 @@ open Printf +let compact_disambiguation_errors all_passes errorll = + let choices = + List.flatten + (List.map + (fun (pass,l) -> + List.map + (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,_,_,_) = + compare p1 p2 in + let rec uniq = + function + [] -> [] + | h::[] -> [h] + | (o1,res1)::(o2,res2)::tl when o1 = o2 -> + let merge_by_name errors = + let merge_by_env errors = + let choices_compare_by_env (_,e1,_) (_,e2,_) = compare e1 e2 in + let choices_compare_by_passes (p1,_,_) (p2,_,_) = + compare p1 p2 in + let rec uniq_by_env = + function + [] -> [] + | h::[] -> [h] + | (p1,e1,_)::(p2,e2,d2)::tl when e1 = e2 -> + uniq_by_env ((p1@p2,e2,d2) :: tl) + | h1::tl -> h1 :: uniq_by_env tl + in + 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,_) = + compare (Lazy.force m1) (Lazy.force m2) in + let rec uniq_by_msg = + function + [] -> [] + | h::[] -> [h] + | (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 + (uniq_by_msg (List.stable_sort choices_compare_by_msg errors)) + in + let res = merge_by_name (res1@res2) in + uniq ((o1,res) :: tl) + | h1::tl -> h1 :: uniq tl + in + (* Errors in phase 3 that are not also in phase 4 are filtered out *) + let filter_phase_3 choices = + if all_passes then choices + else + let filter = + HExtlib.filter_map + (function + (loffset,messages) -> + let filtered_messages = + HExtlib.filter_map + (function + [3],_,_,_ -> None + | item -> Some item + ) messages + in + if filtered_messages = [] then + None + else + Some (loffset,filtered_messages)) + in + filter choices + in + filter_phase_3 + (List.map (fun o,l -> o,List.sort choices_compare_by_passes l) + (uniq (List.stable_sort choices_compare choices))) + in + choices +;; + let rec to_string = function | HExtlib.Localized (floc,exn) -> @@ -68,13 +152,12 @@ let rec to_string = | CoercDb.EqCarrNotImplemented msg -> None, ("EqCarrNotImplemented: " ^ Lazy.force msg) | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> - let rec aux n ?(dummy=false) (prev_msg,phases) = + let rec aux = function - [] -> [prev_msg,phases] + [] -> [] | phase::tl -> let msg = - String.concat "\n\n\n" - (List.map (fun (_,_,floc,msg,significant) -> + (List.map (fun (passes,_,_,floc,msg,significant) -> let loc_descr = match floc with None -> "" @@ -82,14 +165,11 @@ let rec to_string = let (x, y) = HExtlib.loc_of_floc floc in sprintf " at %d-%d" (x+offset) (y+offset) in - "*" ^ (if not significant then "(Ignorable) " else "") - ^ "Error" ^ loc_descr ^ ": " ^ Lazy.force msg) phase) + "*" ^ (if not significant then "(Spurious?) " else "") + ^ "Error" ^ loc_descr ^ ": " ^ Lazy.force msg, + passes) phase) in - if msg = prev_msg then - aux (n+1) (msg,phases@[n]) tl - else - (if not dummy then [prev_msg,phases] else []) @ - (aux (n+1) (msg,[n]) tl) in + msg@aux tl in let loc = match errorll with ((_,_,Some floc,_,_)::_)::_ -> @@ -109,8 +189,28 @@ let rec to_string = String.concat "," (List.map string_of_int phases) ^": *****\n"^ msg ^ "\n\n" in + (* --- *) + let annotated_errorll = + List.rev + (snd + (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res) (0,[]) + errorll)) in + let choices = compact_disambiguation_errors true annotated_errorll in + (* --- *) + let errorll = + (List.map + (function (loffset,l) -> + List.map + (function + passes,envs_and_diffs,msg,significant -> + let _,env,diff = List.hd envs_and_diffs in + passes,env,diff,loffset,msg,significant + ) l + ) choices) in + (* --- *) + loc, "********** DISAMBIGUATION ERRORS: **********\n" ^ - explain (aux 1 ~dummy:true ("",[]) errorll) + explain (aux errorll) | exn -> None, "Uncaught exception: " ^ Printexc.to_string exn diff --git a/helm/software/matita/matitaExcPp.mli b/helm/software/matita/matitaExcPp.mli index 4abe0b4f9..419b04c73 100644 --- a/helm/software/matita/matitaExcPp.mli +++ b/helm/software/matita/matitaExcPp.mli @@ -23,5 +23,11 @@ * http://helm.cs.unibo.it/ *) -val to_string: exn -> Stdpp.location option * string +val compact_disambiguation_errors : + bool -> + (int * ((Stdpp.location list * string * string) list * + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * + Stdpp.location option * string Lazy.t * bool) list) list -> + (Stdpp.location option * (int list * (int list * (Stdpp.location list * string * string) list * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list) list * string Lazy.t * bool) list) list +val to_string: exn -> Stdpp.location option * string diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index de98b49b8..6b1f24743 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -282,86 +282,7 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView. annotated_errorll () end in - let choices = - List.flatten - (List.map - (fun (pass,l) -> - List.map - (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,_,_,_) = - compare p1 p2 in - let rec uniq = - function - [] -> [] - | h::[] -> [h] - | (o1,res1)::(o2,res2)::tl when o1 = o2 -> - let merge_by_name errors = - let merge_by_env errors = - let choices_compare_by_env (_,e1,_) (_,e2,_) = compare e1 e2 in - let choices_compare_by_passes (p1,_,_) (p2,_,_) = - compare p1 p2 in - let rec uniq_by_env = - function - [] -> [] - | h::[] -> [h] - | (p1,e1,_)::(p2,e2,d2)::tl when e1 = e2 -> - uniq_by_env ((p1@p2,e2,d2) :: tl) - | h1::tl -> h1 :: uniq_by_env tl - in - 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,_) = - compare (Lazy.force m1) (Lazy.force m2) in - let rec uniq_by_msg = - function - [] -> [] - | h::[] -> [h] - | (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 - (uniq_by_msg (List.stable_sort choices_compare_by_msg errors)) - in - let res = merge_by_name (res1@res2) in - uniq ((o1,res) :: tl) - | h1::tl -> h1 :: uniq tl - in - (* Errors in phase 3 that are not also in phase 4 are filtered out *) - let filter_phase_3 choices = - if all_passes then choices - else - let filter = - HExtlib.filter_map - (function - (loffset,messages) -> - let filtered_messages = - HExtlib.filter_map - (function - [3],_,_,_ -> None - | item -> Some item - ) messages - in - if filtered_messages = [] then - None - else - Some (loffset,filtered_messages)) - in - filter choices - in - filter_phase_3 - (List.map (fun o,l -> o,List.sort choices_compare_by_passes l) - (uniq (List.stable_sort choices_compare choices))) - in + let choices = MatitaExcPp.compact_disambiguation_errors all_passes errorll' in match choices with [] -> assert false | [loffset,[_,envs_and_diffs,msg,significant]] ->