helm/software/matita/matitaExcPp.ml

   1 (* Copyright (C) 2004-2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id$ *)
  27
  28 open Printf
  29
  30 let compact_disambiguation_errors all_passes errorll =
  31   let choices =
  32    List.flatten
  33     (List.map
  34       (fun (pass,l) ->
  35         List.map
  36          (fun (env,diff,offset,msg,significant) ->
  37            offset, [[pass], [[pass], env, diff], msg, significant]) l
  38       ) errorll) in
  39   (* Here we are doing a stable sort and list_uniq returns the latter
  40      "equal" element. I.e. we are showing the error corresponding to the
  41      most advanced disambiguation pass *)
  42   let choices =
  43    let choices_compare (o1,_) (o2,_) = compare o1 o2 in
  44    let choices_compare_by_passes (p1,_,_,_) (p2,_,_,_) =
  45     compare p1 p2 in
  46    let rec uniq =
  47     function
  48        [] -> []
  49      | h::[] -> [h]
  50      | (o1,res1)::(o2,res2)::tl when o1 = o2 ->
  51         let merge_by_name errors =
  52          let merge_by_env errors =
  53           let choices_compare_by_env (_,e1,_) (_,e2,_) = compare e1 e2 in
  54           let choices_compare_by_passes (p1,_,_) (p2,_,_) =
  55            compare p1 p2 in
  56           let rec uniq_by_env =
  57            function
  58               [] -> []
  59             | h::[] -> [h]
  60             | (p1,e1,_)::(p2,e2,d2)::tl when e1 = e2 ->
  61                 uniq_by_env ((p1@p2,e2,d2) :: tl)
  62             | h1::tl -> h1 :: uniq_by_env tl
  63           in
  64            List.sort choices_compare_by_passes
  65             (uniq_by_env (List.stable_sort choices_compare_by_env errors))
  66          in
  67          let choices_compare_by_msg (_,_,m1,_) (_,_,m2,_) =
  68           compare (Lazy.force m1) (Lazy.force m2) in
  69          let rec uniq_by_msg =
  70           function
  71              [] -> []
  72            | h::[] -> [h]
  73            | (p1,i1,m1,s1)::(p2,i2,m2,s2)::tl
  74              when Lazy.force m1 = Lazy.force m2 && s1 = s2 ->
  75                uniq_by_msg ((p1@p2,merge_by_env (i1@i2),m2,s2) :: tl)
  76            | h1::tl -> h1 :: uniq_by_msg tl
  77          in
  78           List.sort choices_compare_by_msg
  79            (uniq_by_msg (List.stable_sort choices_compare_by_msg errors))
  80         in
  81          let res = merge_by_name (res1@res2) in
  82           uniq ((o1,res) :: tl)
  83      | h1::tl -> h1 :: uniq tl
  84    in
  85    (* Errors in phase 3 that are not also in phase 4 are filtered out *)
  86    let filter_phase_3 choices =
  87     if all_passes then choices
  88     else
  89      let filter =
  90       HExtlib.filter_map
  91        (function
  92            (loffset,messages) ->
  93               let filtered_messages =
  94                HExtlib.filter_map
  95                 (function
  96                     [3],_,_,_ -> None
  97                   | item -> Some item
  98                 ) messages
  99               in
 100                if filtered_messages = [] then
 101                 None
 102                else
 103                 Some (loffset,filtered_messages))
 104      in
 105       filter choices
 106    in
 107     filter_phase_3
 108      (List.map (fun o,l -> o,List.sort choices_compare_by_passes l)
 109        (uniq (List.stable_sort choices_compare choices)))
 110   in
 111    choices
 112 ;;
 113
 114 let rec to_string =
 115   function
 116   | HExtlib.Localized (floc,exn) ->
 117       let _,msg = to_string exn in
 118       let (x, y) = HExtlib.loc_of_floc floc in
 119        Some floc, sprintf "Error at %d-%d: %s" x y msg
 120   | GrafiteTypes.Option_error ("baseuri", "not found" ) ->
 121       None,
 122       "Baseuri not set for this script. "
 123       ^ "Use 'set \"baseuri\" \"<uri>\".' to set it."
 124   | GrafiteTypes.Command_error msg -> None, "Error: " ^ msg
 125   | CicNotationParser.Parse_error err ->
 126       None, sprintf "Parse error: %s" err
 127   | UriManager.IllFormedUri uri -> None, sprintf "invalid uri: %s" uri
 128   | CicEnvironment.Object_not_found uri ->
 129       None, sprintf "object not found: %s" (UriManager.string_of_uri uri)
 130   | Unix.Unix_error (code, api, param) ->
 131       let err = Unix.error_message code in
 132       None, "Unix Error (" ^ api ^ "): " ^ err
 133   | HMarshal.Corrupt_file fname -> None, sprintf "file '%s' is corrupt" fname
 134   | HMarshal.Format_mismatch fname
 135   | HMarshal.Version_mismatch fname ->
 136       None,
 137       sprintf "format/version mismatch for file '%s', please recompile it'"
 138         fname
 139   | ProofEngineTypes.Fail msg -> None, "Tactic error: " ^ Lazy.force msg
 140   | Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s
 141   | ProofEngineHelpers.Bad_pattern msg ->
 142      None, "Bad pattern: " ^ Lazy.force msg
 143   | CicRefine.RefineFailure msg
 144   | CicRefine.AssertFailure msg ->
 145      None, "Refiner error: " ^ Lazy.force msg
 146   | CicTypeChecker.TypeCheckerFailure msg ->
 147      None, "Type checking error: " ^ Lazy.force msg
 148   | CicTypeChecker.AssertFailure msg ->
 149      None, "Type checking assertion failed: " ^ Lazy.force msg
 150   | LibrarySync.AlreadyDefined s ->
 151      None, "Already defined: " ^ UriManager.string_of_uri s
 152   | CoercDb.EqCarrNotImplemented msg ->
 153      None, ("EqCarrNotImplemented: " ^ Lazy.force msg)
 154   | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
 155      let loc =
 156       match errorll with
 157          ((_,_,Some floc,_,_)::_)::_ ->
 158           let (x, y) = HExtlib.loc_of_floc floc in
 159           let x = x + offset in
 160           let y = y + offset in
 161           let floc = HExtlib.floc_of_loc (x,y) in
 162            Some floc
 163        | _ -> None in
 164      let annotated_errorll =
 165       List.rev
 166        (snd
 167          (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res)
 168            (0,[]) errorll)) in
 169      let choices = compact_disambiguation_errors true annotated_errorll in
 170      let errorll =
 171       (List.map
 172        (function (loffset,l) ->
 173          List.map
 174           (function
 175             passes,envs_and_diffs,msg,significant ->
 176              let _,env,diff = List.hd envs_and_diffs in
 177               passes,env,diff,loffset,msg,significant
 178           ) l
 179         ) choices) in
 180      let rec aux =
 181       function
 182          [] -> []
 183        | phase::tl ->
 184           let msg =
 185             (List.map (fun (passes,_,_,floc,msg,significant) ->
 186               let loc_descr =
 187                match floc with
 188                   None -> ""
 189                 | Some floc ->
 190                    let (x, y) = HExtlib.loc_of_floc floc in
 191                     sprintf " at %d-%d" (x+offset) (y+offset)
 192               in
 193                "*" ^ (if not significant then "(Spurious?) " else "")
 194                ^ "Error" ^ loc_descr ^ ": " ^ Lazy.force msg,
 195              passes) phase)
 196           in
 197            msg@aux tl in
 198      let rec explain =
 199       function
 200          [] -> ""
 201        | (msg,phases)::tl ->
 202            explain tl ^
 203            "***** Errors obtained during phase" ^
 204             (if phases = [] then " " else "s ") ^
 205             String.concat "," (List.map string_of_int phases) ^": *****\n"^
 206             msg ^ "\n\n"
 207      in
 208       loc,
 209        "********** DISAMBIGUATION ERRORS: **********\n" ^
 210         explain (aux errorll)
 211   | exn -> None, "Uncaught exception: " ^ Printexc.to_string exn
 212