1 (* Copyright (C) 2004-2005, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 let compact_disambiguation_errors all_passes errorll =
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
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 *)
44 let choices_compare (o1,_) (o2,_) = compare o1 o2 in
45 let choices_compare_by_passes (p1,_,_,_) (p2,_,_,_) =
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,_,_) =
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
65 List.sort choices_compare_by_passes
66 (uniq_by_env (List.stable_sort choices_compare_by_env errors))
68 let choices_compare_by_msg (_,_,m1,_) (_,_,m2,_) =
69 compare (Lazy.force m1) (Lazy.force m2) in
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
79 List.sort choices_compare_by_msg
80 (uniq_by_msg (List.stable_sort choices_compare_by_msg errors))
82 let res = merge_by_name (res1@res2) in
84 | h1::tl -> h1 :: uniq tl
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
94 let filtered_messages =
101 if filtered_messages = [] then
104 Some (loffset,filtered_messages))
109 (List.map (fun o,l -> o,List.sort choices_compare_by_passes l)
110 (uniq (List.stable_sort choices_compare choices)))
117 | HExtlib.Localized (floc,exn) ->
118 let _,msg = to_string exn in
119 let (x, y) = HExtlib.loc_of_floc floc in
120 Some floc, sprintf "Error at %d-%d: %s" x y msg
121 | GrafiteTypes.Command_error msg -> None, "Error: " ^ msg
122 | CicNotationParser.Parse_error err ->
123 None, sprintf "Parse error: %s" err
124 | UriManager.IllFormedUri uri -> None, sprintf "invalid uri: %s" uri
125 | Unix.Unix_error (code, api, param) ->
126 let err = Unix.error_message code in
127 None, "Unix Error (" ^ api ^ "): " ^ err
128 | HMarshal.Corrupt_file fname -> None, sprintf "file '%s' is corrupt" fname
129 | HMarshal.Format_mismatch fname
130 | HMarshal.Version_mismatch fname ->
132 sprintf "format/version mismatch for file '%s', please recompile it'"
134 | Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s
135 | NCicRefiner.RefineFailure msg ->
136 None, "NRefiner failure: " ^ snd (Lazy.force msg)
137 | NCicRefiner.Uncertain msg ->
138 None, "NRefiner uncertain: " ^ snd (Lazy.force msg)
139 | NCicMetaSubst.Uncertain msg ->
140 None, "NCicMetaSubst uncertain: " ^ Lazy.force msg
141 | NCicTypeChecker.TypeCheckerFailure msg ->
142 None, "NTypeChecker failure: " ^ Lazy.force msg
143 | NCicTypeChecker.AssertFailure msg ->
144 None, "NTypeChecker assert failure: " ^ Lazy.force msg
145 | NCicEnvironment.ObjectNotFound msg ->
146 None, "NCicEnvironment object not found: " ^ Lazy.force msg
147 | NCicEnvironment.AlreadyDefined msg ->
148 None, "NCicEnvironment already defined: " ^ Lazy.force msg
149 | NCicRefiner.AssertFailure msg ->
150 None, "NRefiner assert failure: " ^ Lazy.force msg
151 | NCicEnvironment.BadDependency (msg,e) ->
152 None, "NCicEnvironment bad dependency: " ^ Lazy.force msg ^
154 | NCicEnvironment.BadConstraint msg ->
155 None, "NCicEnvironment bad constraint: " ^ Lazy.force msg
156 | NCicUnification.UnificationFailure msg ->
157 None, "NCicUnification failure: " ^ Lazy.force msg
158 | NCicUnification.Uncertain msg ->
159 None, "NCicUnification uncertain: " ^ Lazy.force msg
160 | DisambiguateChoices.Choice_not_found msg ->
161 None, ("Disambiguation choice not found: " ^ Lazy.force msg)
162 | MatitaEngine.EnrichedWithStatus (exn,_) ->
163 None, "EnrichedWithStatus "^snd(to_string exn)
164 | NTacStatus.Error (msg,None) ->
165 None, "NTactic error: " ^ Lazy.force msg
166 | NTacStatus.Error (msg,Some exn) ->
167 None, "NTactic error: " ^ Lazy.force msg ^ "\n" ^ snd(to_string exn)
168 | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
171 | ((_,_,loc_msg,_)::_)::_ ->
172 let floc, _ = Lazy.force loc_msg in
173 if floc = Stdpp.dummy_loc then None else
174 let (x, y) = HExtlib.loc_of_floc floc in
175 let x = x + offset in
176 let y = y + offset in
177 let floc = HExtlib.floc_of_loc (x,y) in
181 let annotated_errorll =
184 (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res)
186 let choices = compact_disambiguation_errors true annotated_errorll in
189 (function (loffset,l) ->
192 passes,envs_and_diffs,msg,significant ->
193 let _,env,diff = List.hd envs_and_diffs in
194 passes,env,diff,loffset,msg,significant
202 (List.map (fun (passes,_,_,floc,msg,significant) ->
204 if floc = HExtlib.dummy_floc then ""
206 let (x, y) = HExtlib.loc_of_floc floc in
207 sprintf " at %d-%d" (x+offset) (y+offset)
209 "*" ^ (if not significant then "(Spurious?) " else "")
210 ^ "Error" ^ loc_descr ^ ": " ^ Lazy.force msg,
217 | (msg,phases)::tl ->
219 "***** Errors obtained during phase" ^
220 (if phases = [] then " " else "s ") ^
221 String.concat "," (List.map string_of_int phases) ^": *****\n"^
225 "********** DISAMBIGUATION ERRORS: **********\n" ^
226 explain (aux errorll)
227 | exn -> None, "Uncaught exception: " ^ Printexc.to_string exn