matita/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            let offset, msg = Lazy.force offset_msg in
  38            offset, [[pass], [[pass], env, diff], lazy msg, significant]) l
  39       ) errorll) in
  40   (* Here we are doing a stable sort and list_uniq returns the latter
  41      "equal" element. I.e. we are showing the error corresponding to the
  42      most advanced disambiguation pass *)
  43   let choices =
  44    let choices_compare (o1,_) (o2,_) = compare o1 o2 in
  45    let choices_compare_by_passes (p1,_,_,_) (p2,_,_,_) =
  46     compare p1 p2 in
  47    let rec uniq =
  48     function
  49        [] -> []
  50      | h::[] -> [h]
  51      | (o1,res1)::(o2,res2)::tl when o1 = o2 ->
  52         let merge_by_name errors =
  53          let merge_by_env errors =
  54           let choices_compare_by_env (_,e1,_) (_,e2,_) = compare e1 e2 in
  55           let choices_compare_by_passes (p1,_,_) (p2,_,_) =
  56            compare p1 p2 in
  57           let rec uniq_by_env =
  58            function
  59               [] -> []
  60             | h::[] -> [h]
  61             | (p1,e1,_)::(p2,e2,d2)::tl when e1 = e2 ->
  62                 uniq_by_env ((p1@p2,e2,d2) :: tl)
  63             | h1::tl -> h1 :: uniq_by_env tl
  64           in
  65            List.sort choices_compare_by_passes
  66             (uniq_by_env (List.stable_sort choices_compare_by_env errors))
  67          in
  68          let choices_compare_by_msg (_,_,m1,_) (_,_,m2,_) =
  69           compare (Lazy.force m1) (Lazy.force m2) in
  70          let rec uniq_by_msg =
  71           function
  72              [] -> []
  73            | h::[] -> [h]
  74            | (p1,i1,m1,s1)::(p2,i2,m2,s2)::tl
  75              when Lazy.force m1 = Lazy.force m2 && s1 = s2 ->
  76                uniq_by_msg ((p1@p2,merge_by_env (i1@i2),m2,s2) :: tl)
  77            | h1::tl -> h1 :: uniq_by_msg tl
  78          in
  79           List.sort choices_compare_by_msg
  80            (uniq_by_msg (List.stable_sort choices_compare_by_msg errors))
  81         in
  82          let res = merge_by_name (res1@res2) in
  83           uniq ((o1,res) :: tl)
  84      | h1::tl -> h1 :: uniq tl
  85    in
  86    (* Errors in phase 3 that are not also in phase 4 are filtered out *)
  87    let filter_phase_3 choices =
  88     if all_passes then choices
  89     else
  90      let filter =
  91       HExtlib.filter_map
  92        (function
  93            (loffset,messages) ->
  94               let filtered_messages =
  95                HExtlib.filter_map
  96                 (function
  97                     [3],_,_,_ -> None
  98                   | item -> Some item
  99                 ) messages
 100               in
 101                if filtered_messages = [] then
 102                 None
 103                else
 104                 Some (loffset,filtered_messages))
 105      in
 106       filter choices
 107    in
 108     filter_phase_3
 109      (List.map (fun o,l -> o,List.sort choices_compare_by_passes l)
 110        (uniq (List.stable_sort choices_compare choices)))
 111   in
 112    choices
 113 ;;
 114
 115 let rec to_string exn =
 116  try
 117   (match exn with
 118     HExtlib.Localized (floc,exn) ->
 119       let _,msg = to_string exn in
 120       let (x, y) = HExtlib.loc_of_floc floc in
 121        Some floc, sprintf "Error at %d-%d: %s" x y msg
 122   | NCicLibrary.IncludedFileNotCompiled (s1,s2) ->
 123       None, "Including: "^s1^" "^s2^ "\nNothing to do... did you run matitadep?"
 124   | GrafiteTypes.Command_error msg -> None, "Error: " ^ msg
 125   | CicNotationParser.Parse_error err ->
 126       None, sprintf "Parse error: %s" err
 127   | Unix.Unix_error (code, api, param) ->
 128       let err = Unix.error_message code in
 129       None, "Unix Error (" ^ api ^ "): " ^ err
 130   | HMarshal.Corrupt_file fname -> None, sprintf "file '%s' is corrupt" fname
 131   | HMarshal.Format_mismatch fname
 132   | HMarshal.Version_mismatch fname ->
 133       None,
 134       sprintf "format/version mismatch for file '%s', please recompile it'"
 135         fname
 136   | Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s
 137   | NCicRefiner.RefineFailure msg ->
 138      None, "NRefiner failure: " ^ snd (Lazy.force msg)
 139   | NCicRefiner.Uncertain msg ->
 140      None, "NRefiner uncertain: " ^ snd (Lazy.force msg)
 141   | NCicMetaSubst.Uncertain msg ->
 142      None, "NCicMetaSubst uncertain: " ^ Lazy.force msg
 143   | NCicMetaSubst.MetaSubstFailure msg ->
 144      None, "NCicMetaSubst failure: " ^ Lazy.force msg
 145   | NCicTypeChecker.TypeCheckerFailure msg ->
 146      None, "NTypeChecker failure: " ^ Lazy.force msg
 147   | NCicTypeChecker.AssertFailure msg ->
 148      None, "NTypeChecker assert failure: " ^ Lazy.force msg
 149   | NCicEnvironment.ObjectNotFound msg ->
 150      None, "NCicEnvironment object not found: " ^ Lazy.force msg
 151   | NCicEnvironment.AlreadyDefined msg ->
 152      None, "NCicEnvironment already defined: " ^ Lazy.force msg
 153   | MatitaEngine.CircularDependency fname ->
 154       None, "Circular dependency including " ^ fname
 155   | MatitaEngine.TryingToAdd msg ->
 156      None, "Attempt to insert an alias in batch mode: " ^ Lazy.force msg
 157   | MatitaEngine.AlreadyLoaded msg ->
 158      None, "The file " ^ Lazy.force msg ^ " needs recompilation but it is
 159      already loaded; undo the inclusion and try again."
 160   | MatitaEngine.FailureCompiling (filename,exn) ->
 161      None, "Compiling " ^ filename ^ ":\n" ^ snd (to_string exn)
 162   | NCicRefiner.AssertFailure msg ->
 163      None, "NRefiner assert failure: " ^ Lazy.force msg
 164   | NCicEnvironment.BadDependency (msg,e) ->
 165      None, "NCicEnvironment bad dependency: " ^ Lazy.force msg ^
 166      snd (to_string e)
 167   | NCicEnvironment.BadConstraint msg ->
 168      None, "NCicEnvironment bad constraint: " ^ Lazy.force msg
 169   | NCicUnification.UnificationFailure msg ->
 170      None, "NCicUnification failure: " ^ Lazy.force msg
 171   | NCicUnification.Uncertain msg ->
 172      None, "NCicUnification uncertain: " ^ Lazy.force msg
 173   | DisambiguateChoices.Choice_not_found msg ->
 174      None, ("Disambiguation choice not found: " ^ Lazy.force msg)
 175   | DisambiguateTypes.Invalid_choice msg ->
 176      None, ("Invalid choice: " ^ snd (Lazy.force msg))
 177   | MatitaEngine.EnrichedWithStatus (exn,_) ->
 178      None, snd(to_string exn)
 179   | NTacStatus.Error (msg,None) ->
 180      None, "NTactic error: " ^ Lazy.force msg
 181   | NTacStatus.Error (msg,Some exn) ->
 182      None, "NTactic error: " ^ Lazy.force msg ^ "\n" ^ snd(to_string exn)
 183   | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
 184      let loc =
 185       match errorll with
 186         | ((_,_,loc_msg,_)::_)::_ ->
 187           let floc, _ = Lazy.force loc_msg in
 188           if floc = Stdpp.dummy_loc then None else
 189             let (x, y) = HExtlib.loc_of_floc floc in
 190             let x = x + offset in
 191             let y = y + offset in
 192             let floc = HExtlib.floc_of_loc (x,y) in
 193              Some floc
 194         | _ -> assert false
 195      in
 196      let annotated_errorll =
 197       List.rev
 198        (snd
 199          (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res)
 200            (0,[]) errorll)) in
 201      let choices = compact_disambiguation_errors true annotated_errorll in
 202      let errorll =
 203       (List.map
 204        (function (loffset,l) ->
 205          List.map
 206           (function
 207             passes,envs_and_diffs,msg,significant ->
 208              let _,env,diff = List.hd envs_and_diffs in
 209               passes,env,diff,loffset,msg,significant
 210           ) l
 211         ) choices) in
 212      let rec aux =
 213       function
 214          [] -> []
 215        | phase::tl ->
 216           let msg =
 217             (List.map (fun (passes,_,_,floc,msg,significant) ->
 218               let loc_descr =
 219                 if floc = HExtlib.dummy_floc then ""
 220                 else
 221                   let (x, y) = HExtlib.loc_of_floc floc in
 222                   sprintf " at %d-%d" (x+offset) (y+offset)
 223               in
 224                "*" ^ (if not significant then "(Spurious?) " else "")
 225                ^ "Error" ^ loc_descr ^ ": " ^ Lazy.force msg,
 226              passes) phase)
 227           in
 228            msg@aux tl in
 229      let rec explain =
 230       function
 231          [] -> ""
 232        | (msg,phases)::tl ->
 233            explain tl ^
 234            "***** Errors obtained during phase" ^
 235             (if phases = [] then " " else "s ") ^
 236             String.concat "," (List.map string_of_int phases) ^": *****\n"^
 237             msg ^ "\n\n"
 238      in
 239       loc,
 240        "********** DISAMBIGUATION ERRORS: **********\n" ^
 241         explain (aux errorll)
 242   | exn -> None, ("Uncaught exception: " ^ Printexc.to_string exn ^ Printexc.get_backtrace ()))
 243  with exn ->
 244   None, ("Exception raised during pretty-printing of an exception: " ^
 245    snd (to_string exn))