]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/mQueryMisc.ml
first moogle template checkin
[helm.git] / helm / ocaml / mathql / mQueryMisc.ml
index bb5bb74aef24488ef686d449ca7db7fcc58de6fb..fb32d8c2425fb49fbd59f254e855a7c790d2ccf7 100644 (file)
  * 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 =
@@ -43,7 +54,6 @@ 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
@@ -72,10 +82,6 @@ let cic_textual_parser_uri_of_string uri' =
   | 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 =
@@ -100,3 +106,15 @@ let term_of_cic_textual_parser_uri 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 ^ ")"