X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2FmatitaExcPp.ml;fp=matita%2FmatitaExcPp.ml;h=24981af6bc6e754b4595b9b04614a26b478ea050;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/matitaExcPp.ml b/matita/matitaExcPp.ml new file mode 100644 index 000000000..24981af6b --- /dev/null +++ b/matita/matitaExcPp.ml @@ -0,0 +1,210 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id$ *) + +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) -> + 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.Command_error msg -> None, "Error: " ^ msg + | CicNotationParser.Parse_error err -> + None, sprintf "Parse error: %s" err + | UriManager.IllFormedUri uri -> None, sprintf "invalid uri: %s" uri + | CicEnvironment.Object_not_found uri -> + None, sprintf "object not found: %s" (UriManager.string_of_uri uri) + | Unix.Unix_error (code, api, param) -> + let err = Unix.error_message code in + None, "Unix Error (" ^ api ^ "): " ^ err + | HMarshal.Corrupt_file fname -> None, sprintf "file '%s' is corrupt" fname + | HMarshal.Format_mismatch fname + | HMarshal.Version_mismatch fname -> + None, + sprintf "format/version mismatch for file '%s', please recompile it'" + fname + | ProofEngineTypes.Fail msg -> None, "Tactic error: " ^ Lazy.force msg + | Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s + | ProofEngineHelpers.Bad_pattern msg -> + None, "Bad pattern: " ^ Lazy.force msg + | CicRefine.RefineFailure msg + | CicRefine.AssertFailure msg -> + None, "Refiner error: " ^ 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) + | MatitaEngine.EnrichedWithLexiconStatus (exn,_) -> + None, "EnrichedWithLexiconStatus "^snd(to_string exn) + | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> + 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 floc = HExtlib.floc_of_loc (x,y) in + Some floc + | _ -> None 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 + [] -> [] + | phase::tl -> + let 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) + in + "*" ^ (if not significant then "(Spurious?) " else "") + ^ "Error" ^ loc_descr ^ ": " ^ Lazy.force msg, + passes) phase) + in + msg@aux tl in + let rec explain = + function + [] -> "" + | (msg,phases)::tl -> + explain tl ^ + "***** Errors obtained during phase" ^ + (if phases = [] then " " else "s ") ^ + String.concat "," (List.map string_of_int phases) ^": *****\n"^ + msg ^ "\n\n" + in + loc, + "********** DISAMBIGUATION ERRORS: **********\n" ^ + explain (aux errorll) + | exn -> None, "Uncaught exception: " ^ Printexc.to_string exn +