* http://cs.unibo.it/helm/.
*)
+(****************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
+(* 15/01/2003 *)
+(* *)
+(* *)
+(****************************************************************************)
+
exception IllFormedUri of string;;
let string_of_cic_textual_parser_uri uri =
;;
let cic_textual_parser_uri_of_string uri' =
- prerr_endline ("cic_textual_parser_uri_of_string INPUT = " ^ uri');
try
(* Constant *)
if String.sub uri' (String.length uri' - 4) 4 = ".con" then
let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
CicTextualParser0.IndTyUri (uri'',typeno)
with
- _ ->
- (* Constructor of an Inductive Type *)
- let uri'',typeno,consno =
- CicTextualLexer.indconuri_of_uri uri'
- in
- CicTextualParser0.IndConUri (uri'',typeno,consno)
+ UriManager.IllFormedUri _
+ | CicTextualParser0.LexerFailure _
+ | Invalid_argument _ ->
+ (* Constructor of an Inductive Type *)
+ let uri'',typeno,consno =
+ CicTextualLexer.indconuri_of_uri uri'
+ in
+ CicTextualParser0.IndConUri (uri'',typeno,consno)
)
with
- _ -> raise (IllFormedUri uri')
+ UriManager.IllFormedUri _
+ | CicTextualParser0.LexerFailure _
+ | Invalid_argument _ ->
+ raise (IllFormedUri uri')
;;
-let cic_textual_parser_uri_of_string uri' =
- let res = cic_textual_parser_uri_of_string uri' in
- prerr_endline ("RESULT: " ^ (string_of_cic_textual_parser_uri res));
- res
(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
let wrong_xpointer_format_from_wrong_xpointer_format' uri =
| CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
;;
+(* conversion functions *****************************************************)
+
+type uriref = UriManager.uri * (int list)
+
+let string_of_uriref (uri, fi) =
+ let module UM = UriManager in
+ let str = UM.string_of_uri uri in
+ let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in
+ match fi with
+ | [] -> str
+ | [t] -> str ^ xp t ^ ")"
+ | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")"