- s/decompilation/cleaning/

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

diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml
index 2690349bc06c6af0ab6dd4d0a1c5c319a5bbf8a9..92926464ba294eeb82d26c6a3f1e0620e9e3016d 100644 (file)
--- a/helm/ocaml/library/librarySync.ml
+++ b/helm/ocaml/library/librarySync.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 exception AlreadyDefined of UriManager.uri
 
 let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
@@ -48,7 +50,7 @@ let merge_coercions obj =
         C.Lambda (name, aux so, aux dest)
     | C.LetIn (name,so,dest) -> 
         C.LetIn (name, aux so, aux dest)
-    | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when 
+    | Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ] when 
       CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
         let source_carr = CoercGraph.source_of c2 in
         let tgt_carr = CoercGraph.target_of c1 in
@@ -178,7 +180,7 @@ let index_obj =
 
 let add_single_obj uri obj ~basedir =
   let obj = 
-    if List.mem `Generated (CicUtil.attributes_of_obj obj) &&
+    if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
        not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
     then
       merge_coercions obj 
@@ -189,7 +191,16 @@ let add_single_obj uri obj ~basedir =
   if CicEnvironment.in_library uri then
     raise (AlreadyDefined uri)
   else begin
+    (*CicUniv.reset_spent_time ();
+    let before = Unix.gettimeofday () in*)
     typecheck_obj uri obj; (* 1 *)
+    (*let after = Unix.gettimeofday () in
+    let univ_time = CicUniv.get_spent_time () in
+    let total_time = after -. before in
+    prerr_endline 
+      (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n" 
+      (univ_time *. 100. /. total_time) (total_time) (univ_time)
+      (UriManager.name_of_uri uri));*)
     let _, ugraph, univlist = 
       CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
     try 
@@ -251,7 +262,7 @@ let generate_elimination_principles ~basedir uri =
    List.iter remove_single_obj !uris;
    raise exn
 
-(* COERICONS ***********************************************************)
+(* COERCIONS ***********************************************************)
   
 let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
@@ -306,6 +317,9 @@ let add_coercion ~basedir ~add_composites uri =
   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 *)
+  prerr_endline ("aggiungo: " ^ string_of_bool add_composites ^ UriManager.string_of_uri uri);
+  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 []);
   lemmas
@@ -315,6 +329,9 @@ let remove_coercion uri =
     let (composites_in_db, composites_in_lib) = 
       UriManager.UriHashtbl.find coercion_hashtbl uri 
     in
+    prerr_endline ("removing: " ^UriManager.string_of_uri 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);
     (* remove from the DB *) 
@@ -338,7 +355,6 @@ let generate_projections ~basedir uri fields =
          CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
        let attrs = [`Class `Projection; `Generated] in
        let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
-       
         add_single_obj ~basedir uri obj;
         let composites = 
          if coercion then