]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/matitamake.ml
Generation of inductive and inversion principles for mutual
[helm.git] / helm / software / matita / matitamake.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 module MK = MatitamakeLib ;;
29
30 let main () =
31   MatitaInit.fill_registry ();
32   MatitaInit.parse_cmdline ();
33   MatitaInit.load_configuration_file ();
34   MK.initialize ();
35   let usage = ref (fun () -> ()) in
36   let dev_of_name name = 
37     match MK.development_for_name name with
38     | None -> 
39         prerr_endline ("Unable to find a development called " ^ name);
40         exit 1
41     | Some d -> d
42   in
43   let dev_for_dir dir =
44     match MK.development_for_dir dir with
45     | None -> 
46         prerr_endline ("Unable to find a development holding directory: "^ dir);
47         exit 1
48     | Some d -> d
49   in
50   let init_dev args =
51     let name, path =
52       match args with
53       | [ name; path ] when path.[0] = '/' -> name, path
54       | [ name; path ] -> name, Unix.getcwd () ^ "/" ^ path
55       | [ name ] -> name, Unix.getcwd ()
56       | _ -> !usage (); (* should not be reached *) assert false
57     in
58     match MK.initialize_development name path with
59     | None -> exit 2
60     | Some _ -> exit 0
61   in
62   let list_dev args =
63     if List.length args <> 0 then !usage ();
64     match MK.list_known_developments () with
65     | [] -> print_string "No developments found.\n"; exit 0
66     | l ->
67         List.iter 
68           (fun (name, root) -> 
69             print_string (Printf.sprintf "%-10s\trooted in %s\n" name root)) 
70           l;
71         exit 0
72   in
73   let destroy_dev args = 
74     if List.length args <> 1 then !usage ();
75     let name = (List.hd args) in
76     let dev = dev_of_name name in
77     MK.destroy_development dev; 
78     exit 0
79   in
80   let clean_dev args = 
81     let dev = 
82       match args with
83       | [] -> dev_for_dir (Unix.getcwd ())
84       | [name] -> dev_of_name name
85       | _ -> !usage (); exit 1
86     in
87     match MK.clean_development dev with
88     | true -> exit 0
89     | false -> exit 1
90   in
91   let build_dev args = 
92     if List.length args <> 1 then !usage ();
93     let name = (List.hd args) in
94     let dev = dev_of_name name in
95     match MK.build_development dev with
96     | true -> exit 0
97     | false -> exit 1
98   in
99   let publish_dev args = 
100     if List.length args <> 1 then !usage ();
101     let name = (List.hd args) in
102     let dev = dev_of_name name in
103     match MK.publish_development dev with
104     | true -> exit 0
105     | false -> exit 1
106   in
107   let target args = 
108     if List.length args < 1 then !usage ();
109     let dev = dev_for_dir (Unix.getcwd ()) in
110     List.iter 
111       (fun t -> 
112         ignore(MK.build_development ~target:t dev)) 
113       args
114   in
115   let params = [
116     "init", init_dev;
117     "clean", clean_dev;
118     "list", list_dev;
119     "destroy", destroy_dev;
120     "build", build_dev;
121     "publish", publish_dev;
122   ]
123   in
124   usage := MatitaInit.die_usage;
125   let parse args = 
126     match args with
127     | [] -> target [ "all" ]
128     | s :: tl ->
129         let f, args = 
130           try 
131             (List.assoc s params), tl
132           with Not_found -> 
133             if s.[0] = '-' then (!usage ();assert false) else target, args
134         in
135         f args
136   in
137   parse (Helm_registry.get_list Helm_registry.string "matita.args")