X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Furimanager%2FuriManager.mli;h=771def7c172913e265008a447f1d753e0b29d89e;hb=de9a83f286eee12117fb478ea2db18f7faebac9a;hp=0f4f15ea2822ce998847a7312759a7352dfb397f;hpb=0d436761ba03acfadbfe913c0a38367068bdbb47;p=helm.git diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli index 0f4f15ea2..771def7c1 100644 --- a/helm/ocaml/urimanager/uriManager.mli +++ b/helm/ocaml/urimanager/uriManager.mli @@ -28,6 +28,7 @@ exception IllFormedUri of string;; type uri val eq : uri -> uri -> bool +val compare : uri -> uri -> int val uri_of_string : string -> uri @@ -40,6 +41,8 @@ val depth_of_uri : uri -> int (* length of the path *) (* 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 @@ -53,3 +56,17 @@ 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 + +module UriSet: Set.S with type elt = uri +