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 auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
  29
  30 let merge_coercions obj =
  31   let module C = Cic in
  32   let rec aux2 = (fun (u,t) -> u,aux t)
  33   and aux = function
  34     | C.Rel _ | C.Sort _ as t -> t
  35     | C.Meta _ | C.Implicit _ -> assert false
  36     | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
  37     | C.Prod (name,so,dest) ->
  38         C.Prod (name, aux so, aux dest)
  39     | C.Lambda (name,so,dest) ->
  40         C.Lambda (name, aux so, aux dest)
  41     | C.LetIn (name,so,dest) ->
  42         C.LetIn (name, aux so, aux dest)
  43     | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when
  44       CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
  45         let source_carr = CoercGraph.source_of c2 in
  46         let tgt_carr = CoercGraph.target_of c1 in
  47         (match CoercGraph.look_for_coercion source_carr tgt_carr
  48         with
  49         | CoercGraph.SomeCoercion c -> Cic.Appl [ c ; head ]
  50         | _ -> assert false) (* the composite coercion must exist *)
  51     | C.Appl l -> C.Appl (List.map aux l)
  52     | C.Var (uri,exp_named_subst) ->
  53         let exp_named_subst = List.map aux2 exp_named_subst in
  54         C.Var (uri, exp_named_subst)
  55     | C.Const (uri,exp_named_subst) ->
  56         let exp_named_subst = List.map aux2 exp_named_subst in
  57         C.Const (uri, exp_named_subst)
  58     | C.MutInd (uri,tyno,exp_named_subst) ->
  59         let exp_named_subst = List.map aux2 exp_named_subst in
  60         C.MutInd (uri,tyno,exp_named_subst)
  61     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
  62         let exp_named_subst = List.map aux2 exp_named_subst in
  63         C.MutConstruct (uri,tyno,consno,exp_named_subst)
  64     | C.MutCase (uri,tyno,out,te,pl) ->
  65         let pl = List.map aux pl in
  66         C.MutCase (uri,tyno,aux out,aux te,pl)
  67     | C.Fix (fno, fl) ->
  68         let fl = List.map (fun (name,idx,ty,bo)->(name,idx,aux ty,aux bo)) fl in
  69         C.Fix (fno, fl)
  70     | C.CoFix (fno, fl) ->
  71         let fl = List.map (fun (name,ty,bo) -> (name, aux ty, aux bo)) fl in
  72         C.CoFix (fno, fl)
  73   in
  74   match obj with
  75   | C.Constant (id, body, ty, params, attrs) ->
  76       let body =
  77         match body with
  78         | None -> None
  79         | Some body -> Some (aux body)
  80       in
  81       let ty = aux ty in
  82         C.Constant (id, body, ty, params, attrs)
  83   | C.Variable (name, body, ty, params, attrs) ->
  84       let body =
  85         match body with
  86         | None -> None
  87         | Some body -> Some (aux body)
  88       in
  89       let ty = aux ty in
  90         C.Variable (name, body, ty, params, attrs)
  91   | C.CurrentProof (_name, _conjectures, _body, _ty, _params, _attrs) ->
  92       assert false
  93   | C.InductiveDefinition (indtys, params, leftno, attrs) ->
  94       let indtys =
  95         List.map
  96           (fun (name, ind, arity, cl) ->
  97             let arity = aux arity in
  98             let cl = List.map (fun (name, ty) -> (name,aux ty)) cl in
  99             (name, ind, arity, cl))
 100           indtys
 101       in
 102         C.InductiveDefinition (indtys, params, leftno, attrs)
 103
 104 let uris_of_obj uri =
 105  let innertypesuri = UriManager.innertypesuri_of_uri uri in
 106  let bodyuri = UriManager.bodyuri_of_uri uri in
 107  let univgraphuri = UriManager.univgraphuri_of_uri uri in
 108   innertypesuri,bodyuri,univgraphuri
 109
 110 let paths_and_uris_of_obj uri ~basedir =
 111   let basedir = basedir ^ "/xml" in
 112   let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
 113   let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
 114         (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
 115   let innertypespath = basedir ^ "/" ^ innertypesfilename in
 116   let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
 117         (UriManager.string_of_uri uri) ^ ".xml.gz" in
 118   let xmlpath = basedir ^ "/" ^ xmlfilename in
 119   let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
 120         (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
 121   let xmlbodypath = basedir ^ "/" ^  xmlbodyfilename in
 122   let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") ""
 123         (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in
 124   let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in
 125   xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
 126   xmlunivgraphpath, univgraphuri
 127
 128 let save_object_to_disk ~basedir uri obj ugraph univlist =
 129   let ensure_path_exists path =
 130     let dir = Filename.dirname path in
 131     HExtlib.mkdir dir
 132   in
 133   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
 134   let annobj = Cic2acic.plain_acic_object_of_cic_object obj in
 135   (* prepare XML *)
 136   let xml, bodyxml =
 137    Cic2Xml.print_object
 138     uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj
 139   in
 140   let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
 141       xmlunivgraphpath, univgraphuri =
 142     paths_and_uris_of_obj uri basedir
 143   in
 144   List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
 145   (* now write to disk *)
 146   ensure_path_exists xmlpath;
 147   Xml.pp ~gzip:true xml (Some xmlpath);
 148   CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist;
 149   (* we return a list of uri,path we registered/created *)
 150   (uri,xmlpath) ::
 151   (univgraphuri,xmlunivgraphpath) ::
 152     (* now the optional body, both write and register *)
 153     (match bodyxml,bodyuri with
 154        None,None -> []
 155      | Some bodyxml,Some bodyuri->
 156          ensure_path_exists xmlbodypath;
 157          Xml.pp ~gzip:true bodyxml (Some xmlbodypath);
 158          [bodyuri, xmlbodypath]
 159      | _-> assert false)
 160
 161
 162 let typecheck_obj =
 163  let profiler = HExtlib.profile "add_obj.typecheck_obj" in
 164   fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
 165
 166 let index_obj =
 167  let profiler = HExtlib.profile "add_obj.index_obj" in
 168   fun ~dbd ~uri ->
 169    profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
 170
 171 let add_single_obj uri obj ~basedir =
 172   let obj =
 173     if List.mem `Generated (CicUtil.attributes_of_obj obj) &&
 174        not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
 175     then
 176       merge_coercions obj
 177     else
 178       obj
 179   in
 180   let dbd = LibraryDb.instance () in
 181   if CicEnvironment.in_library uri then
 182     raise (AlreadyDefined uri)
 183   else begin
 184     typecheck_obj uri obj; (* 1 *)
 185     let _, ugraph, univlist =
 186       CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
 187     try
 188       index_obj ~dbd ~uri; (* 2 must be in the env *)
 189       try
 190         (*3*)
 191         let new_stuff = save_object_to_disk ~basedir uri obj ugraph univlist in
 192         try
 193          HLog.message
 194           (Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
 195         with exc ->
 196           List.iter HExtlib.safe_remove (List.map snd new_stuff); (* -3 *)
 197           raise exc
 198       with exc ->
 199         ignore(LibraryDb.remove_uri uri); (* -2 *)
 200         raise exc
 201     with exc ->
 202       CicEnvironment.remove_obj uri; (* -1 *)
 203     raise exc
 204   end
 205
 206 let remove_single_obj uri =
 207   let derived_uris_of_uri uri =
 208    let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
 209     innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u])
 210   in
 211   let to_remove =
 212     uri ::
 213     (if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else []) @
 214     derived_uris_of_uri uri
 215   in
 216   List.iter
 217     (fun uri ->
 218       (try
 219         let file = Http_getter.resolve' uri in
 220          HExtlib.safe_remove file;
 221          HExtlib.rmdir_descend (Filename.dirname file)
 222       with Http_getter_types.Key_not_found _ -> ());
 223       ignore (LibraryDb.remove_uri uri);
 224       CoercGraph.remove_coercion uri;
 225       CicEnvironment.remove_obj uri)
 226   to_remove
 227
 228 (*** GENERATION OF AUXILIARY LEMMAS ***)
 229
 230 let generate_elimination_principles ~basedir uri =
 231   let uris = ref [] in
 232   let elim sort =
 233     try
 234       let uri,obj = CicElim.elim_of ~sort uri 0 in
 235        add_single_obj uri obj ~basedir;
 236        uris := uri :: !uris
 237     with CicElim.Can_t_eliminate -> ()
 238   in
 239   try
 240     List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
 241     !uris
 242   with exn ->
 243    List.iter remove_single_obj !uris;
 244    raise exn
 245
 246 let generate_projections ~basedir uri fields =
 247  let uris = ref [] in
 248  let projections = CicRecord.projections_of uri (List.map fst fields) in
 249   try
 250    List.iter2
 251     (fun (uri, name, bo) (_name, coercion) ->
 252       try
 253        let ty, ugraph =
 254          CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
 255        let attrs = [`Class `Projection; `Generated] in
 256        let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
 257
 258         add_single_obj ~basedir uri obj;
 259         let composites =
 260           if coercion then
 261             (* this is _NOT_ the place for THIS!!! *)
 262             (* MOO HANDLING IS MISSING *)
 263             let toadd = CoercGraph.add_coercion uri in
 264             List.iter (fun (uri,o) -> add_single_obj ~basedir uri o) toadd;
 265             List.map fst toadd
 266           else
 267             []
 268         in
 269         uris := uri :: composites @ !uris
 270       with
 271          CicTypeChecker.TypeCheckerFailure s ->
 272           HLog.message
 273            ("Unable to create projection " ^ name ^ " cause: " ^ Lazy.force s);
 274        | CicEnvironment.Object_not_found uri ->
 275           let depend = UriManager.name_of_uri uri in
 276            HLog.message
 277             ("Unable to create projection " ^ name ^ " because it requires " ^
 278                depend)
 279     ) projections fields;
 280    !uris
 281   with exn ->
 282    List.iter remove_single_obj !uris;
 283    raise exn
 284
 285
 286 let add_obj uri obj ~basedir =
 287  add_single_obj uri obj ~basedir;
 288  let uris = ref [] in
 289  try
 290   begin
 291    match obj with
 292     | Cic.Constant _ -> ()
 293     | Cic.InductiveDefinition (_,_,_,attrs) ->
 294         uris := !uris @ generate_elimination_principles ~basedir uri;
 295         let rec get_record_attrs =
 296           function
 297           | [] -> None
 298           | (`Class (`Record fields))::_ -> Some fields
 299           | _::tl -> get_record_attrs tl
 300         in
 301          (match get_record_attrs attrs with
 302          | None -> () (* not a record *)
 303          | Some fields ->
 304             uris := !uris @ (generate_projections ~basedir uri fields))
 305     | Cic.CurrentProof _
 306     | Cic.Variable _ -> assert false
 307   end;
 308   UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
 309   !uris
 310  with exn ->
 311   List.iter remove_single_obj !uris;
 312   raise exn
 313
 314 let remove_obj uri =
 315  let uris =
 316   try
 317    let res = UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri in
 318     UriManager.UriHashtbl.remove auxiliary_lemmas_hashtbl uri;
 319     res
 320   with
 321     Not_found -> [] (*assert false*)
 322  in
 323   List.iter remove_single_obj (uri::uris)