* http://cs.unibo.it/helm/.
*)
-(* order, uri, (which, constructor) *)
-type uri = Uri of int * string * (int * int option ) option
+exception IllFormedUri of string Lazy.t
+
+type spec =
+ | Decl
+ | Def
+ | Fix of int * int (* fixno, recparamno *)
+ | CoFix of int
+ | Ind of int
+ | Con 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;;
-let uri_of_string_aux =
- let counter = ref 0 in fun s ->
- incr counter;
- try
- let sharp = String.rindex s '#' in
- let pre = String.sub s 0 sharp in
- let ind = String.sub s (sharp+12) (String.length s - (sharp+13)) in
- try
- let slash = String.rindex ind '/' in
- let indno = String.sub ind 0 slash in
- let constr = String.sub ind (slash+1) (String.length ind - (slash+1)) in
- Uri(!counter,pre,Some(int_of_string indno-1,Some(int_of_string constr-1)))
- with Not_found -> Uri (!counter,pre,Some (int_of_string ind-1, None))
- with Not_found -> Uri (!counter,s,None)
-;;
+(* '.' not allowed in path and foo
+ *
+ * Decl cic:/path/foo.dec
+ * Def cic:/path/foo.def
+ * Fix of int * int cic:/path/foo.fix(i,j)
+ * CoFix of int cic:/path/foo.cfx(i)
+ * Ind of int cic:/path/foo.ind(i)
+ * Con of int * int cic:/path/foo.con(i,j)
+ *)
-let uri_of_string s =
- try
- MapStringsToUri.find s !set_of_uri
+let uri_of_string =
+ let counter = ref 0 in
+ let c () = incr counter; !counter in
+ let get2 s dot =
+ let comma = String.rindex s ',' in
+ let i = int_of_string (String.sub s (dot+5) (comma-dot-5)) in
+ let j = int_of_string (String.sub s (comma+1) (String.length s-comma-2)) in
+ i,j
+ in
+ let get1 s dot =
+ let i = int_of_string (String.sub s (dot+5) (String.length s-1)) in
+ i
+ in
+fun s ->
+ try MapStringsToUri.find s !set_of_uri
with Not_found ->
- let new_uri = uri_of_string_aux s in
+ let new_uri =
+ try
+ let dot = String.rindex s '.' in
+ let suffix = String.sub s (dot+1) 3 in
+ match suffix with
+ | "dec" -> Uri (c (), s, Decl)
+ | "def" -> Uri (c (), s, Def)
+ | "fix" -> let i,j = get2 s dot in Uri (c (), s, Fix (i,j))
+ | "cfx" -> let i = get1 s dot in Uri (c (), s, CoFix (i))
+ | "ind" -> let i = get1 s dot in Uri (c (), s, Ind (i))
+ | "con" -> let i,j = get2 s dot in Uri (c (), s, Con (i,j))
+ | _ -> raise Not_found
+ with Not_found -> raise (IllFormedUri (lazy s))
+ in
set_of_uri := MapStringsToUri.add s new_uri !set_of_uri;
new_uri
;;
let nuri_of_ouri u indinfo =
- uri_of_string (string_of_uri (Uri(0,UriManager.string_of_uri u,indinfo)))
+ let s = UriManager.string_of_uri u in
+ let dot = String.rindex s '.' in
+ let s2 = String.sub s 0 dot in
+ let ns = match indinfo with
+ | Decl -> s2 ^ ".dec"
+ | Def -> s2 ^ ".def"
+ | Fix (i,j) -> s2 ^ ".fix(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")"
+ | CoFix i -> s2 ^ ".cfx(" ^ string_of_int i ^ ")"
+ | Ind i -> s2 ^ ".ind(" ^ string_of_int i ^ ")"
+ | Con (i,j) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")"
+ in uri_of_string ns
;;
let ouri_of_nuri u =
- UriManager.uri_of_string (string_of_uri u)
+ let s = string_of_uri u in
+ let dot = String.rindex s '.' in
+ let prefix = String.sub s 0 dot in
+ let suffix = String.sub s (dot+1) 3 in
+ let os =
+ match suffix with
+ | "dec"
+ | "def" -> prefix ^ ".con"
+ | "ind"
+ | "con" -> prefix ^ ".ind"
+ | _ -> assert false
+ in
+ UriManager.uri_of_string os
;;