* http://cs.unibo.it/helm/.
*)
-(* "cic:/a/b/c.con" => [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c" |] *)
+(*
+* "cic:/a/b/c.con" => [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "" |]
+* "cic:/a/b/c.ind#xpointer(1/1)" =>
+* [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "#xpointer(1/1)" |]
+* "cic:/a/b/c.ind#xpointer(1/1/1)" =>
+* [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "#xpointer(1/1/1)" |]
+*)
type uri = string array;;
let eq uri1 uri2 =
uri1 == uri2
;;
-let string_of_uri uri = uri.(Array.length uri - 2);;
-let name_of_uri uri = uri.(Array.length uri - 1);;
-let buri_of_uri uri = uri.(Array.length uri - 3);;
-let depth_of_uri uri = Array.length uri - 2;;
+let string_of_uri uri =
+ match uri.(Array.length uri - 1) with
+ | "" ->
+ uri.(Array.length uri - 3)
+ | _ ->
+ String.concat "#"
+ [ uri.(Array.length uri - 3); uri.(Array.length uri - 1) ]
+let name_of_uri uri = uri.(Array.length uri - 2);;
+let buri_of_uri uri = uri.(Array.length uri - 4);;
+let depth_of_uri uri = Array.length uri - 3;;
module OrderedStrings =
struct
exception IllFormedUri of string;;
-let mk_prefixes str =
+let mk_prefixes str xpointer =
let rec aux curi =
function
[he] ->
with Failure "hd" | Failure "tl" ->
raise (IllFormedUri str))
in
- aux ty sp
+ (aux ty sp) @ [xpointer]
+;;
+
+
+let sharp_rex =
+ Str.regexp "#"
;;
let uri_of_string str =
- try
- SetOfStrings.find str !set_of_uri
- with
- Not_found ->
- let uri = Array.of_list (mk_prefixes str) in
- set_of_uri := SetOfStrings.add str uri !set_of_uri ;
- uri
+ let base, xpointer =
+ match Str.split sharp_rex str with
+ | [base] -> base,""
+ | [base; xpointer] -> base,xpointer
+ | _ -> raise (IllFormedUri str)
+ in
+ try
+ SetOfStrings.find str !set_of_uri
+ with
+ Not_found ->
+ let uri = Array.of_list (mk_prefixes base xpointer) in
+ set_of_uri := SetOfStrings.add str uri !set_of_uri ;
+ uri
;;
let cicuri_of_uri uri =
uri
else
let newuri = Array.copy uri in
- newuri.(Array.length uri - 2) <- newcompleteuri ;
+ newuri.(Array.length uri - 3) <- newcompleteuri ;
newuri
;;
uri
else
let newuri = Array.copy uri in
- newuri.(Array.length uri - 2) <- completeuri ^ ".ann" ;
+ newuri.(Array.length uri - 3) <- completeuri ^ ".ann" ;
newuri
;;
let struri = string_of_uri uri in
if Str.string_match (Str.regexp ".*\\.con$") (string_of_uri uri) 0 then
let newuri = Array.copy uri in
- newuri.(Array.length uri - 2) <- struri ^ ".body" ;
+ newuri.(Array.length uri - 3) <- struri ^ ".body" ;
Some newuri
else
None
let innertypesuri_of_uri uri =
let cicuri = cicuri_of_uri uri in
let newuri = Array.copy cicuri in
- newuri.(Array.length cicuri - 2) <- (string_of_uri cicuri) ^ ".types" ;
+ newuri.(Array.length cicuri - 3) <- (string_of_uri cicuri) ^ ".types" ;
newuri
;;