From 1df136280cced19d29b62451c8c03948070259d8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 26 Nov 2007 11:54:52 +0000 Subject: [PATCH] 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. --- helm/software/matita/matitaExcPp.ml | 124 ++++++++++++++++++++++++--- helm/software/matita/matitaExcPp.mli | 8 +- helm/software/matita/matitaGui.ml | 81 +---------------- 3 files changed, 120 insertions(+), 93 deletions(-) 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]] -> -- 2.39.2