Bug fixed: inductive types were no longer removed from the environment during

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

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index 1db8f0cfc2c7b8374b79ae334ef068da0cab6c83..5e8ddaf6d5db898229d0cd7aec7b1eb72bda2bcf 100644 (file)
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -157,22 +157,24 @@ let remove_single_obj uri =
    let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
     innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u])
   in
-  let to_remove =
-    uri :: 
-    (if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else []) @
-    derived_uris_of_uri uri
-  in   
+  let uris_to_remove =
+   if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri]
+  in
+  let files_to_remove = uri :: derived_uris_of_uri uri in   
+  List.iter 
+   (fun uri -> 
+     (try
+       let file = Http_getter.resolve' ~writable:true uri in
+        HExtlib.safe_remove file;
+        HExtlib.rmdir_descend (Filename.dirname file)
+     with Http_getter_types.Key_not_found _ -> ());
+   ) files_to_remove ;
   List.iter 
-    (fun uri -> 
-      (try
-        let file = Http_getter.resolve' ~writable:true uri in
-         HExtlib.safe_remove file;
-         HExtlib.rmdir_descend (Filename.dirname file)
-      with Http_getter_types.Key_not_found _ -> ());
-      ignore (LibraryDb.remove_uri uri);
-      (*CoercGraph.remove_coercion uri;*)
-      CicEnvironment.remove_obj uri)
-  to_remove
+   (fun uri -> 
+     ignore (LibraryDb.remove_uri uri);
+     (*CoercGraph.remove_coercion uri;*)
+   ) uris_to_remove ;
+  CicEnvironment.remove_obj uri
 
 (*** GENERATION OF AUXILIARY LEMMAS ***)
 
@@ -209,7 +211,7 @@ let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
   CoercDb.remove_coercion (fun (_,_,u1) -> true)
 
-let add_coercion ~add_composites refinement_toolkit uri =
+let add_coercion ~add_composites refinement_toolkit uri arity =
   let coer_ty,_ =
     let coer = CicUtil.term_of_uri uri in
     CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph 
@@ -225,23 +227,44 @@ let add_coercion ~add_composites refinement_toolkit uri =
    * should we saturate it with metas in case we insert it?
    * 
    *)
-  let extract_last_two_p ty =
+  let spline2list ty =
     let rec aux = function
-      | Cic.Prod( _, _, ((Cic.Prod _) as t)) -> 
-          aux t
-      | Cic.Prod( _, src, tgt) -> src, tgt
-      | _ -> assert false
+      | Cic.Prod( _, src, tgt) -> src::aux tgt
+      | t -> [t]
     in
     aux ty
   in
+  let src_carr, tgt_carr = 
+    let list_remove_from_tail n l = 
+      let rec aux n = function
+        | hd::tl when n > 0 -> aux (n-1) tl
+        | l when n = 0 -> l
+        | _ -> assert false
+      in
+      aux n (List.rev l)
+    in
+    let types = spline2list coer_ty in
+    match arity, list_remove_from_tail arity types with
+    | 0,tgt::src::_ -> 
+        (* if ~delta is true, it is impossible to define an identity coercion *)
+        CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+        CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
+    | n,_::src::_ -> 
+        CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+        CoercDb.Fun arity
+    | _ -> assert false    
+  in
   let already_in = 
      List.exists 
-      (fun (_,_,ul) -> List.exists (fun u -> UriManager.eq u uri) ul)
+      (fun (s,t,ul) -> 
+        List.exists 
+         (fun u -> 
+           UriManager.eq u uri && 
+           CoercDb.eq_carr s src_carr && 
+           CoercDb.eq_carr t tgt_carr) 
+         ul)
       (CoercDb.to_list ())
   in
-  let ty_src, ty_tgt = extract_last_two_p coer_ty in
-  let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
-  let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
   if not add_composites then
     (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
   else
@@ -317,10 +340,13 @@ let remove_coercion uri =
 
 let generate_projections refinement_toolkit uri fields =
  let uris = ref [] in
- let projections = CicRecord.projections_of uri (List.map fst fields) in
+ let projections = 
+   CicRecord.projections_of uri 
+     (List.map (fun (x,_,_) -> x) fields) 
+ in
   try
    List.iter2 
-    (fun (uri, name, bo) (_name, coercion) ->
+    (fun (uri, name, bo) (_name, coercion, arity) ->
       try
        let ty, ugraph =
          CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
@@ -331,7 +357,8 @@ let generate_projections refinement_toolkit uri fields =
          if coercion then
             begin
 (*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
-              let x = add_coercion ~add_composites:true refinement_toolkit uri
+              let x = 
+                add_coercion ~add_composites:true refinement_toolkit uri arity
               in
 (*prerr_endline ("are: ");
   List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;