]> matita.cs.unibo.it Git - helm.git/blob - matita/matitacLib.ml
added metas local context maction: ?n[...]
[helm.git] / matita / matitacLib.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 open GrafiteTypes
31
32 exception AttemptToInsertAnAlias
33
34 let pp_ast_statement =
35   GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
36     ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:CicNotationPp.pp_obj
37
38 (** {2 Initialization} *)
39
40 let grafite_status = (ref None : GrafiteTypes.status option ref)
41 let lexicon_status = (ref None : LexiconEngine.status option ref)
42
43 let run_script is eval_function  =
44   let lexicon_status',grafite_status' = 
45     match !lexicon_status,!grafite_status with
46     | Some ss, Some s -> ss,s
47     | _,_ -> assert false
48   in
49   let slash_n_RE = Pcre.regexp "\\n" in
50   let cb = 
51     if Helm_registry.get_int "matita.verbosity" < 1 then 
52       (fun _ _ -> ())
53     else 
54       (fun grafite_status stm ->
55         (* dump_status grafite_status; *)
56         let stm = pp_ast_statement stm in
57         let stm = Pcre.replace ~rex:slash_n_RE stm in
58         let stm =
59           if String.length stm > 50 then
60             String.sub stm 0 50 ^ " ..."
61           else
62             stm
63         in
64         HLog.debug ("Executing: ``" ^ stm ^ "''"))
65   in
66   try
67    let grafite_status'', lexicon_status'' =
68     match eval_function lexicon_status' grafite_status' is cb with
69        [] -> assert false
70      | (s,None)::_ -> s
71      | (s,Some _)::_ -> raise AttemptToInsertAnAlias
72    in
73     lexicon_status := Some lexicon_status'';
74     grafite_status := Some grafite_status''
75   with
76   | GrafiteEngine.Drop  
77   | End_of_file
78   | CicNotationParser.Parse_error _ as exn -> raise exn
79   | exn -> 
80       HLog.error (snd (MatitaExcPp.to_string exn));
81       raise exn
82
83 let fname () =
84   let rec aux = function
85   | ""::tl -> aux tl
86   | [x] -> x
87   | [] -> MatitaInit.die_usage ()
88   | l -> 
89       prerr_endline 
90         ("Wrong commands: " ^ 
91           String.concat " " (List.map (fun x -> "'" ^ x ^ "'") l));
92       MatitaInit.die_usage ()
93   in
94   aux (Helm_registry.get_list Helm_registry.string "matita.args")
95
96 let pp_ocaml_mode () = 
97   HLog.message "";
98   HLog.message "                      ** Entering Ocaml mode ** ";
99   HLog.message "";
100   HLog.message "Type 'go ();;' to enter an interactive matitac";
101   HLog.message ""
102   
103 let clean_exit n =
104  let opt_exit =
105   function
106      None -> ()
107    | Some n -> exit n
108  in
109   match !grafite_status with
110      None -> opt_exit n
111    | Some grafite_status ->
112       try
113        let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
114        LibraryClean.clean_baseuris ~verbose:false [baseuri];
115        opt_exit n
116       with GrafiteTypes.Option_error("baseuri", "not found") ->
117        (* no baseuri ==> nothing to clean yet *)
118        opt_exit n
119   
120 let rec interactive_loop () = 
121   let str = Ulexing.from_utf8_channel stdin in
122   try
123     run_script str 
124       (MatitaEngine.eval_from_stream ~first_statement_only:false ~prompt:true
125       ~include_paths:(Helm_registry.get_list Helm_registry.string
126         "matita.includes"))
127   with 
128   | GrafiteEngine.Drop -> pp_ocaml_mode ()
129   | GrafiteEngine.Macro (floc,_) ->
130      let x, y = HExtlib.loc_of_floc floc in
131       HLog.error
132        (sprintf "A macro has been found in a script at %d-%d" x y);
133       interactive_loop ()
134   | Sys.Break -> HLog.error "user break!"; interactive_loop ()
135   | GrafiteTypes.Command_error _ -> interactive_loop ()
136   | End_of_file ->
137      print_newline ();
138      clean_exit (Some 0)
139   | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
140      let x, y = HExtlib.loc_of_floc floc in
141       HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
142       interactive_loop ()
143   | exn -> HLog.error (Printexc.to_string exn); interactive_loop ()
144
145 let go () =
146   Helm_registry.load_from BuildTimeConf.matita_conf;
147   Http_getter.init ();
148   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
149   LibraryDb.create_owner_environment ();
150   CicEnvironment.set_trust (* environment trust *)
151     (let trust =
152       Helm_registry.get_opt_default Helm_registry.get_bool
153         ~default:true "matita.environment_trust" in
154      fun _ -> trust);
155   let include_paths =
156    Helm_registry.get_list Helm_registry.string "matita.includes" in
157   grafite_status := Some (GrafiteSync.init ());
158   lexicon_status :=
159    Some (CicNotation2.load_notation ~include_paths
160     BuildTimeConf.core_notation_script);
161   Sys.catch_break true;
162   interactive_loop ()
163
164 let pp_times fname bench_mode rc big_bang = 
165   if bench_mode then
166     begin
167       let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in
168       let r = Unix.gettimeofday () -. big_bang in
169       let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in
170       let cc = 
171         if Str.string_match (Str.regexp ".*opt$") Sys.argv.(0) 0 then 
172           "matitac.opt" 
173         else 
174           "matitac" 
175       in
176       let rc = if rc then "\e[0;32mOK\e[0m" else "\e[0;31mFAIL\e[0m" in
177       let times = 
178         let fmt t = 
179           let seconds = int_of_float t in
180           let cents = int_of_float ((t -. floor t) *. 100.0) in
181           let minutes = seconds / 60 in
182           let seconds = seconds mod 60 in
183           Printf.sprintf "%dm%02d.%02ds" minutes seconds cents
184         in
185         Printf.sprintf "%s %s %s" (fmt r) (fmt u) (fmt s)
186       in
187       let fname = 
188         match MatitamakeLib.development_for_dir (Filename.dirname fname) with
189         | None -> fname
190         | Some d -> 
191             let rootlen = String.length(MatitamakeLib.root_for_development d)in
192             let fnamelen = String.length fname in
193             assert (fnamelen > rootlen); 
194             String.sub fname rootlen (fnamelen - rootlen)           
195       in
196       let fname = 
197         if fname.[0] = '/' then
198           String.sub fname 1 (String.length fname - 1)
199         else
200           fname
201       in
202       let s = Printf.sprintf "%s %-35s %-4s %s %s" cc fname rc times extra in
203       print_endline s;
204       flush stdout
205     end
206 ;;
207
208 let main ~mode = 
209   let big_bang = Unix.gettimeofday () in
210   MatitaInit.initialize_all ();
211   (* must be called after init since args are set by cmdline parsing *)
212   let fname = fname () in
213   let system_mode =  Helm_registry.get_bool "matita.system" in
214   let bench_mode =  Helm_registry.get_bool "matita.bench" in
215   if bench_mode then
216     Helm_registry.set_int "matita.verbosity" 0;
217   let include_paths =
218    Helm_registry.get_list Helm_registry.string "matita.includes" in
219   grafite_status := Some (GrafiteSync.init ());
220   lexicon_status :=
221    Some (CicNotation2.load_notation ~include_paths
222     BuildTimeConf.core_notation_script);
223   Sys.catch_break true;
224   let origcb = HLog.get_log_callback () in
225   let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in
226   let newcb tag s =
227     match tag with
228     | `Debug | `Message -> ()
229     | `Warning | `Error -> origcb tag s
230   in
231   if Helm_registry.get_int "matita.verbosity" < 1 then
232     HLog.set_log_callback newcb;
233   if bench_mode then MatitaMisc.shutup ();
234   let matita_debug = Helm_registry.get_bool "matita.debug" in
235   try
236     let time = Unix.time () in
237     if Helm_registry.get_int "matita.verbosity" < 1 && not bench_mode then
238       origcb `Message ("compiling " ^ Filename.basename fname ^ "...")
239     else
240       HLog.message (sprintf "execution of %s started:" fname);
241     let is =
242       Ulexing.from_utf8_channel
243         (match fname with
244         | "stdin" -> stdin
245         | fname -> open_in fname) in
246     let include_paths =
247      Helm_registry.get_list Helm_registry.string "matita.includes" in
248     (try
249       run_script is 
250        (MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
251          ~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve")))
252      with End_of_file -> ());
253     let elapsed = Unix.time () -. time in
254     let tm = Unix.gmtime elapsed in
255     let sec = string_of_int tm.Unix.tm_sec ^ "''" in
256     let min = 
257       if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min ^ "' ") else "" 
258     in
259     let hou = 
260       if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else ""
261     in
262     let proof_status,moo_content_rev,metadata,lexicon_content_rev = 
263       match !lexicon_status,!grafite_status with
264       | Some ss, Some s ->
265          s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata,
266           ss.LexiconEngine.lexicon_content_rev
267       | _,_ -> assert false
268     in
269     if proof_status <> GrafiteTypes.No_proof then
270      begin
271       HLog.error
272        "there are still incomplete proofs at the end of the script";
273       pp_times fname bench_mode true big_bang;
274       clean_exit (Some 2)
275      end
276     else
277      begin
278        let baseuri, _fullpathforfname =
279         DependenciesParser.baseuri_of_script ~include_paths fname in
280        let moo_fname = 
281          LibraryMisc.obj_file_of_baseuri 
282            ~must_exist:false ~baseuri ~writable:true 
283        in
284        let lexicon_fname= 
285          LibraryMisc.lexicon_file_of_baseuri 
286           ~must_exist:false ~baseuri ~writable:true 
287        in
288        let metadata_fname =
289         LibraryMisc.metadata_file_of_baseuri 
290           ~must_exist:false ~baseuri ~writable:true
291        in
292        GrafiteMarshal.save_moo moo_fname moo_content_rev;
293        LibraryNoDb.save_metadata metadata_fname metadata;
294        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
295        HLog.message 
296          (sprintf "execution of %s completed in %s." fname (hou^min^sec));
297        pp_times fname bench_mode true big_bang;
298        exit 0
299      end
300   with 
301   | Sys.Break ->
302       HLog.error "user break!";
303       pp_times fname bench_mode false big_bang;
304       if mode = `COMPILER then
305         clean_exit (Some ~-1)
306       else
307         pp_ocaml_mode ()
308   | GrafiteEngine.Drop ->
309       if mode = `COMPILER then 
310         begin
311           pp_times fname bench_mode false big_bang;
312           clean_exit (Some 1)
313         end
314       else 
315         pp_ocaml_mode ()
316   | GrafiteEngine.Macro (floc,_) ->
317      let x, y = HExtlib.loc_of_floc floc in
318       HLog.error
319        (sprintf "A macro has been found in a script at %d-%d" x y);
320       if mode = `COMPILER then 
321         begin
322           pp_times fname bench_mode false big_bang;
323           clean_exit (Some 1)
324         end
325       else 
326         pp_ocaml_mode ()
327   | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
328      let (x, y) = HExtlib.loc_of_floc floc in
329      HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
330      if mode = `COMPILER then
331        begin
332          pp_times fname bench_mode false big_bang;
333          clean_exit (Some 1)
334        end
335      else
336        pp_ocaml_mode ()
337   | exn ->
338       if matita_debug then raise exn;
339       if mode = `COMPILER then 
340         begin
341           pp_times fname bench_mode false big_bang;
342           clean_exit (Some 3)
343         end
344       else 
345         pp_ocaml_mode ()
346