]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/matitaInit.ml
LAMBDA-TYPES: level 2 dependences are now correct, at least :)
[helm.git] / helm / software / matita / matitaInit.ml
1 (* Copyright (C) 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 type thingsToInitilaize = 
29   ConfigurationFile | Db | Environment | Getter | CmdLine | Registry
30   
31 exception FailedToInitialize of thingsToInitilaize
32
33 let wants s l = 
34   List.iter (
35     fun item -> 
36       if not (List.exists (fun x -> x = item) l) then
37         raise (FailedToInitialize item)) 
38   s
39
40 let already_configured s l =
41   List.for_all (fun item -> List.exists (fun x -> x = item) l) s
42   
43 let conffile = ref BuildTimeConf.matita_conf
44
45 let registry_defaults = [
46   "matita.debug",                "false";
47   "matita.external_editor",      "gvim -f -c 'go %p' %f";
48   "matita.profile",              "true";
49   "matita.system",               "false";
50   "matita.verbose",              "false";
51   "matita.paste_unicode_as_tex", "false";
52   "matita.noinnertypes",         "false";
53   "matita.do_heavy_checks",      "true";
54   "matita.moo",                  "true";
55   "matita.extract",              "false";
56 ]
57
58 let set_registry_values =
59   List.iter 
60     (fun key, value -> 
61        if not (Helm_registry.has key) then Helm_registry.set ~key ~value)
62
63 let fill_registry init_status =
64   if not (already_configured [ Registry ] init_status) then begin
65     set_registry_values registry_defaults;
66     Registry :: init_status
67   end else
68     init_status
69
70 let load_configuration init_status =
71   if not (already_configured [ConfigurationFile] init_status) then
72     begin
73       Helm_registry.load_from !conffile;
74       if not (Helm_registry.has "user.name") then begin
75         let login = (Unix.getpwuid (Unix.getuid ())).Unix.pw_name in
76         Helm_registry.set "user.name" login
77       end;
78       let home = Helm_registry.get_string "matita.basedir" in
79       let user_conf_file = home ^ "/matita.conf.xml" in
80       if HExtlib.is_regular user_conf_file then
81         begin
82           HLog.message ("Loading additional conf file from " ^ user_conf_file);
83           try
84             Helm_registry.load_from user_conf_file
85           with exn -> 
86             HLog.error
87               ("While loading conf file: " ^ snd (MatitaExcPp.to_string exn))
88         end;
89       ConfigurationFile::init_status 
90     end
91   else
92     init_status
93
94 let initialize_db init_status = 
95   wants [ ConfigurationFile; CmdLine ] init_status;
96   if not (already_configured [ Db ] init_status) then
97     begin
98       if not (Helm_registry.get_bool "matita.system") then
99         MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
100       LibraryDb.create_owner_environment ();
101       Db::init_status
102     end
103   else
104     init_status
105
106 let initialize_environment init_status = 
107   wants [CmdLine] init_status;
108   if not (already_configured [Getter;Environment] init_status) then
109     begin
110       Http_getter.init ();
111       if Helm_registry.get_bool "matita.system" then
112         Http_getter_storage.activate_system_mode ();
113       CicEnvironment.set_trust (* environment trust *)
114         (let trust =
115           Helm_registry.get_opt_default Helm_registry.get_bool
116             ~default:true "matita.environment_trust" in
117          fun _ -> trust);
118       Getter::Environment::init_status
119     end
120   else
121     init_status 
122   
123 let status = ref []
124
125 let usages = Hashtbl.create 11 (** app name (e.g. "matitac") -> usage string *)
126 let _ =
127   List.iter
128     (fun (name, s) -> Hashtbl.replace usages name s)
129     [ "matitac", 
130         Printf.sprintf "Matita batch compiler v%s
131 Usage: matitac [ OPTION ... ] FILE
132 Options:"
133           BuildTimeConf.version;
134         "matitaprover",
135         Printf.sprintf "Matita (TPTP) prover v%s
136 Usage: matitaprover [ -tptppath ] FILE.p
137 Options:"
138           BuildTimeConf.version;
139       "matita",
140         Printf.sprintf "Matita interactive theorem prover v%s
141 Usage: matita [ OPTION ... ] [ FILE ]
142 Options:"
143           BuildTimeConf.version;
144       "matitadep",
145         Printf.sprintf "Matita depency file generator v%s
146 Usage: matitadep [ OPTION ... ] 
147 Options:"
148           BuildTimeConf.version;
149       "matitaclean",
150         Printf.sprintf "MatitaClean v%s
151 Usage: matitaclean all
152        matitaclean ( FILE | URI )
153 Options:"
154           BuildTimeConf.version;
155     ]
156 let default_usage =
157   Printf.sprintf 
158     "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
159
160 let usage () =
161   let basename = Filename.basename Sys.argv.(0) in
162   let usage_key =
163     try Filename.chop_extension basename with Invalid_argument  _ -> basename
164   in
165   try Hashtbl.find usages usage_key with Not_found -> default_usage
166 ;;
167
168 let dump f =
169    let module G = GrafiteAst in
170    let module L = LexiconAst in
171    let module H = HExtlib in
172    Helm_registry.set_bool "matita.moo" false;
173    let floc = H.dummy_floc in
174    let nl_ast = G.Comment (floc, G.Note (floc, "")) in
175    let och = open_out f in
176    let atexit () = close_out och in
177    let out_comment och s =
178       let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in 
179       Printf.fprintf och "%s%s%s\n\n" "(*" s "*)"
180    in
181    let out_line_comment och s =
182       let l = 70 - String.length s in
183       let s = Printf.sprintf " %s %s" s (String.make l '*') in
184       out_comment och s
185    in
186    let out_preamble och (path, lines) =
187       let ich = open_in path in
188       let rec print i =
189          if i > 0 then 
190             let s = input_line ich in
191             begin Printf.fprintf och "%s\n" s; print (pred i) end
192       in 
193       print lines;
194       out_line_comment och "This file was automatically generated: do not edit"
195    in
196    let pp_ast_statement st =
197      GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
198        ~map_unicode_to_tex:(Helm_registry.get_bool
199          "matita.paste_unicode_as_tex")
200        ~lazy_term_pp:CicNotationPp.pp_term 
201        ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st
202    in
203    let nl () =  output_string och (pp_ast_statement nl_ast) in
204    let rt_base_dir = Filename.dirname Sys.argv.(0) in
205    let path = Filename.concat rt_base_dir "matita.ma.templ" in
206    let lines = 14 in
207    out_preamble och (path, lines);
208    let grafite_parser_cb fname = 
209       let ast = G.Executable 
210         (floc, G.Command (floc, G.Include (floc, fname))) in
211       output_string och (pp_ast_statement ast); nl (); nl ()
212    in
213    let matita_engine_cb = function
214       | G.Executable (_, G.Macro (_, G.Inline _)) 
215       | G.Executable (_, G.Command (_, G.Include _)) -> ()
216       | ast                                          ->
217          output_string och (pp_ast_statement ast); nl (); nl ()
218    in
219    let matitac_lib_cb = output_string och in
220    GrafiteParser.set_callback grafite_parser_cb;
221    MatitaEngine.set_callback matita_engine_cb;
222    MatitacLib.set_callback matitac_lib_cb;
223    at_exit atexit
224 ;;
225
226 let extra_cmdline_specs = ref []
227 let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
228
229 let parse_cmdline init_status =
230   if not (already_configured [CmdLine] init_status) then begin
231     wants [Registry] init_status;
232     let includes = ref [] in
233     let default_includes = [ 
234       BuildTimeConf.stdlib_dir_devel;
235       BuildTimeConf.stdlib_dir_installed ; ] 
236     in
237     let absolutize s =
238       if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd () ^"/"^s
239     in
240     let args = ref [] in
241     let add_l l = fun s -> l := s :: !l in
242     let print_version () =
243             Printf.printf "%s\n" BuildTimeConf.version;exit 0 in
244     let no_innertypes () =
245       Helm_registry.set_bool "matita.noinnertypes" true in
246     let set_baseuri s =
247       match Str.split (Str.regexp "::") s with
248       | [path; uri] -> Helm_registry.set "matita.baseuri"
249           (HExtlib.normalize_path (absolutize path)^" "^uri)
250       | _ -> raise (Failure "bad baseuri, use -b 'path::uri'")
251     in
252     let arg_spec =
253       let std_arg_spec = [
254         "-b", Arg.String set_baseuri, "<path::uri> forces the baseuri of path";
255         "-I", Arg.String (add_l includes),
256           ("<path> Adds path to the list of searched paths for the "
257            ^ "include command");
258         "-conffile", Arg.Set_string conffile,
259           (Printf.sprintf ("<filename> Read configuration from filename"
260              ^^ "\n    Default: %s")
261             BuildTimeConf.matita_conf);
262         "-force",
263             Arg.Unit (fun () -> Helm_registry.set_bool "matita.force" true),
264             ("Force actions that would not be executed per default");
265         "-noprofile", 
266           Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
267           "Turns off profiling printings";
268         "-noinnertypes", Arg.Unit no_innertypes, 
269           "Turns off inner types generation while publishing";
270         "-profile-only",
271           Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex),
272           "Activates only profiler with label matching the provided regex";
273         "-system", Arg.Unit (fun () ->
274               Helm_registry.set_bool "matita.system" true),
275             ("Act on the system library instead of the user one"
276              ^ "\n    WARNING: not for the casual user");
277         "-dump", Arg.String dump,
278           "<filename> Dump with expanded macros to <filename>";
279         "-v", 
280           Arg.Unit (fun () -> Helm_registry.set_bool "matita.verbose" true), 
281           "Verbose mode";
282         "--version", Arg.Unit print_version, "Prints version";
283       ] in
284       let debug_arg_spec =
285         if BuildTimeConf.debug then
286           [ "-debug",
287             Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true),
288               ("Do not catch top-level exception "
289               ^ "(useful for backtrace inspection)");
290             "-onepass",
291             Arg.Unit (fun () -> GrafiteDisambiguator.only_one_pass := true),
292             "Enable only one disambiguation pass";    
293           ]
294         else []
295       in
296       std_arg_spec @ debug_arg_spec @ !extra_cmdline_specs
297     in
298     let set_list ~key l =
299       Helm_registry.set_list Helm_registry.of_string ~key ~value:l
300     in
301     Arg.parse arg_spec (add_l args) (usage ());
302     let includes = 
303       List.map (fun x -> HExtlib.normalize_path (absolutize x)) 
304        ((List.rev !includes) @ default_includes) 
305     in
306     set_list ~key:"matita.includes" includes;
307     let args = List.rev (List.filter (fun x -> x <> "") !args) in
308     set_list ~key:"matita.args" args;
309     HExtlib.set_profiling_printings 
310       (fun s -> 
311         Helm_registry.get_bool "matita.profile" && 
312         Pcre.pmatch 
313           ~pat:(Helm_registry.get_opt_default 
314                   Helm_registry.string ~default:".*" "matita.profile_only") 
315           s);
316     CmdLine :: init_status
317   end else
318     init_status
319
320 let die_usage () =
321   print_endline (usage ());
322   exit 1
323
324 let conf_components = 
325   [ load_configuration; fill_registry; parse_cmdline]
326
327 let other_components =
328   [ initialize_db; initialize_environment ]
329
330 let initialize_all () =
331   status := 
332     List.fold_left (fun s f -> f s) !status
333     (conf_components @ other_components)
334
335 let parse_cmdline_and_configuration_file () =
336   status := List.fold_left (fun s f -> f s) !status conf_components
337
338 let initialize_environment () =
339   status := initialize_environment !status
340
341 let _ =
342   Inversion_principle.init ()