* http://cs.unibo.it/helm/.
*)
+exception IllFormedUri of string;;
+
type uri
val eq : uri -> uri -> bool
val buri_of_uri : uri -> string (* base uri only *)
val depth_of_uri : uri -> int (* length of the path *)
-(* relative_depth curi uri cookingsno *)
-(* is the number of times to cook uri to use it when the current uri is curi *)
-(* cooked cookingsno times *)
-val relative_depth : uri -> uri -> int -> int
-
(* given an uri, returns the uri of the corresponding cic file, *)
(* i.e. removes the [.types][.ann] suffix *)
val cicuri_of_uri : uri -> uri
+val strip_xpointer: uri -> uri (* remove trailing #xpointer..., if any *)
+
(* given an uri, returns the uri of the corresponding annotation file, *)
(* i.e. adds the .ann suffix if not already present *)
val annuri_of_uri : uri -> uri
(* given an uri, tells if it refers to an annotation *)
val uri_is_annuri : uri -> bool
+
+(* given an uri of a constant, it gives back the uri of its body *)
+(* it gives back None if the uri refers to a Variable or MutualInductiveType *)
+val bodyuri_of_uri : uri -> uri option
+
+(* given an uri, it gives back the uri of its inner types *)
+val innertypesuri_of_uri : uri -> uri
+
+(*
+val mutind_uri: uri -> int -> uri
+val mutconstruct_uri: uri -> int -> int -> uri
+val mutind: uri -> uri * int
+val mutconstruct: uri -> uri * int * int
+*)
+
+ (* builder for MutInd and MutConstruct URIs *)
+type uriref = uri * (int list)
+val string_of_uriref : uriref -> string
+