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 (* uri |-->  (derived_coercions_in_the_coercion_DB, derived_coercions_in_lib)
  31  *
  32  * in case of remove_coercion uri, the first component is removed from the
  33  * coercion DB, while the second is passed to remove_obj (and is not [] only if
  34  * add_coercion is called with add_composites
  35  * *)
  36 let coercion_hashtbl = UriManager.UriHashtbl.create 3
  37
  38 let merge_coercions obj =
  39   let module C = Cic in
  40   let rec aux2 = (fun (u,t) -> u,aux t)
  41   and aux = function
  42     | C.Rel _ | C.Sort _ as t -> t
  43     | C.Meta _ | C.Implicit _ -> assert false
  44     | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
  45     | C.Prod (name,so,dest) ->
  46         C.Prod (name, aux so, aux dest)
  47     | C.Lambda (name,so,dest) ->
  48         C.Lambda (name, aux so, aux dest)
  49     | C.LetIn (name,so,dest) ->
  50         C.LetIn (name, aux so, aux dest)
  51     | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when
  52       CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
  53         let source_carr = CoercGraph.source_of c2 in
  54         let tgt_carr = CoercGraph.target_of c1 in
  55         (match CoercGraph.look_for_coercion source_carr tgt_carr
  56         with
  57         | CoercGraph.SomeCoercion c -> Cic.Appl [ c ; head ]
  58         | _ -> assert false) (* the composite coercion must exist *)
  59     | C.Appl l -> C.Appl (List.map aux l)
  60     | C.Var (uri,exp_named_subst) ->
  61         let exp_named_subst = List.map aux2 exp_named_subst in
  62         C.Var (uri, exp_named_subst)
  63     | C.Const (uri,exp_named_subst) ->
  64         let exp_named_subst = List.map aux2 exp_named_subst in
  65         C.Const (uri, exp_named_subst)
  66     | C.MutInd (uri,tyno,exp_named_subst) ->
  67         let exp_named_subst = List.map aux2 exp_named_subst in
  68         C.MutInd (uri,tyno,exp_named_subst)
  69     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
  70         let exp_named_subst = List.map aux2 exp_named_subst in
  71         C.MutConstruct (uri,tyno,consno,exp_named_subst)
  72     | C.MutCase (uri,tyno,out,te,pl) ->
  73         let pl = List.map aux pl in
  74         C.MutCase (uri,tyno,aux out,aux te,pl)
  75     | C.Fix (fno, fl) ->
  76         let fl = List.map (fun (name,idx,ty,bo)->(name,idx,aux ty,aux bo)) fl in
  77         C.Fix (fno, fl)
  78     | C.CoFix (fno, fl) ->
  79         let fl = List.map (fun (name,ty,bo) -> (name, aux ty, aux bo)) fl in
  80         C.CoFix (fno, fl)
  81   in
  82   match obj with
  83   | C.Constant (id, 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.Constant (id, body, ty, params, attrs)
  91   | C.Variable (name, body, ty, params, attrs) ->
  92       let body =
  93         match body with
  94         | None -> None
  95         | Some body -> Some (aux body)
  96       in
  97       let ty = aux ty in
  98         C.Variable (name, body, ty, params, attrs)
  99   | C.CurrentProof (_name, _conjectures, _body, _ty, _params, _attrs) ->
 100       assert false
 101   | C.InductiveDefinition (indtys, params, leftno, attrs) ->
 102       let indtys =
 103         List.map
 104           (fun (name, ind, arity, cl) ->
 105             let arity = aux arity in
 106             let cl = List.map (fun (name, ty) -> (name,aux ty)) cl in
 107             (name, ind, arity, cl))
 108           indtys
 109       in
 110         C.InductiveDefinition (indtys, params, leftno, attrs)
 111
 112 let uris_of_obj uri =
 113  let innertypesuri = UriManager.innertypesuri_of_uri uri in
 114  let bodyuri = UriManager.bodyuri_of_uri uri in
 115  let univgraphuri = UriManager.univgraphuri_of_uri uri in
 116   innertypesuri,bodyuri,univgraphuri
 117
 118 let paths_and_uris_of_obj uri ~basedir =
 119   let basedir = basedir ^ "/xml" in
 120   let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
 121   let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
 122         (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
 123   let innertypespath = basedir ^ "/" ^ innertypesfilename in
 124   let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
 125         (UriManager.string_of_uri uri) ^ ".xml.gz" in
 126   let xmlpath = basedir ^ "/" ^ xmlfilename in
 127   let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
 128         (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
 129   let xmlbodypath = basedir ^ "/" ^  xmlbodyfilename in
 130   let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") ""
 131         (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in
 132   let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in
 133   xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
 134   xmlunivgraphpath, univgraphuri
 135
 136 let save_object_to_disk ~basedir uri obj ugraph univlist =
 137   let ensure_path_exists path =
 138     let dir = Filename.dirname path in
 139     HExtlib.mkdir dir
 140   in
 141   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
 142   let annobj = Cic2acic.plain_acic_object_of_cic_object obj in
 143   (* prepare XML *)
 144   let xml, bodyxml =
 145    Cic2Xml.print_object
 146     uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj
 147   in
 148   let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
 149       xmlunivgraphpath, univgraphuri =
 150     paths_and_uris_of_obj uri basedir
 151   in
 152   List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
 153   (* now write to disk *)
 154   ensure_path_exists xmlpath;
 155   Xml.pp ~gzip:true xml (Some xmlpath);
 156   CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist;
 157   (* we return a list of uri,path we registered/created *)
 158   (uri,xmlpath) ::
 159   (univgraphuri,xmlunivgraphpath) ::
 160     (* now the optional body, both write and register *)
 161     (match bodyxml,bodyuri with
 162        None,None -> []
 163      | Some bodyxml,Some bodyuri->
 164          ensure_path_exists xmlbodypath;
 165          Xml.pp ~gzip:true bodyxml (Some xmlbodypath);
 166          [bodyuri, xmlbodypath]
 167      | _-> assert false)
 168
 169
 170 let typecheck_obj =
 171  let profiler = HExtlib.profile "add_obj.typecheck_obj" in
 172   fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
 173
 174 let index_obj =
 175  let profiler = HExtlib.profile "add_obj.index_obj" in
 176   fun ~dbd ~uri ->
 177    profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
 178
 179 let add_single_obj uri obj ~basedir =
 180   let obj =
 181     if List.mem `Generated (CicUtil.attributes_of_obj obj) &&
 182        not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
 183     then
 184       merge_coercions obj
 185     else
 186       obj
 187   in
 188   let dbd = LibraryDb.instance () in
 189   if CicEnvironment.in_library uri then
 190     raise (AlreadyDefined uri)
 191   else begin
 192     typecheck_obj uri obj; (* 1 *)
 193     let _, ugraph, univlist =
 194       CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
 195     try
 196       index_obj ~dbd ~uri; (* 2 must be in the env *)
 197       try
 198         (*3*)
 199         let new_stuff = save_object_to_disk ~basedir uri obj ugraph univlist in
 200         try
 201          HLog.message
 202           (Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
 203         with exc ->
 204           List.iter HExtlib.safe_remove (List.map snd new_stuff); (* -3 *)
 205           raise exc
 206       with exc ->
 207         ignore(LibraryDb.remove_uri uri); (* -2 *)
 208         raise exc
 209     with exc ->
 210       CicEnvironment.remove_obj uri; (* -1 *)
 211     raise exc
 212   end
 213
 214 let remove_single_obj uri =
 215   let derived_uris_of_uri uri =
 216    let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
 217     innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u])
 218   in
 219   let to_remove =
 220     uri ::
 221     (if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else []) @
 222     derived_uris_of_uri uri
 223   in
 224   List.iter
 225     (fun uri ->
 226       (try
 227         let file = Http_getter.resolve' uri in
 228          HExtlib.safe_remove file;
 229          HExtlib.rmdir_descend (Filename.dirname file)
 230       with Http_getter_types.Key_not_found _ -> ());
 231       ignore (LibraryDb.remove_uri uri);
 232       (*CoercGraph.remove_coercion uri;*)
 233       CicEnvironment.remove_obj uri)
 234   to_remove
 235
 236 (*** GENERATION OF AUXILIARY LEMMAS ***)
 237
 238 let generate_elimination_principles ~basedir uri =
 239   let uris = ref [] in
 240   let elim sort =
 241     try
 242       let uri,obj = CicElim.elim_of ~sort uri 0 in
 243        add_single_obj uri obj ~basedir;
 244        uris := uri :: !uris
 245     with CicElim.Can_t_eliminate -> ()
 246   in
 247   try
 248     List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
 249     !uris
 250   with exn ->
 251    List.iter remove_single_obj !uris;
 252    raise exn
 253
 254 (* COERICONS ***********************************************************)
 255
 256 let remove_all_coercions () =
 257   UriManager.UriHashtbl.clear coercion_hashtbl;
 258   CoercDb.remove_coercion (fun (_,_,u1) -> true)
 259
 260 let add_coercion ~basedir ~add_composites uri =
 261   let coer_ty,_ =
 262     let coer = CicUtil.term_of_uri uri in
 263     CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph
 264   in
 265   (* we have to get the source and the tgt type uri
 266    * in Coq syntax we have already their names, but
 267    * since we don't support Funclass and similar I think
 268    * all the coercion should be of the form
 269    * (A:?)(B:?)T1->T2
 270    * So we should be able to extract them from the coercion type
 271    *
 272    * Currently only (_:T1)T2 is supported.
 273    * should we saturate it with metas in case we insert it?
 274    *
 275    *)
 276   let extract_last_two_p ty =
 277     let rec aux = function
 278       | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) ->
 279           assert false
 280           (* not implemented: aux (Cic.Prod(n,t1,t2)) *)
 281       | Cic.Prod( _, src, tgt) -> src, tgt
 282       | _ -> assert false
 283     in
 284     aux ty
 285   in
 286   let ty_src, ty_tgt = extract_last_two_p coer_ty in
 287   let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
 288   let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
 289   let new_coercions = CicCoercion.close_coercion_graph src_uri tgt_uri uri in
 290   let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
 291   (* update the DB *)
 292   List.iter
 293     (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri))
 294       new_coercions;
 295   CoercDb.add_coercion (src_uri, tgt_uri, uri);
 296   (* add the composites obj and they eventual lemmas *)
 297   let lemmas =
 298     if add_composites then
 299       List.fold_left
 300         (fun acc (_,_,uri,obj) ->
 301           add_single_obj ~basedir uri obj;
 302           uri::acc)
 303         composite_uris new_coercions
 304     else
 305       []
 306   in
 307   (* store that composite_uris are related to uri. the first component is the
 308    * stuff in the DB while the second is stuff for remove_obj *)
 309   UriManager.UriHashtbl.add coercion_hashtbl uri
 310     (composite_uris,if add_composites then composite_uris else []);
 311   lemmas
 312
 313 let remove_coercion uri =
 314   try
 315     let (composites_in_db, composites_in_lib) =
 316       UriManager.UriHashtbl.find coercion_hashtbl uri
 317     in
 318     UriManager.UriHashtbl.remove coercion_hashtbl uri;
 319     CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
 320     (* remove from the DB *)
 321     List.iter
 322       (fun u -> CoercDb.remove_coercion (fun (_,_,u1) -> UriManager.eq u u1))
 323       composites_in_db;
 324     (* remove composites from the lib *)
 325     List.iter remove_single_obj composites_in_lib
 326   with
 327     Not_found -> () (* mhh..... *)
 328
 329
 330 let generate_projections ~basedir uri fields =
 331  let uris = ref [] in
 332  let projections = CicRecord.projections_of uri (List.map fst fields) in
 333   try
 334    List.iter2
 335     (fun (uri, name, bo) (_name, coercion) ->
 336       try
 337        let ty, ugraph =
 338          CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
 339        let attrs = [`Class `Projection; `Generated] in
 340        let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
 341
 342         add_single_obj ~basedir uri obj;
 343         let composites =
 344          if coercion then
 345             add_coercion ~basedir ~add_composites:true uri
 346           else
 347             []
 348         in
 349         uris := uri :: composites @ !uris
 350       with
 351          CicTypeChecker.TypeCheckerFailure s ->
 352           HLog.message
 353            ("Unable to create projection " ^ name ^ " cause: " ^ Lazy.force s);
 354        | CicEnvironment.Object_not_found uri ->
 355           let depend = UriManager.name_of_uri uri in
 356            HLog.message
 357             ("Unable to create projection " ^ name ^ " because it requires " ^
 358                depend)
 359     ) projections fields;
 360    !uris
 361   with exn ->
 362    List.iter remove_single_obj !uris;
 363    raise exn
 364
 365
 366 let add_obj uri obj ~basedir =
 367  add_single_obj uri obj ~basedir;
 368  let uris = ref [] in
 369  try
 370   begin
 371    match obj with
 372     | Cic.Constant _ -> ()
 373     | Cic.InductiveDefinition (_,_,_,attrs) ->
 374         uris := !uris @ generate_elimination_principles ~basedir uri;
 375         let rec get_record_attrs =
 376           function
 377           | [] -> None
 378           | (`Class (`Record fields))::_ -> Some fields
 379           | _::tl -> get_record_attrs tl
 380         in
 381          (match get_record_attrs attrs with
 382          | None -> () (* not a record *)
 383          | Some fields ->
 384             uris := !uris @ (generate_projections ~basedir uri fields))
 385     | Cic.CurrentProof _
 386     | Cic.Variable _ -> assert false
 387   end;
 388   UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
 389   !uris
 390  with exn ->
 391   List.iter remove_single_obj !uris;
 392   raise exn
 393
 394 let remove_obj uri =
 395  let uris =
 396   try
 397    let res = UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri in
 398     UriManager.UriHashtbl.remove auxiliary_lemmas_hashtbl uri;
 399     res
 400   with
 401     Not_found -> [] (*assert false*)
 402  in
 403   List.iter remove_single_obj (uri::uris)
 404