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