]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/library/librarySync.ml
d853243ddd06b5a6dc42a423960d8404a546443e
[helm.git] / helm / ocaml / library / librarySync.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 exception AlreadyDefined of UriManager.uri
27
28 let uris_of_obj uri =
29  let innertypesuri = UriManager.innertypesuri_of_uri uri in
30  let bodyuri = UriManager.bodyuri_of_uri uri in
31  let univgraphuri = UriManager.univgraphuri_of_uri uri in
32   innertypesuri,bodyuri,univgraphuri
33
34 let paths_and_uris_of_obj uri ~basedir =
35   let basedir = basedir ^ "/xml" in
36   let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
37   let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
38         (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
39   let innertypespath = basedir ^ "/" ^ innertypesfilename in
40   let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
41         (UriManager.string_of_uri uri) ^ ".xml.gz" in
42   let xmlpath = basedir ^ "/" ^ xmlfilename in
43   let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
44         (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
45   let xmlbodypath = basedir ^ "/" ^  xmlbodyfilename in
46   let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") ""
47         (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in
48   let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in
49   xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
50   xmlunivgraphpath, univgraphuri
51
52 let save_object_to_disk ~basedir uri obj ugraph univlist =
53   let ensure_path_exists path =
54     let dir = Filename.dirname path in
55     HExtlib.mkdir dir
56   in
57   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
58   let annobj = Cic2acic.plain_acic_object_of_cic_object obj in 
59   (* prepare XML *)
60   let xml, bodyxml =
61    Cic2Xml.print_object
62     uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj 
63   in
64   let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
65       xmlunivgraphpath, univgraphuri = 
66     paths_and_uris_of_obj uri basedir 
67   in
68   List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
69   (* now write to disk *)
70   ensure_path_exists xmlpath;
71   Xml.pp ~gzip:true xml (Some xmlpath);
72   CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist;
73   (* we return a list of uri,path we registered/created *)
74   (uri,xmlpath) ::
75   (univgraphuri,xmlunivgraphpath) ::
76     (* now the optional body, both write and register *)
77     (match bodyxml,bodyuri with
78        None,None -> []
79      | Some bodyxml,Some bodyuri->
80          ensure_path_exists xmlbodypath;
81          Xml.pp ~gzip:true bodyxml (Some xmlbodypath);
82          [bodyuri, xmlbodypath]
83      | _-> assert false) 
84
85
86 let typecheck_obj =
87  let profiler = HExtlib.profile "add_obj.typecheck_obj" in
88   fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
89
90 let index_obj =
91  let profiler = HExtlib.profile "add_obj.index_obj" in
92   fun ~dbd ~uri ->
93    profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
94
95 let add_obj uri obj ~basedir =
96   let dbd = LibraryDb.instance () in
97   if CicEnvironment.in_library uri then
98     raise (AlreadyDefined uri)
99   else begin
100     typecheck_obj uri obj; (* 1 *)
101     let _, ugraph, univlist = 
102       CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
103     try 
104       index_obj ~dbd ~uri; (* 2 must be in the env *)
105       try
106         (*3*)
107         let new_stuff = save_object_to_disk ~basedir uri obj ugraph univlist in
108         try 
109          HLog.message
110           (Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
111         with exc ->
112           List.iter HExtlib.safe_remove (List.map snd new_stuff); (* -3 *)
113           raise exc
114       with exc ->
115         ignore(LibraryDb.remove_uri uri); (* -2 *)
116         raise exc
117     with exc ->
118       CicEnvironment.remove_obj uri; (* -1 *)
119     raise exc
120   end
121
122 let remove_obj uri =
123   let derived_uris_of_uri uri =
124    let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
125     innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u])
126   in
127   let to_remove =
128     uri :: 
129     (if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else []) @
130     derived_uris_of_uri uri
131   in   
132   List.iter 
133     (fun uri -> 
134       (try
135         let file = Http_getter.resolve' uri in
136          HExtlib.safe_remove file;
137          HExtlib.rmdir_descend (Filename.dirname file)
138       with Http_getter_types.Key_not_found _ -> ());
139       ignore (LibraryDb.remove_uri uri);
140       CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri);
141       CicEnvironment.remove_obj uri)
142   to_remove