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_single_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_single_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
 143
 144 (*** GENERATION OF AUXILIARY LEMMAS ***)
 145
 146 let generate_elimination_principles ~basedir uri =
 147   let uris = ref [] in
 148   let elim sort =
 149     try
 150       let uri,obj = CicElim.elim_of ~sort uri 0 in
 151        add_single_obj uri obj ~basedir;
 152        uris := uri :: !uris
 153     with CicElim.Can_t_eliminate -> ()
 154   in
 155   try
 156     List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
 157     !uris
 158   with exn ->
 159    List.iter remove_single_obj !uris;
 160    raise exn
 161
 162 let generate_projections ~basedir uri fields =
 163  let uris = ref [] in
 164  let projections = CicRecord.projections_of uri fields in
 165   try
 166    List.iter
 167     (fun (uri, name, bo) ->
 168       try
 169        let ty, ugraph =
 170          CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
 171        let attrs = [`Class `Projection; `Generated] in
 172        let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
 173         add_single_obj ~basedir uri obj;
 174         uris := uri :: !uris
 175       with
 176          CicTypeChecker.TypeCheckerFailure s ->
 177           HLog.message
 178            ("Unable to create projection " ^ name ^ " cause: " ^ Lazy.force s);
 179        | CicEnvironment.Object_not_found uri ->
 180           let depend = UriManager.name_of_uri uri in
 181            HLog.message
 182             ("Unable to create projection " ^ name ^ " because it requires " ^
 183                depend)
 184     ) projections;
 185    !uris
 186   with exn ->
 187    List.iter remove_single_obj !uris;
 188    raise exn
 189
 190 let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
 191
 192 let add_obj uri obj ~basedir =
 193  add_single_obj uri obj ~basedir;
 194  let uris = ref [] in
 195  try
 196   begin
 197    match obj with
 198     | Cic.Constant _ -> ()
 199     | Cic.InductiveDefinition (_,_,_,attrs) ->
 200         uris := !uris @ generate_elimination_principles ~basedir uri;
 201         let rec get_record_attrs =
 202           function
 203           | [] -> None
 204           | (`Class (`Record fields))::_ -> Some fields
 205           | _::tl -> get_record_attrs tl
 206         in
 207          (match get_record_attrs attrs with
 208          | None -> () (* not a record *)
 209          | Some fields ->
 210             uris := !uris @ (generate_projections ~basedir uri fields))
 211     | Cic.CurrentProof _
 212     | Cic.Variable _ -> assert false
 213   end;
 214   UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
 215   !uris
 216  with exn ->
 217   List.iter remove_single_obj !uris;
 218   raise exn
 219
 220 let remove_obj uri =
 221  let uris =
 222   try
 223    let res = UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri in
 224     UriManager.UriHashtbl.remove auxiliary_lemmas_hashtbl uri;
 225     res
 226   with
 227     Not_found -> [] (*assert false*)
 228  in
 229   List.iter remove_single_obj (uri::uris)