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