X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaExcPp.ml;h=24f25c5029d1c0941cd4aaae836ada8dda72bc75;hb=c4c2dc8bc7fd9729ca43ff1ff484fca9ac7b963e;hp=f378e99b0e0c54d65d8528506a71c5a8ce630955;hpb=d4232ba846e48a959637d94445f169deca5464b4;p=helm.git diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml index f378e99b0..24f25c502 100644 --- a/helm/software/matita/matitaExcPp.ml +++ b/helm/software/matita/matitaExcPp.ml @@ -27,16 +27,97 @@ 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) -> + let offset, msg = Lazy.force offset_msg in + offset, [[pass], [[pass], env, diff], lazy 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) -> let _,msg = to_string exn in let (x, y) = HExtlib.loc_of_floc floc in Some floc, sprintf "Error at %d-%d: %s" x y msg - | GrafiteTypes.Option_error ("baseuri", "not found" ) -> - None, - "Baseuri not set for this script. " - ^ "Use 'set \"baseuri\" \"\".' to set it." | GrafiteTypes.Command_error msg -> None, "Error: " ^ msg | CicNotationParser.Parse_error err -> None, sprintf "Parse error: %s" err @@ -54,50 +135,92 @@ let rec to_string = fname | ProofEngineTypes.Fail msg -> None, "Tactic error: " ^ Lazy.force msg | Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s - | CicRefine.RefineFailure msg -> + | ProofEngineHelpers.Bad_pattern msg -> + None, "Bad pattern: " ^ Lazy.force msg + | CicRefine.RefineFailure msg + | CicRefine.AssertFailure msg -> None, "Refiner error: " ^ Lazy.force msg + | NCicRefiner.RefineFailure msg -> + None, "NRefiner failure: " ^ snd (Lazy.force msg) + | NCicRefiner.Uncertain msg -> + None, "NRefiner uncertain: " ^ snd (Lazy.force msg) + | NCicMetaSubst.Uncertain msg -> + None, "NCicMetaSubst uncertain: " ^ Lazy.force msg + | NCicTypeChecker.TypeCheckerFailure msg -> + None, "NTypeChecker failure: " ^ Lazy.force msg + | NCicTypeChecker.AssertFailure msg -> + None, "NTypeChecker assert failure: " ^ Lazy.force msg + | NCicEnvironment.ObjectNotFound msg -> + None, "NCicEnvironment object not found: " ^ Lazy.force msg + | NCicRefiner.AssertFailure msg -> + None, "NRefiner assert failure: " ^ Lazy.force msg + | NCicEnvironment.BadDependency (msg,e) -> + None, "NCicEnvironment bad dependency: " ^ Lazy.force msg ^ + snd (to_string e) + | NCicEnvironment.BadConstraint msg -> + None, "NCicEnvironment bad constraint: " ^ Lazy.force msg + | NCicUnification.UnificationFailure msg -> + None, "NCicUnification failure: " ^ Lazy.force msg | CicTypeChecker.TypeCheckerFailure msg -> None, "Type checking error: " ^ Lazy.force msg | CicTypeChecker.AssertFailure msg -> None, "Type checking assertion failed: " ^ Lazy.force msg | LibrarySync.AlreadyDefined s -> None, "Already defined: " ^ UriManager.string_of_uri s - | CoercDb.EqCarrNotImplemented msg -> - None, ("EqCarrNotImplemented: " ^ Lazy.force msg) - | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> - let rec aux n ?(dummy=false) (prev_msg,phases) = + | DisambiguateChoices.Choice_not_found msg -> + None, ("Disambiguation choice not found: " ^ Lazy.force msg) + | MatitaEngine.EnrichedWithStatus (exn,_) -> + None, "EnrichedWithStatus "^snd(to_string exn) + | NTacStatus.Error (msg,None) -> + None, "NTactic error: " ^ Lazy.force msg + | NTacStatus.Error (msg,Some exn) -> + None, "NTactic error: " ^ Lazy.force msg ^ "\n" ^ snd(to_string exn) + | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> + let loc = + match errorll with + | ((_,_,loc_msg,_)::_)::_ -> + let floc, _ = Lazy.force loc_msg in + if floc = Stdpp.dummy_loc then None else + let (x, y) = HExtlib.loc_of_floc floc in + let x = x + offset in + let y = y + offset in + let floc = HExtlib.floc_of_loc (x,y) in + Some floc + | _ -> assert false + 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 + let rec aux = function - [] -> [prev_msg,phases] + [] -> [] | phase::tl -> let msg = - String.concat "\n\n\n" - (List.map (fun (_,floc,msg) -> + (List.map (fun (passes,_,_,floc,msg,significant) -> let loc_descr = - match floc with - None -> "" - | Some floc -> - let (x, y) = HExtlib.loc_of_floc floc in - sprintf " at %d-%d" (x+offset) (y+offset) + if floc = HExtlib.dummy_floc then "" + else + 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) - 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 - let loc = - match errorll with - ((_,Some floc,_)::_)::_ -> - let (x, y) = HExtlib.loc_of_floc floc in - let x = x + offset in - let y = y + offset in - let flocb,floce = floc in - let floc = - {flocb with Lexing.pos_cnum = x}, {floce with Lexing.pos_cnum = y} + "*" ^ (if not significant then "(Spurious?) " else "") + ^ "Error" ^ loc_descr ^ ": " ^ Lazy.force msg, + passes) phase) in - Some floc - | _ -> None in + msg@aux tl in let rec explain = function [] -> "" @@ -110,6 +233,6 @@ let rec to_string = in loc, "********** DISAMBIGUATION ERRORS: **********\n" ^ - explain (aux 1 ~dummy:true ("",[]) errorll) + explain (aux errorll) | exn -> None, "Uncaught exception: " ^ Printexc.to_string exn