All the equalityTactics have now been ported to use both the equality of

[helm.git] / helm / matita / matitaSync.ml

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 3a7f6dd32099beff643b6e87d7cd7b8a695f0900..660be6c10b76856a78fef83800945ccbf16ee03e 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -32,41 +32,19 @@ open MatitaTypes
 let extract_alias types uri = 
   fst(List.fold_left (
     fun (acc,i) (name, _, _, cl) -> 
-      ((name, UriManager.string_of_uriref (uri,[i]))
+      (name, UriManager.string_of_uri (UriManager.uri_of_uriref uri i None))
       ::
       (fst(List.fold_left (
         fun (acc,j) (name,_) ->
-          (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1)
-        ) (acc,1) cl))),i+1
+          (((name,UriManager.string_of_uri (UriManager.uri_of_uriref uri i
+          (Some j))) :: acc) , j+1)
+        ) (acc,1) cl)),i+1
   ) ([],0) types)
 
 let env_of_list l env =
- let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri suri) l in
+ let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri (UriManager.uri_of_string suri)) l in
   DisambiguateTypes.env_of_list l' env
 
-(*
-let add_aliases_for_inductive_def status types suri = 
-  let uri = UriManager.uri_of_string suri in
-  (* aliases for the constructors and types *)
-  let aliases = env_of_list (extract_alias types uri) status.aliases in
-  (* aliases for the eliminations principles *)
-  let base = String.sub suri 0 (String.length suri - 4)  in
-  let alisases = 
-    env_of_list
-      (List.fold_left (
-        fun acc suffix -> 
-          if List.exists (
-            fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix
-          ) status.objects then
-            let u = base ^ suffix in
-            (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc
-          else
-            acc
-      ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases
-  in
-  {status with aliases = aliases }
-*)
-
 let add_aliases_for_inductive_def status types suri = 
   let uri = UriManager.uri_of_string suri in
   let aliases = env_of_list (extract_alias types uri) status.aliases in
@@ -145,9 +123,6 @@ let save_object_to_disk status uri obj =
          [bodyuri,xmlbodypath]
      | _-> assert false) 
 
-let unregister_if_some = function 
-  | Some u -> Http_getter.unregister' u | None -> ()
-
 let remove_object_from_disk uri path =
   Sys.remove path;
   Http_getter.unregister' uri
@@ -247,3 +222,32 @@ let alias_diff ~from status =
          acc)
     status.aliases Map.empty
 
+let remove uri =
+  let derived_uris_of_uri uri =
+    UriManager.innertypesuri_of_uri uri ::
+    UriManager.annuri_of_uri uri ::
+    (match UriManager.bodyuri_of_uri uri with
+    | None -> []
+    | Some u -> [u])
+  in
+  let to_remove =
+    uri :: 
+    (if UriManager.uri_is_ind uri then MatitaDb.xpointers_of_ind uri else []) @
+    derived_uris_of_uri uri   
+  in   
+  List.iter 
+    (fun uri -> 
+      (try
+        let path = 
+          let path = Http_getter.resolve' (UriManager.strip_xpointer uri) in
+          assert (String.sub path 0 7 = "file://");
+          String.sub path 7 (String.length path - 7)
+        in
+        remove_object_from_disk uri path; 
+      with
+        Http_getter_types.Key_not_found _ -> Http_getter.unregister' uri);
+      remove_coercion uri; 
+      ignore(MatitaDb.remove_uri uri))
+  to_remove
+  
+