]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/matitaExcPp.ml
Another bug.
[helm.git] / 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.Command_error msg -> None, "Error: " ^ msg
121   | CicNotationParser.Parse_error err ->
122       None, sprintf "Parse error: %s" err
123   | UriManager.IllFormedUri uri -> None, sprintf "invalid uri: %s" uri
124   | CicEnvironment.Object_not_found uri ->
125       None, sprintf "object not found: %s" (UriManager.string_of_uri uri)
126   | Unix.Unix_error (code, api, param) ->
127       let err = Unix.error_message code in
128       None, "Unix Error (" ^ api ^ "): " ^ err
129   | HMarshal.Corrupt_file fname -> None, sprintf "file '%s' is corrupt" fname
130   | HMarshal.Format_mismatch fname
131   | HMarshal.Version_mismatch fname ->
132       None,
133       sprintf "format/version mismatch for file '%s', please recompile it'"
134         fname
135   | ProofEngineTypes.Fail msg -> None, "Tactic error: " ^ Lazy.force msg
136   | Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s
137   | ProofEngineHelpers.Bad_pattern msg ->
138      None, "Bad pattern: " ^ Lazy.force msg
139   | CicRefine.RefineFailure msg
140   | CicRefine.AssertFailure msg ->
141      None, "Refiner error: " ^ Lazy.force msg
142   | CicTypeChecker.TypeCheckerFailure msg ->
143      None, "Type checking error: " ^ Lazy.force msg
144   | CicTypeChecker.AssertFailure msg ->
145      None, "Type checking assertion failed: " ^ Lazy.force msg
146   | LibrarySync.AlreadyDefined s -> 
147      None, "Already defined: " ^ UriManager.string_of_uri s
148   | DisambiguateChoices.Choice_not_found msg ->
149      None, ("Disambiguation choice not found: " ^ Lazy.force msg)
150   | MatitaEngine.EnrichedWithLexiconStatus (exn,_) ->
151      None, "EnrichedWithLexiconStatus "^snd(to_string exn)
152   | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
153      let loc =
154       match errorll with
155          ((_,_,Some floc,_,_)::_)::_ ->
156           let (x, y) = HExtlib.loc_of_floc floc in
157           let x = x + offset in
158           let y = y + offset in
159           let floc = HExtlib.floc_of_loc (x,y) in
160            Some floc
161        | _ -> None in
162      let annotated_errorll =
163       List.rev
164        (snd
165          (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res)
166            (0,[]) errorll)) in
167      let choices = compact_disambiguation_errors true annotated_errorll in
168      let errorll =
169       (List.map
170        (function (loffset,l) ->
171          List.map
172           (function
173             passes,envs_and_diffs,msg,significant ->
174              let _,env,diff = List.hd envs_and_diffs in
175               passes,env,diff,loffset,msg,significant
176           ) l
177         ) choices) in
178      let rec aux =
179       function
180          [] -> []
181        | phase::tl ->
182           let msg =
183             (List.map (fun (passes,_,_,floc,msg,significant) ->
184               let loc_descr =
185                match floc with
186                   None -> ""
187                 | Some floc ->
188                    let (x, y) = HExtlib.loc_of_floc floc in
189                     sprintf " at %d-%d" (x+offset) (y+offset)
190               in
191                "*" ^ (if not significant then "(Spurious?) " else "")
192                ^ "Error" ^ loc_descr ^ ": " ^ Lazy.force msg,
193              passes) phase)
194           in
195            msg@aux tl in
196      let rec explain =
197       function
198          [] -> ""
199        | (msg,phases)::tl ->
200            explain tl ^
201            "***** Errors obtained during phase" ^
202             (if phases = [] then " " else "s ") ^
203             String.concat "," (List.map string_of_int phases) ^": *****\n"^
204             msg ^ "\n\n"
205      in
206       loc,
207        "********** DISAMBIGUATION ERRORS: **********\n" ^
208         explain (aux errorll)
209   | exn -> None, "Uncaught exception: " ^ Printexc.to_string exn
210