X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql%2FmQueryUtil.ml;h=ea1829719f37bfd86641ecf4cadecb4f8deba55c;hb=6cd9c31edf69f619789a9802e840fbb61f4b6b40;hp=75eb86d442c02cf5e59afb731c5c6df235c9b7cf;hpb=32f737bea2029db1f4870ec8a3a39ba6d2e4a57d;p=helm.git

diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml
index 75eb86d44..ea1829719 100644
--- a/helm/ocaml/mathql/mQueryUtil.ml
+++ b/helm/ocaml/mathql/mQueryUtil.ml
@@ -54,19 +54,21 @@ let text_of_query x =
       | M.SuperOp -> "super "
    in
    let txt_vvar_list l =
-      txt_list txt_vvar "," l
+      l
    in
    let rec txt_val = function
       | M.Const [s]           -> txt_qstr s
-      | M.Const l             -> "{" ^ txt_list txt_qstr "," l ^ "}"
-      | M.Record (rv, vv)     -> txt_rvar rv ^ "." ^ txt_rvar vv
+      | M.Const l             -> "{" ^ txt_list txt_qstr ", " l ^ "}"
+      | M.VVar vv             -> txt_vvar vv
+      | M.Record (rv, vv)     -> txt_rvar rv ^ "." ^ txt_vvar vv
       | M.Fun (s, x)          -> "fun " ^ txt_qstr s ^ " " ^ txt_val x
-      | M.Attribute (r, s, x) -> "attribute " ^ txt_ref r ^ txt_qstr s ^ " " ^ txt_val x
+      | M.Attribute (r, p, x) -> "attribute " ^ txt_ref r ^ txt_list txt_qstr "/" p ^ " " ^ txt_val x
       | M.RefOf x             -> "refof " ^ txt_set x
    and txt_boole = function
       | M.False       -> "false"
       | M.True        -> "true"
-      | M.Ex x        -> "ex " ^ txt_boole x
+      | M.Ex b x      -> "ex " ^ txt_boole x
+(*    | M.Ex b x      -> "ex [" ^ txt_list txt_rvar "," b ^ "] " ^ txt_boole x *)
       | M.Not x       -> "not " ^ txt_boole x
       | M.And (x, y)  -> "(" ^ txt_boole x ^ " and " ^ txt_boole y ^ ")"
       | M.Or (x, y)   -> "(" ^ txt_boole x ^ " or " ^ txt_boole y ^ ")"
@@ -76,29 +78,30 @@ let text_of_query x =
    and txt_set = function
       | M.SVar sv                -> txt_svar sv
       | M.RVar rv                -> txt_rvar rv
-      | M.Relation (r, s, x, []) -> "relation " ^ txt_ref r ^ txt_qstr s ^ " " ^ txt_set x
-      | M.Relation (r, s, x, l)  -> "relation " ^ txt_ref r ^ txt_qstr s ^ " " ^ txt_set x ^ " attr " ^ txt_vvar_list l
+      | M.Relation (r, p, x, []) -> "relation " ^ txt_ref r ^ txt_list txt_qstr "/" p ^ " " ^ txt_set x
+      | M.Relation (r, p, x, l)  -> "relation " ^ txt_ref r ^ txt_list txt_qstr "/" p ^ " " ^ txt_set x ^ " attr " ^ txt_list txt_vvar ", " l
       | M.Union (x, y)           -> "(" ^ txt_set x ^ " union " ^ txt_set y ^ ")"
       | M.Intersect (x, y)       -> "(" ^ txt_set x ^ " intersect " ^ txt_set y ^ ")"
       | M.Diff (x, y)            -> "(" ^ txt_set x ^ " diff " ^ txt_set y ^ ")"
-      | M.Let (sv, x, y)         -> "let " ^ txt_svar sv ^ " be " ^ txt_set x ^ " in " ^ txt_set y
+      | M.LetSVar (sv, x, y)     -> "let " ^ txt_svar sv ^ " be " ^ txt_set x ^ " in " ^ txt_set y
+      | M.LetVVar (vv, x, y)     -> "let " ^ txt_vvar vv ^ " be " ^ txt_val x ^ " in " ^ txt_set y
       | M.Select (rv, x, y)      -> "select " ^ txt_rvar rv ^ " in " ^ txt_set x ^ " where " ^ txt_boole y
       | M.Pattern x              -> "pattern " ^ txt_val x
       | M.Ref x                  -> "ref " ^ txt_val x
-   in
+   in 
    txt_set x
 
-let text_of_result x =
+let text_of_result x sep =
    let txt_attr = function
       | (s, []) -> txt_qstr s
-      | (s, l)  -> txt_qstr s ^ "=" ^ txt_list txt_qstr "," l
+      | (s, l)  -> txt_qstr s ^ "=" ^ txt_list txt_qstr ", " l
    in
-   let txt_group l = "{" ^ txt_list txt_attr ";" l ^ "}" in
+   let txt_group l = "{" ^ txt_list txt_attr "; " l ^ "}" in
    let txt_res = function
       | (s, []) -> txt_qstr s 
-      | (s, l)  -> txt_qstr s ^ " attr " ^ txt_list txt_group "," l
+      | (s, l)  -> txt_qstr s ^ " attr " ^ txt_list txt_group ", " l
    in   
-   let txt_set l = txt_list txt_res ";" l in
+   let txt_set l = txt_list txt_res ("; " ^ sep) l ^ sep in
    txt_set x
 
 let query_of_text lexbuf =
@@ -107,41 +110,15 @@ let query_of_text lexbuf =
 let result_of_text lexbuf =
    MQueryTParser.result MQueryTLexer.result_token lexbuf 
 
-(*
-
-(* Converting functions *****************************************************)
-
-let tref_uref u =
-   let s = str_uref u in
-   MQueryTParser.ref MQueryTLexer.rtoken (Lexing.from_string s) 
-
-(* implementazione manuale di tref_uref da controllare 
-
-let split s =
-   try 
-      let i = Str.search_forward (Str.regexp_string ":/") s 0 in
-      let p = Str.string_before s i in
-      let q = Str.string_after s (i + 2) in
-         (p, q)
-   with 
-      Not_found -> (s, "")
-
-let encode = function
-   | Str.Text s  -> MQBC s
-   | Str.Delim s ->  
-      if s = "?"  then MQBQ else
-      if s = "*"  then MQBS else
-      if s = "**" then MQBSS else
-      if s = "/"  then MQBD  else MQBC s
-
-let tref_uref (u, i) =
-   let s = UriManager.string_of_uri u in
-   match split s with
-      | (p, q) -> 
-         let rx = Str.regexp "\?\|\*\*\|\*\|/" in
-         let l = Str.full_split rx q in
-         (Some p, List.map encode l, i) 
+(* 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 ^ ")"