matita/components/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 let object_declaration_hook = ref []
  29 let add_object_declaration_hook f =
  30  object_declaration_hook := f :: !object_declaration_hook
  31
  32 exception AlreadyDefined of UriManager.uri
  33
  34 type coercion_decl =
  35   UriManager.uri -> int (* arity *) ->
  36    int (* saturations *) -> string (* baseuri *) ->
  37     UriManager.uri list (* lemmas (new objs) *)
  38
  39
  40 let stack = ref [];;
  41
  42 let push () =
  43   stack := CoercDb.dump () :: !stack;
  44   CoercDb.restore CoercDb.empty_coerc_db;
  45 ;;
  46
  47 let pop () =
  48   match !stack with
  49   | [] -> raise (Failure "Unable to POP from librarySync.ml")
  50   | db :: tl ->
  51       stack := tl;
  52       CoercDb.restore db;
  53 ;;
  54
  55 let uris_of_obj uri =
  56  let innertypesuri = UriManager.innertypesuri_of_uri uri in
  57  let bodyuri = UriManager.bodyuri_of_uri uri in
  58  let univgraphuri = UriManager.univgraphuri_of_uri uri in
  59   innertypesuri,bodyuri,univgraphuri
  60
  61 let paths_and_uris_of_obj uri =
  62   let resolved = Http_getter.filename' ~local:true ~writable:true uri in
  63   let basepath = Filename.dirname resolved in
  64   let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
  65   let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in
  66   let innertypespath = basepath ^ "/" ^ innertypesfilename in
  67   let xmlfilename = (UriManager.nameext_of_uri uri) ^ ".xml.gz" in
  68   let xmlpath = basepath ^ "/" ^ xmlfilename in
  69   let xmlbodyfilename = (UriManager.nameext_of_uri uri) ^ ".body.xml.gz" in
  70   let xmlbodypath = basepath ^ "/" ^  xmlbodyfilename in
  71   let xmlunivgraphfilename=(UriManager.nameext_of_uri univgraphuri)^".xml.gz"in
  72   let xmlunivgraphpath = basepath ^ "/" ^ xmlunivgraphfilename in
  73   xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
  74   xmlunivgraphpath, univgraphuri
  75
  76 let save_object_to_disk uri obj ugraph univlist =
  77   assert false (*
  78   let write f x =
  79     if not (Helm_registry.get_opt_default
  80               Helm_registry.bool "matita.nodisk" ~default:false)
  81     then
  82       f x
  83   in
  84   let ensure_path_exists path =
  85     let dir = Filename.dirname path in
  86     HExtlib.mkdir dir
  87   in
  88   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
  89   let annobj, innertypes, ids_to_inner_sorts, generate_attributes =
  90    if Helm_registry.get_bool "matita.system" &&
  91       not (Helm_registry.get_bool "matita.noinnertypes")
  92    then
  93     let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
  94      Cic2acic.acic_object_of_cic_object obj
  95     in
  96     let innertypesxml =
  97      Cic2Xml.print_inner_types
  98       uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false
  99     in
 100     annobj, Some innertypesxml, Some ids_to_inner_sorts, false
 101    else
 102     let annobj = Cic2acic.plain_acic_object_of_cic_object obj in
 103     annobj, None, None, true
 104   in
 105   (* prepare XML *)
 106   let xml, bodyxml =
 107    Cic2Xml.print_object
 108     uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false
 109     ~generate_attributes annobj
 110   in
 111   let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
 112       xmlunivgraphpath, univgraphuri =
 113     paths_and_uris_of_obj uri
 114   in
 115   write (List.iter HExtlib.mkdir) (List.map Filename.dirname [xmlpath]);
 116   (* now write to disk *)
 117   write ensure_path_exists xmlpath;
 118   write (Xml.pp ~gzip:true xml) (Some xmlpath);
 119   write (CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph) univlist;
 120   (* we return a list of uri,path we registered/created *)
 121   (uri,xmlpath) ::
 122   (univgraphuri,xmlunivgraphpath) ::
 123     (* now the optional inner types, both write and register *)
 124     (match innertypes with
 125      | None -> []
 126      | Some innertypesxml ->
 127          write ensure_path_exists innertypespath;
 128          write (Xml.pp ~gzip:true innertypesxml) (Some innertypespath);
 129          [innertypesuri, innertypespath]
 130     ) @
 131     (* now the optional body, both write and register *)
 132     (match bodyxml,bodyuri with
 133        None,_ -> []
 134      | Some bodyxml,Some bodyuri->
 135          write ensure_path_exists xmlbodypath;
 136          write (Xml.pp ~gzip:true bodyxml) (Some xmlbodypath);
 137          [bodyuri, xmlbodypath]
 138      | _-> assert false)
 139      *)
 140
 141
 142 let typecheck_obj =
 143  let profiler = HExtlib.profile "add_obj.typecheck_obj" in
 144   fun uri obj ->
 145   assert false (* MATITA 1.0
 146      profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
 147   *)
 148
 149 let index_obj =
 150  let profiler = HExtlib.profile "add_obj.index_obj" in
 151   fun ~dbd ~uri ->
 152   assert false (* MATITA 1.0
 153    profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
 154    *)
 155
 156 let remove_obj uri =
 157   assert false (* MATITA 1.0
 158   let derived_uris_of_uri uri =
 159    let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
 160     innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u])
 161   in
 162   let uris_to_remove =
 163    if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri]
 164   in
 165   let files_to_remove = uri :: derived_uris_of_uri uri in
 166   List.iter
 167    (fun uri ->
 168      (try
 169        let file = Http_getter.resolve' ~local:true ~writable:true uri in
 170         HExtlib.safe_remove file;
 171         HExtlib.rmdir_descend (Filename.dirname file)
 172      with Http_getter_types.Key_not_found _ -> ());
 173    ) files_to_remove ;
 174   List.iter (fun uri -> ignore (LibraryDb.remove_uri uri)) uris_to_remove ;
 175   CicEnvironment.remove_obj uri
 176 ;;
 177 *)
 178
 179 let rec add_obj uri obj ~pack_coercion_obj =
 180   assert false (* MATITA 1.0
 181   let obj =
 182     if CoercDb.is_a_coercion (Cic.Const (uri, [])) = None
 183     then pack_coercion_obj obj
 184     else obj
 185   in
 186   let dbd = LibraryDb.instance () in
 187   if CicEnvironment.in_library uri then raise (AlreadyDefined uri);
 188   begin (* ATOMIC *)
 189     typecheck_obj uri obj; (* 1 *)
 190     let obj, ugraph, univlist =
 191       try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri
 192       with CicEnvironment.Object_not_found _ -> assert false
 193     in
 194     try
 195       index_obj ~dbd ~uri; (* 2 must be in the env *)
 196       try
 197         (*3*)
 198         let new_stuff = save_object_to_disk uri obj ugraph univlist in
 199         try
 200          HLog.message
 201           (Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
 202         with exc ->
 203           List.iter HExtlib.safe_remove (List.map snd new_stuff); (* -3 *)
 204           raise exc
 205       with exc ->
 206         ignore(LibraryDb.remove_uri uri); (* -2 *)
 207         raise exc
 208     with exc ->
 209       CicEnvironment.remove_obj uri; (* -1 *)
 210       raise exc
 211   end;
 212   let added = ref [] in
 213   let add_obj_with_parachute u o =
 214     added := u :: !added;
 215     add_obj u o ~pack_coercion_obj in
 216   let old_db = CoercDb.dump () in
 217   try
 218     List.fold_left
 219       (fun lemmas f ->
 220         f ~add_obj:add_obj_with_parachute
 221         ~add_coercion:(add_coercion ~add_composites:true ~pack_coercion_obj)
 222         uri obj @ lemmas)
 223       [] !object_declaration_hook
 224   with exn ->
 225     List.iter remove_obj !added;
 226     remove_obj uri;
 227     CoercDb.restore old_db;
 228     raise exn
 229   (* /ATOMIC *)
 230     *)
 231
 232 and
 233  add_coercion ~add_composites ~pack_coercion_obj uri arity saturations baseuri
 234 =
 235   assert false (* MATITA 1.0
 236   let coer_ty,_ =
 237     let coer = CicUtil.term_of_uri uri in
 238     CicTypeChecker.type_of_aux' [] [] coer CicUniv.oblivion_ugraph
 239   in
 240   (* we have to get the source and the tgt type uri
 241    * in Coq syntax we have already their names, but
 242    * since we don't support Funclass and similar I think
 243    * all the coercion should be of the form
 244    * (A:?)(B:?)T1->T2
 245    * So we should be able to extract them from the coercion type
 246    *
 247    * Currently only (_:T1)T2 is supported.
 248    * should we saturate it with metas in case we insert it?
 249    *
 250    *)
 251   let spine2list ty =
 252     let rec aux = function
 253       | Cic.Prod( _, src, tgt) -> src::aux tgt
 254       | t -> [t]
 255     in
 256     aux ty
 257   in
 258   let src_carr, tgt_carr, no_args =
 259     let get_classes arity saturations l =
 260       (* this is the ackerman's function revisited *)
 261       let rec aux = function
 262          0,0,None,tgt::src::_ -> src,Some (`Class tgt)
 263        | 0,0,target,src::_ -> src,target
 264        | 0,saturations,None,tgt::tl -> aux (0,saturations,Some (`Class tgt),tl)
 265        | 0,saturations,target,_::tl -> aux (0,saturations - 1,target,tl)
 266        | arity,saturations,None,_::tl ->
 267             aux (arity, saturations, Some `Funclass, tl)
 268        | arity,saturations,target,_::tl ->
 269             aux (arity - 1, saturations, target, tl)
 270        | _ -> assert false
 271       in
 272        aux (arity,saturations,None,List.rev l)
 273     in
 274     let types = spine2list coer_ty in
 275     let src,tgt = get_classes arity saturations types in
 276      CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src) 0,
 277      (match tgt with
 278      | None -> assert false
 279      | Some `Funclass -> CoercDb.coerc_carr_of_term (Cic.Implicit None) arity
 280      | Some (`Class tgt) ->
 281          CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) 0),
 282      List.length types - 1
 283   in
 284   let already_in_obj src_carr tgt_carr uri obj =
 285      List.exists
 286       (fun (s,t,ul) ->
 287         if not (CoercDb.eq_carr s src_carr &&
 288                 CoercDb.eq_carr t tgt_carr)
 289         then false
 290         else
 291         List.exists
 292          (fun u,_,_ ->
 293            let bo, ty =
 294             match obj with
 295             | Cic.Constant (_, Some bo, ty, _, _) -> bo, ty
 296             | _ ->
 297                (* this is not a composite coercion, thus the uri is valid *)
 298               let bo = CicUtil.term_of_uri uri in
 299               bo,
 300               fst (CicTypeChecker.type_of_aux' [] [] bo
 301               CicUniv.oblivion_ugraph)
 302            in
 303            let are_body_convertible =
 304             fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
 305                   CicUniv.oblivion_ugraph)
 306            in
 307            if not are_body_convertible then
 308              (HLog.warn
 309               ("Coercions " ^
 310                UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri
 311                uri^" are not convertible, but are between the same nodes.\n"^
 312                "From now on unification can fail randomly.");
 313              false)
 314            else
 315              match t, tgt_carr with
 316              | CoercDb.Sort (Cic.Type i), CoercDb.Sort (Cic.Type j)
 317              | CoercDb.Sort (Cic.CProp i), CoercDb.Sort (Cic.CProp j)
 318               when not (CicUniv.eq i j) ->
 319               (HLog.warn
 320                ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^
 321                "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^
 322                "different universe : " ^
 323                  CicUniv.string_of_universe j ^ " <> " ^
 324                  CicUniv.string_of_universe i); false)
 325              | CoercDb.Sort Cic.Prop , CoercDb.Sort Cic.Prop
 326              | CoercDb.Sort (Cic.Type _) , CoercDb.Sort (Cic.Type _)
 327              | CoercDb.Sort (Cic.CProp _), CoercDb.Sort (Cic.CProp _) ->
 328                 (HLog.warn
 329                 ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^
 330                  "it is a duplicate of " ^ UriManager.string_of_uri u);
 331                 true)
 332              | CoercDb.Sort s1, CoercDb.Sort s2 ->
 333               (HLog.warn
 334                ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^
 335                "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^
 336                "different universe : " ^
 337                  CicPp.ppterm (Cic.Sort s1) ^ " <> " ^
 338                  CicPp.ppterm (Cic.Sort s2)); false)
 339              | _ ->
 340                 let ty', _ =
 341                   CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u)
 342                   CicUniv.oblivion_ugraph
 343                 in
 344                 if CicUtil.alpha_equivalence ty ty' then
 345                 (HLog.warn
 346                 ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^
 347                  "it is a duplicate of " ^ UriManager.string_of_uri u);
 348                 true)
 349                 else false
 350
 351                 )
 352          ul)
 353       (CoercDb.to_list (CoercDb.dump ()))
 354   in
 355   let cpos = no_args - arity - saturations - 1 in
 356   if not add_composites then
 357     (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos); [])
 358   else
 359     let _ =
 360       if already_in_obj src_carr tgt_carr uri
 361        (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri)) then
 362         raise (AlreadyDefined uri);
 363     in
 364     let new_coercions =
 365       CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
 366        baseuri
 367     in
 368     let new_coercions =
 369       List.filter (fun (s,t,u,_,obj,_,_) -> not(already_in_obj s t u obj))
 370       new_coercions
 371     in
 372     (* update the DB *)
 373     let lemmas =
 374       List.fold_left
 375         (fun acc (src,tgt,uri,saturations,obj,arity,cpos) ->
 376            CoercDb.add_coercion (src,tgt,uri,saturations,cpos);
 377            let acc = add_obj uri obj pack_coercion_obj @ uri::acc in
 378            acc)
 379         [] new_coercions
 380     in
 381     CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
 382 (*     CoercDb.prefer uri; *)
 383     lemmas
 384     *)
 385 ;;
 386
 387