compose tactic restore and added nocomposites keyword

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

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index 9b08ba6dc5a662dcc0f6dd2865f686ad7374a4f9..c36d84c90dd88de02938fdef9507906a55659edb 100644 (file)
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -25,6 +25,10 @@
 
 (* $Id$ *)
 
+let object_declaration_hook = ref (fun _ _ -> ());;
+let set_object_declaration_hook f =
+ object_declaration_hook := f
+
 exception AlreadyDefined of UriManager.uri
 
 let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
@@ -71,7 +75,9 @@ let save_object_to_disk uri obj ugraph univlist =
   in
   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
   let annobj, innertypes, ids_to_inner_sorts, generate_attributes =
-   if Helm_registry.get_bool "matita.system" then
+   if Helm_registry.get_bool "matita.system" &&
+      not (Helm_registry.get_bool "matita.noinnertypes")
+   then
     let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
      Cic2acic.acic_object_of_cic_object obj 
     in
@@ -160,6 +166,10 @@ let add_single_obj uri obj refinement_toolkit =
       try
         (*3*)
         let new_stuff = save_object_to_disk uri obj ugraph univlist in
+        (* EXPERIMENTAL: pretty print the object in natural language *)
+       (try !object_declaration_hook uri obj
+        with exc ->
+         prerr_endline "Error: object_declaration_hook failed");
         try 
          HLog.message
           (Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
@@ -308,7 +318,9 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
       (CoercDb.to_list ())
   in
   if not add_composites then
-    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[])
+    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+    UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]);
+    [])
   else
     let new_coercions = 
       CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
@@ -327,14 +339,11 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
     CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
     (* add the composites obj and they eventual lemmas *)
     let lemmas = 
-      if add_composites then
         List.fold_left
           (fun acc (_,tgt,uri,saturations,obj,arity) -> 
             add_single_obj uri obj refinement_toolkit;
              (uri,arity,saturations)::acc) 
           [] new_coercions
-      else
-        []
     in
     (* store that composite_uris are related to uri. the first component is
      * the stuff in the DB while the second is stuff for remove_obj *)
@@ -344,8 +353,8 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
        List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
         composite_uris; 
     *)
-    UriManager.UriHashtbl.add coercion_hashtbl uri 
-      (composite_uris,if add_composites then composite_uris else []);
+    UriManager.UriHashtbl.add 
+      coercion_hashtbl uri (composite_uris,composite_uris);
     (*
     prerr_endline ("lemmas:");
       List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
@@ -363,7 +372,8 @@ let remove_coercion uri =
     List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
       composites_in_db;*)
     UriManager.UriHashtbl.remove coercion_hashtbl uri;
-    CoercDb.remove_coercion (fun (_,_,u,_) -> UriManager.eq uri u);
+    CoercDb.remove_coercion 
+      (fun (_,_,u,_) -> UriManager.eq uri u);
     (* remove from the DB *) 
     List.iter 
       (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1))
@@ -371,7 +381,7 @@ let remove_coercion uri =
     (* remove composites from the lib *)
     List.iter remove_single_obj composites_in_lib
   with
-    Not_found -> () (* mhh..... *)
+    Not_found -> HLog.warn "Coercion removal raise Not_found" (* mhh..... *)
     
 
 let generate_projections refinement_toolkit uri fields =