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 =
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
+
+