fixed undo support for coercions inside records

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

diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml
index 707b355b0995304bbe1da901a0a27daac07a1227..2690349bc06c6af0ab6dd4d0a1c5c319a5bbf8a9 100644 (file)
--- a/helm/ocaml/library/librarySync.ml
+++ b/helm/ocaml/library/librarySync.ml
@@ -27,6 +27,14 @@ exception AlreadyDefined of UriManager.uri
 
 let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
 
+(* uri |-->  (derived_coercions_in_the_coercion_DB, derived_coercions_in_lib)
+ * 
+ * in case of remove_coercion uri, the first component is removed from the
+ * coercion DB, while the second is passed to remove_obj (and is not [] only if
+ * add_coercion is called with add_composites 
+ * *)
+let coercion_hashtbl = UriManager.UriHashtbl.create 3
+
 let merge_coercions obj =
   let module C = Cic in
   let rec aux2 = (fun (u,t) -> u,aux t)
@@ -221,7 +229,7 @@ let remove_single_obj uri =
          HExtlib.rmdir_descend (Filename.dirname file)
       with Http_getter_types.Key_not_found _ -> ());
       ignore (LibraryDb.remove_uri uri);
-      CoercGraph.remove_coercion uri;
+      (*CoercGraph.remove_coercion uri;*)
       CicEnvironment.remove_obj uri)
   to_remove
 
@@ -243,6 +251,82 @@ let generate_elimination_principles ~basedir uri =
    List.iter remove_single_obj !uris;
    raise exn
 
+(* COERICONS ***********************************************************)
+  
+let remove_all_coercions () =
+  UriManager.UriHashtbl.clear coercion_hashtbl;
+  CoercDb.remove_coercion (fun (_,_,u1) -> true)
+
+let add_coercion ~basedir ~add_composites uri =
+  let coer_ty,_ =
+    let coer = CicUtil.term_of_uri uri in
+    CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph 
+  in
+  (* we have to get the source and the tgt type uri
+   * in Coq syntax we have already their names, but
+   * since we don't support Funclass and similar I think
+   * all the coercion should be of the form
+   * (A:?)(B:?)T1->T2
+   * So we should be able to extract them from the coercion type
+   * 
+   * Currently only (_:T1)T2 is supported.
+   * should we saturate it with metas in case we insert it?
+   * 
+   *)
+  let extract_last_two_p ty =
+    let rec aux = function
+      | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> 
+          assert false
+          (* not implemented: aux (Cic.Prod(n,t1,t2)) *)
+      | Cic.Prod( _, src, tgt) -> src, tgt
+      | _ -> assert false
+    in
+    aux ty
+  in
+  let ty_src, ty_tgt = extract_last_two_p coer_ty in
+  let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
+  let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
+  let new_coercions = CicCoercion.close_coercion_graph src_uri tgt_uri uri in
+  let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
+  (* update the DB *)
+  List.iter 
+    (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) 
+      new_coercions;
+  CoercDb.add_coercion (src_uri, tgt_uri, uri);
+  (* add the composites obj and they eventual lemmas *)
+  let lemmas = 
+    if add_composites then
+      List.fold_left
+        (fun acc (_,_,uri,obj) -> 
+          add_single_obj ~basedir uri obj;
+          uri::acc) 
+        composite_uris 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 *)
+  UriManager.UriHashtbl.add coercion_hashtbl uri 
+    (composite_uris,if add_composites then composite_uris else []);
+  lemmas
+
+let remove_coercion uri =
+  try
+    let (composites_in_db, composites_in_lib) = 
+      UriManager.UriHashtbl.find coercion_hashtbl uri 
+    in
+    UriManager.UriHashtbl.remove coercion_hashtbl uri;
+    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))
+      composites_in_db;
+    (* remove composites from the lib *)
+    List.iter remove_single_obj composites_in_lib
+  with
+    Not_found -> () (* mhh..... *)
+    
+
 let generate_projections ~basedir uri fields =
  let uris = ref [] in
  let projections = CicRecord.projections_of uri (List.map fst fields) in
@@ -257,12 +341,8 @@ let generate_projections ~basedir uri fields =
        
         add_single_obj ~basedir uri obj;
         let composites = 
-          if coercion then
-            (* this is _NOT_ the place for THIS!!! *)
-            (* MOO HANDLING IS MISSING *)
-            let toadd = CoercGraph.add_coercion uri in
-            List.iter (fun (uri,o) -> add_single_obj ~basedir uri o) toadd;
-            List.map fst toadd
+         if coercion then
+            add_coercion ~basedir ~add_composites:true uri
           else  
             []
         in
@@ -321,3 +401,4 @@ let remove_obj uri =
     Not_found -> [] (*assert false*)
  in
   List.iter remove_single_obj (uri::uris)
+