* http://cs.unibo.it/helm/.
*)
-(* order, uri, (which, constructor) *)
-type uri = Uri of int * string * (int * int option ) option
+type spec =
+ | Decl
+ | Def
+ | Fix of int * int (* fixno, recparamno *)
+ | CoFix of int
+ | Ind of int
+ | IConstr of int * int (* indtyno, constrno *)
+
+type uri = Uri of int * string * spec
let eq = (==);;
-let string_of_uri = function
- | Uri (_,s,None) -> s
- | Uri (_,s,Some (i,None)) ->
- s ^ "#xpointer(1/" ^ string_of_int (i+1) ^ ")"
- | Uri (_,s,Some (i, Some k)) ->
- s ^ "#xpointer(1/" ^ string_of_int (i+1) ^ "/" ^ string_of_int (k+1) ^ ")"
-;;
+let string_of_uri (Uri (_,s,_)) = s ;;
module OrderedStrings =
struct
let set_of_uri = ref MapStringsToUri.empty;;
+(* '.' not allowed in path and foo
+ *
+ * Decl cic:/path/foo.decl
+ * Def cic:/path/foo.def
+ * Fix of int * int cic:/path/foo.fix(i,j)
+ * CoFix of int cic:/path/foo.cofix(i)
+ * Ind of int cic:/path/foo.ind(i)
+ * Constr of int * int cic:/path/foo.constr(i,j)
+ *)
+
let uri_of_string_aux =
let counter = ref 0 in fun s ->
incr counter;
* http://cs.unibo.it/helm/.
*)
-(* order, uri, (which, constructor) *)
-type spec = Normal of (int * int option) option |
-type uri = private Uri of int * string * spec
+type spec =
+ | Decl
+ | Def
+ | Fix of int * int (* fixno, recparamno *)
+ | CoFix of int
+ | Ind of int
+ | IConstr of int * int (* indtyno, constrno *)
+
+type uri = Uri of int * string * spec
val eq: uri -> uri -> bool
val string_of_uri: uri -> string