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