]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/matitaExcPp.ml
Added copy machine (mockup)
[helm.git] / matitaB / 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 = 
116   function
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   | NCicLibrary.IncludedFileNotCompiled (s1,s2) ->
122       None, "Including: "^s1^" "^s2^ "\nNothing to do... did you run matitadep?"
123   | GrafiteTypes.Command_error msg -> None, "Error: " ^ msg
124   | CicNotationParser.Parse_error err ->
125       None, sprintf "Parse error: %s" err
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   | Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s
136   | NCicRefiner.RefineFailure msg ->
137      None, "NRefiner failure: " ^ snd (Lazy.force msg)
138   | NCicRefiner.Uncertain msg ->
139      None, "NRefiner uncertain: " ^ snd (Lazy.force msg)
140   | NCicMetaSubst.Uncertain msg ->
141      None, "NCicMetaSubst uncertain: " ^ Lazy.force msg
142   | NCicTypeChecker.TypeCheckerFailure msg ->
143      None, "NTypeChecker failure: " ^ Lazy.force msg
144   | NCicTypeChecker.AssertFailure msg ->
145      None, "NTypeChecker assert failure: " ^ Lazy.force msg
146   | NCicEnvironment.ObjectNotFound msg ->
147      None, "NCicEnvironment object not found: " ^ Lazy.force msg
148   | NCicEnvironment.AlreadyDefined msg ->
149      None, "NCicEnvironment already defined: " ^ Lazy.force msg
150   | MatitaEngine.CircularDependency fname ->
151       None, "Circular dependency including " ^ fname
152   | MatitaEngine.TryingToAdd msg ->
153      None, "Attempt to insert an alias in batch mode: " ^ Lazy.force msg
154   | MatitaEngine.AlreadyLoaded msg ->
155      None, "The file " ^ Lazy.force msg ^ " needs recompilation but it is
156      already loaded; undo the inclusion and try again."
157   | MatitaEngine.FailureCompiling (filename,exn) ->
158      None, "Compiling " ^ filename ^ ":\n" ^ snd (to_string exn)
159   | NCicRefiner.AssertFailure msg ->
160      None, "NRefiner assert failure: " ^ Lazy.force msg
161   | NCicEnvironment.BadDependency (msg,e) ->
162      None, "NCicEnvironment bad dependency: " ^ Lazy.force msg ^ 
163      snd (to_string e)
164   | NCicEnvironment.BadConstraint msg ->
165      None, "NCicEnvironment bad constraint: " ^ Lazy.force msg
166   | NCicUnification.UnificationFailure msg ->
167      None, "NCicUnification failure: " ^ Lazy.force msg
168   | NCicUnification.Uncertain msg ->
169      None, "NCicUnification uncertain: " ^ Lazy.force msg
170   | DisambiguateChoices.Choice_not_found msg ->
171      None, ("Disambiguation choice not found: " ^ Lazy.force msg)
172   | MatitaEngine.EnrichedWithStatus (exn,_) ->
173      None, snd(to_string exn)
174   | NTacStatus.Error (msg,None) ->
175      None, "NTactic error: " ^ Lazy.force msg 
176   | NTacStatus.Error (msg,Some exn) ->
177      None, "NTactic error: " ^ Lazy.force msg ^ "\n" ^ snd(to_string exn)
178 (*  | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
179      let loc =
180       match errorll with
181         | ((_,_,loc_msg,_)::_)::_ ->
182           let floc, _ = Lazy.force loc_msg in
183           if floc = Stdpp.dummy_loc then None else
184             let (x, y) = HExtlib.loc_of_floc floc in
185             let x = x + offset in
186             let y = y + offset in
187             let floc = HExtlib.floc_of_loc (x,y) in
188              Some floc
189         | _ -> (* assert false *) None
190      in
191      let annotated_errorll =
192       List.rev
193        (snd
194          (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res)
195            (0,[]) errorll)) in
196      let choices = compact_disambiguation_errors true annotated_errorll in
197      let errorll =
198       (List.map
199        (function (loffset,l) ->
200          List.map
201           (function
202             passes,envs_and_diffs,msg,significant ->
203              let _,env,diff = List.hd envs_and_diffs in
204               passes,env,diff,loffset,msg,significant
205           ) l
206         ) choices) in
207      let rec aux =
208       function
209          [] -> []
210        | phase::tl ->
211           let msg =
212             (List.map (fun (passes,_,_,floc,msg,significant) ->
213               let loc_descr =
214                 if floc = HExtlib.dummy_floc then "" 
215                 else 
216                   let (x, y) = HExtlib.loc_of_floc floc in
217                   sprintf " at %d-%d" (x+offset) (y+offset)
218               in
219                "*" ^ (if not significant then "(Spurious?) " else "")
220                ^ "Error" ^ loc_descr ^ ": " ^ Lazy.force msg,
221              passes) phase)
222           in
223            msg@aux tl in
224      let rec explain =
225       function
226          [] -> ""
227        | (msg,phases)::tl ->
228            explain tl ^
229            "***** Errors obtained during phase" ^
230             (if phases = [] then " " else "s ") ^
231             String.concat "," (List.map string_of_int phases) ^": *****\n"^
232             msg ^ "\n\n"
233      in
234       loc,
235        "********** DISAMBIGUATION ERRORS: **********\n" ^
236         explain (aux errorll) *)
237   | exn -> None, "Uncaught exception: " ^ Printexc.to_string exn
238