maxipatch for support of multiple DBs.

[helm.git] / helm / software / components / library / librarySync.ml

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index a4908ce7c893141cb040a42e640fb78c7a46e4c3..1e60133a797eefb41e85c46334bac7b607fda499 100644 (file)
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -44,7 +44,7 @@ let uris_of_obj uri =
   innertypesuri,bodyuri,univgraphuri
 
 let paths_and_uris_of_obj uri =
-  let resolved = Http_getter.filename' ~writable:true uri in
+  let resolved = Http_getter.filename' ~local:true ~writable:true uri in
   let basepath = Filename.dirname resolved in
   let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
   let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in
@@ -149,7 +149,7 @@ let add_single_obj uri obj refinement_toolkit =
         raise exc
     with exc ->
       CicEnvironment.remove_obj uri; (* -1 *)
-    raise exc
+      raise exc
   end
 
 let remove_single_obj uri =
@@ -164,7 +164,7 @@ let remove_single_obj uri =
   List.iter 
    (fun uri -> 
      (try
-       let file = Http_getter.resolve' ~writable:true uri in
+       let file = Http_getter.resolve' ~local:true ~writable:true uri in
         HExtlib.safe_remove file;
         HExtlib.rmdir_descend (Filename.dirname file)
      with Http_getter_types.Key_not_found _ -> ());
@@ -282,7 +282,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
     (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
   else
     let new_coercions = 
-      CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri 
+      CicCoercion.close_coercion_graph src_carr tgt_carr uri 
        baseuri
     in
     let new_coercions = 
@@ -405,12 +405,55 @@ let generate_inversion refinement_toolkit uri obj =
        add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri)
     (!build_inversion_principle uri obj)
 
+let
+ generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid
+=
+ function
+    Cic.Fix (_,funs) ->
+     snd (
+      List.fold_right
+       (fun (name,idx,ty,bo) (n,uris) ->
+         if name = name_to_avoid then
+          (n+1,uris)
+         else
+          let uri =
+           UriManager.uri_of_string
+            (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+          let bo = Cic.Fix (n,funs) in 
+          let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+           add_single_obj uri obj refinement_toolkit;
+           (n+1,uri::uris)
+       ) funs (1,[]))
+  | Cic.CoFix (_,funs) ->
+     snd (
+      List.fold_right
+       (fun (name,ty,bo) (n,uris) ->
+         if name = name_to_avoid then
+          (n+1,uris)
+         else
+          let uri =
+           UriManager.uri_of_string
+            (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+          let bo = Cic.CoFix (n,funs) in 
+          let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+           add_single_obj uri obj refinement_toolkit;
+           (n+1,uri::uris)
+       ) funs (1,[]))
+  | _ -> assert false
+
 let add_obj refinement_toolkit uri obj =
  add_single_obj uri obj refinement_toolkit;
  let uris = ref [] in
+ let not_debug = not (Helm_registry.get_bool "matita.debug") in
  try
   begin
    match obj with
+    | Cic.Constant (name,Some bo,_,_,attrs) when
+       List.mem (`Flavour `MutualDefinition) attrs ->
+        uris :=
+         !uris @
+           generate_sibling_mutual_definitions refinement_toolkit uri attrs
+            name bo
     | Cic.Constant _ -> ()
     | Cic.InductiveDefinition (_,_,_,attrs) ->
         uris := !uris @ 
@@ -432,9 +475,10 @@ let add_obj refinement_toolkit uri obj =
   end;
   UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
   !uris
- with exn ->
-  List.iter remove_single_obj !uris;
-  raise exn
+ with 
+ | exn when not_debug ->
+    List.iter remove_single_obj !uris;
+    raise exn
 
 let remove_obj uri =
  let uris =